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 Languages of Data Words
du groupe Modélisation et Verification

Date 2012-04-12  11:30-12:30
TitreModel Checking Languages of Data Words 
Résumé We consider the model-checking problem for data multi- pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic. This is a joint work with Benedikt Bollig, Paul Gastin and K. Narayan Kumar. 
Lieu076 
OrateurAiswarya Cyriac 
Emailaiswarya.cyriac@lsv.ens-cachan.fr 
UrlLSV, ENS Cachan 



Aucun document lié à cet événement.

Retour
Retour à l'index