Department of Information Technology

Bisimulation

Bisimulation equivalence allows one to relate equivalent systems and to reduce the state space of a system by combining equivalent states.
In formal verification, several existing tools use minimization with respect to bisimulation in order to reduce the size of the state space to be analyzed. Bisimulation minimization of non-deterministic devices with respect to bisimulation consequently also gives an algorithm for minimizing deterministic devices modulo language equivalence.

One of the most famous algorithms for solving the bisimulation minimization problem for finite automata is the one suggested by Paige and Tarjan. The algorithm has a complexity of O(m log n) where m is the number of edges and n the number of states.

The aim of this project is to develop algorithms for minimization modolu bisimulation for different kinds of automata.

Non-Deterministic Automata with Large Alphabets

alphabet2.jpg

There are many applications that give rise to automata with large alphabets. For instance, transition systems generated by verification tools such as SPIN usually have very large alphabets and the bottle-neck in applications of regular model checking is often the size of the alphabet in the automata which arise during the analysis. Therefore, we have adopted Paige and Tarjans partition refinement algorithm to consider automata which have large alphabets.

To deal with the size of the alphabet, we use a symbolic representation of labels on the edges of the automaton. We characterize the set of symbols on which the automaton can move from one state to another through a Binary Decision Diagram (BDD). We have adopted each step of Paige and Tarjans algorithm which operates on explicit representation of the transition relation into a symbolic one which operates on BDDs.

Non-Deterministic Tree Automata

tree.jpg

Bisimulation minimization of tree automata is of particular interest in tree regular model checking (an extension of regular model checking). In this field, the verification of infinite state systems with tree-like architecture is considered, and many of the associated algorithms would benefit from an efficient method to reduce the size of non-deterministic tree automata

The algorithm presented in this paper takes advantage of the fact that bisimulation equivalence is computationally easier to decide than language equivalence, and that bisimulation equivalence implies language equivalence (although the converse does not hold in the general case). When minimizing an non-determinisitic tree automata (NTA), states that are observationally equivalent are grouped and the groups of states are used as states in the output NTA. The time complexity for bisimulation minimization of NTA becomes 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.

Publications

  • Here is a list of our published work on bisimulation.
Updated  2007-06-15 08:22:53 by Lisa Kaati.