Muestra las diferencias entre dos versiones de la página.

grupos:avispa:researchproposals [2011/01/24 15:30] 127.0.0.1 editor externo |
grupos:avispa:researchproposals [2013/06/18 16:26] (actual) japerez [Thesis] |
||
---|---|---|---|

Línea 19: | Línea 19: | ||

|Bibliography| | | |Bibliography| | | ||

- | ^ Thesis Title: Evaluating Model-checking Algorithms for Timed CCP||^ | + | | |

- | | Primary (Local) Supervisors | Camilo Rueda (?)| | + | |

- | | Secondary (External) Supervisors | [[http://www.japerez.phipages.com|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. | Notice that "Description" preferably should include 1. Motivation, 2. Approach, and 3. Goal. |