Technical Reports

The report FIMU-RS-2004-10

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.


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.

Responsible contact: unix(atsign)fi(dot)muni(dot)cz