Expansive-Bisimulation for Context-Free Processes - Formal Methods and Hybrid Real-Time Systems - page 481

generate a given pair of bisimulation equivalent context-free processes. Compar-
ing the results, note that whether a finite relation is an expansive-bisimulation
is decidable while whether a finite relation is a self-bisimulation is only semi-
decidable, thus our characterization result based on expansive-bisimulation im-
plies a complete proof method in that in order to show bisimilarity of two
context-free processes we can just present a finite expansive-bisimulation. In
this respect it is an obvious advantage to the characterization result based on
self-bisimulation.
Also from this characterization result semi-decidability of checking bisimilarity
of arbitrary context-free processes is easily obtained. In this case one just need
to enumerate all finite relations on

and check if there is one which contains
the pair of processes in question and which at the same time is an expansive
bisimulation. Thus the dovetailing technique used in the proof in [CHS92] can
be avoided.

S

4Con lu on

In this paper we proposed a notion of expansive-bisimulation which is defined
so that checking whether a finite relation is an expansive-bisimulation is de-
cidable. We proved that for equivalent context-free processes finite expansive-
bisimulations always exist. Thus expansive-bisimulation can also be considered as
providing a witness or proof for bisimulation equivalence of two BPA processes.
To the best of our knowledge no other complete proof method for bisimulation
of context-free processes is published. An ideal framework for such kind of proof
method would be in the style of Milner's equational proof system for regular
processes [Mil82]. However this is not been done even for normed context-free
processes, and this could be a result to expect. For normed context-free processes
there are Huttel and Stirling's tableau proof method and a sequent style proof
system. One can also seek to extend their results to deal with arbitrary context-
free processes.

References

[BBK87] Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Decidability of bisimulation
equivalence for processes generating context-free languages. In: de Bakker,
J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE Parallel Architectures and
Languages Europe. LNCS, vol. 259. Springer, Heidelberg (1987)
[BCS95] Burkart, O., Caucal, D., Steffen, B.: An elementary bisimulation decision
procedure for arbitrary context-free processes. In: Hajek, P., Wiedermann, J.
(eds.) MFCS 1995. LNCS, vol. 969, Springer, Heidelberg (1995)
[BPS01] Bergstra, J., Ponse, A., Smolka, S.: Handbook of Process Algebra. Elsevier,
Amsterdam (2001)
[Cau90] Caucal, D.: Graphes canoniques de graphes algebriques. Theoret. Inform. and
Appl. 24, 339-352 (1990)
[CHS92] Christensen, S., Huttel, H., Stirling, C.: Bisimulation equivalence is decidable
for all context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992.
LNCS, vol. 630, Springer, Heidelberg (1992)