  We consider the problem of model--checking for Process Rewrite Systems (PRSs)
in normal form. In a PRS in normal form every rewrite rule either only deals
with procedure calls and procedure termination, possibly with value return,
(this kind of rules allows to capture Pushdown Processes), or only deals with
dynamic activation of processes and synchronization (this kind of rules allows
to capture Petri Nets). The model-checking problem for PRSs and action-based
linear temporal logic (ALTL) is undecidable. However, decidability of
model--checking for PRSs and 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 rewritings) in
PRSs in normal form. As a consequence, we obtain decidability of the
model-checking (restricted to infinite runs) for PRSs in normal form and a
meaningful fragment of ALTL.
