The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00006381" target="_blank" >RIV/00216224:14330/02:00006381 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
Original language description
It is known that LTL formulae without the `next' operator are invariant under the so-called stutter-equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of the `next' and `until' operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. As another interesting corollary we obtain an alternative characterization of LTL languages, which are exactly the regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.
Czech name
—
Czech description
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2002
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02)
ISBN
3-540-44240-5
ISSN
—
e-ISSN
—
Number of pages
16
Pages from-to
276
Publisher name
Springer
Place of publication
Berlin
Event location
September 22-25, 2002, Edinburgh, Scotland
Event date
Jan 1, 2002
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)