¡Esta es una revisión vieja del documento!

Potential Research Topics

This pages aims at gathering potential research topics to be carried out within the group. Potential students (at all levels) are encouraged to propose new topics or to refine existing ones. Members of the group are encouraged to provide concise, clearly written proposals (in a standardized format) and to follow those interested students.

Work at the PhD Level

Work at the MSc Level

Work at the BSc Level


Thesis Title
Primary (Local) Supervisors
Secondary (External) Supervisors
Description of the work
Thesis Title: Evaluating Model-checking Algorithms for Timed CCP
Primary (Local) Supervisors Camilo Rueda (?)
Secondary (External) Supervisors Jorge A. Perez
Description of the work PCTL is a probabilistic logic defined to reason concurrent systems using time and probabilities [1]. Satisfaction of formulas in PCTL is defined over a finite structure, and efficient model-checking procedures that take advantage of it have been proposed. Some of them have been fruitfully implemented in tools and frameworks for verification.

This thesis aims at evaluating existing PCTL model-checking algorithms in the Timed CCP context, mainly by considering their applicability in the existing tools for programming and simulating Timed CCP processes. The Timed CCP language to be used is pntcc [2], a probabilistic extension of ntcc [3]. The thesis work thus not only involves understanding, implementing and testing the mentioned algorithms, but also analyzing whether the theory supporting the relationship between pntcc and PCTL admits further refinements. Furthermore, the resulting implementations should work in an harmonic way with the tools for programming Timed CCP processes developed by the group. Apart from carrying out performance analysis of the implemented algorithms following an engineering approach, it is expected that this development and analysis work be complemented by meaningful case studies, drawn from real application areas such as systems biology and computer music.

Notice that the scope and goals of the thesis can be adjusted according to the interests and skills of the interested student(s).
Bibliography [1] H. Hansson and B. Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6(5):512–535,1994.
[2] J. A. Perez and C. Rueda. A probabilistic timed concurrent constraint calculus. Technical Report AVISPA.
[3] M. Nielsen, C. Palamidessi, and F. Valencia. Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing, 9(2):145–188, 2002.

Notice that “Description” preferably should include 1. Motivation, 2. Approach, and 3. Goal.

Small Research Projects

Also known as “Proyectos Dirigidos”, aimed at creating a solid background on a given topic before taking up a BSc thesis.

grupos/avispa/researchproposals.1295901028.txt.gz · Última modificación: 2013/06/18 16:26 (editor externo)
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki