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é:   
Safety of parametrized asynchronous shared-memory systems is almost always decidable
du groupe Modélisation et Verification

Date 2015-06-04  11:00-12:00
TitreSafety of parametrized asynchronous shared-memory systems is almost always decidable 
RésuméVerification of concurrent systems is a difficult problem in general, and this is the case even more in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague proposed an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory for which safety properties can be effectively verified. All processes in Hague's setting are pushdown automata. We extend this setting by considering other formal models and, as a main contribution, find very liberal conditions on the individual processes under which the safety problem is decidable: the only substantial condition we require is the effective computability of the downward closure for the class of the leader processes. Furthermore, our result allows for a hierarchical approach to constructing models of concurrent systems with decidable safety problem: networks with tree-like architecture, where each process shares a register with its children processes (and another register with its parent). Nodes in such networks can be for instance pushdown automata, Petri nets, or multi-pushdown systems with decidable reachability problem. Joint work with Salvatore La Torre and Anca Muscholl. 
Lieu076 
OrateurIgor Walukiewicz 
Emailigw@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index