D 2009

Almost Linear Büchi Automata

BABIAK, Tomáš, Vojtěch ŘEHÁK a Jan STREJČEK

Základní údaje

Originální název

Almost Linear Büchi Automata

Název česky

Skoro lineární Büchiho automaty

Autoři

BABIAK, Tomáš (703 Slovensko), Vojtěch ŘEHÁK (203 Česká republika, garant) a Jan STREJČEK (203 Česká republika)

Vydání

1st ed. internet, Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09), od s. 16-25, 10 s. 2009

Nakladatel

EPTCS

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Itálie

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/09:00029631

Organizační jednotka

Fakulta informatiky

ISSN

Klíčová slova česky

LTL; logiky lineárního času; ověřování modelu

Klíčová slova anglicky

LTL; linear time logic; model checking

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 23. 11. 2009 16:12, doc. RNDr. Vojtěch Řehák, Ph.D.

Anotace

ORIG CZ

V originále

We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Büchi automata studied in this context and we indicate possible applications.

Česky

V článku zavádíme nový fragment logiky lineárního času (LTL) nazvaný LIO a dále také novou třídu Büchiho automatů (BA) nazývanou Skoro lineární automaty (ALBA). Předvádíme efektivní transformaci mezi LIO a ALBA a ukazujeme tak, že tyto formalizmy mají stejnou vyjadřovací sílu. Naproti tomu, že standardní transformace LTL do BA používá pomocného meziformalizmu, naše transformace LIO na ALBA je přímá. Protože očekáváme praktické uplatnění ALBA v ověřování modelů, srovnáváme též vyjadřovací sílu ALBA s dalšími třídami BA.

Návaznosti

GP201/08/P375, projekt VaV
Název: Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
Investor: Grantová agentura ČR, Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
GP201/08/P459, projekt VaV
Název: Nové možnosti automatické verifikace síťových protokolů
Investor: Grantová agentura ČR, Nové možnosti automatické verifikace síťových protokolů
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
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky