2010
LTL to Büchi Automata: Improved Once Again
BABIAK, TomášZákladní údaje
Originální název
LTL to Büchi Automata: Improved Once Again
Název česky
LTL na Büchiho Automaty: Opětovně vylepšeno
Autoři
BABIAK, Tomáš (703 Slovensko, garant, domácí)
Vydání
Young Researchers Forum, YRF@MFCSL 2010, 2010
Další údaje
Jazyk
angličtina
Typ výsledku
Prezentace na konferencích
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/10:00045895
Organizační jednotka
Fakulta informatiky
ISBN
978-80-87342-09-1
Klíčová slova česky
LTL; logika lineárního času; překlad LTL; Büchiho automaty; ověřování modelu
Klíčová slova anglicky
LTL; linear time logic; translation of LTL; Büchi Automata; model checking
Příznaky
Mezinárodní význam
Změněno: 16. 1. 2011 23:02, RNDr. Tomáš Babiak, Ph.D.
V originále
We present an improvement of an algorithm translating LTL formulae into Büchi automata via alternating automata. In particular, we improve the transformation of alternating Büchi automata to generalized Büchi automata, where we temporarily ignore some transitions leading from the alternating automata states corresponding to subformulae that are prefix-invariant, that can lead to a faster translation.
Česky
Představujeme vylepšení algoritmu, který překládá LTL formule na Büchiho automaty pomocí alternujících automatů. Konkrétněji zlepšujeme převod alternujících Büchiho automatů na generalizované Büchiho automaty, kde dočasně ignorujeme některé přechody vedoucí ze stavů alternujícího automatu, které odpovídají prefixově invariantním formulím, což může vést k rychlejšímu překladu.
Návaznosti
| MSM0021622419, záměr |
| ||
| MUNI/A/0914/2009, interní kód MU |
|