BRICS RS-95-52 A. Ku� cera: Deciding Regularity in Process Algebras

BRICS

Basic Research in Computer Science

Deciding Regularity in Process Algebras

Anton��n Ku� cera

BRICS Report Series RS-95-52 ISSN 0909-0878 October 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Deciding Regularity in Process Algebras

Antonín Kučera^{∗}

email: tony@informatics.muni.cz

Abstract

We consider the problem of deciding regularity of normed BPP and normed BPA processes. A process is regular if it is bisimilar to a process with finitely many states. We show, that regularity of normed BPP processes is decidable and we provide a constructive regularity test. We also show, that the same result can be obtained for the class of normed BPA processes.

Regularity can be defined also w.r.t. other behavioural equivalences. We define notions of strong regularity and finite characterisation and we examine their relationship with notions of regularity and finite representation. The introduced notion of the finite characterisation is especially interesting from the point of view of possible verification of concurrent systems.

In the last section we present some negative results. If we extend the BPP algebra with the operator of restriction, regularity becomes undecidable and similar results can be obtained also for other process algebras.

∗Presented results were obtained during the author’s stay at BRICS (Basic Research in Computer Science), Department of Computer Science, University of Aarhus. The stay was supported by The Danish Ministry of Education.

Contents

1 Introduction 3

2 Basic definitions 4 2.1 Subclasses of CCS - BPA, BPP, BPP_{τ} . . . . . . . . . . . . . 4 2.2 Normed processes . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 Greibach normal form . . . . . . . . . . . . . . . . . . . . . . 6 2.5 Regularity of processes . . . . . . . . . . . . . . . . . . . . . . 7

3 The constructive test of regularity for normed BPP processes 8 3.1 The inheritence tree . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Decidability of regularity for normed BPP processes . . . . . 11 3.3 The constructive algorithm . . . . . . . . . . . . . . . . . . . 15 3.4 Replacing merge with the full parallel operator . . . . . . . . 19

4 The constructive test of regularity for normed BPA processes 21

5 Deciding regularity w.r.t. other behavioural equivalences 23

6 Negative results 34 6.1 The Minsky machine . . . . . . . . . . . . . . . . . . . . . . . 34 6.2 Extending BPP_{τ} with the operator of restriction . . . . . . . 34

7 Conclusions, future work 37

1 Introduction

One of the most popular models for concurrency are process algebras like CCS, CSP or ACP. Various properties of these models have beed studied in the last decades. This paper belongs to the bunch which could be labeled “decidability results”. The dominating subject in this area is the problem of deciding various behavioural equivalences in certain subclasses of mentioned algebras.

Milner in [1] has shown that bisimulation equivalence is decidable in the class of regular (finite-state) process. In [3] Baeten, Bergstra and Klop proved that bisimulation equivalence is decidable in the class of normed BPA processes. It was the first result, showing that bisimulation equivalence can remain decidable in a class of processes, in which the language equivalence is undecidable. Much simpler proof of this was later given by Caucal [4] and Groote [5]. In [6] Hüttel and Stirling used a tableau decision method and gave also sound and complete equational theory for the class of normed BPA processes.

This result was later extended to the whole class of BPA processes by Christensen, Hüttel and Stirling [7]. Another class of processes, BPP, is examined in [8]. Christensen, Hirsfeld and Moller proved that bisimulation equivalence is decidable in this class, using a tableau technique similar to [6].

An open problem was the question whether it is decidable if a given process is regular (i.e. it is bisimilar to a process with finitely many states). This natural problem is generally undecidable (see [11]), but Mauw and Mulder showed in [2], that regularity is decidable in the class of BPA systems.

In this paper we prove that regularity is decidable in the class of normed BPP processes. Moreover, if the tested process is regular then our algorithm outputs also the normal form of this regular process. We also show, that the result of [2] can serve as a constructive regularity test for the class of normed BPA processes.

The notion of regularity can be defined also w.r.t. other behavioural equivalences. Regular processes have finite representations (see [11]), but a finite representation of a process Δ generally does not express the behaviour of reachable states of Δ. We introduce the notion of strong regularity, which in many cases guarantees an existence of a finite characterisation, which describes a process as a whole. We also study the relationship between finite representations and finite characterisations.

In the last section we present some negative results, stating that regularity and strong regularity are undecidable in some process classes. First we consider a calculus, obtained by extending BPP with the rectriction operator and we prove that regularity and strong regularity are undecidable. This result is obtained via a simple reduction, which can be applied also to other process algebras.

2 Basic definitions

2.1 Subclasses of CCS - BPA, BPP, BPP_{τ}

Let Act = Λ ∪ \overline{Λ} ∪ \{τ\} be a set of atomic actions, where Λ = \{a, b, c, …\} is a countably infinite set of labels, \overline{Λ} = \{\overline{a}, \overline{b}, \overline{c}, …\} is a countably infinite set of co-labels with the convention \overline{\overline{a}} = a and τ is a distinguished element which does not belong to Λ ∪ \overline{Λ}. Let V ar be a countably infinite set of variables, V ar = {X, Y, Z, …}. The classes of recursive BPA, BPP and BPP_{τ} expressions are defined by the following abstract syntax equations:

\begin{aligned}E_{BP A} & ::= & a | X | E_{BP A}.E_{BP A} | E_{BP A} + E_{BP A} \\ E_{BP P} & ::= & a | X | a.E_{BP P} | E_{BP P} ∥E_{BP P} | E_{BP P} + E_{BP P} \\ E_{BP P_{τ}} & ::= & a | X | a.E_{BP P_{τ}} | E_{BP P_{τ}} |E_{BP P_{τ}} | E_{BP P_{τ}} + E_{BP P_{τ}} \end{aligned}

Here a ranges over Act and X ranges over V ar. We also let greek letters α, β, … to range over process expressions. The symbol Act^{∗} denotes the set of all finite strings over Act and the symbol Act^{+} denotes the set of all nonempty finite strings over Act. The parallel operator “∥” of BPP is sometimes called the merge operator, and the operator “|” of BPP_{τ} is called the full parallel operator because it allows synchronizations

As usual, we restrict our attention to guarded expressions. A process expression (BPA, BPP or BPP_{τ}) is guarded iff every variable occurence is within the scope of an atomic action.

A guarded process (BPA, BPP or BPP_{τ}) is defined by a finite family Δ of recursive process equations

Δ = {X_{i} =^{def} E_{i} | 1 ≤ i ≤ n}

where X_{i} are distinct, and the E_{i} are guarded expressions (BPA, BPP or BPP_{τ}), containing the variables from {X_{1}, …, X_{n}}. The set of variables, which appear in Δ, is denoted by V ar(Δ).

Variable X_{1} plays a special role (X_{1} is sometimes called the “leading variable”) - it is a root of a labelled transition system, defined by the process Δ and following rules (ϵ denotes empty expression):

\overline{a →^{a} ϵ}  \frac{E →^{a} E′}{E.F →^{a} E′.F}  \frac{E →^{a} E′}{E + F →^{a} E′}
\frac{F →^{a} F′}{E + F →^{a} F′}  \frac{E →^{a} E′}{E|F →^{a} E′|F}  \frac{F →^{a} F′}{E|F →^{a} E|F′}

\frac{E →^{a} E′ F →^{\overline{a}} F′}{E|F →^{τ} E′|F′}  \frac{E →^{a} E′}{E∥F →^{a} E′∥F}  \frac{F →^{a} F′}{E∥F →^{a} E∥F′}

\frac{E →^{a} E′}{X →^{a} E′} (X =^{def} E ∈ Δ)

Nodes of the transition system generated by Δ are process expressions, which are often called states of Δ, or just “states” when Δ is understood from the context. The transitive closure of “→” is denoted by “→_{+}”, the reflexive and transitive closure by “→_{∗}”. Given two states α, β, we say that β is reachable from α, if α→^{w}_{∗}β for some w ∈ Act^{∗}. States of Δ, which are reachable from X_{1} are said to be reachable.

Remark 1 Processes are often identified with their leading variables. Furthermore, if we assume a fixed process Δ, we can view any variable Y ∈ V ar(Δ) as a process too; we simply change the order of defining equations so that Y becomes the leading variable of the process. Similarly, any guarded expression α, containing variables from V ar(Δ) denotes a process - we simply define a new system Δ′, which is identical to Δ with one exception - it has a new leading variable N and the equation N =^{def} α. All notions originally defined for processes can be used for variables and process expressions in this sense too.

Remark 2 Guarded processes generate finitely branching transition graphs, that is, the set {β | α →^{a} β} is finite for each state α. It is easy to show, that it would not be true if we allowed unguarded expressions.

2.2 Normed processes

An important subclass of processes can be obtained by an extra restriction of normedness. A variable X ∈ V ar(Δ) is normed iff there is w ∈ Act^{∗} such that X →^{w} ϵ. In that case we define the norm of X, [X], to be the length of the shortest such w, counting the length of “τ” as two; all other actions have the length one. Thus [X] = min{length(w) | X →^{w} ϵ}. A process Δ is normed, if all variables of V ar(Δ) are normed. The norm of the process is then defined to be the norm of X_{1}.

As normed processes are intensively studied in this paper, we emphasize some properties of norm:

• The norm of a normed process is easy to compute:

[a] = 1, [α + β] = min{[α], [β]}, [α.β] = [α] + [β], [α∥β] = [α] + [β], [α|β] = [α] + [β], and if X_{i} =^{def} E_{i} and [E_{i}] = n, then [X_{i}] = n.

• For each normed BPA, BPP or BPP_{τ} process α there are a ∈ Act and α′, such that α →^{a} α′ and [α] = [α′] + 1

• Bisimilar processes (see section 2.3) must have the same norm.

2.3 Bisimulation

The equivalence between process expressions (states) we are here interested in is bisimilarity [1], defined as follows:

Definition 1 A binary relation R over process expressions is a bisimulation if whenever αRβ then for each a ∈ Act

• if α →^{a} α′, then β →^{a} β′ for some β′ such that α′Rβ′

• if β →^{a} β′, then α →^{a} α′ for some α′ such that α′Rβ′

Processes Δ and Δ′ are bisimilar, written Δ ∼ Δ′, if their leading variables are related by some bisimulation.

2.4 Greibach normal form

Any BPA process Δ can be effectively presented in so-called 3-Greibach normal form (see [3]):

