Name
Title | ||
|---|---|---|
Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. |
Abstract | ||
|---|---|---|
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 Hagueu0027s setting are pushdown automata. Here, we extend it 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. |
Year | Venue | Field |
|---|---|---|
2015 | CONCUR | Discrete mathematics,Asynchronous communication,Petri net,Shared memory,Computer science,Decidability,Computability,Theoretical computer science,Pushdown automaton,Reachability problem,Almost surely |
DocType | Citations | PageRank |
Conference | 6 | 0.46 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Salvatore La Torre | 1 | 912 | 52.42 |
| Anca Muscholl | 2 | 1179 | 74.92 |
| Igor Walukiewicz | 3 | 1239 | 90.24 |