In: Radhia Cousot (Ed.): Lecture Notes in Computer Science, Vol. 3385: Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, pages 282-297. Springer-Verlag, 2005.
Abstract: We consider the model checking problem for Process Rewrite Systems (PRSs), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRSs can be adopted as formal models for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem for PRSs w.r.t. 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 PRSs. As a consequence, we obtain decidability of the model-checking (restricted to infinite runs) for PRSs and a meaningful fragment of ALTL.