Definition 2 A BPA process Δ is said to be in Greibach normal form (GNF) if all its equations are of the form

X_{i} =^{def} ∑_{j=1}^{n_{i}} a_{ij}α_{ij}

where 1 ≤ i ≤ n, n_{i} ∈ N, a_{ij} ∈ Act and α_{ij} ∈ V ar(Δ)^{∗}. If length(α_{ij}) ≤ 2, then Δ is said to be in 3-GNF. (V ar(Δ)^{∗} denotes the set of all finite sequences of variables from V ar(Δ)).

A similar result holds for BPP, resp. BPP_{τ} (see [10]). Any BPP resp. BPP_{τ} process Δ′ can be effectively represented in the normal form, which is very similar to the 3-GNF of BPA - hence it is called 3-GNF too. Before its presentation we need to introduce the set V ar(Δ′)^{⊗} of all finite multisets over V ar(Δ′). Each multiset of V ar(Δ′)^{⊗} denotes a BPP resp. BPP_{τ} expression by combining its elements in parallel using the merge, resp. the full parallel operator.

Definition 3 A BPP, resp. BPP_{τ} process Δ′ is said to be in Greibach normal form (GNF) if all its equations are of the form

X_{i} =^{def} ∑_{j=1}^{n_{i}} a_{ij}α_{ij}

where 1 ≤ i ≤ n, n_{i} ∈ N, a_{ij} ∈ Act and α_{ij} ∈ V ar(Δ′)^{⊗}. If card(α_{ij}) ≤ 2, then Δ′ is said to be in 3-GNF. (card(α_{ij}) denotes the cardinality of α_{ij}).

From now on we assume, that all BPA, BPP and BPP_{τ} processes we are working with are presented in 3-GNF. This justifies also the assumption, that all reachable states of a BPA process Δ are elements of V ar(Δ)^{∗} and all reachable states of a BPP or BPP_{τ} process Δ′ are elements of V ar(Δ′)^{⊗}. Furthermore, all variables of a normed BPA, BPP or BPP_{τ} process in 3-GNF have norm at least one. Occasionally we will also use the notation α^{i}, where α is a state of some BPA, BPP or BPP_{τ} process, i ∈ N. The notation has the following meaning:

α^{i} = \underbrace{α.α. … α}_{i}  if α is a state of some BPA process
α^{i} = \underbrace{α∥α∥ … ∥α}_{i}  if α is a state of some BPP process
α^{i} = \underbrace{α|α| … |α}_{i}  if α is a state of some BPP_{τ} process

2.5 Regularity of processes

The main question considered in this paper is, whether the behaviour of a given process is regular, i.e. whether it is bisimilar to a process with finitely many states.

Definition 4 A process Δ is regular if there is a process Δ′ with finitely many states, such that Δ ∼ Δ′.

It is easy to show that a process is regular iff it can reach only finitely many states up to bisimilarity. In [1] it is shown, that regular processes can be represented in the following normal form:

Definition 5 A regular process Δ is said to be in normal form if all its equations are of the form

X_{i} =^{def} ∑_{j=1}^{n_{i}} a_{ij}X_{ij}

where 1 ≤ i ≤ n, n_{i} ∈ N, a_{ij} ∈ Act and X_{ij} ∈ V ar(Δ).

Thus a process Δ is regular iff there is a regular process Δ′ in normal form, such that Δ ∼ Δ′.

3 The constructive test of regularity for normed BPP processes

3.1 The inheritence tree

Let Δ be a BPP process in 3-GNF, given by the set of equations

X_{i} =^{def} ∑_{j=1}^{n_{i}} a_{ij}α_{ij}

where 1 ≤ i ≤ n. With each α_{i,j} we associate some linear ordering ⪯_{i,j} on α_{i,j}. We define a partial function Lbl : N × N × N → V ar(Δ):

Lbl(i, j, k) = \{ \begin{matrix}k^{th} element of α_{i,j} w.r.t. ⪯_{i,j} & if 1 ≤ i ≤ n ∧ 1 ≤ j ≤ n_{i} \\ & ∧ k ≤ card(α_{i,j}) \\ ⊥ & otherwise \end{matrix}

Now let X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} … be an infinite path. Each transition β_{i} →^{a_{i}} β_{i+1} is due to some variable X_{r} ∈ β_{i}, which emits the action a_{i} and enters the state α_{r,s}, where a_{i}α_{r,s} is a summand in the defining equation of X_{r} in Δ. We say, that X_{r} is the active variable of β_{i} and α_{r,s} is the step of β_{i}. Generally, X_{r_{i}} denotes the active variable of β_{i} and α_{r_{i},s_{i}} denotes the step of β_{i} for each i ∈ N ∪ {0}. To be able to examine properties of such an infinite path, we define the associated inheritence tree. Nodes of the inheritence tree are formed by a subset of (N ∪ {0}) × (N ∪ {0}):

Nodes = ⋃_{i=0}^{∞} {[i, j] | 0 ≤ j < card(β_{i})}

Furthermore, we define the function Label : Nodes → V ar(Δ):

Label([0, 0]) = X_{1}

Label([i + 1, j]) =

= \{ \begin{matrix}Label([i, j]) & if 0 ≤ j < k_{i} \\ Lbl(r_{i}, s_{i}, j − k_{i} + 1) & if k_{i} ≤ j < k_{i} + card(α_{r_{i},s_{i}}) \\ Label([i, j − card(α_{r_{i},s_{i}}) + 1]) & if k_{i} + card(α_{r_{i},s_{i}}) ≤ j < card(β_{i+1}) \end{matrix}

where k_{i} = max{j ∈ N ∪ {0} | 0 ≤ j < card(β_{i}) ∧ Label[i, j] = X_{r_{i}}}

The way how k_{i} is chosen is not crucial in fact. There is no need to distinguish between multiple occurence of the same variable within a single state, but we want to keep our construction of the inheritence tree deterministic. Finally, we define the binary relation Edges on Nodes:

[i, j] Edges [l, m] ⟺^{def} l = i + 1 and one of the following conditions holds:

\begin{matrix}1. 0 ≤ j < k_{i} & ∧ j = m \\ 2. j = k_{i} & ∧ k_{i} ≤ m < k_{i} + card(α_{r_{i},s_{i}}) \\ 3. k_{i} < j < card(β_{i}) & ∧ m = j + card(α_{r_{i},s_{i}}) − 1 \end{matrix}

The inheritence tree associated with the path X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} … is a triple [Nodes, Edges, [0, 0]]. We also need some further notions:

Definition 6 Let Δ be a normed BPP process, X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} … be an infinite path and let IT be the inheritence tree associated with this path.

A node [i, j] is a son of a node [k, l] iff [[k, l], [i, j]] ∈ Edges. Moreover, if [i, j] is a son of [k, l], then [k, l] is said to be the father of [i, j]. Note that each node may have 0,1 or 2 sons, but each node except [0, 0] has exactly one father.

Similarly, [i, j] is a descendant of [k, l] iff there exists a path from [k, l] to [i, j] in IT. Finally, a node [i, j] is branching iff it has two different sons.

Example 1 Let Δ be a process given by the following set of equations:

X =^{def} a(Y ∥Z)
Y =^{def} b + c(T ∥U)
Z =^{def} b + cT + a(Y ∥T)
T =^{def} a + a(U∥U)
U =^{def} b(Z∥T) + a(X∥Z)

Process Δ is normed and its leading variable is X. The linear ordering ⪯_{i,j} is determined by the position of variables in α_{i,j}, e.g. ⪯_{0,0}=

{[Y, Y], [Z, Z], [Y, Z]}, that is Y ⪯_{0,0} Z. Let X →^{a} Y ∥Z →^{c} Y ∥T →^{b} T →^{a}

U∥U →^{b} U∥Z∥T … be an infinite path. If we draw a fragment of the associated inheritence tree and replace each [i, j] with Label([i, j]), we get the following picture (active variables are placed in a box):

[figure: X; Y; Z; Y; T; T; U; U; U; Z; T; ….; ….; ….]

3.2 Decidability of regularity for normed BPP processes

Definition 7 Let Δ be a normed BPP process. We define the binary relation “⇝” on V ar(Δ):

X ⇝ Y ⟺^{def} ∃ w ∈ Act^{+}, γ ∈ V ar(Δ)^{⊗}, such that X→^{w}_{+}Y ∥γ ∧ γ ≠ ∅

A variable Y ∈ V ar(Δ) is said to be growing iff Y ⇝ Y

We show, that “⇝” is the least fixed-point of a function, which represents an iterative procedure. We also show, that this fixed-point must be reached after a finite number of iterations. We need several definitions:

Definition 8 Let Δ be a normed BPP process. We define the binary relation “↪” on V ar(Δ):

X ↪ Y ⟺^{def} there is a summand a_{ij}α_{ij} in the defining equation of X, such that Y ∈ α_{ij}.

The symbol “↪_{∗}” denotes the reflexive and transitive closure of “↪”.

It is a standard result that for any binary relation R on a finite set, the reflexive and transitive closure of R can be effectively constructed. Hence there is an algorithm, which constructs “↪_{∗}”.

Definition 9 Let Δ be a normed BPP process. We define the function F over subsets of V ar(Δ) × V ar(Δ) as follows. If M ⊆ V ar(Δ) × V ar(Δ), then [X, Y] ∈ F(M) ⟺^{def} one of the following conditions holds:

• [X, Y] ∈ M
• ∃ Z ∈ V ar(Δ), such that [X, Z] ∈ M ∧ Z ↪_{∗} Y
• ∃ Z ∈ V ar(Δ), such that [Z, Y] ∈ M ∧ X ↪_{∗} Z

Definition 10 Let Δ be a normed BPP process. For each i ∈ N ∪ {0} we define the binary relation “⇝_{i}” over V ar(Δ):

⇝_{0} = {[X, Y] | there is a summand a_{ij}α_{ij} in the defining equation

of X, such that Y ∈ α_{ij} ∧ card(α_{ij}) = 2}

⇝_{i+1} = F(⇝_{i})

Now it is easy to see, that the relation “⇝” is exactly the least fixed-point of F, which belongs to the set {⇝_{i} | i ∈ N ∪ {0}}:

⇝ = ⇝_{k}, where k = min{i ∈ N ∪ {0} | ⇝_{i} = F(⇝_{i})}

