Parameterised pushdown systems with non-atomic writes
From MaRDI portal
Abstract: We consider the master/slave parameterised reachability problem for networks of pushdown systems, where communication is via a global store using only non-atomic reads and writes. We show that the control-state reachability problem is decidable. As part of the result, we provide a constructive extension of a theorem by Ehrenfeucht and Rozenberg to produce an NFA equivalent to certain kinds of CFG. Finally, we show that the non-parameterised version is undecidable.
Recommendations
- On the Reachability Analysis of Acyclic Networks of Pushdown Systems
- Reachability analysis of communicating pushdown systems
- Reachability analysis of communicating pushdown systems
- Reachability for dynamic parametric processes
- Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
Cited in
(7)- Liveness in broadcast networks
- Reachability for dynamic parametric processes
- On the Reachability Analysis of Acyclic Networks of Pushdown Systems
- On the Complexity of Bounded Context Switching.
- Fine-grained complexity of safety verification
- Parameterized verification under TSO with data types
- Model-checking parametric lock-sharing systems against regular constraints
This page was built for publication: Parameterised pushdown systems with non-atomic writes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2911646)
