"Ku\u010Dera, Anton\u00EDn" . . . . . "Characteristic Patterns for LTL" . "Characteristic Patterns for LTL"@en . "model-checking; linear temporal logic"@en . . "[C330CD5B5296]" . . "Strej\u010Dek, Jan" . . . "RIV/00216224:14330/05:00012348" . . . "3381" . "P(1M0545), P(GA201/03/1161), Z(MSM0021622419)" . . "239-249" . "SK - Slovensk\u00E1 republika" . . "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."@en . . "Charakteristick\u00E9 vzorce pro LTL"@cs . . "Characteristic Patterns for LTL"@en . "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." . "RIV/00216224:14330/05:00012348!RIV08-MSM-14330___" . "2"^^ . "14330" . . "Lecture Notes in Computer Science" . "11"^^ . "514985" . "Characteristic Patterns for LTL" . . "0302-9743" . . . "2005" . "2"^^ . "Popisujeme nov\u00E9 charakterizace jazyk\u016F, kter\u00E9 jsou definovateln\u00E9 pomoc\u00ED fragment\u016F LTL s danou hloubkou zano\u0159en\u00ED oper\u00E1tor\u016F X a U. Tyto charakterizace vyu\u017E\u00EDv\u00E1 nov\u011B navr\u017Een\u00E1 obecn\u00E1 metoda rozkladu LTL formule na ekvivalentn\u00ED disjunkci "s\u00E9manticky jemn\u011Bj\u0161\u00EDch" formul\u00ED. D\u00E1le ukazujeme, jak m\u016F\u017Ee b\u00FDt tento rozklad pou\u017Eit k vylep\u0161en\u00ED existuj\u00EDc\u00EDch n\u00E1stroj\u016F pro LTL model checking."@cs . "Charakteristick\u00E9 vzorce pro LTL"@cs .