As V ar(Δ) × V ar(Δ) is finite and ⇝_{i} ⊆ ⇝_{i+1} for each i ∈ N ∪ {0}, the least fixed-point must be reached in a finite number of steps.

Definition 11 Let Δ be a normed BPP process. A variable Y ∈ V ar(Δ) is said to be accessible iff there is a reachable state α ∈ V ar(Δ)^{⊗}, such that Y ∈ α.

Again, it is easy to define a function, such that the set of all accessible variables of V ar(Δ) is the least fixed-point of this function. So we have the following lemma:

Lemma 1 Let Δ be a normed BPP process. It is decidable, whether the set V ar(Δ) contains an accessible growing variable.

Lemma 2 Let Δ be a normed BPP process and let α, β ∈ V ar(Δ)^{⊗} be its states. If β is reachable from α, then for each variable Y ∈ β the state {Y } is reachable from α.

Proof: Since β is reachable from α, there is v ∈ Act^{∗}, such that α →^{v} β. Suppose β = Y ∥A_{1}∥ … ∥A_{n}. As Δ is normed, each of the variables A_{1}, …, A_{n} is normed. Hence for each i, 1 ≤ i ≤ n, there is w_{i} ∈ Act^{+}, such that A_{i}→^{w_{i}}_{+}ϵ. Let w denotes the concatenation of w_{i}, 1 ≤ i ≤ n. The state {Y } is reachable from α, because α→^{v}_{∗}Y ∥A_{1}∥ … ∥A_{n}→^{w}_{+}Y.

□

We have emphasized this trivial property of normed BPP processes, because this becomes a crucial point when we start to think about possible extension of the presented result to the whole class of BPP processes.

Lemma 3 A process Δ is not regular iff there is an infinite path, X_{1} =

β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} …, such that β_{i} ≁ β_{j} for i ≠ j.

Proof: “⇐:” Obvious - Δ can reach infinitely many pairwise non-bisimilar states. “⇒:” Let T S(Δ) be a transition system generated by Δ. If we identify bisimilar nodes in T S(Δ), we get a transition system T S(Δ)/ ∼, which is bisimilar to T S(Δ) and all its states are pairwise non-bisimilar. The set of reachable states of T S(Δ)/ ∼ is infinite and T S(Δ)/ ∼ is finitely branching (see Remark 2). Hence due to König lemma there must be an infinite path X_{1}^{∼} →^{a_{0}}β_{1}^{∼} →^{a_{1}}β_{2}^{∼} →^{a_{2}}β_{3}^{∼} →^{a_{3}} …, where β_{i}^{∼} denotes the equivalence class containing β_{i}. Using this path (whose elements are pairwise non-bisimilar), we can construct the required path in T S(Δ) - just by taking a suitable representative of β_{i}^{∼}.

□

Lemma 4 Let Δ be a normed BPP process, X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} … be an infinite path, such that β_{i} ≁ β_{j} for i ≠ j. Then there is a path in the corresponding inheritence tree, which contains infinitely many branching nodes.

Proof: First we show that the inheritence tree contains infinitely many branching nodes. It suffices to prove that for any i ∈ N there exists a branching node [j, p], such that j > i. Assume the opposite - then there is k ∈ N, such that [j, p] is branching ⇒ j < k. But then there is no way how the number of variables in β_{q}, q > k, could increase - each β_{q}, q > k contains at most card(β_{k}) variables. As Δ has only finitely many variables, the set of all multisets over V ar(Δ), whose cardinality is at most card(β_{k}), is finite. Therefore there must be r ≠ s such that β_{r} = β_{s}; hence β_{r} ∼ β_{s}, so we have a contradiction.

It remains to find a path containing infinitely many branching nodes. To do this, we first construct the branching tree: Nodes of the branching tree are branching nodes of the inheritence tree. Edges are determined as follows: [[i, j], [k, l]] is an egde in the branching tree iff there is a path from [i, j] to [k, l] in the inheritence tree, which does not contain any branching nodes except [i, j] and [k, l]. The root of the branching tree is the branching node [i, j], such that all other branching nodes are its descendants (there is just one node of this property). We have already proved that the branching tree is infinite. As each node which is not leaf has exactly two successors, we can use König lemma and conclude that the branching tree contains an infinite path. This path corresponds to an infinite path in the inheritence tree, which contains infinitely many branching nodes (realize that each edge of the branching tree represents a finite path in the inheritence tree).

□

Now we are ready to prove the main result of this section:

Theorem 1 A normed BPP process Δ is regular iff V ar(Δ) does not contain any accessible growing variable.

Proof: “⇒:” Assume there is an accessible growing variable Y ∈ V ar(Δ). Then

X_{1}→^{w}_{∗}Y for some w ∈ Act^{∗} and Y →^{v}_{+}Y ∥γ, where v ∈ Act^{+}, γ ∈ V ar(Δ)^{⊕}

and γ ≠ ∅. But then each state of the form Y ∥γ^{i}, i ∈ N is reachable. Furthemore, Y ∥γ^{i} ≁ Y ∥γ^{j} for i ≠ j, as these two states have different norms. Hence Δ is not regular, as it can reach infinitely many pairwise non-bisimilar states. “⇐:” Assume Δ is not regular. We show, that then V ar(Δ) contains an accessible growing variable. As Δ is not regular, there is an infinite sequence X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} …, whose elements are pairwise non-bisimilar. Now we examine the corresponding inheritence tree. With each node [i, j] we associate the set Seek([i, j]) ⊆ V ar(Δ) in the following way:

Seek([0, 0]) = ∅

Seek([i + 1, k]) = \{ \begin{matrix}Seek(F ather([i + 1, k])) & if F ather([i + 1, k]) \\ & is not branching. \\ Seek(F ather([i + 1, k])) & if F ather([i + 1, k]) \\ ∪\{Label(F ather([i + 1, k]))\} & is branching. \end{matrix}

F ather([i + 1, k]) denotes the father of [i + 1, k]. Seek([i, j]) contains in fact accessible variables, which are potential candidates to be growing - if we find a node [i, j], such that Label([i, j]) ∈ Seek([i, j]), we can conclude that Label([i, j]) is an accessible growing variable. This is due to the following consideration: As Label([i, j]) ∈ Seek([i, j]), there is a branching node [p, k], p < i, such that Label([p, k]) = Label([i, j]) and [i, j] is a descendant of [p, k]. Since [p, k] is branching, it has two sons [p + 1, l], [p + 1, l + 1], thus

Label([p, k]) →^{a_{p}} Label([p + 1, l]) ∥ Label([p + 1, l + 1]),

where a_{p} ∈ Act. As [i, j] is a descendant of [p, k], one of these four possibilities holds:

1. [p + 1, l] = [i, j]

2. [p + 1, l + 1] = [i, j] 3. [i, j] is a descendant of [p + 1, l]

4. [i, j] is a descendant of [p + 1, l + 1]

In the first two cases we immediately get that Label([i, j]) ( = Label([p, k])) is an accessible growing variable. If [i, j] is a descendant of [p + 1, l], then due to Lemma 1:

Label([p + 1, l]) →^{w}_{+} Label([i, j])

for some w ∈ Act^{+}, hence

\begin{matrix}Label([p, k]) →^{a_{p}} Label([p + 1, l]) ∥ Label([p + 1, l + 1]) →^{w}_{+} \\ Label([i, j]) ∥ Label([p + 1, l + 1]) \end{matrix}

so the variable Label([p, k]) is again accessible and growing. Possibility 4 is handled in a similar way.

Due to Lemma 4 we know, that our inheritence tree contains a path with infinitely many branching nodes. Going down this path, labels of branching nodes are successively added to the Seek set. As V ar(Δ) is finite, we must find a branching node [i, j], such that Label([i, j]) ∈ Seek([i, j]), thus Label([i, j]) is the desired accessible growing variable.

□

3.3 The constructive algorithm

Each regular process can be represented in normal form (see Section 2). In this section we provide an algorithm, which inputs a normed BPP process Δ in 3-GNF and outputs YES iff Δ is regular and NO otherwise. In the first case our algorithm also constructs a regular process Δ′ in normal form, such that Δ ∼ Δ′. During the construction of Δ′ we take advantage of the fact, that bisimilarity is known to be decidable in the class of normed BPP processes (see [8]).

The algorithm first checks, whether V ar(Δ) contains any accessible growing variable. If so, it outputs NO and terminates. Otherwise it initiates Δ′ to be Δ and starts to remove the multisets α_{i,j}, card(α_{i,j}) > 1 from the defining equations of Δ′. Note this is the only thing which has to be done to obtain normal form of Δ′.

Each such α_{i,j} is first compared with elements of V ar(Δ′). If we find a variable Y ∈ V ar(Δ′), such that Y ∼ α_{i,j}, we simply replace α_{i,j} with Y.

Otherwise we introduce a new variable P ∈ V ar, P ∉ V ar(Δ′) and a new equation

P =^{def} α_{i,j}

But this equation cannot be immediately added to Δ′, as it is not of the form, which is prescribed by GNF (α_{i,j} is even not guarded). To obtain the desired form of this equation, we have to apply the CCS expansion law (see [1]):

A_{1}∥ … ∥A_{n} = ∑ { a(A_{1}∥ … ∥α_{i}∥ … ∥A_{n}) : A_{i} →^{a} α_{i}, a ∈ Act}

After the application of the expansion law we get an equation, which is of the form of GNF (not necessarly 3-GNF), thus it can be added to Δ′.

We go on in this fashion, until all multisets α_{i,j}, card(α_{i,j}) > 1 are removed. The construction must terminate, because otherwise the process Δ′ could reach infinitely many pairwise non-bisimilar states (realize that newly added variables are reachable and pairwise non-bisimilar states of Δ′). As Δ′ remains bisimilar to Δ after the processing of each α_{i,j}, it contradicts the regularity of Δ.

We also describe this algorithm formally, using a Pascal-like pseudocode. The form is very simple in order to keep the description as short as possible:

Algorithm: The constructive regularity test for normed BPP processes Input: A normed BPP process Δ in 3-GNF Output: YES and a regular process Δ′ in normal form, such that

Δ ∼ Δ′ if Δ is regular;

NO otherwise; IF V ar(Δ) contains an accessible growing variable

    THEN output:=NO;
ELSE BEGIN

Δ′ := Δ;
WHILE (Δ′ contains α_{i,j}, such that card(α_{i,j}) > 1) DO

              BEGIN
                  I:=TRUE;

FOR each V ∈ V ar(Δ′) DO

IF (V ∼ α_{i,j})

                          THEN BEGIN I:=FALSE;

replace α_{i,j} with V;

                                    EXITFOR;
                               END;
                  IF(I=TRUE)

THEN BEGIN N:=newvariable(Δ′);

Δ′ := Δ′ ∪ {N =^{def} expand(α_{i,j})};

                           END;
              END;
              output:=YES;
     END;

The function expand applies the CCS expansion law on its argument and returns the expanded expression. The function newvariable returns a variable from V ar, which is not in V ar(Δ). Here is an example:

Example 2: Let Δ be a normed BPP process in 3-GNF, given by the following set of equations:

X =^{def} bC + a(B∥C)
A =^{def} a
B =^{def} b
C =^{def} b(B∥A)
D =^{def} aB + bA

The set V ar(Δ) does not contain any accessible growing variable, hence our algorithm can be applied. We show, how Δ′ changes its form after each pass through the WHILE loop:

X =^{def} bC + aE

A =^{def} a

B =^{def} b

C =^{def} b(B∥A)

D =^{def} aB + bA

E =^{def} expand(B∥C) = bC + b(B∥B∥A)

X =^{def} bC + aE

A =^{def} a

B =^{def} b

C =^{def} bD

D =^{def} aB + bA

E =^{def} bC + b(B∥B∥A)

X =^{def} bC + aE

A =^{def} a

B =^{def} b

C =^{def} bD

D =^{def} aB + bA

E =^{def} bC + bF

F =^{def} expand(B∥B∥A) = a(B∥B) + b(A∥B)

X =^{def} bC + aE

A =^{def} a

B =^{def} b

C =^{def} bD

D =^{def} aB + bA

E =^{def} bC + bF

F =^{def} aG + b(A∥B)

G =^{def} expand(B∥B) = bB

X =^{def} bC + aE

A =^{def} a

B =^{def} b

C =^{def} bD

D =^{def} aB + bA

E =^{def} bC + bF

F =^{def} aG + bD

G =^{def} bB

3.4 Replacing merge with the full parallel operator

A natural question is, whether our algorithm still works if we replace the merge operator with the full parallel operator and thus move to the class BPP_{τ}. The answer is positive, but some modifications of definitions and proofs are needed. We could in fact start the Section 3 directly with this version of our algorithm, but the main idea is more or less the same - therefore we have given the simplified version first and now we show what has to be changed to obtain the full result.

We begin with a new version of the inheritence tree (we denote it IT_{τ}). Let Δ be a normed BPP_{τ} process and let X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} … be an infinite sequence of transitions. Each transition β_{i} →^{a_{i}} β_{i+1} is either due to a single variable X_{r_{i}}, which emits the action a_{i} and enters the state α_{r_{i},s_{i}}, or due to a communication between two variables X_{r_{i}} and X_{t_{i}}, which emit the complementary actions b, \overline{b} ∈ Act (hence producing τ) and enter states α_{r_{i},s_{i}} and α_{t_{i},u_{i}}. In the latter case we say that the transition β_{i} →^{a_{i}} β_{i+1} is synchronized, variables X_{r_{i}} and X_{t_{i}} are communicating and α_{r_{i},s_{i}}, α_{t_{i},u_{i}} are steps of communication. Nodes of IT_{τ} are defined as previously:

