Detail výsledku

Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

HOLÍK, L.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. FIT-TR-2011-04, Brno: Faculty of Information Technology BUT, 2011. 22 p.
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Šimáček Jiří, Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking.

Klíčová slova

tree automata, binary decision diagrams, language inclusion, downward inclusion checking, symbolic encoding

URL
Rok
2011
Strany
22
Vydavatel
Faculty of Information Technology BUT
Místo
FIT-TR-2011-04, Brno
BibTeX 
@misc{BUT192739,
  author="Lukáš {Holík} and Ondřej {Lengál} and Jiří {Šimáček} and Tomáš {Vojnar}",
  title="Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata",
  year="2011",
  pages="22",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2011-04, Brno",
  url="http://www.fit.vutbr.cz/~ilengal/pub/FIT-TR-2011-04.pdf"
}
Projekty
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ů, GAČR, Doktorské granty, GD102/09/H042, zahájení: 2009-01-30, ukončení: 2012-12-31, ukončen
Pokročilé bezpečné, spolehlivé a adaptivní IT, VUT, Vnitřní projekty VUT, FIT-S-11-1, zahájení: 2011-01-01, ukončení: 2013-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru