For the most recent entries see the Petri Nets Newsletter.

Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties.

Bozzelli, Laura

In: Radhia Cousot (Ed.): Lecture Notes in Computer Science, Vol. 3385: Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, pages 282-297. Springer-Verlag, 2005.

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 w.r.t. 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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography