KUČERA, Antonín and Jan STREJČEK. The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. J. Bradfield (Ed.). In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02). Berlin: Springer, 2002. p. 276-291. ISBN 3-540-44240-5.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
Authors KUČERA, Antonín (203 Czech Republic, guarantor) and Jan STREJČEK (203 Czech Republic).
J. Bradfield (Ed.).
Edition Berlin, Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02), p. 276-291, 2002.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 20206 Computer hardware and architecture
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/02:00006381
Organization unit Faculty of Informatics
ISBN 3-540-44240-5
UT WoS 000187294300019
Keywords in English verification; concurrency; weak bisimilarity; infinite-state systems
Tags concurrency, infinite-state systems, verification, weak bisimilarity
Tags International impact, Reviewed
Changed by Changed by: doc. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 20/12/2011 18:12.
Abstract
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.
Links
GA201/00/0400, research and development projectName: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Czech Science Foundation, Standard Projects
GA201/00/1023, research and development projectName: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Czech Science Foundation, Standard Projects
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
PrintDisplayed: 30/5/2020 11:58