Evènement pour le groupe Modélisation et Verification


Date 2011-10-06  11:30-12:30
TitreModel Checking the Quantitative mu-Calculus on Infinite Transition Systems 
RésuméWe consider the model-checking problem for a quantitative extension of the modal mu-calculus on two classes of infinite quantitative transition systems. The first class, initialized linear hybrid systems, is motivated by verification of systems which exhibit continuous dynamics. We show that the value of a formula of the quantitative mu-calculus can be approximated with arbitrary precision on initialized linear hybrid systems. The other class, increasing tree rewriting systems, is motivated by efforts to allow counting formulas in discrete verification. On such systems, we show that the value of a quantitative formula can be computed exactly. For both these classes of systems, the problem in the end reduces to solving a new form of parity games with counters. 
Lieu076 
OrateurLukasz Kaiser 
Emailkaiser@liafa.jussieu.fr 
UrlLIAFA, CNRS 



Aucun document lié à cet événement.

Retour
Retour à l'index