"SOFSEM 2005: Theory and Practice of Computer Science" . "[5DC07C114C5D]" . "Characteristic Patterns for LTL" . "Characteristic Patterns for LTL"@en . "000228554400027" . . "RIV/00216224:14330/05:00012348" . . "2005-01-01+01:00"^^ . "3-540-24302-X" . "14330" . "Strej\u010Dek, Jan" . . . . . "Liptovsk\u00FD J\u00E1n, Slovakia" . "514984" . "Characteristic Patterns for LTL"@en . "P(1M0545), P(GA201/03/1161), Z(MSM0021622419)" . . "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 %22semantically refined%22 LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers." . . "Characteristic Patterns for LTL" . "RIV/00216224:14330/05:00012348!RIV10-GA0-14330___" . "2"^^ . . . . "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 %22semantically refined%22 LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers."@en . . . "2"^^ . "Springer-Verlag" . . . . . "Ku\u010Dera, Anton\u00EDn" . "Berlin, Heidelberg" . "model-checking; linear temporal logic"@en . "11"^^ . . .