On Decidability of LTL Model Checking for Process Rewrite Systems

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BOZZELLI Laura KŘETÍNSKÝ Mojmír ŘEHÁK Vojtěch STREJČEK Jan

Year of publication 2009
Type Article in Periodical
Magazine / Source Acta informatica
MU Faculty or unit

Faculty of Informatics

Citation
Web http://springerlink.com/content/4610330747913678/?p=9daadd38980f4b8695a892fd058e8e5e&pi=0
Field Informatics
Keywords infinite-state systems; linear time logic; decidability; model checking
Description 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) with both future and past operators. 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. We show that the problem is decidable for wPRS if we consider properties defined by LTL formulae with only modalities strict eventually, strict always, and their past counterparts. 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.