Other formats:
BibTeX
LaTeX
RIS
@article{769242,
author = {Bozzelli, Laura and Křetínský, Mojmír and Řehák, Vojtěch and Strejček, Jan},
article_location = {Berlin},
article_number = {1},
keywords = {infinite-state systems; linear time logic; decidability; model checking},
language = {eng},
issn = {0001-5903},
journal = {Acta informatica},
note = {DOI: 10.1007/s00236-008-0082-3},
title = {On Decidability of LTL Model Checking for Process Rewrite Systems},
url = {http://springerlink.com/content/4610330747913678/?p=9daadd38980f4b8695a892fd058e8e5e&pi=0},
volume = {46},
year = {2009}
}
TY - JOUR
ID - 769242
AU - Bozzelli, Laura - Křetínský, Mojmír - Řehák, Vojtěch - Strejček, Jan
PY - 2009
TI - On Decidability of LTL Model Checking for Process Rewrite Systems
JF - Acta informatica
VL - 46
IS - 1
SP - 1-28
EP - 1-28
PB - Springer-Verlag
SN - 00015903
N1 - DOI: 10.1007/s00236-008-0082-3
KW - infinite-state systems
KW - linear time logic
KW - decidability
KW - model checking
UR - http://springerlink.com/content/4610330747913678/?p=9daadd38980f4b8695a892fd058e8e5e&pi=0
N2 - 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.
ER -
BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK and Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. \textit{Acta informatica}. Berlin: Springer-Verlag, 2009, vol.~46, No~1, p.~1-28. ISSN~0001-5903.
|
