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

fewer results. Nevertheless this problem is also important. The decidability re-
sults for context-free processes settled the foundation for automatic tools to test
if two context free processes are bisimulation equivalent. However, in general we
want more than just a “YES” or “NO” answer from such an automatic tool. In
particular, when told that two processes are equivalent we want to be convinced
by some verifiable evidence. For finite state processes there are satisfactory so-
lutions. For two finite state processes, if they are bisimulation equivalent then
1. a proof of their equality can be constructed in Milner's equational proof
system for regular processes [Mil82]; and also
2. a finite bisimulation relation can be constructed which contains the pair of
processes in question.
Clearly both a proof in Milner's equational proof system and a finite bisimula-
tion can qualify as verifiable evidences. The situation for context-free processes
is very different. First, no equational proof systems for context-free processes
have been reported so far. Second, for two bisimulation equivalent context-free
processes, there may not exist a finite bisimulation relation which contains them.
Here it is important that we put emphasis on finiteness. If the relation is infi-
nite, it can hardly be taken as an evidence because we do not have a general
procedure to verify infinite bisimulation relations. So far, main results for prov-
ing bisimilarity of context-free processes include Huttel and Stirling's tableau
proof method and a sequent style proof system for normed context-free processes
[HS91]. For the full class of context-free processes to the best of our knowledge
no similar result is known. In [Cau90] Caucal first introduced the useful notion
of self-bisimulation and showed that if two normed context-free processes are
bisimilar then there is a finite self-bisimulation containing the two processes.
Christensen, Huttel and Stirling showed in [CHS92] that this also holds for ar-
bitrary context-free processes. Unfortunately since checking whether a finite re-
lation is a self-bisimulation is only semi-decidable, finite self-bisimulation falls
short of a verifiable evidance.
In this paper we propose a notion of expansive-bisimulation, and with it we
give a finite characterization of bisimulation equivalence for arbitrary context-
free processes. More precisely, we show that two context-free processes are bisim-
ulation equivalent if and only if there is a finite expansive-bisimulation which
contains them. This immediately suggests a complete proof method for bisimi-
larity of context-free processes: in order to prove equality of two processes we just
need to construct a finite expansive-bisimulation which contains the processes
in question.
The paper is organized as follows. In section 2 we present the syntax and oper-
ational semantics of context-free processes, and study some important finiteness
properties of such processes. Our presentation of this part is in a more direct
approach compared with previous works. Section 3 contains the main technical
contribution, where we study expansive-bisimulation. We conclude in section 4
with some discussions and possible future directions.