Reachability is decidable for weakly extended process rewrite systems

Process rewrite systems (PRS) are widely accepted as a formalism for the description of infinite-state systems. It is known that the reachability problem for PRS is decidable. The problem becomes undecidable when PRS are extended with a finite-state control unit. In this paper, we show that the problem remains decidable when PRS are extended with a weak (i. e. acyclic except for self-loops) finite-state control unit. We also present some applications of this decidability result.

Authors

• Mojmír Křetínský
• Vojtěch Řehák
• Jan Strejček

Keywords

No keywords are indexed for this paper.