KUČERA, Antonín a Jan STREJČEK. The stuttering principle revisited. Acta informatica. Berlin: Springer-Verlag, 2005, roč. 41, 7/8, s. 415-434. ISSN 0001-5903. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | The stuttering principle revisited |
Název česky | Znovu o principu periodických vzorů |
Autoři | KUČERA, Antonín (203 Česká republika, garant) a Jan STREJČEK (203 Česká republika). |
Vydání | Acta informatica, Berlin, Springer-Verlag, 2005, 0001-5903. |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Článek v odborném periodiku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Německo |
Utajení | není předmětem státního či obchodního tajemství |
Impakt faktor | Impact factor: 1.100 |
Kód RIV | RIV/00216224:14330/05:00012554 |
Organizační jednotka | Fakulta informatiky |
UT WoS | 000230311400002 |
Klíčová slova anglicky | linear temporal logic; stuttering |
Štítky | linear temporal logic, stuttering |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 27. 11. 2006 15:12. |
Anotace |
---|
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. |
Anotace česky |
---|
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". |
Návaznosti | |
---|---|
GA201/03/1161, projekt VaV | Název: Verifikace nekonečně stavových systémů |
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1ET408050503, projekt VaV | Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 18. 10. 2024 12:48