| KUČERA, Antonín and Jan STREJČEK. Characteristic Patterns for LTL. P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.). In SOFSEM 2005: Theory and Practice of Computer Science. Berlin, Heidelberg: Springer-Verlag, 2005, p. 239-249. ISBN 3-540-24302-X. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{563442,
author = {Kučera, Antonín and Strejček, Jan},
address = {Berlin, Heidelberg},
booktitle = {SOFSEM 2005: Theory and Practice of Computer Science},
keywords = {model-checking; linear temporal logic},
language = {eng},
location = {Berlin, Heidelberg},
isbn = {3-540-24302-X},
pages = {239-249},
publisher = {Springer-Verlag},
title = {Characteristic Patterns for LTL},
year = {2005}
}
TY - JOUR
ID - 563442
AU - Kučera, Antonín - Strejček, Jan
PY - 2005
TI - Characteristic Patterns for LTL
PB - Springer-Verlag
CY - Berlin, Heidelberg
SN - 354024302X
KW - model-checking
KW - linear temporal logic
N2 - We give a new characterization of those languages that are definable in fragments of LTL where the nesting depths of X and U modalities are bounded by given constants. This brings further results about various LTL fragments. We also propose a generic method for decomposing LTL formulae into an equivalent disjunction of "semantically refined" LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers.
ER -
KUČERA, Antonín and Jan STREJČEK. Characteristic Patterns for LTL. P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.). In \textit{SOFSEM 2005: Theory and Practice of Computer Science}. Berlin, Heidelberg: Springer-Verlag, 2005, p.~239-249. ISBN~3-540-24302-X.
|
