  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
and 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.

Other Computer Science