Characteristic Patterns for LTL
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Article in Proceedings |
| Conference | SOFSEM 2005: Theory and Practice of Computer Science |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | model-checking; linear temporal logic |
| Description | 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: |