The stuttering principle revisited

KUČERA, Antonín and Jan STREJČEK. The stuttering principle revisited. Acta informatica. Berlin: Springer-Verlag, 2005, vol. 41, 7/8, p. 415-434. ISSN 0001-5903.

Basic information

Original name

The stuttering principle revisited

Name in Czech

Znovu o principu periodických vzorů

Authors

KUČERA, Antonín (203 Czech Republic, guarantor) and Jan STREJČEK (203 Czech Republic)

Edition

Acta informatica, Berlin, Springer-Verlag, 2005, 0001-5903

---

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Impact factor

Impact factor: 1.100

RIV identification code

RIV/00216224:14330/05:00012554

Organization unit

Faculty of Informatics

UT WoS

000230311400002

Keywords in English

linear temporal logic; stuttering

Tags

linear temporal logic, stuttering

Tags

International impact, Reviewed

---

Abstract

V originále

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 both `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. Further, we provide an effective characterization of languages definable by LTL formulae with a bounded nesting depth of the `next' operator.

In Czech

Je známo, že LTL formule bez operátoru "next" jsou invariantní vzhledem k ekvivalenci na slovech obsahující právě ty dvojice, které mají stejné vzorky neopakujících se písmen. V tomto článku je tento princip rozšířen na obecné LTL formule s danou hlobkou zanoření operátorů "next" a "until". Užitím této techniky je dále dokázana sémantická striktnost tří přirozených hierarchií LTL formulí, které jsou paramatrizované hloubkou zanoření zmiňovaných operátorů. Dále je podána efektivní chrakterizace jazyků definivatelných v LTL formulí s omezenou hloubkou zanoření operátoru "next".

---

Links

GA201/03/1161, research and development project	Name: Verifikace nekonečně stavových systémů Investor: Czech Science Foundation, Verification of infinite-state systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science