Almost linear Büchi automata

BABIAK, Tomáš, Jan STREJČEK a Vojtěch ŘEHÁK. Almost linear Büchi automata. Mathematical Structures in Computer Science. Cambridge: Cambridge University Press, 2012, roč. 22, č. 2, s. 203-235. ISSN 0960-1295. Dostupné z: https://dx.doi.org/10.1017/S0960129511000399.

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, domácí), Jan STREJČEK (203 Česká republika, domácí) a Vojtěch ŘEHÁK (203 Česká republika, garant, domácí).
• Vydání: Mathematical Structures in Computer Science, Cambridge, Cambridge University Press, 2012, 0960-1295.

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: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• WWW: URL
• Impakt faktor: Impact factor: 0.722
• Kód RIV: RIV/00216224:14330/12:00057181
• Organizační jednotka: Fakulta informatiky
• Doi: http://dx.doi.org/10.1017/S0960129511000399
• UT WoS: 000300844900004
• 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: to appear
• 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. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller.

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 Almost linear Büchi automata (ALBA). Prezentujeme efektivní transformace mezi LIO a ALBA a ukazujeme tak, že tyto formalizmy mají stejnou vyjadřovací sílu. Protože očekáváme aplikace našich výsledků v oblasti model checkingu, používamé dva standardní zdroje specifikačních formulí (Spec Patterns a BEEM) k posouzení praktické relevance LIO fragmentu a k porovnání našeho překladu LIO na ALBA s dvojicí standardních překladů LTL na BA pomocí alternujících automatů. Na závěr ukazujeme, že překlad LIO na ALBA může být mnohem rychlejší než standardní překlad a může také produkovat podstatně menší automaty.

Návaznosti

• GAP202/10/1469, projekt VaV: Název: Formální metody pro analýzu a verifikaci komplexních systémů

Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů

• GA201/09/1389, projekt VaV: Název: Verifikace a analýza velmi velkých počítačových systémů

Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů

• GD102/09/H042, projekt VaV: Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů

Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů

• 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

• MUNI/A/0914/2009, interní kód MU: Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky