Evènement pour le 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. 
OrateurIgor Walukiewicz 

Aucun document lié à cet événement.

Retour à l'index