| 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. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin: Springer-Verlag, 2006, p. 248-259. ISBN 978-3-540-49994-7. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{698768,
author = {Bozzelli, Laura and Křetínský, Mojmír and Řehák, Vojtěch and Strejček, Jan},
address = {Berlin},
booktitle = {FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings},
keywords = {infinite-state systems; linear time logic; decidability; model checking},
language = {eng},
location = {Berlin},
isbn = {978-3-540-49994-7},
note = {Lecture Notes in Computer Science 4337},
pages = {248-259},
publisher = {Springer-Verlag},
title = {On Decidability of LTL Model Checking for Process Rewrite Systems},
year = {2006}
}
TY - JOUR
ID - 698768
AU - Bozzelli, Laura - Křetínský, Mojmír - Řehák, Vojtěch - Strejček, Jan
PY - 2006
TI - On Decidability of LTL Model Checking for Process Rewrite Systems
PB - Springer-Verlag
CY - Berlin
SN - 9783540499947
N1 - Lecture Notes in Computer Science 4337
KW - infinite-state systems
KW - linear time logic
KW - decidability
KW - model checking
N2 - We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS), possibly extended with a weak finite-state control unit, 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".
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. In \textit{FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings}. Berlin: Springer-Verlag, 2006, p.~248-259. ISBN~978-3-540-49994-7.
|
