Parameterised Pushdown Systems with Non-Atomic Writes

Author Matthew Hague

Thumbnail PDF


  • Filesize: 395 kB
  • 12 pages

Document Identifiers

Author Details

Matthew Hague

Cite AsGet BibTex

Matthew Hague. Parameterised Pushdown Systems with Non-Atomic Writes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 457-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


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.
  • Verification
  • Concurrency
  • Pushdown Systems
  • Reachability
  • Parameterised Systems
  • Non-atomicity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail