Almost Linear Büchi Automata

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou 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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.