Název:
Efektivní algoritmy pro práci s konečnými automaty
Překlad názvu:
Efficient Algorithms for Finite Automata
Autoři:
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce) Typ dokumentu: Bakalářské práce
Rok:
2013
Jazyk:
cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze][eng]
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
Nondeterministic finite automata are used in many areas of computer science, including, but not limited to, formal verification, the design of digital circuits or for the representation of a regular language. Their advantages over deterministic finite automata is that they may represent a language in even exponentially conciser way. However, this advantage may be lost if a naive approach to some operations is taken, in particular for checking language inclusion of a pair of automata, the naive implementation of which performs an explicit determinization of one of the automata. Recently, several new techniques for this operation that avoid explicit determinization (using the so-called antichains or bisimulation up to congruence) have been proposed. The main goal of the presented work is to efficiently implement these techniques as a new extension of the VATA library. The implementation has been evaluated and is superior to other implementations in over 90% of tested cases by the factor of 2 to 100.
Klíčová slova:
antichain; bisimulace vzhůru ke kongruenci; formální verifikace; jazyková inkluze; knihovna VATA; konečné automaty; antichains; bisimulation up to congruence; finite automata; formal verification; language inclusion; VATA library
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: http://hdl.handle.net/11012/54815