Verification of Process Rewrite Systems in normal form

2004/01/16 by Laura Bozzelli, Bozzelli, Laura
Computer Science · #68Q60 #FOS: Computer and information sciences #Other Computer Science (cs.OH) #cs.OH

paper · pdf · doi:10.48550/arxiv.cs/0401013

53 pages, 1 figure

arxiv created 2004/01/16 · arxiv updated 2009/12/01

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.

Related

• Model checking for Process Rewrite Systems and a class of action--based regular properties
• Verification of recursive parallel systems
• Regular Model Checking Revisited (Technical Report)
• Algorithmic metatheorems for decidable LTL model checking over infinite systems
• CTL* model checking for data-aware dynamic systems with arithmetic