
Evènement pour le groupe Modélisation et Verification
Date  20111006 11:3012:30 
Titre  Model Checking the Quantitative muCalculus on Infinite Transition Systems 
Résumé  We consider the modelchecking problem for a quantitative
extension of the modal mucalculus 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 mucalculus 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. 
Lieu  076 
Orateur  Lukasz Kaiser 
Email  kaiser@liafa.jussieu.fr 
Url  LIAFA, CNRS 
Aucun document lié à cet événement. RetourRetour à l'index
 