| Abstract: | In Process Algebra, processes are often specified in a framework of bisimulation semantics. The notion of bisimulation therefore plays an important role. In this paper some existing and new decision methods are presented for strong bisimulation, τ-bisimulation and η-bisimulation. Each of these bisimulation equivalences corresponds to a certain abstraction mechanism. In strong bisimulation, all events in a system are treated equally whereas τ-bisimulation takes into account the silent step τ; η-bisimulation was introduced recently for an alternative silent step η that is less abstract than τ. It is shown that the problem of η-bisimulation decision can be reduced to an abstract graph partitioning problem called the Product Relational Coarsest Partition problem. Special attention is paid to computational complexity of the decision methods. As it turns out. finite process graphs can be reduced to unique minimal normalforms under all three bisimulation semantics mentioned. The last section demonstrates how the decision methods can be used with a particular algebraic model to enable effective verification of specifications. |
