Almost Linear Büchi Automata

BABIAK, Tomáš, Vojtěch ŘEHÁK a Jan STREJČEK. Almost Linear Büchi Automata. In Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09). 1st ed. internet: EPTCS, 2009, s. 16-25. ISSN 2075-2180.

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

• Originální 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í
• WWW: DOI
• Kód RIV: RIV/00216224:14330/09:00029631
• Organizační jednotka: Fakulta informatiky
• ISSN: 2075-2180
• 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: linear time logic, Model checking
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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.

Anotace č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