Characteristic Patterns for LTL

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.

• Type: Conference
• Year: 2005
• Where: SOFSEM
• Authors: Antonín Kucera, Jan Strejcek
• Keywords: LTL Formulae, Nesting Depths, SOFSEM 2005, Theoretical Computer Science, Various Ltl Fragments