Publication details
Characteristic Patterns for LTL
| Basic information | |
|---|---|
| Original title: | Characteristic Patterns for LTL |
| Authors: | Antonín Kučera, Jan Strejček |
| Inferior responsibility: | P. Vojtas, M. Bielikova, B. Charron -Bost, O. Sykora (Eds.) |
| Further information | |
|---|---|
| Citation: | KUČERA, Antonín - STREJČEK, Jan. Characteristic Patterns for LTL. In SOFSEM 2005: Theory and Practice of Computer Science. Berlin, Heidelberg : Springer-Verlag, 2005. ISBN 3-540-24302-X, pp. 239-249. 2005, Liptovský Ján, Slovakia. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | model-checking; linear temporal logic |
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.
Related projects:
- Verification of infinite-state systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