Nodes_{τ} = ⋃_{i=0}^{∞} {[i, j] | 0 ≤ j < card(β_{i})}

Now we introduce a new version of the function Label, denoted Label_{τ}:

Label_{τ} ([0, 0]) = X_{1}

Label_{τ} ([i + 1, j]) = \{ \begin{matrix}Label([i + 1, j]) & if β_{i} →^{a_{i}} β_{i+1} is not synchronized \\ Label2([i + 1, j]) & if β_{i} →^{a_{i}} β_{i+1} is synchronized \end{matrix}

where the function Label2 : Nodes_{τ} → V ar(Δ) is defined as follows:

Label2([i + 1, j]) =

= \{ \begin{matrix}Label_{τ} ([i, j]) & if 0 ≤ j < k_{i} \\ Lbl(r_{i}, s_{i}, j − k_{i} + 1) & if k_{i} ≤ j < k_{i} + C_{1} \\ Label_{τ} ([i, j − C_{1} + 1]) & if k_{i} + C_{1} ≤ j < l_{i} + C_{1} − 1 \\ Lbl(t_{i}, u_{i}, j − l_{i} − C_{1} + 2) & if l_{i} + C_{1} − 1 ≤ j < l_{i} + C_{1} + C_{2} − 1 \\ Label_{τ} ([i, j − C_{1} − C_{2} + 2]) & if l_{i} + C_{1} + C_{2} − 1 ≤ j < card(β_{i+1}) \end{matrix}

where

k_{i} = max{j ∈ N ∪ {0} | 0 ≤ j < card(β_{i}) ∧ Label_{τ} [i, j] = X_{r_{i}}}

l_{i} = \{ \begin{matrix}max\{j ∈ N ∪ \{0\} | 0 ≤ j < card(β_{i}) ∧ Label_{τ} [i, j] = X_{t_{i}}\} & if X_{r_{i}} ≠ X_{t_{i}} \\ max\{j ∈ N ∪ \{0\} | 0 ≤ j < k_{i} ∧ Label_{τ} [i, j] = X_{t_{i}}\} & if X_{r_{i}} = X_{t_{i}} \end{matrix}

where X_{r_{i}} and X_{t_{i}} are communicating variables and α_{r_{i},s_{i}}, α_{t_{i},u_{i}} are corresponding steps of communication. We can assume w.l.o.g., that k_{i} < l_{i} (otherwise we change their roles). Constants C_{1}, C_{2} are just abbreviations:

\begin{matrix}C_{1} = card(α_{r_{i},s_{i}}) \\ C_{2} = card(α_{t_{i},u_{i}}) \end{matrix}

Finally, we define the edges of IT_{τ}:

[i, j] Edges_{τ} [l, m] ⟺^{def} l = i + 1 and one of these two conditions holds:

1. β_{i} →^{a_{i}} β_{i+1} is not synchronized and [i, j] Edges [l, m]

2. β_{i} →^{a_{i}} β_{i+1} is synchronized and one of the following conditions holds:

\begin{matrix}• 0 ≤ j < k_{i} & ∧ m = j \\ • j = k_{i} & ∧ k_{i} ≤ m < k_{i} + C_{1} \\ • k_{i} < j < l_{i} & ∧ m = j + C_{1} − 1 \\ • j = l_{i} & ∧ l_{i} + C_{1} − 1 ≤ m < l_{i} + C_{1} + C_{2} − 1 \\ • l_{i} < j < card(β_{i}) & ∧ m = j + C_{1} + C_{2} − 2 \end{matrix}

The inheritence tree associated with the sequence X_{1} = β_{0} →^{a_{0}} β_{1} →^{a_{1}} β_{2} →^{a_{2}} β_{3} →^{a_{3}} … is a triple IT_{τ} = [Nodes_{τ} , Edges_{τ} , [0, 0]]. We can keep previously defined notions of the son, father, descendant and branching node. Lemmas 1, 2 and 3 are still valid. Theorem 1 holds too, but the proof has to be done more carefully. Seek sets are associated with nodes of the inheritence tree in the same way. Again, if we find a node [i, j], such that Label_{τ} ([i, j]) ∈ Seek([i, j]), we can conclude that Label_{τ} ([i, j]) is an accessible growing variable. The consideration is similar to the previous one, but the crucial thing is to realize that whenever X|Y |γ →^{τ} α|β|γ, where X, Y are communicating variables and α, β are steps of communication, then also

X|Y |γ →^{b} α|Y |γ and X|Y |γ →^{\overline{b}} X|β|γ, where b, \overline{b} ∈ Act are complementary

actions - there is no way how to force synchronizations. The proof is now easy to complete.

The constructive algorithm described in the previous section also requires a small modification - we need a more general version of the CCS expansion law, which reflects the new possibility of synchronizations (see [1]):

A_{1}| … |A_{n} = ∑ { a(A_{1}| … |α_{i}| … |A_{n}) : A_{i} →^{a} α_{i}, a ∈ Act}
+ ∑ \{ τ(A_{1}| … |α_{i}| … |α_{j}| … |A_{n}) : A_{i} →^{b} α_{i}, A_{j} →^{\overline{b}} α_{j}, b, \overline{b} ∈ Act\}

Now we can finish this section with the following theorem:

Theorem 2 There is a constructive regularity test for the class of normed BPP_{τ} processes.

4 The constructive test of regularity for normed BPA processes

In [2] Mauw and Mulder presented a constructive regularity test for BPA systems. Their notion of the BPA system is exactly what we call the BPA process here. But we keep this notion, because the regularity of BPA systems is defined differently from the regularity of processes:

Definition 12 Let Δ be a BPA process in GNF. A variable Y ∈ V ar(Δ) is said to be accessible if ∃ w ∈ Act^{∗}, γ ∈ V ar(Δ)^{∗}, such that X_{1}→^{w}_{∗}Y γ.

Definition 13 A BPA system Δ is regular iff each accessible variable Y ∈ V ar(Δ) is a regular process.

Remember that if we have a BPA system Δ, each of its variables can be seen as a process (see Remark 1).

Each regular BPA system is a regular BPA process. The following example shows, that there is a regular BPA process, which is not a regular BPA system (this example is also due to [2]):

Example 3: Let Δ be a BPA process given by the following set of equations:

X =^{def} aY Z
Y =^{def} bY C + d
Z =^{def} cZ
C =^{def} c

It is easy to check that Δ is a regular process, but it contains an accessible variable Y, which is not regular (process Y can reach infinitely many pairwise non-bisimilar states). Hence Δ is not a regular BPA system.

Furthermore, the result of [2] is constructive - it not only checks the regularity of BPA systems, but if the answer is positive, it also outputs a regular process in the normal form, which is bisimilar to the original one. In this section we prove, that if we restrict out attention to the class of normed BPA processes, then the result of [2] can serve as a constructive regularity test for processes of this class. The following lemma is due to D. Caucal [4]:

Lemma 5 (Cancelation) Let Δ be a normed BPA process in GNF, α, β, γ ∈ V ar(Δ)^{∗}. If αγ ∼ βγ, then also α ∼ β.

Proof: The set {[δ_{1}, δ_{2}] | δ_{1}, δ_{2} ∈ V ar(Δ)^{∗}, δ_{1}γ ∼ δ_{2}γ} is a bisimulation containing the pair [α, β].

□

Now it is possible to prove the promised result:

Lemma 6 A normed BPA process Δ is regular iff all accessible variables of V ar(Δ) are regular processes.

Proof: “⇐:” trivial. “⇒:” Let Y be an accessible variable, which is not a regular process. Due to Lemma 2 there must be an infinite sequence Y = α_{0} →^{a_{0}} α_{1} →^{a_{1}} α_{2} →^{a_{2}} α_{3} …, such that α_{i} ≁ α_{j} for i ≠ j. As Y is accessible, there exists w ∈ Act^{∗}, such that X_{1}→^{w}_{∗}Y β. But then the states α_{0}β, α_{1}β, α_{2}β, … are reachable. As Δ is regular, it cannot have infinitely many reachable states, which are pairwise non-bisimilar. Thus there are i, j ∈ N, i ≠ j, such that α_{i}β ∼ α_{j}β. But now we can use the Lemma 5 and conclude α_{i} ∼ α_{j}, so we have a contradiction.

□

We present here also the main theorem of [2] (in a slightly different form):

Definition 14 Let Δ be a BPA system. A variable Y ∈ V ar(Δ) is said to be growing iff ∃w ∈ Act^{+}, α ∈ V ar(Δ)^{∗}, such that Y →^{w} Y α and Y α is a normed state.

Theorem 3 Let Δ be a BPA system. System Δ is regular iff V ar(Δ) does not contain any accessible growing variable.

Proof: can be found in [2].

□

As a consequence of Theorem 3 and Lemma 6 we get the following:

Theorem 4 Let Δ be a normed BPA process. Process Δ is regular iff V ar(Δ) does not contain any accessible growing variable.

5 Deciding regularity w.r.t. other behavioural equivalences

Bisimilarity is not the only behavioural equivalence which appeared in the literarure. In certain situations it may be advantageous to define the notion of “sameness” in another way. R. van Glabbeek presented in [13] various equivalences in a uniform way, relating them w.r.t. their coarseness, i.e. how many identifications they make:

[figure: bisimilarity; 2-nested simulation equivalence; ready simulation equivalence; ready trace equivalence; readiness equivalence; failure trace equivalence; failure equivalence; completed trace equivalence; trace equivalence; simulation equivalence; possible-futures equivalence]

The order is determined by the relation “makes strictly more identifications than”. Definitions of these equivalences can be found in Appendix A.

The notion of regularity can be defined also w.r.t. these equivalences in the same way as in the case of bisimilarity. In this section we examine properties of these equivalences. We introduce notions of strong regularity and finite characterisation and then we describe their relationship with regularity and finite representations.

As we want to keep this section general, we abstract from the concrete model of process algebras and assume that all behavioural equivalences are binary relations over the class of transition systems:

Definition 15 A transition system is a 4-tuple (N,L,→,r) consisting of a set of nodes N, a set of labels L, a transition relation →⊆ N × L × N and a distinguished element r ∈ N called root.

As usual we write A →^{a} B if [A, a, B] ∈→ and we extend this notation also to elements of L^{∗} in an obvious way. A node A ∈ N is reachable if there is w ∈ L^{∗} such that r →^{w} A. The class of all transition systems is denoted by T .

Remark 3 Each node A of the transition system T = [N, L, →, r] determines a unique transition system T (A) = [N, L, →, A]. All notions originally defined for transition systems can be used for their nodes in this sense too.

Definition 16 Let ↔ be an equivalence over T . A transition system T ∈ T is said to be regular w.r.t. ↔ if there is a finite system T′ ∈ T , such that T ↔ T′.

The transition system T′ from the previous definition can be seen as a finite representation of T, because it represents the behaviour of the process which is associated with the root of T. As we will see, representations generally do not say much about the behaviour of reachable nodes of T. We need another notion:

Definition 17 Let T ∈ T be a transition system and let ↔ be an equivalence over T . T has a finite characterisation w.r.t. ↔ if there is a finite T′ ∈ T , whose nodes are pairwise non-equivalent w.r.t. ↔, T ↔ T′ and for each reachable node n of T there is a reachable node n′ of T′ with n ↔ n′.

A finite characterisation T′ of T describes the system T as a whole - for each reachable node of T there is its finite characterisation within T′. An existence of a finite characterisation is especially interesting from the point of view of possible verification of concurrent systems.

Now we examine the question when finite characterisations exist and what is their relationship with representations. First we need to introduce further notions:

Definition 18 Let T ∈ T be a transition system and let ↔ be an equivalence over T . T is strongly regular w.r.t. ↔ if each reachable node of T is regular and T can reach only finitely many nodes up to ↔.

Definition 19 Let ↔ be an equivalence over T . For each T ∈ T we define the transition system T/ ↔: Nodes of T/ ↔ are equivalence classes of ↔, root is the class [r] and transitions are determined as follows: if n →^{a} n′ is a transition in T, then [n] →^{a} [n′] is a transition in T/ ↔.

The equivalence ↔ is said to have quotients if for any T ∈ T the natural projection p : T ⟶ T/ ↔, assigning to each node n of T the node [n] of T/ ↔, is a part of ↔ (i.e. n ↔ [n] for each node n of T).

Lemma 7 Let T ∈ T and let ↔ be an equivalence over T which has quotients. Then T has a finite characterisation w.r.t. ↔ iff T is strongly regular w.r.t. ↔.

Proof: “⇒” Let T′ be a finite characterisation of T. Each reachable node n of T is regular, because it is equivalent to some node n′ of T′ and T′ is finite. Assume that T can reach infinitely many pairwise non-equivalent nodes n_{i}, i ∈ N. Each n_{i} is equivalent to some node n′_{i} of T′. As T′ is finite, there are i, j ∈ N, i ≠ j such that n′_{i} ↔ n′_{j}. Hence also n_{i} ↔ n_{j} and we have a contradiction. “⇐” As T is strongly regular and ↔ has quotients, the transition system T/ ↔ is a finite characterisation of T.

□

The first theorem of this section shows, that the requirement of “having quotients” of the previous lemma is not too restrictive in fact. There are many reasonable equivalences, which fulfil this condition.

Lemma 8 Equivalences =_{tr}, =_{ct}, =_{f}, =_{r}, =_{ft}, =_{rt}, =_{pf} have quotients.

Proof: We will not give a separate proof for each of these equivalences, because the main idea is always the same. It corresponds to the fact, that all these equivalences are defined in a similar way. The crucial thing is to realize, that in spite of the fact that none of these equivalences is a congruence w.r.t. the transition relation, equivalent nodes have always the same sets of initial actions (see Appendix A). We present here a full proof for failure equivalence. The other proofs should be easy to complete using the same kind of argument.

Let T ∈ T be a transition system and let n ∈ N be a node of T. We show that F (n) = F ([n]), where [n] denotes the equivalence class of T/ =_{f} containing the node n:

“⊆”: Let [w, Φ] ∈ L^{∗} × P(L) be a failure pair of n (see Appendix A). By definition, there is a node n′ ∈ N such that n →^{w} n′ ∧ I(n′) ∩ Φ = ∅. But then also [n] →^{w} [n′]. The set I([n′]) is the union of all I(p), such that p ∈ [n′]. As p =_{f} q implies I(p) = I(q), we can conclude that I([n′]) = I(n′), hence I([n′]) ∩ Φ = ∅, thus [w, Φ] ∈ F ([n]).

“⊇”: Let [w, Φ] ∈ L^{∗}×P(L) be a failure pair of [n] and let w = a_{k}a_{k−1} … a_{1}. By definition, there is a sequence [n_{k}] →^{a_{k}} [n_{k−1}] →^{a_{k−1}} … →^{a_{1}} [n_{0}] in T/ =_{f}, such that n ∈ [n_{k}] and I([n_{0}]) ∩ Φ = ∅. We show, that for each node m of T such that m ∈ [n_{i}], where i ∈ {0, …, k}, the pair [a_{i} … a_{1}, Φ] belongs to F (m). We proceed by induction on i:

• i = 0: as I(m) = I([n_{0}]), the pair [ϵ, Φ] ∈ F (m).

• induction step: as [n_{i}] →^{a_{i}} [n_{i−1}], there are nodes p, q of T, such that p →^{a_{i}} q, p ∈ [n_{i}] and q ∈ [n_{i−1}]. By induction hypothesis, the pair [a_{i−1} … a_{1}, Φ] ∈ F (q), hence [a_{i} … a_{1}, Φ] ∈ F (p). As m =_{f} p, the pair [a_{i} … a_{1}, Φ] belongs to F (m).

□

Lemma 9 Simulation equivalence, ready simulation equivalence and 2nested simulation equivalence have quotients.

Proof: Let T ∈ T be a transition system and let n ∈ N be a node of T. First we show that n =_{s} [n], where [n] denotes the equivalence class of T/ =_{s}. By definition, two simulations R, S, such that [n, [n]] ∈ R, [[n], n] ∈ S have to be defined. The simulation R is exactly the natural projection p : T → T/ =_{s}:

R = {[k, [k]] : k ∈ N}

It is easy to check, that R is indeed a simulation. The way how S is defined is more complicated:

[[p], q] ∈ S iff there exists a derivation scheme for [[p], q].

The derivation scheme for [[p], q] consists of:

• a path [m_{0}] →^{a_{1}} [m_{1}] →^{a_{2}} … →^{a_{k}} [m_{k}] in T/ =_{s}, k ≥ 0

• a set of nodes {p_{0}, …, p_{k−1}} ⊆ N, if k > 0 • a set of nodes {q_{i,j} | 0 ≤ i ≤ k, i ≤ j ≤ k} ⊆ N

• a set of simulations {S_{0}, …, S_{k−1}}, if k > 0 such that:

• n = q_{0,0}, q = q_{0,k}, n ∈ [m_{0}], p ∈ [m_{k}]

• p_{i} ∈ [m_{i}] for i ∈ {0, …, k − 1}, q_{i,i} ∈ [m_{i}] for i ∈ {0, …, k}

• p_{i} →^{a_{i+1}} q_{i+1,i+1} for i ∈ {0, …, k − 1}

• q_{i,j} →^{a_{i+1}} q_{i,j+1} for 0 ≤ i ≤ k − 1, i ≤ j < k − 1

• [p_{i}, q_{i,i}] ∈ S_{i} for i ∈ {0, …, k − 1}

• [q_{i+1,j}, q_{i,j}] ∈ S_{i} for 0 ≤ i ≤ k − 1, i < j ≤ k The following picture could be helpful:

[figure: q_{0,0} = n; p_{0}; q_{0,1}; q_{1,1}; p_{1}; q_{0,2}; q_{1,2}; q_{2,2}; p_{2}; q_{0,k−1}; q_{1,k−1}; q_{2,k−1}; q_{3,k−1}; q_{k−1,k−1}; p_{k−1}; q_{0,k} = q; q_{1,k}; q_{2,k}; q_{3,k}; q_{k−1,k}; q_{k,k}; a_{1}; a_{1}; a_{2}; a_{2}; a_{2}; S_{0}; S_{0}; S_{0}; S_{1}; S_{1}; S_{2}; S_{0}; S_{0}; S_{1}; S_{1}; S_{2}; S_{2}; S_{k−1}; S_{k−1}; a_{k}; a_{k}; a_{k}; a_{k}; a_{k}; a_{k}; . . . . . .; . . . . . .; . . . . . .; . . . . . .; .........; .........; [n] = [m_{0}] =; p_{0} q_{0,0}; [m_{1}] =; p_{1} q_{1,1}; [m_{2}] =; p_{2} q_{2,2}; [m_{k−1}] =; p_{k−1} q_{k−1,k−1}; [p] = [m_{k}] =; q_{k,k}; a_{1}; a_{2}; a_{k}; . . . . . .]

Relation S is a simulation - whenever [[p], q] ∈ S and [p] →^{a} [p′], then there is a q′, such that q →^{a} q′ and [[p′], q′] ∈ S. This is due to the existence of a derivation scheme for the pair [[p], q]. We can simply add a new “layer” to the scheme and construct a derivation scheme for the pair [[p′], q′]. The way how it is done is obvious. Moreover, S contains the pair [[n], n].

This construction can be used also for ready simulation equivalence. The simulation R becomes a ready simulation. It follows directly from the fact that two nodes, which are ready simulation equivalent, have the same sets of initial actions. The notion of the derivation scheme has to be modified slightly - we now require {S_{0}, …, S_{k−1}} to be a set of ready simulations. Then S is also a ready simulation: assume that [[p], q] ∈ S. Then I([p]) = I(q) because q_{k,k} ∈ [p] and the simulations S_{0}, …, S_{k−1} are ready simulations now.

In the case of 2-nested simulation equivalence the construction can be used too. The simulation R becomes a 2-nested simulation, because we have already proved that n =_{s} [n] for each node n of T. The notion of the derivation scheme has to be modified again - {S_{0}, …, S_{k−1}} are 2-nested simulations now. We prove that S is a 2-nested simulation. Let [[p], q] ∈ S. We need to show that [p] =_{s} q. By definition, two simulations P, Q such that [[p], q] ∈ P and [q, [p]] ∈ Q have to be constructed. Clearly S is a simulation which contains the pair [[p], q], hence we can choose P = S. The construction of Q is slightly more complicated. As [[p], q] ∈ S, there is a derivation scheme for [[p], q]. Now S_{0}, …, S_{k−1} are not only simulations, but 2-nested simulations, hence q_{k,k} =_{s} q. Therefore there is a simulation T containing the pair [q, q_{k,k}]. It is easy to check that Q = {[u, [v]] : [u, v] ∈ T } is a simulation. Moreover, [q, [p]] ∈ Q because q_{k,k} ∈ [p].

□

We have proved the first theorem of this section:

Theorem 5 Each equivalence in van Glabbeek hierarchy has quotients.

There are also other well-known equivalences which have quotients - e.g. weak bisimilarity (see [1]) or branching bisimilarity (see [14]). But this property is naturally not general; there are also equivalences which do not have quotients. A simple example is language equivalence. Two transition systems are language equivalent if their roots have the same completed traces (realize that language equivalence is different from completed trace equivalence and is even incomparable with trace equivalence). A counterexample is easy to find.

We have seen that in many cases the condition of strong regularity becomes sufficient and necessary for the existence of a finite characterisation. An interesting question is, what is the exact relationship between conditions of regularity and strong regularity (the first one guarantees the existence of a finite representation, the other guarantees the existence of a finite characterisation). Strong regularity always implies regularity, but the converse is not generally true.

Definition 20 An equivance ↔ over T is safe if whenever T ↔ T′ then:

• for each reachable node n of T there is a reachable node n′ of T′ such that n ↔ n′

• for each reachable node n′ of T′ there is a reachable node n of T such that n ↔ n′

Lemma 10 Let ↔ be a safe equivalence over T . Then T is strongly regular w.r.t. ↔ iff T is regular w.r.t. ↔

Proof: “⇒” Obvious. “⇐” The arguments of Lemma 7 can be used.

□

An immediate consequence of Lemma 7 and Lemma 8 is:

Lemma 11 Let ↔ be a safe equivalence over T which has quotients. Then ∀T ∈ T : T has a finite representation iff T has a finite characterisation.

Thus in the case of a safe equivalence which has quotients the notions of regularity and strong regularity coincide. We have already mentioned some examples - bisimilarity, weak bisimilarity and branching bisimilarity are safe and have quotients. But there are also equivalences, for which these two notions are really different.

Lemma 12 For each behavioural equivalence ↔ which lies under ready simulation equivalence in van Glabbeek hierarchy (including this relation) there is a transition system T ∈ T , such that T is regular w.r.t. ↔ and T is not strongly regular w.r.t. ↔.

Proof: Let T_{1} = [N_{1}, L_{1}, →_{1}, r_{1}], T_{2} = [N_{2}, L_{2}, →_{2}, r_{2}] be transition systems, where N_{1} ⊆ N ∪ {0} × N ∪ {0}:

N_{1} = ⋃_{i=0}^{∞} {[i, j] | 0 ≤ j ≤ i + 1}

L_{1} = {a}
→_{1} = ⋃_{i=0}^{∞} { [[i, j], a, [i, j + 1]] | j ∈ {0, …, i}} ∪ {[[0, 0], a, [0, 0]]}
∪ { [[i, 0], a, [i + 1, 0]] | i ∈ N ∪ {0}}
r_{1} = [0, 0]
N_{2} = {A, B}
L_{2} = {a}
→_{2} = {[A, a, A], [A, a, B]}
r_{2} = A

If we draw these transition systems, we obtain the following pictures:

[figure: a; a; a; a; a; a; a; a; a; a; a; a; a; a; a; a; a; a; a; a; .....; a; a; T_{1}; T_{2}]

System T_{1} is not strongly regular w.r.t. trace equivalence, because tr([i, 1]) ⊂ tr([i + 1, 1]) for each i ∈ N ∪ {0}, thus T_{1} contains infinitely many states w.r.t. trace equivalence. Therefore T_{1} is not strongly regular w.r.t. any equivalence in van Glabbeek hierarchy.

Now we show that T_{1} =_{rs} T_{2}. By definition, two ready simulations R, S, such that r_{1}Rr_{2} and r_{2}Sr_{1} have to be constructed:

R = ⋃_{i=0}^{∞}{ [[i, j], A] : 0 ≤ j ≤ i} ∪ ⋃_{i=0}^{∞}{ [[i, i + 1], B] }
S = { [A, [0, 0]], [B, [0, 1]] }

It is easy to check that R, S are ready simulations. Moreover, [0, 0] = r_{1} R r_{2} = A and A = r_{2} S r_{1} = [0, 0].

As T_{1} =_{rs} T_{2}, transition systems T_{1}, T_{2} are equivalent w.r.t. any behavioural equivalence which lies under ready simulation equivalence in van Glabbeek hierarchy. As T_{2} is finite, the system T_{1} is regular w.r.t. each of these equivalences.

□

Lemma 13 There is a transition system T ∈ T , such that T is regular w.r.t. possible-futures equivalence and 2-nested simulation equivalence, but T is not strongly regular w.r.t. these equivalences.

Proof: Let T_{1} = [N_{1}, L_{1}, →_{1}, r_{1}], T_{2} = [N_{2}, L_{2}, →_{2}, r_{2}] be transition systems, where:

N_{1} = N ∪ {0}
L_{1} = {a}
→_{1} = { [i, i + 1] | i ∈ N} ∪ { [i, i − 1] | i ∈ N}
r_{1} = 1
N_{2} = {A, B, C}
L_{2} = {a}
→_{2} = { [A, a, B], [A, a, C], [C, a, A] }
r_{2} = A

Systems T_{1}, T_{2} can be depicted as follows:

[figure: a; a; a; a; a; a; a; a; a; .....; a; a; a; T_{1}; T_{2}]

We show that T_{1} has infinitely many nodes w.r.t. =_{pf} and =_{2}. Let i, j ∈ N, i < j be nodes of T_{1}. The node i has a possible future [a^{i}, ∅]. Clearly [a^{i}, ∅] ∉ P F (j), hence i ≠_{pf} j. As 2-nested simulation equivalence is above possible-futures equivalence in van Glabbeek hierarchy, the system T_{1} has infinitely many states also w.r.t. =_{2}, thus T_{1} is not strongly regular w.r.t. =_{2} and =_{pf}.

It remains to prove that T_{1} is regular w.r.t. =_{2} and =_{pf}. We show, that T_{1} =_{2} T_{2}. First we have to classify which nodes of T_{1} and T_{2} are simulation equivalent. Clearly 0 =_{s} B. If i ∈ N is odd then i =_{s} A, and if i ∈ N is even then i =_{s} C. Following relations are the required simulations:

R_{i} = { [k, A] | k ∈ N ∧ k is odd} ∪ { [k, C] | k ∈ N ∪ {0} ∧ k is even}
S_{i} = { [A, i], [B, i + 1], [C, i + 1] }

Now we can define two 2-nested simulations, which relate roots of T_{1} and T_{2}:

R = { [i, A] | i ∈ N ∧ i is odd} ∪ { [i, C] | k ∈ N ∧ i is even} ∪ {[0, B]}
S = { [A, 1], [B, 0], [C, 2] }

Elements of R, S are pairs of simulation equivalent nodes. Now it is easy to check that R, S are 2-nested simulations. As [1, A] ∈ R ∧ [A, 1] ∈ S, transition systems T_{1}, T_{2} are 2-nested simulation equivalent.

As T_{1} =_{2} T_{2} and possible-futures equivalence lies under 2-nested simulation equivalence in van Glabbeek hierarchy, systems T_{1} and T_{2} are also possible-futures equivalent. Thus T_{1} is regular w.r.t. =_{2} and =_{pf}

□

We have just proved the following theorem:

Theorem 6 Let ↔ be an equivalence in van Glabbeek hierarchy, which lies under bisimilarity. Then there is T ∈ T , such that T is regular w.r.t. ↔ and T is not strongly regular w.r.t. ↔

An open problem is, whether the notions of regularity and strong regularity have different features w.r.t. their decidability. In the next section we present some negative results, stating that both regularity and strong regularity can be undecidable in certain process algebras. From the practical point of view it would be much more interesting to obtain some positive results, but this area seems to be quite unexplored. Recently, Jančar and Moller presented in [15] an interesting result, stating that trace, simulation and bisimulation equivalence are decidable for pairs of Petri nets, such that one member of this pair is a bounded Petri net (i.e. a finite-state process).

6 Negative results

In this section we present some negative results, stating that regularity and strong regularity are undecidable in some process algebras. This area was first examined by Taubner in [11]. We generalize these results using a simple reduction of the halting problem of Minsky machine.

6.1 The Minsky machine

A Minsky machine (denoted here by M) is equipped with two counters C_{1}, C_{2}, which can store non-negative integers. The behaviour of M is determined by a finite-state program, composed of m ∈ N labelled statements:

l_{1} : s_{1}
l_{2} : s_{2}
⋮
l_{m−1} : s_{m−1}

            l_{m}  : HALT

where for each i, 1 ≤ i < m the statement s_{i} has one of the two forms:

s_{i} = \{ \begin{matrix}C_{j} = C_{j} + 1; goto l_{k} \\ if C_{j} = 0 then goto l_{k} else C_{j} = C_{j} − 1; goto l_{n}; \end{matrix}

where j ∈ {1, 2}. The machine M starts its execution (with given input values on C_{1}, C_{2}) from the command with the label l_{1}. M halts if it reaches the command HALT in a finite number of steps, and diverges otherwise. Naturally, the halting problem of Minsky machine is undecidable (see [12]).

6.2 Extending BPP_{τ} with the operator of restriction

In this section we explore a calculus obtained by extending BPP_{τ} with the restriction operator. In [11] Taubner proved that there is no algorithm which, for some process Δ of this class as input, outputs a regular process Δ′ in normal form with Δ ∼ Δ′ if such a Δ′ exists, and which outputs “no” otherwise. We extend this result also for other equivalences and for the notion of strong regularity, which was introduced in the previous section. All negative results are proved in a uniform way using a very simple technique.

We begin by formally introducing the restriction operator. Let L be a subset of Act, such that τ ∉ L. The restriction operator, denoted by “\L”, has the following meaning:

\frac{E →^{a} E′}{E\L →^{a} E′\L} (a ∉ L ∪ \overline{L})

It is mainly used as a tool for forcing synchronizations on certain actions. If we extend BPP_{τ} expressions with the restriction operator, we get a new class of processes, denoted by BPP_{τ}^{R}.

Processes of BPP_{τ}^{R} are able to simulate the execution of an arbitrary Minsky machine M (see [11]). The simulating process can be automaticly constructed and has the following form:

S = (K_{1}|K_{2}|P_{1})\L

Processes K_{1}, K_{2} simulate counters. We will not describe the way how they are defined - it is not important for our purposes (see [11] or [10] for details). Process P_{1} simulates the program of M and L contains all visible actions of K_{1}, K_{2} and P_{1}, forcing the three components to cooperate.

The program of M is simulated by P_{1}, which consists of m defining equations containing variables from {P_{1}, …, P_{m}}. Each equation is determined as follows:

1. P_{i} =^{def} i_{j}P_{l_{k}}

if s_{i} is of the form C_{j} = C_{j} + 1; goto l_{k};

2. P_{i} =^{def} z_{j}P_{l_{k}} + d_{j}P_{l_{n}}

if s_{i} is of the form if C_{j} = 0 then goto l_{k} else C_{j} = C_{j} − 1; goto l_{n};

3. P_{i} =^{def} 0

if s_{i} = HALT

Actions i_{j}, d_{j}, z_{j}, j ∈ {1, 2} represent operations on counters and have their complements in K_{1} and K_{2}. The expression 0 denotes a process which does nothing (it is an explicit name for the empty process expression). The execution of M is thus simulated by communications among K_{1}, K_{2} and P_{1}. Machine M diverges iff S ∼ X, where X =^{def} τX.

Lemma 14 There is a BPP_{τ}^{R} process Y, which is not regular w.r.t. trace equivalence.

Proof: Let Y =^{def} (a.(A|C))\\{b\}, A =^{def} a.(A|C) + b, C =^{def} \overline{b}.c.b. Process

Y is normed, hence its traces are just prefixes of its completed traces. The set ct(Y) = {a^{k}(τc)^{k} | k ∈ N}. Assume that there is a finite process Y′ with n states, such that Y and Y′ are trace equivalent. As a^{n+1}(τc)^{n+1} ∈ ct(Y), this sequence of actions is also a trace of Y′. As Y′ has only n states, there is a state φ of Y′ such that

Y′ →^{a^{k}} φ →^{a^{l}} φ →^{a^{m}} ψ →^{(τc)^{n+1}} χ

where ψ, χ are states of Y′, k + l + m = n + 1 and l > 0. But then also

Y′ →^{a^{k}} φ →^{a^{m}} ψ →^{(τc)^{n+1}} χ

thus a^{k}a^{m}(τc)^{n+1} is a trace of Y′. But this sequence of actions is not a prefix of any completed trace of Y, hence a^{k}a^{m}(τc)^{n+1} ∉ tr(Y) and Y ≠_{tr} Y′.

□

As Y is not regular w.r.t. trace equivalence, it is not (strongly) regular w.r.t. any equivalence in van Glabbeek hierarchy.

Theorem 7 Regularity w.r.t. any equivalence in van Glabbeek hierarchy is undecidable in the class BPP_{τ}^{R}.

Proof: Let ↔ be an equivalence in van Glabbeek hierarchy. We define a new process P′_{1} with variables from {P′_{1}, …, P′_{m}, A, C}. These variables are defined in the same way as variables of P_{1} except A, C and P′_{i}, where s_{i} = HALT (we denote this variable just P′):

P′ =^{def} (a.(A|C))\\{b\}, A =^{def} a.(A|C) + b, C =^{def} \overline{b}.c.b

where a, b, \overline{b}, c ∉ L. Let S′ = (K_{1}|K_{2}|P′_{1})\L. If M diverges, then S′ is regular w.r.t ↔, because S′ ∼ X where X =^{def} τX, thus also S′ ↔ X. If S′ is regular w.r.t ↔, then it cannot reach a state of the form (K′_{1}|K′_{2}|P′)\L in a finite number of τ moves. To see this, assume the converse. As (K′_{1}|K′_{2}|P′)\L ∼ P′ and (K′_{1}|K′_{2}|P′)\L was reached from S′ under a finite number of τ moves, we can conclude S′ ∼ τ^{k}.P′ where k ∈ N (realize that the first k moves of S′ are completely deterministic). The process τ^{k}.P′ is clearly non-regular w.r.t. trace equivalence (arguments of Lemma 10 can be used), hence S′ is also non-regular w.r.t. trace equivalence (otherwise we can use the fact that bisimilarity implies trace equivalence and conclude that τ^{k}.P′ is regular w.r.t. trace equivalence just by transitivity). As S′ is not regular w.r.t trace equivalence, it is not regular w.r.t. ↔ and we have a contradiction.

We have just proved that M diverges iff S′ is regular w.r.t. ↔. As S′ can be for any Minsky machine M constructed by an algorithm, we have the desired reduction.

□

This method can be used also for other equivalences and other process algebras which have a parallel operator and can simulate counters (see [11]). Moreover, it works also for strong regularity.

7 Conclusions, future work

If we compare the decidability results, obtained for classes of normed BPP and normed BPA processes, we can observe that they are of a similar form. This is not surprising if fact - the only difference between BPP and BPA algebras is the way of binary composition they provide - the parallel composition in the case of BPP and the sequential composition in the case of BPA. But these two operators have similar algebraic properties and it reflects in many things - processes of BPP and BPA can be represented in similar normal forms (GNF), there are similar cancelation properties, the notion of self-bisimulation, introduced in [4], can be defined in a uniform way (see [9]) and so on.

An open problem still remains the question of deciding regularity in the whole classes of BPP and BPA. This problem is at least semi-decidable, because bisimilarity is known to be decidable in these algebras - hence we can take a BPA or BPP process Δ in GNF and start to remove sequences (in the case of BPA) or multisets (in the case of BPP) of variables, whose cardinality is greater then one, from defining equations. We have already described the removal procedure for BPP class (see Section 3.3). The procedure for BPA is similar, but the right distributivity law (see [3]) has to be used instead of the expansion law.

Another interesting question mentioned already in the Section 5 is, whether there are behavioural equivalences, for which conditions of regularity and strong regularity have different decidability properties and this is the area we would like to examine in the future.

Acknowledgement

All presented results were obtained during my stay at BRICS (Basic Research in Computer Science), Department of Computer Science, University of Aarhus. I would like to thank Mogens Nielsen for his support and encouragement. He was always willing to listen to my ideas, commenting them in a very inspiring way. Thanks are also due to Mojmír Křetínský for reading the first draft of this paper and providing me with various helpful information.

References

[1] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

[2] S.Mauw, H.Mulder. Regularity of of BPA-systems is decidable. In Proceedings of CONCUR’94, LNCS 836, pages 34-47. Springer-Verlag, 1994

[3] J.C.M. Beaten, J.A. Bergstra, J.W. Klop. Decideability of bisimulation equivalence for processes generating contex-free languages. In LNCS 259, pages 93-114. Springer-Verlag, 1987.

[4] D. Caucal. Graphes canoniques de graphes algebriques. Rapport de Recherche 872, INRIA, Juillet 1988.

[5] J.F Groote. A short proof of the decidability of bisimulation for normed BPA processes. Information Processing Letters 42, pages 167-171, 1991.

[6] H. Hüttel, C. Stirling. Actions speak louder than words: Proving bisimilarity for contex free processes. In Proceedings of the 6th annual symposium on logic in computer science (LICS91), pages 376-386. IEEE computer society press, 1991.

[7] S. Christensen, H. Hüttel, C. Stirling. Bisimulation equivalence is decidable for all contex-free processes. In Proceedings of CONCUR 92, Lecture Notes in Computer Science 630, pages 138-147. Springer-Verlag, 1992.

[8] S. Christensen, Y. Hirsfeld, F. Moller. Bisimulation equivalence is Decidable for basic parallel processes. In Proceedings of CONCUR 93, Lecture Notes in Computer Science 715, pages 143-157. Springer-Verlag, 1993.

[9] Y. Hirshfeld. Deciding equivalences in simple process algebras. Technical report ECS-LFCS-94-294, Department of Computer Science, University of Edinburgh, 1994.

[10] S. Christensen. Decidability and Decomposition in Process Algebras. Ph.D Thesis, University of Edinburgh, 1993.

[11] D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. Lecture Notes in Computer Science 369. Springer-Verlag, 1989.

[12] M.L. Minsky. Computation-Finite and Infinite machines. Prentice-Hall, 1967

[13] R.J. van Glabbeek. The Linear Time - Branching Time spectrum. In Proceedings of CONCUR 90, Lecture Notes in Computer Science 458, pages 278-297. Springer-Verlag, 1990.

[14] R.J. van Glabbeek, W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In G.X. Ritter, editor, Information Processing 89, pages 613-618. North-Holland, 1989.

[15] P. Jančar, F. Moller. Checking Regular Properties of Petri Nets. In Proceedings of CONCUR 95, Lecture Notes in Computer Science 962. Springer-Verlag, 1995.

Appendix A

To keep this report self-contained, we present here also the definitions of behavioural equivalences in van Glabbeek hierarchy. We adopt here the definition of the transition system from Section 5 (T = [N, L, →, r]). If

A ∈ N, then I(A) = {a ∈ L | ∃B ∈ N such that A →^{a} B} denotes the set

of initial actions (labels) of A. Moreover, if M is a set, then P(M) denotes the power-set of M.

Definition 21 (Trace equivalence) Let T ∈ T be a transition system. We define the set of traces of T, denoted tr(T), in the following way:

tr(T) = {w ∈ L^{∗} | ∃A ∈ N, such that r →^{w} A}

Transition systems T_{1}, T_{2} are trace equivalent, notation T_{1} =_{tr} T_{2}, if tr(T_{1}) = tr(T_{2}).

Definition 22 (Completed trace equivalence) Let T ∈ T be a transition system. We define the set of completed traces of T, denoted ct(T), in the following way:

ct(T) = {w ∈ L^{∗} | ∃A ∈ N, such that r →^{w} A ∧ A ↛^{a} B for any a ∈ Act, B ∈ N}

Transition systems T_{1}, T_{2} are completed trace equivalent, notation T_{1} =_{ct} T_{2}, if tr(T_{1}) = tr(T_{2}) ∧ ct(T_{1}) = ct(T_{2}).

Definition 23 (Failure equivalence) Let T ∈ T be a transition system. A pair [w, Φ] ∈ L^{∗} × P(L) is a failure pair of T, if there is a node A ∈ N such that r →^{w} A and I(A) ∩ Φ = ∅. Let F (T) denote the set of all failure pairs of T. Transition systems T_{1}, T_{2} are failure equivalent, notation T_{1} =_{f} T_{2}, if F (T_{1}) = F (T_{2})

Definition 24 (Readiness equivalence) Let T ∈ T be a transition system. A pair [w, Φ] ∈ L^{∗} × P(L) is a ready pair of T, if there is a node A ∈ N such that r →^{w} A and I(A) = Φ. Let R(T) denote the set of all ready pairs of T. Transition systems T_{1}, T_{2} are readiness equivalent, notation T_{1} =_{r} T_{2}, if R(T_{1}) = R(T_{2}).

Definition 25 (Failure trace equivalence) Let T ∈ T be a transition system. The refusal relations →^{Φ} for Φ ∈ P(L) are definined by: A →^{Φ} B iff A = B ∧ I(A) ∩ Φ = ∅. The failure trace relations →^{δ} for δ ∈ (L ∪ P(L))^{∗} are defined as the reflexive and transitive closure of both the transition and the refusal relations. δ ∈ (L ∪ P(L))^{∗} is a failure trace of T, if there is a node A ∈ N such that r →^{δ} A. Let F T (T) denote the set of failure traces of T. Transition systems T_{1}, T_{2} are failure trace equivalent, notation T_{1} =_{ft} T_{2}, if F T (T_{1}) = F T (T_{2}).

Definition 26 (Ready trace equivalence) Let T ∈ T be a transition system. The ready trace relations ⇒^{δ} for δ ∈ (L ∪ P(L))^{∗} are defined inductively by:

1. A ⇒^{ϵ} A for any A ∈ N.

2. A →^{a} B implies A ⇒^{a} B.

3. A ⇒^{Φ} B with Φ ∈ P(L) whenever A = B and I(A) = Φ.

4. A ⇒^{δ} B ⇒^{ρ} C implies A ⇒^{δρ} C.

δ ∈ (L ∪ P(L))^{∗} is a ready trace of T, if there is a node A ∈ N such that r ⇒^{δ} A. Let RT (T) denote the set of ready traces of T. Transition systems T_{1}, T_{2} are ready trace equivalent, notation T_{1} =_{rt} T_{2}, if RT (T_{1}) = RT (T_{2}).

Definition 27 (Simulation equivalence) Let T_{1}, T_{2} ∈ T . A binary relation R ⊆ N_{1} × N_{2} is a simulation if whenever A_{1}RA_{2} then

∀a ∈ L_{1} : A_{1}RA_{2} ∧ A_{1} →^{a} A′_{1} ⇒ ∃A′_{2} : A_{2} →^{a} A′_{2} ∧ A′_{1}RA′_{2}

Transition systems T_{1}, T_{2} are simulation equivalent, notation T_{1} =_{s} T_{2}, if there exists a simulation R with r_{1}Rr_{2} and a simulation S with r_{2}Sr_{1}.

Definition 28 (Ready simulation equivalence) Let T_{1}, T_{2} ∈ T . A binary relation R ⊆ N_{1} × N_{2} is a ready simulation if whenever A_{1}RA_{2} then:

• ∀a ∈ L_{1} : A_{1}RA_{2} ∧ A_{1} →^{a} A′_{1} ⇒ ∃A′_{2} : A_{2} →^{a} A′_{2} ∧ A′_{1}RA′_{2}

• I(A_{1}) = I(A_{2})

Transition systems T_{1}, T_{2} are ready simulation equivalent, notation T_{1} =_{rs} T_{2}, if there exists a ready simulation R with r_{1}Rr_{2} and a ready simulation S with r_{2}Sr_{1}.

Definition 29 (Possible futures equivalence) Let T ∈ T be a transition system. A pair [w, Φ] ∈ L^{∗} × P(L^{∗}) is a possible future of T, if there is a node B ∈ N such that A →^{w} B and tr(B) = Φ. The set of all possible futures of T is denoted P F (T). Transition systems T_{1}, T_{2} are possible-futures equivalent, notation T_{1} =_{pf} T_{2}, if P F (T_{1}) = P F (T_{2}).

Definition 30 (2-nested simulation equivalence) Let T_{1}, T_{2} ∈ T . A binary relation R ⊆ N_{1} × N_{2} is a 2-nested simulation if whenever A_{1}RA_{2} then

• ∀a ∈ L_{1} : A_{1}RA_{2} ∧ A_{1} →^{a} A′_{1} ⇒ ∃A′_{2} : A_{2} →^{a} A′_{2} ∧ A′_{1}RA′_{2}

• A_{1} =_{s} A_{2}

Transition systems T_{1}, T_{2} are 2-nested simulation equivalent, notation T_{1} =_{2} T_{2}, if there exists a 2-nested simulation R with r_{1}Rr_{2} and a 2-nested simulation S with r_{2}Sr_{1}.

Recent Publications in the BRICS Report Series

RS-95-52 Anton��n Ku� cera. Deciding Regularity in Process Algebras. October 1995. 42 pp.

RS-95-51 Rowan Davies. A Temporal-Logic Approach to Binding-Time Analysis. October 1995. 11 pp.

RS-95-50 Dany Breslauer. On Competitive On-Line Paging with Lookahead. September 1995. 12 pp.

RS-95-49 Mayer Goldberg. Solving Equations in the λ-Calculus using Syntactic Encapsulation. September 1995. 13 pp.

RS-95-48 Devdatt P. Dubhashi. Simple Proofs of Occupancy Tail Bounds. September 1995. 7 pp. To appear in Random Structures and Algorithms.

RS-95-47 Dany Breslauer. The Suf�x Tree of a Tree and Minimizing Sequential Transducers. September 1995. 15 pp.

RS-95-46 Dany Breslauer, Livio Colussi, and Laura Toniolo. On the Comparison Complexity of the String Pre�x-Matching Problem. August 1995. 39 pp. Appears in Leeuwen, editor, Algorithms - ESA ’94: Second Annual European Symposium proceedings, LNCS 855, 1994, pages 483�494.

RS-95-45 Gudmund Skovbjerg Frandsen and Sven Skyum. Dynamic Maintenance of Majority Information in Constant Time per Update. August 1995. 9 pp.

RS-95-44 Bruno Courcelle and Igor Walukiewicz. Monadic Second-Order Logic, Graphs and Unfoldings of Transition Systems. August 1995. 39 pp. To be presented at CSL ’95.

RS-95-43 Noam Nisan and Avi Wigderson. Lower Bounds on Arithmetic Circuits via Partial Derivatives (Preliminary Version). August 1995. 17 pp. To appear in 36th Annual Conference on Foundations of Computer Science, FOCS ’95, IEEE, 1995.

RS-95-42 Mayer Goldberg. An Adequate Left-Associated Binary Numeral System in the λ-Calculus. August 1995. 16 pp.