Informace o publikaci
Almost Linear Büchi Automata
Název česky | Skoro lineární Büchiho automaty |
---|---|
Autoři | |
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 | |
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: |