# 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.