Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time.
We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.
Introduction
Recently, a lot of attention has been devoted to the study of decidability
and complexity of verification problems for infinite-state systems [33,12,5].
We consider the problem of weak bisimilarity between certain infinite-state
processes and finite-state ones. The motivation is that the intended behavior
of a process is often easy to specify (by a finite-state system), but a 'real' implementation
can contain components which are essentially infinite-state (e.g.,
counters, buffers, recursion, creation of new parallel subprocesses). The aim is
On leave at the Institute for Informatics, Technical University Munich. Supported
by the Alexander von Humboldt Foundation and by the Grant Agency of the Czech
Republic, grant No. 201/00/0400.
Supported by DAAD Post-Doc grant D/98/28804.
Preprint submitted to Elsevier Preprint 8 November 2000
to check if the finite-state specification and the infinite-state implementation
are semantically equivalent, i.e., weakly bisimilar.
We concentrate on the classes of infinite-state processes definable by the syntax
of BPA (Basic Process Algebra) and normed BPP (Basic Parallel Pro-
cesses) systems. BPA processes (also known as context-free processes) can be
seen as simple sequential programs (due to the binary operator of sequential
composition). They have recently been used to solve problems of data-flow
analysis in optimizing compilers [13]. BPP [8] model simple parallel systems
(due to the binary operator of parallel composition). They are equivalent to
communication-free nets, the subclass of Petri nets [36] where every transition
has exactly one input-place [11]. A process is normed iff at every reachable
state it can terminate via a finite sequence of computational steps.
Although the syntax of BPA and BPP allows to define simple infinite-state
systems, from the practical point of view it is also important that they can give
very compact definitions of finite-state processes (i.e., the size of a BPA/BPP
definition of a finite-state process F can be exponentially smaller than the
number of states of F -see the next section). As our verification algorithms
are polynomial in the size of the BPA/BPP definition, we can (potentially)
verify very large processes. Thus, our results can be also seen as a way how
to overcome the well-known problem of state-space explosion.
The state of the art. Baeten, Bergstra, and Klop [1] proved that strong
bisimilarity [35] is decidable for normed BPA processes. Simpler proofs have
been given later in [20,14], and there is even a polynomial-time algorithm
[17]. The decidability result has later been extended to the class of all (not
necessarily normed) BPA processes in [10], but the best known algorithm is
doubly exponential [4]. Decidability of strong bisimilarity for BPP processes
has been established in [9], but the associated complexity analysis does not
yield an elementary upper bound (although some deeper examination might in
principle show that the algorithm is elementary). Strong bisimilarity of BPP
has been shown to be co-NP-hard in [28]. However, there is a polynomial-time
algorithm for the subclass of normed BPP [18]. Strong bisimilarity between
normed BPA and normed BPP is also decidable [7]. This result even holds
for parallel compositions of normed BPA and normed BPP processes [22].
Recently, this has even been generalized to the class of all normed PA-processes
[16].
For weak bisimilarity, much less is known. Semidecidability of weak bisimilarity
for BPP has been shown in [11]. In [15] it is shown that weak bisimilarity is
decidable for those BPA and BPP processes which are 'totally normed' (a process
is totally normed if it can terminate at any moment via a finite sequence
of computational steps, but at least one of those steps must be 'visible', i.e.,
non-internal). Decidability of weak bisimilarity for general BPA and BPP is
open; those problems might be decidable, but they are surely intractable (as-
suming P 6= NP ). Weak bisimilarity of (normed) BPA is PSPACE-hard [38].
An NP lower bound for weak bisimilarity of BPP has been shown by St-r'ibrn'a
in [38]. This result has been improved to \Pi p
-hardness by Mayr [28] and very
recently to PSPACE-hardness by Srba in [37]. Moreover, the PSPACE lower
bound for weak bisimilarity of BPP in [37] holds even for normed BPP.
The situation is dramatically different if we consider weak bisimilarity between
certain infinite-state processes and finite-state ones. This study is motivated
by the fact that the intended behavior of a process is often easy to specify
(by a finite-state system), but a 'real' implementation can contain components
which are infinite-state (e.g., counters, buffers, recursion, creation of
new parallel subprocesses). It has been shown in [26] that weak bisimilarity
between BPP and finite-state processes is decidable. A more general result
has recently been obtained in [21], where it is shown that many bisimulation-
like equivalences (including the strong and weak ones) are decidable between
PAD and finite-state processes. The class PAD [31,30] strictly subsumes not
only BPA and BPP, but also PA [2] and pushdown processes. The result in
[21] is obtained by a general reduction to the model-checking problem for the
simple branching-time temporal logic EF, which is decidable for PAD [30].
As the model-checking problem for EF is hard (for example, it is known to
be PSPACE-complete for BPP [26] and PSPACE-complete for BPA [39,27]),
this does not yield an efficient algorithm.
Our contribution. We show that weak (and hence also strong) bisimilarity
is decidable in polynomial time between BPA and finite-state processes, and
between normed BPP and finite-state processes. To the best of our knowl-
edge, these are the first polynomial algorithms for weak bisimilarity with
infinite-state systems. Moreover, the algorithm for BPA is the first example
of an efficient decision procedure for a class of unnormed infinite-state systems
(the polynomial algorithms for strong bisimilarity of [17,18] only work
for the normed subclasses of BPA and BPP, respectively). Due to the afore-mentioned
hardness results for the 'symmetric case' (when we compare two
BPA or two (normed) BPP processes) we know that our results cannot be
extended in this direction. A recent work [29] shows that strong bisimilarity
between pushdown processes (a proper superclass of BPA) and finite-state
ones is already PSPACE-hard. Furthermore, weak bisimilarity remains computationally
intractable (DP-hard) even between processes of one-counter nets
and finite-state processes [23] (one-counter nets are computationally equivalent
to the subclass of Petri nets with at most one unbounded place and can
be thus also seen as very simple pushdown automata). Hence, our result for
BPA is rather tight. The question whether the result for normed BPP can
be extended to the class of all (not necessarily normed) BPP processes is left
open. It should also be noted that simulation equivalence with a finite-state
process is co-NP-hard for BPA/BPP processes [25], EXPTIME-complete for
pushdown processes [24], but polynomial for one-counter nets [24].
The basic scheme of our constructions for BPA and normed BPP processes is
the same. The main idea is that weak bisimilarity between BPA (or normed
BPP) processes and finite-state ones can be generated from a finite base of
'small' size and that certain infinite subsets of BPA and BPP state-space can
be 'symbolically' described by finite automata and context-free grammars,
respectively. A more detailed intuition is given in Section 3. An interesting
point about this construction is that it works although weak bisimulation is
not a congruence w.r.t. sequential composition, but only a left congruence.
In Section 4, we propose a natural refinement of weak bisimilarity called
termination-sensitive bisimilarity which is a congruence and which is also
decidable between BPA and finite-state processes in polynomial time. The result
demonstrates that the technique which has been used for weak bisimilarity
actually has a wider applicability-it can be adapted to many 'bisimulation-
like' equivalences. Finally, we should note that our aim is just to show that the
mentioned problems are in although we do compute the degrees of bounding
polynomials explicitly, our analysis is quite simple and rough. Moreover,
both presented algorithms could be easily improved by employing standard
techniques. See the final section for further comments.
We use process rewrite systems [31] as a formal model for processes. Let Act =
countably infinite sets of
actions and process constants, respectively. The class of process expressions E
is defined by
Const and " is a special constant that denotes the empty expres-
sion. Intuitively, ':' is sequential composition and `k' is parallel composition.
We do not distinguish between expressions related by structural congruence
which is given by the following laws: ':' and `k' are associative, 'k' is commu-
tative, and '"' is a unit for `:' and 'k'.
A process rewrite system [31] is specified by a finite set of rules \Delta which have
the form E a
Act . Const (\Delta) and Act (\Delta) denote
the sets of process constants and actions which are used in the rules of \Delta,
respectively (note that these sets are finite). Each process rewrite system \Delta
defines a unique transition system where states are process expressions over
Const (\Delta), Act (\Delta) is the set of labels, and transitions are determined by \Delta
and the following inference rules (remember that 'k' is commutative):
a
E:F a
EkF a
We extend the notation E a
F to elements of Act   in the standard way. F is
reachable from E if E w
Sequential and parallel expressions are those process expressions which do not
contain the 'k' and the `:' operator, respectively. Finite-state, BPA, and BPP
systems are subclasses of process rewrite systems obtained by putting certain
restrictions on the form of the rules. Finite-state, BPA, and BPP allow only
a single constant on the left-hand side of rules, and a single constant, sequential
expression, and parallel expression on the right-hand side, respectively.
The set of states of a transition system which is generated by a finite-state,
BPA, or BPP process \Delta is restricted to Const (\Delta), the set of all sequential expressions
over Const (\Delta), or the set of all parallel expressions over Const (\Delta),
respectively.
Example
"g be a process
rewrite system. We see that \Delta is a BPA system; a part of the transition system
associated to \Delta which is reachable from Z looks as follows:
Z I.Z I.I.Z I.I.I.Z
z
d d
d
If we replace each occurrence of the ':' operator with the `k' operator, we obtain
a BPP system which generates the following transition system (again, we only
draw the part reachable from Z):
Z Z || I Z || I || I Z || I || I || I
d d
d
z z z z
A process is normed iff at every reachable state it can (successfully) terminate
via a finite sequence of computational steps. For a BPA or BPP process, this
is equivalent to the condition that for each constant X 2 Const (\Delta) of its
underlying system \Delta there is some w 2 Act   such that X w
". We call such
constants X with this property normed.
The semantical equivalence we are interested in here is weak bisimilarity [32].
This relation distinguishes between 'observable' and `internal' moves (compu-
tational steps); the internal moves are modeled by a special action which is
denoted '- ' by convention. In what follows we consider process expressions
over Const (\Delta) where \Delta is some fixed process rewrite system.
Definition 2 The extended transition relation ' a
)' is defined by E a
binary relation R over process expressions is a weak bisimulation iff whenever
then for each a 2 Act :
there is F a
ffl if F a
then there is E a
are weakly bisimilar, written E - F , iff there is a weak bisimulation
relating them.
Weak bisimilarity can be approximated by the family of - i relations, which
are defined as follows:
and the following conditions hold:
there is F a
then there is E a
It is worth noting that - i is not an equivalence for i - 1, as it is not transitive.
It is possible to approximate weak bisimilarity in a different way so that the
approximations are equivalences (see [21]). However, we do not need this for
our purposes.
\Gamma be a finite-state system with n states, f; g 2 Const (\Gamma). It is easy to
show that the problem whether f - g is decidable in O(n 3 ) time. First we
compute in O(n 3 ) time the transitive closure of the transition system w.r.t.
the -
transitions and thus obtain a new system in which a
! is the same as
a
) in the old system. Then it suffices to decide strong bisimilarity of f and
g in the new system. This can be done in O(n 2 log n) time, using partition
refinement techniques from [34].
Sometimes we also consider weak bisimilarity between processes of different
process rewrite systems, say \Delta and \Gamma. Formally, \Delta and \Gamma can be considered
as a single system by taking their disjoint union.
In this section we prove that weak bisimilarity is decidable between BPA and
finite-state processes in polynomial time.
Let E be a BPA process with the underlying system \Delta, F a finite-state process
with the underlying system \Gamma such that Const (\Delta) " Const
(w.l.o.g.) that E 2 Const (\Delta). Moreover, we also assume that for all f; g 2
Const (\Gamma), a 2 Act such that f 6= g or a 6= - we have that f a
implies
f a
\Gamma. If those ' a
!' transitions are missing in \Gamma, we can add them
safely. Adding these transitions does not change the weak bisimilarity relation
among the states. In order to do this it suffices to compute (in cubic time)
the transitive closure of \Gamma w.r.t. the - transitions. These extra transitions do
not influence our complexity estimations, as we always consider the worst case
when \Gamma has all possible transitions. The condition that a 6= - is there because
we do not want to add new transitions of the form f -
our proof for weak bisimilarity would not immediately work for termination-
sensitive bisimilarity (which is defined at the end of this section).
We use upper-case letters to denote elements of Const (\Delta), and lower-case
letters f; to denote elements of Const (\Gamma). Greek letters ff; are
used to denote elements of Const (\Delta)   . The size of \Delta is denoted by n, and the
size of \Gamma by m (we measure the complexity of our algorithm in (n; m)).
The set Const (\Delta) can be divided into two disjoint subsets of normed and
unnormed constants (remember that X 2 Const (\Delta) is normed iff X w
for some w 2 Act   ). Note that it is decidable in O(n 2 a constant is
normed. The set of all normed constants of \Delta is denoted Normed (\Delta). In our
constructions we also use processes of the form fff ; they should be seen as
BPA processes with the underlying system \Delta [ \Gamma.
Intuition: Our proof can be divided into two parts: first we show that the
greatest weak bisimulation between processes of \Delta and \Gamma is finitely repre-
sentable. There is a finite relation B of size O(nm 2 ) (called bisimulation base)
such that each pair of weakly bisimilar processes can be generated from that
base (a technique first used by Caucal [6]). Then we show that the bisimulation
base can be computed in polynomial time. To do that, we take a sufficiently
large relation G which surely subsumes the base and 'refine' it (this refinement
technique has been used in [17,18]). The size of G is still O(nm 2 ), and
each step of the refinement procedure possibly deletes some of the elements
of G. If nothing is deleted, we have found the base (hence we need at most
steps). The refinement step is formally introduced in Definition 9 (we
compute the expansion of the currently computed approximation of the base).
Intuitively, a pair of processes belongs to the expansion iff for each a
move
of one component there is a a
move of the other component such that the
resulting pair of processes can be generated from the current approximation
of B. We have to overcome two problems:
1. The set of pairs which can be generated from B (and its approximations) is
infinite.
2. The set of states which are reachable from a given BPA state in one ' a
move is infinite.
We employ a 'symbolic' technique to represent those infinite sets (similar to
the one used in [3]), taking advantage of the fact that they have a simple (reg-
ular) structure which can be encoded by finite-state automata (see Theorem 6
and 12). This allows to compute the expansion in polynomial time.
relation K is well-formed iff it is a subset of the relation G
defined by
Const (\Gamma)) \Theta Const (\Gamma))
(Const (\Delta) \Theta Const (\Gamma))
(Const (\Gamma) \Theta Const (\Gamma))
Const (\Gamma))
Note that the size of any well-formed relation is O(nm 2 ) and that G is the
greatest well-formed relation.
One of the well-formed relations is of special importance.
Definition 4 The bisimulation base for \Delta and \Gamma, denoted B, is defined as
follows:
As weak bisimilarity is a left congruence w.r.t. sequential composition, we
can 'generate' from B new pairs of weakly bisimilar processes by substitution
(it is worth noting that weak bisimilarity is not a right congruence w.r.t.
sequencing-to see this, it suffices to define X -
Z. Now
generation procedure can be defined for any
well-formed relation as follows:
Definition 5 Let K be a well-formed relation. The closure of K, denoted
is the least relation M which satisfies the following conditions:
contains an unnormed constant, then (fffi; g); (fffih; g) 2
M for every fi 2 Const (\Delta)   and h 2 Const (\Gamma).
Note that Cl(K) contains elements of just two forms - (ff; g) and (fff; g).
consists of
and the pairs which can be immediately derived from Cl(K) i by the
rules 2-6 of Definition 5.
Although the closure of a well-formed relation can be infinite, its structure is in
some sense regular. This fact is precisely formulated in the following theorem:
Theorem 6 Let K be a well-formed relation. For each g 2 Const (\Gamma) there
is a finite-state automaton A g of size O(nm 2 ) constructible in O(nm 2
such that
PROOF. We construct a regular grammar of size O(nm 2 ) which generates
the mentioned language. Let G
Const (\Gamma)g [ fUg
Const (\Delta) [ Const (\Gamma)
ffl ffi is defined as follows:
for each ("; h) 2 K we add the rule h ! ".
for each (f; h) 2 K we add the rules h
for each (Y f; h) 2 K we add the rules
for each (X; h) 2 K we add the rule h ! X and if X is unnormed, then
we also add the rule h ! XU .
for each X 2 Const (\Delta), f 2 Const (\Gamma) we add the rules U ! XU , U ! X,
A proof that G g indeed generates the mentioned language is routine. Now we
translate G g to A g (see, e.g., [19]). Note that the size of A g is essentially the
same as the size of G g ; A g is non-deterministic and can contain "-rules.
It follows immediately that for any well-formed relation K, the membership
problem for Cl(K) is decidable in polynomial time. Another property of Cl(K)
is specified in the lemma below.
Cl(K). Similarly, if (fi; f) 2
PROOF. We just give a proof for the first claim (the second one is similar).
Let (fff; g) 2 Cl(K) i . By induction on i.
and we can immediately apply the rule 3 or 5 of
Definition 5 (remember that ff can be ").
ffl Induction step. Let (fff; g) 2 Cl(K) i+1 . There are three possibilities (cf.
Definition 5).
I. There is r such that (fff; r) 2 K. By induction hypothesis
we know (fffih; r) 2 due to the rule 3 of
Definition 5.
II. there is r such that (Y
hypothesis we have (flfih; r) 2 Cl(K), and hence also (Y flfih; r) 2
Cl(K) by the rule 5 of Definition 5.
III. contains an unnormed constant.
Then (fl ffifih; g) 2 Cl(K) by the last rule of Definition 5.
The importance of the bisimulation base is clarified by the following theorem.
It says that Cl(B) subsumes the greatest weak bisimulation between processes
of \Delta and \Gamma.
Theorem 8 For all ff; f; g we have ff - g iff (ff; g) 2 Cl(B), and fff - g iff
PROOF. The 'if' part is obvious in both cases, as B contains only weakly
bisimilar pairs and all the rules of Definition 5 produce pairs which are again
weakly bisimilar. The 'only if' part can, in both cases, be easily proved by
induction on the length of ff (we just show the first proof; the second one is
similar).
and (Y; g) 2 B. By the rule 6
of Definition 5 we obtain (Y fi; g) 2 Cl(B). If Y is normed, then Y fi w
for some w 2 Act   and g must be able to match the sequence w by some
such that fi - g 0 . By substitution we now obtain that Y g 0 - g.
induction hypothesis. Hence
due to the rule 4 of Definition 5.
The next definition formalizes one step of the 'refinement procedure' which
is applied to G to compute B. The intuition is that we start with G as an
approximation to B. In each refinement step some pairs are deleted from the
current approximation. If in a refinement step no pairs are deleted any more
then we have found B. The next definition specifies the condition on which
a given pair is not deleted in a refinement step from the currently computed
approximation of B.
Definition 9 Let K be a well-formed relation. We say that a pair (X; g) of
K expands in K iff the following two conditions hold:
ffl for each X a
! ff there is some g a
ffl for each g a
there is some X a
ff such that (ff;
The expansion of a pair of the form (Y f; g), (f; g), ("; g) in K is defined in the
same way-for each ' a
!' move of the left component there must be some ' a
move of the right component such that the resulting pair of processes belongs
to Cl(K), and vice versa (note that " -
"). The set of all pairs of K which
expand in K is denoted by Exp(K).
The notion of expansion is in some sense 'compatible' with the definition of
bisimulation. This intuition is formalized in the following lemma.
K be a well-formed relation such that
Cl(K) is a weak bisimulation.
PROOF. We prove that every pair (ff; g); (fff; g) of Cl(K) i has the property
that for each ' a
!' move of one component there is a ' a
)' move of the other
component such that the resulting pair of processes belongs to Cl(K) (we
consider just pairs of the form (fff; g); the other case is similar). By induction
on i.
the claim follows directly from
the definitions.
ffl Induction step. Let (fff; g) 2 Cl(K) i+1 . There are three possibilities:
I. There is an h such that (fff;
Let fff a
flf (note that ff can be empty; in this case we have to
consider moves of the form f a
. It is done in a similar way as below).
As (fff; h) 2 Cl(K) i , we can use the induction hypothesis and conclude
that there is h a
We distinguish two cases:
and as (h; g) 2 K, we obtain
due to Lemma 7. Hence g can use the move g -
g.
. Then there is a transition h a
(see the beginning
of this section) and as (h; g) 2 K, by induction hypothesis we know that
there is some g a
due to Lemma 7.
Now let g a
As (h; g) 2 K, there is h a
Cl(K). We distinguish two possibilities again:
use the move fff -
a 6= - or h 6= h 0 . Then h a
there is fff a
(or fff a
is handled in the same way) such that (flf; h 0
Hence also (flf; g 0 ) 2 Cl(K) by Lemma 7.
II. there is h such that (Y h; g) 2 K, (fif;
Let Y fif a
flfif . As (Y h; g) 2 K, we can use induction hypothesis and
conclude that there is g a
As (fif;
we obtain (flfif;
Let g a
. As (Y h; g) 2 K, by induction hypothesis we know that Y h
can match the move g a
there are two possibilities:
flh such that (flh;
As
immediately have (flfif;
Cl(K). The transition Y h a
can be
h, h y
h, we are done immediately because then Y fi a
and as (h; g 0 ); (fi; needed.
If y 6= - or h 0 6= h, there is a transition h y
As (fif;
due to induction hypothesis we know that there is some fif y
fif y
this is handled in the same way) with (flf; h 0
Y fif a
As
III. contains an unnormed constant and (fi; g) 2 Cl(K) i .
Let ff a
ffi. As (fi; g) 2 Cl(K) i , there is
a
due to the induction hypothesis. Clearly
contains an unnormed constant, hence (ffifl; by the last rule
of Definition 5.
Let g a
As (fi; g) 2 Cl(K) i , there is fi a
and ffi contains an unnormed constant. Hence ff a
due to the last rule of Definition 5.
The notion of expansion allows to approximate B in the following way:
Theorem 11 There is a j 2 N, bounded by O(nm 2 ), such that
PROOF. Exp (viewed as a function on the complete lattice of well-formed
relations) is monotonic, hence the greatest fixed-point exists and must be
reached after O(nm 2 ) steps, as the size of G is O(nm 2 ). We prove that
'':' First, let us realize that immediately from Definition
4, Definition 9, and Theorem 8). The inclusion can be proved
by a simple inductive argument; clearly
by definition of the expansion and the fact
":' As Exp(B j we know that Cl(B j ) is a weak bisimulation due to
Lemma 10. Thus, processes of every pair in B j are weakly bisimilar.
In other words, B can be obtained from G in O(nm 2 ) refinement steps which
correspond to the construction of the expansion. The only thing which remains
to be shown is that Exp(K) is effectively constructible in polynomial time. To
do that, we employ a 'symbolic' technique which allows to represent infinite
subsets of BPA state-space in an elegant and succinct way.
Theorem 12 For all X 2 Const (\Delta), a 2 Act (\Delta) there is a finite-state automaton
A (X;a) of size O(n 2 ) constructible in O(n 2 ) time such that
PROOF. We define a left-linear grammar G (X;a) of size O(n 2 ) which generates
the mentioned language. This grammar can be converted to A (X;a)
by a standard algorithm known from automata theory (see, e.g., [19]). Note
that the size of A (X;a) is essentially the same as the size of G (X;a) . First, let
us realize that we can compute in O(n 2 ) time the sets M - and M a consisting
of all Y 2 Const (\Delta) such that Y -
Const (\Delta)g [ fSg. Intuitively, the index indicates
whether the action 'a' has already been emitted.
Const (\Delta)
ffl ffi is defined as follows:
We add the production S ! X a to ffi, and if X a
we also add the
production
\Delta For every transition Y a
of \Delta and every i such that 1 -
we test whether Z j
i. If this is the case, we add to
ffi the productions
\Delta For every transition Y -
of \Delta and every i such that 1 -
we do the following:
We test whether Z j
i. If this is the case, we
add to ffi the productions
Y a ! Z a
We test whether there is a t ! i such that Z t
a
every t. If this is the case, we add to ffi the productions
The fact that G (X;a) generates the mentioned language is intuitively clear and
a formal proof of that is easy. The size of G (X;a) is O(n 2 ), as \Delta contains O(n)
basic transitions of length O(n).
The crucial part of our algorithm (the 'refinement step') is presented in the
proof of the next theorem. Our complexity analysis is based on the following
facts: Let be a non-deterministic automaton with "-rules,
and let t be the total number of states and transitions of A.
ffl The problem whether a given w 2 \Sigma   belongs to L(A) is decidable in
O(jwj \Delta t) time.
ffl The problem whether decidable in O(t) time.
Theorem 13 Let K be a well-formed relation. The relation Exp(K) can be
effectively constructed in
PROOF. First we construct the automata A g of Theorem 6 for every g 2
Const (\Gamma). This takes O(nm 3 ) time. Then we construct the automata A (X;a) of
Theorem 12 for all X; a. This takes O(n 4 ) time. Furthermore, we also compute
the set of all pairs of the form (f; g); ("; g) which belong to Cl(K). It can be
done in O(m 2 ) time. Now we show that for each pair of K we can decide in
expands in K.
The pairs of the form (f; g) and ("; g) are easy to handle; there are at most m
states f 0 such that f a
, and at most m states g 0 with g a
hence we need
to check only O(m 2 ) pairs to verify the first (and consequently also the second)
condition of Definition 9. Each such pair can be checked in constant time,
because the set of all pairs (f; g); ("; g) which belong to Cl(K) has already
been computed at the beginning.
Now let us consider a pair of the form (Y; g). First we need to verify that for
each Y a
! ff there is some g a
h such that (ff; h) 2 Cl(K). This requires
O(nm) tests whether ff 2 As the length of ff is O(n) and the size
of A h is O(nm 2 ), each such test can be done in O(n 2 hence we
need O(n total. As for the second condition of Definition 9,
we need to find out whether for each g a
! h there is some X a
ff such that
To do that, we simply test the emptiness of
The size of the product automaton is O(n 3 we need to perform only
O(m) such tests, hence O(n 3 suffices.
Pairs of the form (Y f; g) are handled in a similar way; the first condition of
Definition 9 is again no problem, as we are interested only in the ' a
!' moves
of the left component. Now let g a
An existence of a 'good' a
move of
Y f can be verified by testing whether one of the following conditions holds:
ffl Y a
" and there is some f -
" and there is some f a
All those conditions can be checked in O(n 3 required analysis
has been in fact done above). As K contains O(nm 2 ) pairs, the total time
which is needed to compute Exp(K) is O(n 4 m 5 ).
As the BPA process E (introduced at the beginning of this section) is an
element of Const (\Delta), we have that To compute B,
we have to perform the computation of the expansion O(nm 2 ) times (see
Theorem 11). This gives us the following main theorem:
Theorem 14 Weak bisimilarity is decidable between BPA and finite-state
processes in O(n 5
4 Termination-Sensitive Bisimilarity
As we already mentioned in the previous section, weak bisimilarity is not a
congruence w.r.t. sequential composition. This is a major drawback, as any
equivalence which is to be considered as 'behavioral' should have this prop-
erty. We propose a solution to this problem by designing a natural refinement
of weak bisimilarity called termination-sensitive bisimilarity. This relation respects
some of the main features of sequencing which are 'overlooked' by weak
consequently, it is a congruence w.r.t. sequential composition. We
also show that termination-sensitive bisimilarity is decidable between BPA and
finite-state processes in polynomial time by adapting the method of the previous
section. It should be noted right at the beginning that we do not aim
to design any new 'fundamental' notion of the theory of sequential processes
(that is why the properties of termination-sensitive bisimilarity are not studied
in detail). We just want to demonstrate that our method is applicable to a
larger class of bisimulation-like equivalences and the relation of termination-
sensitive bisimilarity provides a (hopefully) convincing evidence that some of
them might be interesting and useful.
In our opinion, any 'reasonable' model of sequential behaviors should be able
to express (and distinguish) the following 'basic phenomena' of sequencing:
ffl successful termination of the process which is currently being executed. The
system can then continue to execute the next process in the queue;
ffl unsuccessful termination of the executed process (deadlock). This models a
severe error which causes the whole system to 'get stuck';
ffl entering an infinite internal loop (cycling).
The difference between successful and unsuccessful termination is certainly
significant. The need to distinguish between termination and cycling has also
been recognized in practice; major examples come, e.g., from the theory of
operating systems.
BPA processes are a very natural model of recursive sequential behaviors.
Successful termination is modeled by reaching '"'. There is also a `hidden'
syntactical tool to model deadlock-note that by the definition of BPA systems
there can be an X 2 Const (\Delta) such that \Delta does not contain any rule of the
form X a
us call such constants undefined ). A state Xfi models the
situation when the executed process reaches a deadlock-there is no transition
(no computational step) from Xfi, the process is 'stuck'. It is easy to see that
we can safely assume that \Delta contains at most one undefined constant (the
other ones can be simply renamed to X), which is denoted ffi by convention
[2]. Note that ffi is unnormed by definition. States of the form ffiff are called
deadlocked.
In the case of finite-state systems, we can distinguish between successful and
unsuccessful termination in a similar way. Deadlock is modeled by a distinguished
undefined constant ffi, and the other undefined constants model successful
termination.
Note that by definition of weak bisimilarity. As '"' represents a successful
termination, this is definitely not what we want. Before we define the promised
relation of termination-sensitive bisimilarity, we need to clarify what is meant
by cycling; intuitively, it is the situation when a process enters an infinite
internal loop. In other words, it can do '- ' forever without a possibility to do
anything else or to terminate (either successfully or unsuccessfully).
Definition 15 The set of initial actions of a process E, denoted I(E), is
defined by
Fg. A process E is cycling iff
every state F which is reachable from E satisfies I(F
Note that it is easily decidable in quadratic time whether a given BPA process
is cycling; in the case of finite-state systems we only need linear time.
Definition We say that an expression E is normal iff E is not cycling,
deadlocked, or successfully terminated.
binary relation R over process expressions is a termination-sensitive bisimulation
then the following conditions hold:
ffl if one of the expressions E; F is cycling then the other is also cycling;
ffl if one of the expressions E; F is deadlocked then the other is either normal
or it is also deadlocked;
ffl if one of the expressions E; F is successfully terminated then the other is
either normal or it is also successfully terminated;
there is F a
ffl if F a
then there is E a
are termination-sensitive bisimilar, written E ' F , iff there is
a termination-sensitive bisimulation relating them.
Termination-sensitive bisimilarity seems to be a natural refinement of weak
bisimilarity which better captures an intuitive understanding of 'sameness' of
sequential processes. It distinguishes among the phenomena mentioned at the
beginning of this section, but it still allows to ignore internal computational
steps to a large extent. For example, a deadlocked process is still equivalent to
a process which is not deadlocked yet but which necessarily deadlocks after a
finite number of - transitions (this example also explains why the first three
conditions of Definition are stated so carefully).
The family of ' i approximations is defined in the same way as in case of weak
bisimilarity; the only difference is that ' 0 relates exactly those processes which
satisfy the first three conditions of Definition 16. The following theorem follows
immediately from this definition.
Theorem 17 Termination-sensitive bisimilarity is a congruence w.r.t. sequential
composition.
The technique which has been used in the previous section also works for
termination-sensitive bisimilarity.
Theorem Termination-sensitive bisimilarity is decidable between BPA and
finite-state processes in O(n 5
PROOF. First, all assumptions about \Delta and \Gamma which were mentioned at the
beginning of Section 3 are also safe w.r.t. termination-sensitive bisimilarity;
note that it would not be true if we also assumed the existence of a -loop
f for every f 2 Const (\Gamma). Now we see why the assumptions about \Gamma
are formulated so carefully. The only thing which has to be modified is the
notion of well-formed relation; it is defined in the same way, but in addition
we require that processes of every pair which is contained in a well-formed
relation K are related by ' 0 . It can be easily shown that processes of pairs
contained in Cl(K) are then also related by ' 0 . In other words, we do not
have to take care about the first two requirements of Definition 16 in our
constructions anymore; everything works without a single change.
The previous proof indicates that the 'method' of Section 3 can be adapted to
other bisimulation-like equivalences. See the final section for further comments.
5 Normed BPP Processes
In this section we prove that weak bisimilarity is decidable in polynomial time
between normed BPP and finite-state processes. The basic structure of our
proof is similar to the one for BPA. The key is that the weak bisimulation
problem can be decomposed into problems about the single constants and
their interaction with each other. In particular, a normed BPP process is
finite w.r.t. weak bisimilarity iff every single reachable process constant is
finite w.r.t. weak bisimilarity. This does not hold for general BPP and thus
our construction does not carry over to general BPP.
Example 19 Consider the unnormed BPP that is defined by the following
rules.
a
a i
an
Then the process X 1 w.r.t. bisimilarity, but every subprocess
(e.g. X 3 kX 4 kX 7 or every single constant X i ) is infinite w.r.t. bisimilarity.
Even for normed BPP, we have to solve some additional problems. The bisimulation
base and its closure are simpler due to the normedness assumption,
but the 'symbolic' representation of BPP state-space is more problematic (see
below). The set of states which are reachable from a given BPP state in one
' a
)' move is no longer regular, but it can be in some sense represented by
a CF-grammar. In our algorithm we use the facts that emptiness of a CF
language is decidable in polynomial time, and that CF languages are closed
under intersection with regular languages.
Let E be a BPP process and F a finite-state process with the underlying
systems \Delta and \Gamma, respectively. We can assume w.l.o.g. that E 2 Const (\Delta).
Elements of Const (\Delta) are denoted by X; Y; elements of Const (\Gamma) by
The set of all parallel expressions over Const (\Delta) is denoted by
Const
(\Delta)\Omega and its elements by Greek letters ff; The size of \Delta is denoted
by n, and the size of \Gamma by m.
In our constructions we represent certain subsets of Const
(\Delta)\Omega by finite automata
and CF grammars. The problem is that elements of Const
(\Delta)\Omega are
considered modulo commutativity; however, finite automata and CF grammars
of course distinguish between different 'permutations' of the same word.
As the classes of regular and CF languages are not closed under permutation,
this problem is important. As we want to clarify the distinction between ff
and its possible 'linear representations', we define for each ff the set Lin(ff)
as follows:
is a permutation of the set f1; \Delta
For example, Lin(XkY Xg. We
also assume that each Lin(ff) contains some (unique) element called canonical
form of Lin(ff). It is not important how the canonical form is chosen; we need
it just to make some constructions deterministic (for example, we can fix some
linear order on process constants and let the canonical form of Lin(ff) be the
sorted order of constants of ff).
relation K is well-formed iff it is a subset of (Const (\Delta)[
f"g) \Theta Const (\Gamma). The bisimulation base for \Delta and \Gamma, denoted B, is defined
as follows:
Definition 21 Let K be a well-formed relation. The closure of K, denoted
is the least relation M which satisfies
The family of Cl(K) i approximations is defined in the same way as in Section 3.
Lemma 22 Let (ff; f) 2
Cl(K).
PROOF. Let (ff; f) 2 Cl(K) i . By induction on i.
and we can immediately apply the rule 2 or 3 of
Definition 21.
ffl Induction step. Let (ff; f) 2 Cl(K) i+1 . There are two possibilities.
I. and there are s such that (X; r) 2 K, (fl; s) 2 Cl(K) i , and
rks - f . Clearly rkskg - h, hence also skg - t for some t. By induction
hypothesis we have (flkfi; due to
the second rule of Definition 21 (note that rkt - h).
II. (ff; r) 2 Cl(K) i and there is some s such that ("; s) 2 K and rks - f .
As rkskg - h, there is some t such that rkg - t. By induction hypothesis
we obtain (ffkfi; due to the third
rule of Definition 21.
Again, the closure of the bisimulation base is the greatest weak bisimulation
between processes of \Delta and \Gamma.
Theorem 23 Let ff 2 Const
Const (\Gamma). We have that ff - f iff
PROOF. The 'if' part is obvious. The `only if' part can be proved by induction
on length(ff).
As \Delta is normed and Xkfi - f , there are w; v 2 Act   such that
X. The process f must be able to match the sequences
w; v by entering weakly bisimilar states-there are Const (\Delta) such
that fi - g, X - h, and consequently also f - gkh (here we need the fact
that weak bisimilarity is a congruence w.r.t. the parallel operator). Clearly
induction hypothesis, hence (Xkfi; f) 2
by Definition 21.
The closure of any well-formed relation can in some sense be represented by
a finite-state automaton, as stated in the next theorem. For this construction
we first need to compute the set f(fkg; hg. We consider the parallel
composition of the finite-state system with itself, i.e., the states of this system
are of the form fkg. Let our new system be the union of this system with the
old system. The new system has size O(m 2 ) and its states are of the form fkg
or h. Then we apply the usual cubic-time partition refinement algorithm to
decide bisimilarity on the new system (see Section 2). This gives us the set
Theorem 24 Let K be a well-formed relation. For each g 2 Const (\Gamma) there
is a finite-state automaton A g of size O(nm) constructible in O(nm) time
such that the following conditions hold:
ffl whenever A g accepts an element of Lin(ff), then (ff; g) 2 Cl(K)
accepts at least one element of Lin(ff)
PROOF. We design a regular grammar of size O(nm) such that L(G g ) has
the mentioned properties. Let G
Const (\Gamma) [ fSg
Const (\Delta)
ffl ffi is defined as follows:
for each (X; f) 2 K we add the rule S ! Xf .
for each ("; f) 2 K we add the rule S ! f .
\Delta for all f; Const (\Gamma), X 2 Const (\Delta) such that (X; r) 2 K, f - rks
we add the rule s ! Xf .
\Delta for all f; Const (\Gamma) such that ("; r) 2 K, f - rks we add the rule
\Delta we add the rule g ! ".
The first claim follows from an observation that whenever we have ff 2 Lin(ff)
such that fff is a sentence of G g , then (ff; f) 2 Cl(K). This can be easily
proved by induction on the length of the derivation of fff . For the second
part, it suffices to prove that if (ff; f) 2 Cl(K) i , then there is ff 2 Lin(ff) such
that fff is a sentence of G g . It can be done by a straightforward induction on
i.
It is important to realize that if (ff; g) 2 does not necessarily
accept all elements of Lin(ff). For example, if
Const
Const (\Gamma), then A g accepts the string XY Z but not the string XZY . Generally,
A g cannot be 'repaired' to do so (see the beginning of this section); however,
there is actually no need for such 'repairs', because A g has the following nice
property:
Lemma 25 Let K be a well-formed relation such that B ' K. If ff - g, then
the automaton A g of (the proof of) Theorem 24 constructed for K accepts all
elements of Lin(ff).
PROOF. Let G g be the grammar of the previous proof. First we prove that
for all s; Const (\Gamma), Const
(\Delta)\Omega such that fl - r, skr - f there is a
derivation s !   flf in G g for every fl 2 Lin(fl). By induction on length(fl).
the pair ("; r) belongs to B. Hence s ! f by definition of
G g .
is of the form Xkfi
where fi 2 Lin(fi). As Xkfi - r and \Delta is normed, there are u; v 2 Const (\Gamma)
such that X - u, fi - v, and ukv - r. Hence we also have skukv - f , thus
Const (\Gamma). As X - u, the pair (X; u) belongs to B.
by definition of G g . As fi - v and vkt - f , we can use the
induction hypothesis and conclude t !   fif . Hence s !   Xfif as required.
Now let ff - g. As \Delta is normed, there is some r 2 Const (\Gamma) such that " - r.
Hence by definition of G g . Clearly rkg - g and due to
the above proved property we have r !   ffg for every ff 2 Lin(ff). As
is a rule of G g , we obtain
The set of states which are reachable from a given X 2 Const (\Delta) in one ' a
move is no longer regular, but it can, in some sense, be represented by a CF
grammar.
Theorem 26 For all X 2 Const (\Delta), a 2 Act (\Delta) there is a context-free grammar
G (X;a) in 3-GNF (Greibach normal form, i.e., with at most 2 variables at
the right hand side of every production) of size O(n 4 ) constructible in O(n 4 )
time such that the following two conditions hold:
ffl if G (X;a) generates an element of Lin(ff), then X a
(X;a) generates at least one element of Lin(ff)
PROOF. Let G
Const (\Delta)
ffl ffi is defined as follows:
\Delta the rule S ! X a is added to ffi.
for each transition Y a
of \Delta we add the rule
we add the rule Y a ! ").
for each transition Y -
of \Delta we add the rule
also add the rule
for each Y 2 Const (\Delta) we add the rule
The fact that G (X;a) satisfies the above mentioned conditions follows directly
from its construction. Note that the size of G (X;a) is O(n 2 ) at the moment. Now
we transform G (X;a) to 3-GNF by a standard procedure of automata theory
(see [19]). It can be done in O(n 4 time and the size of resulting grammar is
O(n 4 ).
The notion of expansion is defined in a different way (when compared to the
one of the previous section).
Definition 27 Let K be a well-formed relation. We say that a pair (X; f) 2
K expands in K iff the following two conditions hold:
ffl for each X a
! ff there is some f a
such that ff 2 L(A g ), where ff is the
canonical form of Lin(ff).
ffl for each f a
! g the language
A pair ("; f) 2 K expands in K iff f a
implies for each f -
we have that " 2 L(A g ). The set of all pairs of K which expand in K is denoted
by Exp(K).
Theorem 28 Let K be a well-formed relation. The set Exp(K) can be computed
in O(n 11 m 8 ) time.
PROOF. First we compute the automata A g of Theorem 24 for all g 2
Const (\Gamma). This takes O(nm 2 ) time. Then we compute the grammars G (X;a)
of Theorem 26 for all X 2 Const (\Delta), a 2 Act . This takes O(n 6 ) time. Now
we show that it is decidable in O(n f) of K
expands in K.
The first condition of Definition 27 can be checked in O(n 3 time, as there
are O(n) transitions X a
states g such that f a
g, and for each
such pair (ff; g) we verify whether ff 2 is the canonical form
of Lin(ff); this membership test can be done in O(n 2 m) time, as the size of
ff is O(n) and the size of A g is O(nm).
The second condition of Definition 27 is more expensive. To test the emptiness
of first construct a pushdown automaton P which recognizes
this language. P has O(m) control states and its total size is O(n 5 m).
Furthermore, each rule pX a
! qff of P has the property that length(ff) - 2,
because G (X;a) is in 3-GNF. Now we transform this automaton to an equivalent
CF grammar by a well-known procedure described, e.g., in [19]. The size of
the resulting grammar is O(n 5 m 3 ), and its emptiness can be thus checked in
This construction has to be performed O(m) times,
hence we need O(n
Pairs of the form ("; f) are handled in a similar (but less expensive) way. As
K contains O(nm) pairs, the computation of Exp(K) takes O(n
The previous theorem is actually a straightforward consequence of Definition
27. The next theorem says that Exp really does what we need.
Theorem 29 Let K be a well-formed relation such that
Cl(K) is a weak bisimulation.
PROOF. Let (ff; f) 2 Cl(K) i . We prove that for each ff a
! fi there is some
f a
such that (fi; g) 2 Cl(K) and vice versa. By induction on i.
and we can distinguish the following two possibilities

Let X a
fi. By Definition 27 there is f a
such that fi 2
some fi 2 Lin(fi). Hence (fi; g) 2 Cl(K) due to the first part of Theorem
24.
Let f a
g. By Definition 27 there is some string w 2
Let w 2 Lin(fi). We have X a
due to the first part of Theorem 26, and
due to Theorem 24.
Let f a
g. Then Hence ("; g) 2
Cl(K) due to Theorem 24.
ffl Induction step. Let (ff; f) 2 Cl(K) i+1 . There are two possibilities.
I. and there are s such that (X; r) 2 K, (fl; s) 2 Cl(K) i , and
rks - f .
Let Xkff a
fi. The action 'a' can be emitted either by X or by ff. We
distinguish the two cases.
ffikfl. As (X; r) 2 K and X a
! ffi, there is some r a
such that (ffi; r 0 As rks - f and r a
there is some f a
such that r 0 ks - g. To sum up, we have (ffi; r 0
ks - g, hence (ffikfl; g) 2 Cl(K) due to Lemma 22.
Xkae. As (fl; s) 2 Cl(K) i and fl a
ae, there is s a
that (ae; s 0 As rks - f and s a
there is f a
such that
(rks g. Due to Lemma 22 we obtain (Xkae; g) 2 Cl(K).
Let f a
g. As rks - f , there are r x
a such that r 0 ks 0 - g. As (X; r) 2 K, (fl; s) 2 Cl(K) i , there
are X x
ae such that (ffi; r 0
and (ffikae; g) 2 Cl(K) due to Lemma 22.
II. (ff; r) 2 Cl(K) i and there is some s such that ("; s) 2 K and rks - f .
The proof can be completed along the same lines as above.
Now we can approximate (and compute) the bisimulation base in the same
way as in the Section 3.
Theorem There is a j 2 N, bounded by O(nm), such that
PROOF. '':' It suffices to show that
Const (\Delta) or ff = ". We show that (X; f)
expands in B (a proof for the pair ("; f) is similar).
Let X a
fi. As X - f , there is f a
such that fi - g. Let fi be the canonical
form of Lin(fi). Due to Lemma 25 we have
Let f a
g. As X - f , there is X a
g. Due to Theorem 26
there is fi 2 Lin(fi) such that fi 2 L(G (X;a) ). Moreover, fi 2 due to
Lemma 25. Hence,
":' It follows directly from Theorem 29.
Theorem 31 Weak bisimilarity between normed BPP and finite-state processes
is decidable in O(n 12 m 9 ) time.
PROOF. By Theorem 30 the computation of the expansion of Theorem 28
(which costs O(n 11 m 8 ) time) has to be done O(nm) times.
6 Conclusions
We have proved that weak bisimilarity is decidable between BPA processes
and finite-state processes in O(n 5 m 7 ) time, and between normed BPP and
finite-state processes in O(n 12 m 9 ) time. It may be possible to improve the algorithm
by re-using previously computed information, for example about sets
of reachable states, but the exponents would still be very high. This is because
the whole bisimulation basis is constructed. To get a more efficient algorithm,
one could try to avoid this. Note however, that once we have constructed B
(for a BPA/nBPP system \Delta and a finite-state system \Gamma) and the automaton
A g of Theorem 6/Theorem 24 (for Const (\Gamma)), we can
decide weak bisimilarity between a BPA/nBPP process ff over \Delta and a process
Const (\Gamma) in time O(jffj)-it suffices to test whether A f accepts ff
(observe that there is no substantial difference between A f and A g except for
the initial state).
The technique of bisimulation bases has also been used for strong bisimilarity
in [17,18]. However, those bases are different from ours; their design and the
way how they generate 'new' bisimilar pairs of processes rely on additional
algebraic properties of strong bisimilarity (which is a full congruence w.r.t.
sequencing, allows for unique decompositions of normed processes w.r.t. sequencing
and parallelism, etc. The main difficulty of those proofs is to show
that the membership in the 'closure' of the defined bases is decidable in polynomial
time. The main point of our proofs is the use of 'symbolic' representation
of infinite subsets of BPA and BPP state-space.
We would also like to mention that our proofs can be easily adapted to other
bisimulation-like equivalences, where the notion of 'bisimulation-like' equivalence
is the one of [21]. A concrete example is termination-sensitive bisimilarity
of Section 4. Intuitively, almost every bisimulation-like equivalence has the algebraic
properties which are needed for the construction of the bisimulation
base, and the 'symbolic' technique for state-space representation can also be
adapted. See [21] for details.



--R

Decidability of bisimulation equivalence for processes generating context-free languages
Process Algebra.
Reachability analysis of pushdown automata: application to model checking.
An elementary decision procedure for arbitrary context-free processes
More infinite results.
Graphes canoniques des graphes alg'ebriques.

Decidability and Decomposition in Process Algebras.
Bisimulation is decidable for all basic parallel processes.
Bisimulation equivalence is decidable for all context-free processes
Petri nets
Decidability of model checking for infinite-state concurrent systems
An automata-theoretic approach to interprocedural data-flow analysis
A short proof of the decidability of bisimulation for normed BPA processes.
Bisimulation trees and the decidability of weak bisimulations.
Bisimulation equivalence is decidable for normed process algebra.
A polynomial algorithm for deciding bisimilarity of normed context-free processes
A polynomial algorithm for deciding bisimulation equivalence of normed basic parallel processes.
Introduction to Automata Theory
Actions speak louder than words: Proving bisimilarity for context-free processes
Deciding bisimulation-like equivalences with finite-state processes
Effective decomposability of sequential behaviours.
Efficient verification algorithms for one-counter processes
On simulation-checking with sequential systems
Simulation preorder on simple process algebras.
Weak bisimulation and model checking for basic parallel processes.
Strict lower bounds for model checking BPA.
On the complexity of bisimulation problems for basic parallel processes.
On the complexity of bisimulation problems for pushdown automata.
Decidability of model checking with the temporal logic EF.
Process rewrite systems.

Infinite results.
Three partition refinement algorithms.
Concurrency and automata on infinite sequences.
Petri Net Theory and the Modelling of Systems.
Complexity of weak bisimilarity and regularity for BPA and BPP.
Hardness results for weak bisimilarity of simple process algebras.
Model checking CTL properties of pushdown systems.
--TR
Three partition refinement algorithms
Communication and concurrency
Process algebra
A short proof of the decidability of bisimulation for normed BPA-processes
Decidability of bisimulation equivalence for process generating context-free languages
Bisimulation equivalence is decidable for all context-free processes
A polynomial algorithm for deciding bisimilarity of normed context-free processes
Process rewrite systems
Effective decomposability of sequential behaviours
Decidability of model checking with the temporal logic EF
Petri Net Theory and the Modeling of Systems
Introduction To Automata Theory, Languages, And Computation
An Elementary Bisimulation Decision Procedure for Arbitrary Context-Free Processes
Simulation Preorder on Simple Process Algebras
Bisimulation Equivanlence Is Decidable for Normed Process Algebra
Efficient Verification Algorithms for One-Counter Processes
Deciding Bisimulation-Like Equivalences with Finite-State Processes
Reachability Analysis of Pushdown Automata
Bisimulation Equivalence is Decidable for Basic Parallel Processes
Infinite Results
An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis
Weak Bisimulation and Model Checking for Basic Parallel Processes
Model Checking CTL Properties of Pushdown Systems
Concurrency and Automata on Infinite Sequences
On the Complexity of Bisimulation Problems for Pushdown Automata
Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes
On Simulation-Checking with Sequential Systems
On the Complexity of Bisimulation Problems for Basic Parallel Processes

--CTR
Richard Mayr, Weak bisimilarity and regularity of context-free processes is EXPTIME-hard, Theoretical Computer Science, v.330 n.3, p.553-575, 9 February 2005
Antonn Kuera , Richard Mayr, Simulation preorder over simple process algebras, Information and Computation, v.173 n.2, p.184-198, March 15, 2002
Antonn Kuera, The complexity of bisimilarity-checking for one-counter processes, Theoretical Computer Science, v.304 n.1-3, p.157-183, 28 July
Antonn Kuera , Petr Janar, Equivalence-checking on infinite-state systems: Techniques and results, Theory and Practice of Logic Programming, v.6 n.3, p.227-264, May 2006
concurrency;bisimulation;infinite-state systems;process algebras;verification