Technical Reports

The report FIMU-RS-2006-05

On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems

by Laura Bozzelli, Mojmír Køetínský, Vojtìch Øehák, Jan Strejèek, A full version of the paper presented at FSTTCS 2006. November 2006, 27 pages.

FIMU-RS-2006-05. Available as Postscript, PDF.

Abstract:

We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (wPRS), and properties described by basic fragments of action-based Linear Temporal Logic (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes. As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities strict eventually and strict always. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality until or the fragment with modalities next and infinitely often.