Characteristic Patterns for LTL

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KUČERA Antonín STREJČEK Jan

Year of publication 2005
Type Article in Proceedings
Conference SOFSEM 2005: Theory and Practice of Computer Science
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.