Model checking for Process Rewrite Systems and a class of action--based regular properties

TL;DR

This paper investigates the decidability of model checking for Process Rewrite Systems (PRSs), focusing on a fragment of action-based linear temporal logic (ALTL) and establishing new decidability results for infinite derivations.

Contribution

It provides new decidability results for model checking PRSs against a fragment of ALTL, addressing an open problem for infinite derivations.

Findings

Decidability of model checking for PRSs with certain ALTL fragments.

Decidability results for infinite derivations in PRSs.

Extension of model checking capabilities for infinite-state systems.

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