Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Model Checking the Quantitative mu-Calculus on Infinite Transition Systems
du 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