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. |
Další formáty:
BibTeX
LaTeX
RIS
|
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 |
Změnil | Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 22. 4. 2013 05:15. |
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 |
VytisknoutZobrazeno: 21. 9. 2024 02:40