Bisimulation minimisation of
nondeterministic tree automata

Written

Johanna Högberg and Andreas Maletti and Jonathan May. Bisimulation minimisation for weighted tree automata. Proc. 11th Int. Conf. Developments in Language Theory, volume 4588 of LNCS, pages 229-241.
© Springer-Verlag, 2007.

Johanna Högberg and Andreas Maletti and Jonathan May. Bisimulation Minimisation of Weighted Tree Automata. Technical Report ISI-TR-634, Information Sciences Institute, University of Southern California, 2007. [pdf]

Johanna Högberg and Andreas Maletti and Jonathan May. Backward and forward bisimulation minimisation of tree automata. Proc. 12th Int. Conf. Implementation and Application of Automata, LNCS.
© Springer-Verlag, 2007.

Johanna Högberg and Andreas Maletti and Jonathan May. Backward and Forward Bisimulation Minimisation of Tree Automata. Technical Report ISI-TR-633, Information Sciences Institute, University of Southern California, 2007. [pdf]

Parosh Aziz Abdulla, Johanna Högberg, and Lisa Kaati, Bisimulation Minimization of Tree Automata To appear in International journal of foundations of computer science. World Scientific, 2007.

Implementation

The minimisation algorithms based on akh and backward bisimulation have been implemented in Java. To try these out, download the jar file bisim.jar and type

at the prompt, where automaton.aut is the name of the file containing the input automaton (in .aut format). A couple of example automata are provided by automata.tar.gz. The option verbose makes the program print debug information, the option backward tells the program to use backward bisimulation (the default is akh bisimulation), and the option bdd informs the program that the input automaton uses so-called binary decision diagram encoding. If the input automaton is very large, then the program might run out of heap space. To avoid this, one can tell the Java VM to allocate more heap space than usual with the option -Xmx 512m.

Last updated June 7th, 2007 by Johanna Högberg.