Model checking for process rewrite systems and a class of action-based regular properties

AbstractWe consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL