Almost Linear Büchi Automata

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Skoro lineární Büchiho automaty
Autoři	BABIAK Tomáš ŘEHÁK Vojtěch STREJČEK Jan
Rok publikování	2009
Druh	Článek ve sborníku
Konference	Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	DOI
Obor	Informatika
Klíčová slova	LTL; linear time logic; model checking
Popis	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.
Související projekty:	Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik Nové možnosti automatické verifikace síťových protokolů