Dissertation

HOLÍK Lukáš. Simulations and Antichains for Efficient Handling of Finite Automata. Brno: Department of Intelligent Systems FIT BUT, 2011.
Publication language:english
Original title:Simulations and Antichains for Efficient Handling of Finite Automata
Title (cs):Simulace a protiřetězce pro práci s konečnými automaty
Pages:128
Place:Brno, CZ
Year:2011
Publisher:Department of Intelligent Systems FIT BUT
Files: 
+Type Name Title Size Modified
iconphdthesis.pdf3,01 MB2011-03-18 16:24:13
^ Select all
With selected:
Keywords
Finite automata, finite tree automata, alternating Büchi automata, nondeterminism,
simulation, bisimulation, universality, language inclusion, antichain,
quotienting, regular tree model checking.
Abstract
This thesis is focused on techniques for finite automata and their use in practice,
with the main emphasis on nondeterministic tree automata. This concerns
namely techniques for size reduction and language inclusion testing, which are
two problems that are crucial for many applications of tree automata. For size
reduction of tree automata, we adapt the simulation quotient technique that is
well established for finite word automata. We give efficient algorithms for computing
tree automata simulations and we also introduce a new type of relation
that arises from a combination of tree automata downward and upward simulation
and that is very well suited for quotienting. The combination principle
is relevant also for word automata. We then generalise the so called antichain
universality and language inclusion checking technique developed originally for
finite word automata for tree automata. Subsequently, we improve the antichain
technique for both word and tree automata by combining it with the simulationbased
inclusion checking techniques, significantly improving efficiency of the
antichain method. We then show how the developed reduction and inclusion
checking methods improve the method of abstract regular tree model checking,
the method that was the original motivation for starting the work on tree automata.
Both the reduction and the language inclusion methods are based on
relatively simple and general principles that can be further extended for other
types of automata and related formalisms. An example is our adaptation of the
reduction methods for alternating Büchi automata, which results in an efficient
alternating automata size reduction technique.
BibTeX:
@PHDTHESIS{
   author = {Lukáš Holík},
   title = {Simulations and Antichains for Efficient Handling of Finite
	Automata},
   pages = {128},
   year = {2011},
   location = {Brno, CZ},
   publisher = {Department of Intelligent Systems FIT BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en?id=9517}
}

Your IPv4 address: 54.166.8.138
Switch to IPv6 connection

DNSSEC [dnssec]