J 2012

Almost linear Büchi automata

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

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

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í

Odkazy

Impakt faktor

Impact factor: 0.722

Kód RIV

RIV/00216224:14330/12:00057181

Organizační jednotka

Fakulta informatiky

DOI

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

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 4. 2013 05:15, RNDr. Pavel Šmerk, 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. 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.

Č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