TBIS Prototype
Introduction
The TBIS prototype can be used to minimize non-deterministic bottom up tree automata modolu bisimulation. The algorithm used in the prototype is an extention of an algorithm by Paige and Tarjan that solves the coarsest stable refinement problem to the domain of trees. The algorithm is used to minimize non-deterministic tree automata with respect to bisimulation. We show that our algorithm has an overall complexity of O(r m log n ) where r is the maximum rank of the input alphabet, m is the total size of the transition table, and n is the number of states.
|
|
|
Download
|
Coming soon! |
Instructions
|
|
Coming soon! |
Case studies
To test our algorithm on real life examples we have use the TBIS Prototype to minimize tree automata that arose during computations in the framework of tree regular model checking. Tree regular model checking is the name of a family of techniques for analyzing infinite state systems in which states are represented by trees, set of states by tree automata, and transitions by tree transducers. Most tree regular model checking algorithms rely heavily on efficient methods for checking bisimulation since the automata often increase in size during the verification process and some computations are simply not feasible without minimization.
The NTAs that we have minimized arose during verification of the Percolate protocol and the Leader Election protocol. The Percolate protocol operates on a tree of processes. The protocol simulates the way results propagate in a set of logical-or gates organized in a tree. The Leader Election protocol consists of a set of processes (represented by the leaves of a tree) that wants to elect a leader. Each process first decides whether to be a candidate or not. The election process then proceeds in two phases. First, the internal nodes checks their children to see if at least one of them has decided to be a candidate. If that is the case, the internal node becomes a candidate as well. Secondly, the root elects one candidate non-deterministically among its children. After this, every internal node that has been elected, elects one of its children (that has declared that it is a candidate).
Related Publications
Parosh Aziz Abdulla, Johanna Högberg, and Lisa Kaati. Minimization of tree automata. Proc. CIAA'06, The 11th International Conference on Implementation and Application of Automata, Taipei, Taiwan, 2006. Best Paper Award. Paper in .ps format.
Parosh Aziz Abdulla, Johanna Högberg, and Lisa Kaati. Minimization of tree automata (journal version). To appear in International Journal of Foundations of Computer Science (IJFCS), 2007. Draft in .ps format.
 |