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é:   
Global Model Checking of Ordered Multi-Pushdown Systems
du groupe Modélisation et Verification

Date 2011-02-03  11:30-12:45
TitreGlobal Model Checking of Ordered Multi-Pushdown Systems 
RésuméIn this talk, we address the verification problem of ordered multi-pushdown systems, a multi-stack extension of pushdown systems that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time µ-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of w-regular properties for ordered multi-pushdown systems (matching its lower-bound).  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurMohamed Faouzi Atig 
Emailmohamed_faouzi.atig@it.uu.se 
UrlLIAFA, PARIS 



Aucun document lié à cet événement.

Retour
Retour à l'index