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. |
Other formats:
BibTeX
LaTeX
RIS
|
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 | |
---|---|
Original language | English |
Type of outcome | Article in a journal |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | Germany |
Confidentiality degree | is not subject to a state or trade secret |
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 |
Changed by | Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 27/11/2006 15: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 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. |
Abstract (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 |
PrintDisplayed: 22/9/2024 05:34