Other formats:
BibTeX
LaTeX
RIS
@misc{701734, author = {Bozzelli, Laura and Křetínský, Mojmír and Řehák, Vojtěch and Strejček, Jan}, address = {Brno}, keywords = {infinite-state systems; linear time logic; decidability; model checking}, language = {eng}, location = {Brno}, note = {full and extended version of FST&TCS'06 paper}, publisher = {FI MU}, title = {On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems}, url = {http://www.fi.muni.cz/reports/2006/abstract/FIMU-RS-2006-05.shtml}, year = {2006} }
TY - GEN ID - 701734 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 Weakly Extended Process Rewrite Systems VL - FIMU-RS-2006-05 PB - FI MU CY - Brno N1 - full and extended version of FST&TCS'06 paper KW - infinite-state systems KW - linear time logic KW - decidability KW - model checking UR - http://www.fi.muni.cz/reports/2006/abstract/FIMU-RS-2006-05.shtml L2 - http://www.fi.muni.cz/reports/2006/abstract/FIMU-RS-2006-05.shtml N2 - We establish a decidability boundary of the model checking problem for infinite-state systems defined by \emph{Process Rewrite Systems} (PRS) or \emph{weakly extended Process Rewrite Systems} (wPRS), % possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based \emph{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 \emph{strict eventually} and \emph{strict always}. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality \emph{until} or the fragment with modalities \emph{next} and \emph{infinitely often}. ER -
BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK and Jan STREJČEK. \textit{On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems}. Brno: FI MU, 2006. FIMU-RS-2006-05.
|