KUČERA, Antonín a Jan STREJČEK. The stuttering principle revisited. Acta informatica. Berlin: Springer-Verlag, roč. 41, 7/8, s. 415-434. ISSN 0001-5903. 2005.
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 VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměrNá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 VaVNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 28. 3. 2024 18:03