Verification of Process Rewrite Systems in normal form

TL;DR

This paper investigates the decidability of model-checking for Process Rewrite Systems in normal form, showing decidability results for certain infinite derivations and a fragment of ALTL, despite the general problem being undecidable.

Contribution

It establishes decidability results for infinite derivations and a fragment of ALTL in PRSs in normal form, advancing understanding of model-checking in this domain.

Findings

Decidability of infinite derivations in PRSs in normal form.

Decidability of model-checking for a fragment of ALTL.

Undecidability of the general model-checking problem for PRSs.

Abstract

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.