J.C.M. Baeten et al. (Lecture Notes in Computer Science, vol. 259, pp. 93-114, 1987) proved that bisimulation equivalence is decidable for irredundant context-free grammars. A much simpler and much more direct proof of this result is provided now. It uses a tableau decision method involving goal-directed rules. The decision procedure yields an upper bound on a tableau depth. Moreover, it provides the essential part of the bisimulation relation between two processes which underlies their equivalence. A second virtue is that it provides a sound and complete equational theory for such processes.
展开▼
