2026-07-18T19:36:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4875 2024-03-06T10:35:29Z ddc:004 open_access

On Bounded Reachability Analysis of Shared Memory Systems Atig, Mohamed Faouzi Bouajjani, Ahmed Narayan Kumar, K. Saivasan, Prakash Reachability problem Pushdown systems Counter systems This paper addresses the reachability problem for pushdown systems communicating via shared memory. It is already known that this problem is undecidable. It turns out that undecidability holds even if the shared memory consists of a single boolean variable. We propose a restriction on the behaviours of such systems, called stage bound, towards decidability. A k stage bounded run can be split into a k stages, such that in each stage there is at most one process writing to the shared memory while any number of processes may read from it. We consider several versions of stage-bounded systems and establish decidability and complexity results. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohamed Faouzi Atig and Ahmed Bouajjani and K. Narayan Kumar and Prakash Saivasan 2014 Is Part Of LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2014.611 urn:nbn:de:0030-drops-48754 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.611 eng https://creativecommons.org/licenses/by/3.0/legalcode