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. |