Characteristic Patterns for LTL
by
Antonín Kučera,
Jan Strejček,
A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.
FIMU-RS-2004-10.
Available as Postscript,
PDF.
Abstract:
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.