BRICS RS-01-50 J. Srba: Note on the Tableau Technique for Commutative Transition Systems BRICS

Basic Research in Computer Science

Note on the Tableau Technique for Commutative Transition Systems

Jiří Srba BRICS Report Series RS-01-50 ISSN 0909-0878 December 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Jiří Srba.

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 BRICS Report Series publications. 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@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/50/

Note on the Tableau Technique for Commutative Transition Systems^{⋆}

Jiří Srba^{⋆⋆}
BRICS^{⋆ ⋆ ⋆}

Department of Computer Science University of Aarhus Ny Munkegade bldg. 540, 8000 Aarhus C, Denmark

                              srba@brics.dk

Abstract. We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableaubased proof for BPP, that strong bisimilarity between any two states of such a transition system is decidable. It gives a general technique for extending decidability borders of strong bisimilarity for a wide class of infinite-state transition systems. This is demonstrated for several process formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets.

1 Introduction

Semantics of various formalisms for description of concurrent processes like process algebra, Petri nets, pushdown systems and many others is usually given in terms of labelled transition systems. This provides a common ground for studying such systems, and the usually considered problems as model checking and equivalence checking (see e.g. [BCMS01]) can be defined purely in terms of labelled transition systems. In this paper we focus on the equivalence checking problem and show a general approach for extending known decidability borders of strong bisimilarity for commutative-based process formalisms. In particular, we examine the class of transition systems generated by algebras with the operator of parallel composition and we discuss its extensions with lossiness, interrupt and with time features.

It is known that strong bisimilarity is undecidable for a typical representative of fully parallel models — Petri nets [Jan95]. Nevertheless, in [Chr93,CHM93] Christensen, Hirshfeld and Moller proved using a tableau

⋆ Full version of [Srb02a]. ⋆⋆ The author is supported in part by the GACR, grant No. 201/00/0400.

⋆ ⋆ ⋆

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

technique, that bisimilarity is decidable for an important fragment of Petri nets called communication free Petri nets. The complexity of this algorithm is still open — no primitive recursive upper bound is known. PSPACE-hardness of the problem was recently shown in [Srb02b]. The class of transition systems definable by communication free Petri nets can be equivalently described in terms of process algebra with a commutative operator for parallel composition and recursion. It is this formalism, usually called Basic Parallel Processes (BPP), that is used in the original tableau-based proof in [CHM93]. For an overview on the tableau technique consult e.g. [JM99].

We abstract from the specific BPP syntax and generalise the proof for a class of transition systems called effective commutative transition systems (ECTS). We give six simple conditions on a transition system to be an ECTS and if all of them are satisfied, bisimilarity between any two states of the transition system is decidable. There is no need to know the syntactic description of the system. Moreover, the generalisation is achieved in several ways: (i) states can be tuples of bounded multisets of natural numbers and not only tuples of natural numbers, (ii) we do not insist on a specific computation of successors of a given state — any effectively computable and finite set of successors is acceptable, and (iii) an auxiliary equivalence relation on states is introduced in order to check invariants for pairs in a bisimulation relation.

Semantics of many formalisms can be defined as an ECTS and this yields immediately decidability of bisimilarity. We demonstrate this on four examples — BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets — thus extending in several ways the known decidability border which lies somewhere between BPP systems and state-extended BPP systems (state-extended BPP systems are a strict subclass of Petri nets where bisimilarity is still undecidable [BCMS01,JM99]).

2 General Method

Let ℕ_{0} = {0, 1, …} be the set of natural numbers. A multiset of ℕ_{0} is a function M : ℕ_{0} → ℕ_{0}. Let i ∈ ℕ_{0}, then M(i) denotes the number of occurrences of i in the multiset M. The empty multiset ∅ is a function such that ∅(i) = 0 for all i ∈ ℕ_{0}. The multiset union of two multisets M_{1} and M_{2} is defined by (M_{1} ⊎M_{2})(i) = M_{1}(i)+M_{2}(i) for all i ∈ ℕ_{0}. By B_{∞} we denote the set of all multisets of ℕ_{0}. Let m ∈ ℕ_{0}. We define a set B_{m} of all multisets of {0, 1, …, m}, i.e., M ∈ B_{m} iff M ∈ B_{∞} and M(i) = 0 for all i ∈ ℕ_{0} such that i > m. We call a multiset M ∈ B_{∞} finite if there is some m ∈ ℕ_{0} such that M ∈ B_{m}. For finite multisets we sometimes use an alternative set-like notation: e.g. a multiset {0, 1, 1, 4, 4, 4} is the same as a multiset M such that M(0) = 1, M(1) = 2, M(4) = 3 and M(i) = 0 for i ∈ ℕ_{0} ∖ {0, 1, 4}.

Let M, N ∈ B_{m}. We write M ≺_{ℓ} N iff there is k, 0 ≤ k ≤ m, such that M(k) < N(k) and M(i) = N(i) for all i, 0 ≤ i < k. Let M, N ∈ B_{m} then M ≠ N implies that either M ≺_{ℓ} N or N ≺_{ℓ} M. We write M ⪯_{c} N iff M(i) ≤ N(i) for every i, 1 ≤ i ≤ m, i.e., iff there is M′ ∈ B_{m} such that N = M ⊎ M′.

Let m, n ∈ ℕ_{0} and n > 0. We define a structure S = (B_{m}^{n}, ⊕, ∅^{n}) where B_{m}^{n} is a set of n-tuples of elements from B_{m}. Let α = (M_{1}, M_{2}, …, M_{n}) ∈ B_{m}^{n} and β = (N_{1}, N_{2}, …, N_{n}) ∈ B_{m}^{n}, then α ⊕ β = (M_{1} ⊎ N_{1}, M_{2} ⊎ N_{2}, …, M_{n} ⊎ N_{n}). Of course, α ⊕ β ∈ B_{m}^{n}. The structure S is a commutative monoid. If α ∈ B_{m}^{n} then α_{i}, 1 ≤ i ≤ n, is the i’th coordinate of α. We introduce two orderings on B_{m}^{n}. Let α, β ∈ B_{m}^{n}, then α <_{ℓ} β iff there is k, 1 ≤ k ≤ n, such that α_{k} ≺_{ℓ} β_{k} and α_{i} = β_{i} for every i, 1 ≤ i < k; and α ≤_{c} β iff α_{i} ⪯_{c} β_{i} for every i, 1 ≤ i ≤ n.

Observe that <_{ℓ} is a well-founded ordering (there is no infinite sequence α_{1}, α_{2}, … such that α_{1} >_{ℓ} α_{2} >_{ℓ} …) since ≺_{ℓ} is well-founded. Moreover for any α ≠ β either α <_{ℓ} β or β <_{ℓ} α. Also notice that α ≤_{c} β iff there is α′ ∈ B_{m}^{n} such that β = α ⊕ α′. We write α <_{c} β iff α ≤_{c} β and α ≠ β. The following lemma is a simple generalisation of Dickson’s Lemma [Dic13].

Lemma 1. Every infinite sequence of elements from B_{m}^{n} has an infinite nondecreasing subsequence w.r.t. ≤_{c}.

A labelled transition system is a 4-tuple (S, Act, ⟶, Eqv) where S is a set of states (or processes), Act is a set of labels (or actions), ⟶⊆ S×Act×S is a transition relation, written α ⟶^{a} β, for (α, a, β) ∈⟶, and Eqv ⊆ S × S is an equivalence relation on states.

Our definition of labelled transition systems is a generalisation of labelled transition systems with final states — see an overview paper [BCMS01]. Let F ⊆ S be a set of final states. In order to recover the definition from [BCMS01] we define (α, β) ∈ Eqv iff α ∈ F and β ∈ F, or α ∉ F and β ∉ F.

Let α ∈ S. We write α −̸→ whenever there is no β ∈ S and a ∈ Act such that α ⟶^{a} β. As usual we extend the transition relation to the elements of Act^{∗}. We define a norm of α ∈ S by N (α) = min{|w| | w ∈ Act^{∗} such that ∃β ∈ S. α ⟶^{w} β −̸→}. By definition min ∅ = ∞.

Let T = (S, Act, ⟶, Eqv) be a labelled transition system. A binary relation R ⊆ S × S is a bisimulation iff whenever (α, β) ∈ R then for each

a ∈ Act: if α ⟶^{a} α′ then ∃β′ ∈ S such that β ⟶^{a} β′ and (α′, β′) ∈ R;

if β ⟶^{a} β′ then ∃α′ ∈ S such that α ⟶^{a} α′ and (α′, β′) ∈ R; and (α, β) ∈ Eqv.

States α, β ∈ S are bisimulation equivalent or bisimilar in a transition system T, written α ∼_{T} β, iff (α, β) ∈ R for some bisimulation R. If T is clear from the context, we write only α ∼ β instead of α ∼_{T} β.

Remark 1. Sometimes the bisimilarity checking problem is formulated in this way: we are given a pair of labelled transition systems T_{1} and T_{2} with states α_{1} from T_{1} and α_{2} from T_{2}, and the question α_{1} ∼ α_{2} is asked. In this case, we can consider a disjoint union of T_{1} and T_{2} (i.e. the sets of states of T_{1} and T_{2} are disjoint) as a new transition system T and ask the question α_{1} ∼_{T} α_{2}.

Let (S, Act, ⟶, Eqv) be a labelled transition system. The stratified bisimulation relations [Mil89] ∼_{k}⊆ S × S for k ∈ ℕ_{0} are defined as follows:

– α ∼_{0} β for all α, β ∈ S such that (α, β) ∈ Eqv, i.e., ∼_{0}= Eqv

– α ∼_{k+1} β iff for each a ∈ Act: if α ⟶^{a} α′ then ∃β′ ∈ S such that

β ⟶^{a} β′ and α′ ∼_{k} β′; if β ⟶^{a} β′ then ∃α′ ∈ S such that α ⟶^{a} α′

and α′ ∼_{k} β′; and (α, β) ∈ Eqv.

Given a labelled transition system T = (S, Act, ⟶, Eqv) we define a set next(α, a) = {β ∈ S | α ⟶^{a} β} for α ∈ S and a ∈ Act. We also define next(α, ∗) = ⋃_{a∈Act} next(α, a). The system T is image-finite iff the set next(α, a) is finite for every α ∈ S and a ∈ Act. The following lemma is a standard one.

Lemma 2. Let (S, Act, ⟶, Eqv) be an image-finite labelled transition system and α, β ∈ S. Then α ∼ β iff α ∼_{k} β for all k ∈ ℕ_{0}.

Let us introduce the following class of labelled transition systems.

Definition 1 (Effective Commutative Transition System). A labelled transition system T = (S, Act, ⟶, Eqv) is an effective commutative transition system (ECTS) iff there exist n, m ∈ ℕ_{0}, n > 0 such that the following conditions are satisfied:

(1) S = B_{m}^{n},

(2) Act is a finite set,

(3) given α, β ∈ S it is decidable whether (α, β) ∈ Eqv,

(4) next(α, a) is effectively constructible for every α ∈ B_{m}^{n} and a ∈ Act, (5) T is image-finite,

(6) if α ∼_{k} β then (α ⊕ γ) ∼_{k} (β ⊕ γ) for every α, β, γ ∈ B_{m}^{n} and k ∈ ℕ_{0}.

Let us call the elements of B_{m}^{n} processes. Since any ECTS is image-finite (5), the fact that ∼_{k} are congruences (6) together with Lemma 2 implies: (6’) if α ∼ β then (α ⊕ γ) ∼ (β ⊕ γ) for every α, β, γ ∈ B_{m}^{n}.

Theorem 1. Let T = (B_{m}^{n}, Act, ⟶, Eqv) be an ECTS. Given A, B ∈ B_{m}^{n}, it is decidable whether A ∼ B.

Proof. The proof is by tableau-technique and it is a generalisation of the tableau-based proof used by Christensen, Hirshfeld and Moller in order to demonstrate decidability of bisimilarity for BPP [Chr93,CHM93].

A tableau for (A, B) ∈ B_{m}^{2n} is a maximal proof tree rooted with (A, B) and built according to the following rules. Let (α, β) be a node in the tree. A node (α, β) is either terminal (leaf) or nonterminal. The following nodes are terminal:

– (α, α) is a successful leaf for any α ∈ B_{m}^{n} (note that always (α, α) ∈ Eqv),

– (α, β) is a successful leaf if next(α, ∗)∪next(β, ∗) = ∅ and (α, β) ∈ Eqv,

– (α, β) is an unsuccessful leaf if for some a ∈ Act it is the case that next(α, a) ∪ next(β, a) ≠ ∅, and either next(α, a) = ∅ or next(β, a) = ∅,

– (α, β) is an unsuccessful leaf if (α, β) ∉ Eqv.

We say that a node is an ancestor of (α, β) if it is on the path from the root to (α, β) and at least one application of the rule EXPAND (defined later) separates them. If (α, β) is not a leaf then we reduce it using the following RED rules as long as possible.

RED

L

\frac{(α, β)}{(γ ⊕ ω, β)}

if there is an ancestor (γ, δ) or (δ, γ) of (α, β) such that γ <_{ℓ} δ and α = δ ⊕ ω for some ω ∈ B_{m}^{n}

RED

R

\frac{(α, β)}{(α, γ ⊕ ω)}

if there is an ancestor (γ, δ) or (δ, γ) of (α, β) such that γ <_{ℓ} δ and β = δ ⊕ ω for some ω ∈ B_{m}^{n}

If no other reduction RED is applicable and the resulting node is not a leaf, we apply the rule EXPAND for a set of relations S_{a}, a ∈ Act, where S_{a} ⊆ next(α, a) × next(β, a) such that ∀α′ ∈ next(α, a).∃β′ ∈ next(β, a). (α′, β′) ∈ S_{a} and ∀β′ ∈ next(β, a).∃α′ ∈ next(α, a). (α′, β′) ∈ S_{a}.

EXPAND \frac{(α, β)}{\{(α′, β′) | a ∈ Act ∧ (α′, β′) ∈ S_{a}\}}

The set notation used in the rule EXPAND means that each element (α′, β′) in the conclusion of the rule becomes a new child in the proof tree. Now, we start again applying the RED-rules to every such child (which is not a leaf) as long as possible. Note that reduction rules are applicable to a node iff the node is not terminal (leaf).

Lemma 3. Any tableau for (A, B) is finite and there are only finitely many tableaux.

Proof. Observe that any tableau for (A, B) is finitely branching because of the assumption (5) and the condition that Act is finite (2), which implies that for a given a ∈ Act any relation S_{a} is finite and there are finitely many such relations. Should the tableau be infinite, there is an infinite branch, which gives an infinite sequence of vectors from B_{m}^{2n}. Since the rules RED can be used only finitely many times in a sequence (they decrease the <_{ℓ} order, which is well founded), there must be an infinite subsequence of vectors on which the rule EXPAND was applied. Using Lemma 1, this sequence must contain an infinite nondecreasing subsequence p_{1} ≤_{c} p_{2} ≤_{c} . . .. However, the rule EXPAND cannot be applied on p_{2} since one of the rules RED is applicable. This is a contradiction.

Since there are only finitely many relations S_{a} for an a ∈ Act available for the EXPAND rule and finitely many possibilities for an application of the RED rule, there are always finitely many possibilities how to extend already existing partial tableau. Suppose that there are infinitely many tableaux starting from (A, B). Then there must be a tableau for (A, B) with an infinite branch, which contradicts that every tableau is finite. ⊓ ⊔

We call a tableau for (A, B) successful if it is maximal (no further rules are applicable) and all its leaves are successful.

Lemma 4 (Completeness). If A ∼ B then there is a successful tableau for (A, B).

Proof. We construct a tableau from the root (A, B) such that every node (α, β) in the tableau satisfies α ∼ β. Hence this tableau cannot contain any unsuccessful leaf and it must be finite because of Lemma 3. Suppose that (α, β) is already a node in the tableau such that α ∼ β and consider the rule RED_{L} applied on (α, β). We may assume that γ ∼ δ, which means using (6’) that (γ ⊕ ω) ∼ (δ ⊕ ω) = α ∼ β. Hence (γ ⊕ ω) ∼ β. Similarly for RED_{R}. From the definition of ∼ follows that the rule EXPAND is also forward sound, i.e., if α ∼ β then we can choose for every a ∈ Act a relation S_{a} such that (α′, β′) ∈ S_{a} implies that α′ ∼ β′. ⊓ ⊔ Lemma 5 (Soundness). If there is a successful tableau for (A, B) then A ∼ B.

Proof. For the sake of contradiction assume that there is a successful tableau for (A, B) and A ≁ B. We show that we can construct a path from the root (A, B) to some leaf, such that for any pair (α, β) on this path α ≁ β.

If A ≁ B then using Lemma 2 there is a minimal k such that A ≁_{k} B. Notice that if α ≁_{k} β such that k is minimal and we apply the rule EXPAND, then at least one of its children (α′, β′) satisfies that α′ ≁_{k−1} β′. We choose such a child to extend our path from the root.

If we apply RED_{L} on (α, β) where α ≁_{k} β and k is minimal, then the corresponding ancestor (γ, δ) is separated by at least one application of EXPAND and so γ ∼_{k} δ. This implies that (γ ⊕ ω) ≁_{k} β, otherwise using the assumption (6) we get that α = (δ ⊕ ω) ∼_{k} (γ ⊕ ω) ∼_{k} β, which is a contradiction with α ≁_{k} β. The same is true for RED_{R}. Thus there must be a path from the root to some leaf such that for any pair (α, β) on this path α ≁ β. This is a contradiction with the fact that the path contains a successful leaf. ⊓ ⊔

We have proved that it is decidable whether A ∼ B, since it is the case iff there is a successful tableau for (A, B). There are only finitely many tableaux and all of them are finite, moreover the conditions (3) and (4) ensure that they are effectively constructible. ⊓ ⊔

3 Applications

In this section we consider several specific classes of commutative transition systems. We study in particular BPP and lossy BPP processes, interrupt BPP systems and timed-arc BPP nets.

3.1 BPP and deadlock-sensitive BPP

The class of Basic Parallel Processes (BPP) [Chr93] is a natural subclass of PA (Process Algebra [BW90]) where only the operator of parallel composition is used. It is a well known fact that bisimilarity is decidable for BPP [Chr93,CHM93]. We give the definition of BPP by means of process rewrite systems [May00a], which is more convenient for our purposes than the usual one by process equations used by Milner [Mil89]. We remind the reader of the fact that these two definitions are equivalent in the sense that they define the same class of processes up to bisimilarity.

\frac{(X ⟶^{a} E) ∈ Δ}{X ⟶^{a} E}  \frac{E ⟶^{a} E′}{E||F ⟶^{a} E′||F}

Fig. 1. SOS rules for BPP

Let Act and Var be countable sets of actions and process constants such that Act ∩ Var = ∅. We define a class of process expressions EVar over Var by the following abstract syntax E ::= ϵ | X | E||E, where ϵ is the empty process and X ranges over Var. The operator ‘||’ stands for a parallel composition. We do not distinguish between process expressions related by a structural congruence ≡ ⊆ EVar×EVar, which is the smallest congruence over process expressions such that the following laws hold:

– ‘||’ is associative and commutative, and

– ‘ϵ’ is a unit for ‘||’.

A BPP process rewrite system (PRS) [May00a] is a finite set Δ ⊆ Var × Act × EVar of rules, written X ⟶^{a} E for (X, a, E) ∈ Δ. Let us denote the set of actions and process constants that appear in Δ as Act(Δ) resp. Var(Δ) (note that these sets are finite).

A process rewrite system Δ determines a labelled transition system T (Δ) = (EVar(Δ)/≡, Act(Δ), ⟶, Eqv) where states are ≡-equivalence classes of process expressions over Var(Δ), Act(Δ) is the set of labels, the transition relation ⟶ is the least relation satisfying the SOS rules in Figure 1 (recall that ‘||’ is commutative and in what follows we often abuse the notation and write only E instead of [E]_{≡}, i.e., the equivalence class represented by E). There are two possibilities for defining the equivalence relation Eqv. In the usual setting Eqv = (EVar(Δ)/≡) × (EVar(Δ)/≡) is the universal relation (thus it is in fact unused) and we call this class BPP. Another possibility is to define Eqv by

Eqv = {(E, F) ∈ (EVar(Δ)/≡) × (EVar(Δ)/≡) | E = [ϵ]_{≡} iff F = [ϵ]_{≡}}.

We call this class deadlock-sensitive BPP. A study of strict (deadlocksensitive) and nonstrict (deadlock-nonsensitive) bisimilarity for a sequential analogue of BPP called Basic Process Algebra (BPA) is provided in [Srb01].

We show that given a BPP system Δ, we can interpret its semantics as a commutative transition system such that states are elements of B_{n−1} = B_{n−1}^{1} where n = |Var(Δ)|. Because of the structural congruence ≡, any process expression E over Var(Δ) can be represented by a vector of n natural numbers. Suppose a fixed ordering on Var(Δ) = {X_{0}, X_{1}, …, X_{n−1}}. Then the corresponding vector contains on i’th coordinate the number of occurrences of the variable X_{i} in E. Formally, we define a mapping ϕ : EVar(Δ) → B_{n−1}^{1} by

ϕ(ϵ) = ∅
ϕ(X_{i}) = M such that M(i) = 1 and M(j) = 0 for j ≠ i
ϕ(E_{1}||E_{2}) = ϕ(E_{1}) ⊕ ϕ(E_{2}).

The following proposition is an easy observation.

Proposition 1. Let E, F ∈ EVar(Δ). Then E ≡ F iff ϕ(E) = ϕ(F).

Hence any rule (X ⟶^{a} E) ∈ Δ can be represented by ϕ(X) ⟶^{a} ϕ(E). The system Δ, where n = |Var(Δ)|, generates a commutative labelled transition system T^{c}(Δ) = (B_{n−1}^{1}, Act(Δ), ⟶, Eqv), where α ⟶^{a} β iff there exists a rule (X ⟶^{a} E) ∈ Δ such that α = ϕ(X) ⊕ ω and β = ϕ(E) ⊕ ω for some ω ∈ B_{n−1}^{1}. The relation Eqv for BPP and deadlocksensitive BPP is defined in the same fashion as above.

Example 1. Let us consider Δ =

{X_{0} ⟶^{a} X_{0}||X_{1}||X_{2}||X_{1}, X_{0} ⟶^{a} ϵ, X_{1} ⟶^{b} ϵ, X_{2} ⟶^{c} ϵ}.

Then n = 3 and e.g. ϕ(X_{0}) = {0}, ϕ(X_{0}||X_{1}||X_{2}||X_{1}) = {0, 1, 1, 2} and ϕ(ϵ) = ∅. A sequence of transitions

X_{0} ⟶^{a} X_{0}||X_{1}||X_{2}||X_{1} ⟶^{a} X_{0}||X_{1}||X_{2}||X_{1}||X_{1}||X_{2}||X_{1} ⟶^{b}

X_{0}||X_{2}||X_{1}||X_{1}||X_{2}||X_{1} ⟶^{c} X_{0}||X_{1}||X_{1}||X_{2}||X_{1}

has a straightforward analogue in B_{2}^{1}:

{0} ⟶^{a} {0, 1, 1, 2} ⟶^{a} {0, 1, 1, 1, 1, 2, 2} ⟶^{b}

{0, 1, 1, 1, 2, 2} ⟶^{c} {0, 1, 1, 1, 2}.

Obviously, T (Δ) and T^{c}(Δ) are isomorphic labelled transition systems.

Theorem 2. Given a BPP^{1} process rewrite system Δ (or a deadlocksensitive BPP process rewrite system Δ) and a pair of processes P_{1}, P_{2} ∈ EVar(Δ)/≡, it is decidable whether P_{1} ∼_{T (Δ)} P_{2}.

Proof. It can be easily verified that T^{c}(Δ) defined above is an ECTS. Then we use Theorem 1. ⊓ ⊔

1 For BPP this is already proved in [Chr93,CHM93]. We repeat the theorem in order to demonstrate that our technique is general enough to cover already known results.

\frac{(X ⟶^{a} E) ∈ Δ}{X ⟶^{a} E}  \frac{E ⟶^{a} E′}{E||F ⟶^{a} E′||F}  \overline{E ⟶^{drop} F} if ∃F′≠ϵ s.t. E = F ||F′

Fig. 2. SOS rules for lossy BPP

3.2 Lossy BPP

The notion of unreliability, in particular lossiness, has been intensively studied with a number of interesting results. Let us mention e.g. models like Lossy Channel Systems [AJ96] or Lossy Vector Addition Systems [BM99,May00b]. Lossy BPP systems were studied in [May00b] in the context of model checking problems. In lossy BPP we allow process constants disappear spontaneously at any time. We give a formal definition of lossy BPP systems first.

A lossy BPP process rewrite system is a finite set Δ ⊆ Var×Act×EVar of rules, written X ⟶^{a} E for (X, a, E) ∈ Δ.

A process rewrite system Δ determines a labelled transition system T (Δ) = (EVar(Δ)/ ≡, Act(Δ) ∪ {drop}, ⟶, Eqv) where states are ≡- equivalence classes of process expressions over Var(Δ), Act(Δ) ∪ {drop} is the set of labels with a distinguished label drop ∉ Act(Δ) modelling lossiness, the transition relation ⟶ is defined by the SOS rules in Figure 2 (we again abuse the notation and write only E instead of [E]_{≡}) and Eqv for lossy BPP can be defined as in the case of BPP — deadlock sensitive or deadlock nonsensitive. Example 2. Let Δ =

{X_{0} ⟶^{a} X_{0}||X_{0}, X_{0} ⟶^{b} ϵ}.

Then X_{0} ⟶^{∗} X_{0}^{k} for any k ∈ ℕ_{0} where X_{0}^{0} = ϵ and X_{0}^{k+1} = X_{0}||X_{0}^{k}.

Also, X_{0}^{k} ⟶^{drop} X_{0}^{k′} for any k′, 0 ≤ k′ < k, in particular, X_{0}^{k} ⟶^{drop} ϵ and ϵ −̸→. This means that any reachable state in T (Δ) has norm at most 1. Moreover, X_{0}^{k} ≁_{T (Δ)} X_{0}^{k′} for any k ≠ k′. Hence there cannot be any BPP process bisimilar to X_{0} (there are only finitely many nonbisimilar BPP states of norm less or equal to 1). On the other hand this property in general disallows to find a bisimilar lossy BPP process for a given BPP process. Thus the classes BPP and lossy BPP are, as expected, incomparable w.r.t. bisimilarity.

We are now ready to define semantics of lossy BPP in terms of commutative transition systems, similarly as for BPP. Let Δ be a lossy BPP system, where n = |Var(Δ)|. By T^{c}(Δ) = (B_{n−1}^{1}, Act(Δ) ∪ {drop}, ⟶, Eqv) we denote a commutative transition system, where α ⟶^{a} β iff either (i) there is a rule (X ⟶^{a} E) ∈ Δ such that α = ϕ(X) ⊕ ω and β = ϕ(E) ⊕ ω for some ω ∈ B_{n−1}^{1}, or (ii) β <_{c} α and a = drop. The relation Eqv for lossy BPP is defined in the same fashion as mentioned above (deadlock sensitive or deadlock nonsensitive).

Obviously, T (Δ) and T^{c}(Δ) are isomorphic labelled transition systems. This implies the following decidability theorem for lossy BPP systems.

Theorem 3. Given a lossy BPP process rewrite system Δ (either deadlock sensitive or deadlock nonsensitive) and a pair of processes P_{1}, P_{2} ∈ EVar(Δ)/≡, it is decidable whether P_{1} ∼_{T (Δ)} P_{2}.

Proof. We show that T^{c}(Δ) is an ECTS and then we use Theorem 1 and the isomorphism between T (Δ) and T^{c}(Δ).

To verify conditions (1) – (5) of Definition 1 is easy. Let us now examine the condition (6). Assume that α ∼_{k} β for some k ∈ ℕ_{0} and let γ ∈ B_{n−1}^{1}. By induction on k we show that also α ⊕ γ ∼_{k} β ⊕ γ. Base case: If k = 0 then it is enough to show that if (α, β) ∈ Eqv then also (α ⊕ γ, β ⊕ γ) ∈ Eqv. This is true for both deadlock sensitive and nonsensitive Eqv. Inductive step: Let k > 0 and α ∼_{k} β. Of course, (α ⊕ γ, β ⊕ γ) ∈ Eqv. We will analyse the transitions from α ⊕ γ only (the arguments for β ⊕ γ are symmetric).

Let α ⊕ γ ⟶^{a} κ and a ≠ drop. Then either κ = α′ ⊕ γ and α ⟶^{a} α′, or κ = α ⊕ γ′ and γ ⟶^{a} γ′. In the first case, because of our assumption

that α ∼_{k} β, also β ⟶^{a} β′ such that α′ ∼_{k−1} β′. Thus β ⊕ γ ⟶^{a} β′ ⊕ γ

and using the induction hypothesis α′ ⊕ γ ∼_{k−1} β′ ⊕ γ. The second case where κ = α ⊕ γ′ is analogical.

Let α ⊕ γ ⟶^{drop} κ. Then κ = α′ ⊕ γ′ such that α′ ≤_{c} α and γ′ ≤_{c} γ, and

α′ ⊕ γ′ <_{c} α ⊕ γ. If α′ = α then β ⊕ γ ⟶^{drop} β ⊕ γ′ and using the induction hypothesis and the fact that α ∼_{k−1} β we get that α⊕γ′ ∼_{k−1} β ⊕γ′. Let

α <_{c} α′. Since α ∼_{k} β and α ⟶^{drop} α′, also β ⟶^{drop} β′ such that α′ ∼_{k−1} β′.

Hence β ⊕ γ ⟶^{drop} β′ ⊕ γ′ and using the induction hypothesis we know that α′ ⊕ γ′ ∼_{k−1} β′ ⊕ γ′. ⊓ ⊔

3.3 Interrupt BPP

In this subsection we investigate mode transfer operators in BPP process algebra, in particular the interrupt operator. Quoting [BB00]:“A useful feature in programming languages and specification languages is the ability to denote mode switches. In particular, most languages have means to describe the disrupt and interrupt of the normal execution of a system.” Various mode transfer operators were considered in the literature [BBK86,BB00,Ber89,CE98,Die94]. We define interrupt BPP systems that extend the pure BPP systems with an interrupt vector and a mechanism for handling the interrupt. The motivation is that every state is annotated with a set of allowed interrupts and if no interrupt appears, a normal execution of the process is performed. At any time an interrupt can be raised by performing the action int. A normal execution of the process is interrupted and the raised interrupt is handled. During this all interrupts are disallowed. After the interrupt is finished, the action iret is performed and a normal execution of the interrupted process continues.

Formally, an interrupt BPP process rewrite system Δ is a pair (Δ_{1}, Δ_{2}) where Δ_{1} is a finite set Δ_{1} ⊆ Var × Act × EVar × 2Var(Δ^{2}) and Δ_{2} is

a BPP system. We write (X ⟶^{a} E, enable) for (X, a, E, enable) ∈ Δ_{1}.

By Var(Δ_{1}) we denote the set of variables that occur in the first and the third component of Δ_{1}.

A process rewrite system Δ = (Δ_{1}, Δ_{2}) determines a labelled transition system T (Δ) = ((EVar(Δ^{1})/≡)×2Var(Δ^{2}) ×{0, 1}×(EVar(Δ^{2})/≡),

Act(Δ_{1}) ∪ Act(Δ_{2}) ∪ {int, iret}, ⟶, Eqv^{u}) where states are 4-tuples (E_{1}, IV, IF, E_{2}) such that E_{1} is a BPP process, IV is an interrupt vector, IF is an interrupt flag (0 means normal execution and 1 means interrupt call) and E_{2} is ϵ if IF = 0 or it contains the interrupt handling process in the case IF = 1. We assume that int, iret ∉ Act(Δ_{1}) ∪ Act(Δ_{2}). The SOS rules for ⟶ are defined in Figure 3 (E again represents [E]_{≡} and ‘||’ is commutative) and for the sake of simplicity let us assume that Eqv^{u} is the universal relation on states.

Example 3. Let Δ =

({(X_{0} ⟶^{a} X_{0}||X_{0}, {Y_{0}}), (X_{0} ⟶^{b} ϵ, {Y_{1}})}, {Y_{0} ⟶^{c} ϵ, Y_{1} ⟶^{d} Y_{1}}).

Consider an initial state (X_{0}, ∅, 0, ϵ). Then the following sequence of transitions is possible in T (Δ):

(X_{0}, ∅, 0, ϵ) ⟶^{a} (X_{0}||X_{0}, {Y_{0}}, 0, ϵ) ⟶^{b} (X_{0}, {Y_{0}, Y_{1}}, 0, ϵ) ⟶^{int}

(X_{0}, {Y_{0}, Y_{1}}, 1, Y_{0}) ⟶^{c} (X_{0}, {Y_{0}, Y_{1}}, 1, ϵ) ⟶^{iret} (X_{0}, {Y_{0}, Y_{1}}, 0, ϵ) ⟶^{int}

(X_{0}, {Y_{0}, Y_{1}}, 1, Y_{1}) ⟶^{d} (X_{0}, {Y_{0}, Y_{1}}, 1, Y_{1}) ⟶^{d} · · · .

\frac{(X ⟶^{a} E_{1}, enable) ∈ Δ_{1}}{(X, IV, 0, ϵ) ⟶^{a} (E_{1}, IV ∪ enable, 0, ϵ)}

\frac{(E_{1}, IV, 0, ϵ) ⟶^{a} (E′_{1}, IV′, 0, ϵ)}{(E_{1}||F_{1}, IV, 0, ϵ) ⟶^{a} (E′_{1}||F_{1}, IV′, 0, ϵ)}

\frac{X ∈ IV}{(E_{1}, IV, 0, ϵ) ⟶^{int} (E_{1}, IV, 1, X)}  \overline{(E_{1}, IV, 1, ϵ) ⟶^{iret} (E_{1}, IV, 0, ϵ)}
\frac{(X ⟶^{a} E_{2}) ∈ Δ_{2}}{(E_{1}, IV, 1, X) ⟶^{a} (E_{1}, IV, 1, E_{2})}  \frac{(E_{1}, IV, 1, E_{2}) ⟶^{a} (E_{1}, IV, 1, E′_{2})}{(E_{1}, IV, 1, E_{2}||F_{2}) ⟶^{a} (E_{1}, IV, 1, E′_{2}||F_{2})}

Fig. 3. SOS rules for interrupt BPP

It is an easy observation that there is no BPP process bisimilar to the initial state (X_{0}, ∅, 0, ϵ) of T (Δ) — we use similar arguments as in Example 2.

We remind the reader of the fact that for any BPP system we can find a bisimilar interrupt BPP system simply by disallowing interrupts at all — we define enable = ∅ in every rule of the BPP system. Hence the class of interrupt BPP is strictly more expressive (w.r.t. bisimilarity) than the class of BPP.

We demonstrate now, how to give an alternative semantics in terms of a commutative transition system T^{c}. The idea is that the normal process execution is simulated one-to-one in T^{c} and the interrupt calls are checked using the relation Eqv — thus there are no actions int and iret. Let Δ = (Δ_{1}, Δ_{2}) be an interrupt BPP system such that Var(Δ_{1}) = {X_{0}, …, X_{n_{1}−1}} and Var(Δ_{2}) = {Y_{0}, …, Y_{n_{2}−1}}. In what follows we denote by T (Δ_{2}) the deadlock sensitive transition system generated by the BPP process Δ_{2}. Since bisimilarity in T (Δ_{2}) is decidable (Theorem 2), we may assume w.l.o.g. that Y_{i} ≁_{T (Δ_{2})} Y_{j} for all i, j such that 0 ≤ i < j ≤ n_{2} − 1. Let n = max{n_{1} − 1, n_{2} − 1}.

Let T^{c}(Δ) = (B_{n}^{2}, Act(Δ_{1}) ∪ Act(Δ_{2}), ⟶, Eqv). The intuition is that in the first component of a state (M, N) ∈ B_{n}^{2} we remember a BPP expression of normal process execution and in the second component we remember an interrupt vector IV in the following sense: N(i) = 0 if Y_{i} ∉ IV, and N(i) > 0 if Y_{i} ∈ IV. For α = (M, N) ∈ B_{n}^{2}, let IV (α) = {Y_{i} | 0 ≤ i ≤ n_{2} − 1 ∧ N(i) > 0} and let cut(α) = (M, N′) ∈ B_{n}^{2} such that

N′(i) = \begin{cases}0 & if N(i) = 0 \\ 1 & if N(i) > 0 \end{cases}

for all i ∈ ℕ_{0}. We define

α = (M, N) ⟶^{a} (M′, N′) = α′

iff (E, IV (α), 0, ϵ) ⟶^{a} (E′, IV (α′), 0, ϵ) such that a ∉ {int, iret}, ϕ(E) =

M, ϕ(E′) = M′, and cut(α′) = α′. The last condition (cut(α′) = α′) ensures that T^{c}(Δ) becomes image-finite. Finally we define Eqv as such a relation that for states α, β ∈ B_{n}^{2}: (α, β) ∈ Eqv iff IV (α) = IV (β).

The following property is an immediate consequence of the definition.

Property 1. Let α ∈ B_{n}^{2}. Then α ∼_{T^{c}(Δ)} cut(α).

Proposition 2. Let Δ = (Δ_{1}, Δ_{2}) be an interrupt BPP system. Then it holds that (E, ∅, 0, ϵ) ∼_{T (Δ)} (F, ∅, 0, ϵ) iff (ϕ(E), ∅) ∼_{T^{c}(Δ)} (ϕ(F), ∅) for any E, F ∈ EVar(Δ^{1}).

Proof. It is obvious that any transition under a where a ∉ {int, iret} in T (Δ) can be simulated naturally in the system T^{c}(Δ) and vice versa. An interrupt call in T (Δ) is checked using the relation Eqv and whenever (α, β) ∉ Eqv in T^{c}(Δ) then we can distinguish the corresponding states in T (Δ) by an appropriate interrupt call. ⊓ ⊔

We can now present the following decidability theorem for interrupt BPP.

Theorem 4. Given an interrupt BPP process rewrite system Δ and a pair of processes (E, ∅, 0, ϵ), (F, ∅, 0, ϵ) in T (Δ), it is decidable whether (E, ∅, 0, ϵ) ∼_{T (Δ)} (F, ∅, 0, ϵ).

Proof. By Proposition 2 it is enough to show that T^{c}(Δ) is an ECTS and use Theorem 1. The validity of conditions (1) – (5) of Definition 1 is straightforward. Remains to verify condition (6). We proceed by induction on k. Let α ∼_{k} β and γ ∈ B_{n}^{2}. We show that α ⊕ γ ∼_{k} β ⊕ γ. Base case: If k = 0 then it is enough to show that if (α, β) ∈ Eqv then also (α ⊕ γ, β ⊕ γ) ∈ Eqv. This is trivially true. Inductive step: Let k > 0 and α ∼_{k} β. Of course, (α ⊕ γ, β ⊕ γ) ∈ Eqv. We will analyse the transitions from α ⊕ γ only (the arguments for β ⊕ γ are symmetric).

Let α ⊕ γ ⟶^{a} κ. Then either κ = cut(α′ ⊕ γ) and α ⟶^{a} α′, or κ = cut(α ⊕ γ′) and γ ⟶^{a} γ′. In the first case, because of our assumption that α ∼_{k} β, also β ⟶^{a} β′ such that α′ ∼_{k−1} β′. Hence β ⊕ γ ⟶^{a} cut(β′ ⊕ γ). Using the induction hypothesis we get α′ ⊕ γ ∼_{k−1} β′ ⊕ γ and by Property 1 this implies that cut(α′ ⊕ γ) ∼_{k−1} cut(β′ ⊕ γ). The second case where κ = cut(α ⊕ γ′) is similar. ⊓ ⊔ Remark 2. We used BPP processes for interrupt handling (the system Δ_{2}). In fact, any process algebra where bisimilarity is decidable can be used.

3.4 Timed-Arc BPP

In this subsection we establish decidability of bisimilarity for a timed extension of BPP systems, called timed-arc BPP. It is worth mentioning another positive decidability result for timed BPP. The authors in [BLS00] show that performance equivalence (a version of timed bisimilarity) is decidable in a polynomial time for BPP processes where actions have a certain time duration. However, their definition of timed BPP does not allow to interpret ordinary BPP systems as timed ones since a duration of an action cannot be equal to 0 and must be strictly positive. We define timed-arc BPP as a natural subclass of timed-arc Petri nets where time (age) is associated to tokens and transitions are labelled by time intervals, which restrict the age of tokens available for firing a transition — see e.g. [BLT90,Han93]. Our definition implies that timed-arc BPP are a strict extension (w.r.t. bisimilarity) of ordinary BPP systems, as it is demonstrated later.

First, we introduce labelled timed-arc Petri nets, following definitions from [RdFEA00] and then we define timed-arc BPP as its subclass where each transition has exactly one input place. A labelled timed-arc Petri net (LTAPN) is a tuple N = (P, T, F, c, L, λ, Σ), where

– P is a finite set of places,

– T is a finite set of transitions such that T ∩ P = ∅,

– F ⊆ (P × T) ∪ (T × P) is a flow relation,

– c : F |_{P ×T} → ℕ_{0} × (ℕ_{0} ∪ {∞}) is a time constraint on transitions such that for each arc (p, t) ∈ F holds that t_{1} ≤ t_{2} where c(p, t) = (t_{1}, t_{2}),

– L is a finite set of labels,

– λ : T → L is a labelling function, and

– Σ ⊆ ℕ_{0} is a recursive set of allowed time-elapsing steps.

Let x ∈ ℕ_{0} and c(p, t) = (t_{1}, t_{2}). We write x ∈ c(p, t) whenever t_{1} ≤ x ≤ t_{2}. We also define ^{•}t = {p | (p, t) ∈ F } and t^{•} = {p | (t, p) ∈ F }. A marking M on N is a function M: P → B where B denotes the set of all finite multisets on ℕ_{0}. Each place is thus assigned a certain number of tokens, and each token is annotated with a natural number (age). Let x ∈ B and a ∈ ℕ_{0}. We define x<+a such that we add the value a to every element of x, i.e., x <+ a = {b + a | b ∈ x}.

Let us now define the dynamics of LTAPNs. We introduce two types of transition rules: firing of a transition and time-elapsing. Let N = (P, T, F, c, L, λ, Σ) be a LTAPN, M a marking and t ∈ T. We say that t is enabled by M iff

∀p ∈ ^{•}t. ∃x ∈ M(p). x ∈ c(p, t).

If t is enabled by M then it can be fired, producing a marking M′ (written M[t⟩M′) such that

∀p ∈ P. M′(p) = (M(p) ∖ C^{−}(p, t)) ∪ C^{+}(t, p)

where C^{−} and C^{+} are chosen to satisfy the following equations (note that there may be more possibilities and that all the operations are on multisets):

C^{−}(p, t) = \{ \begin{matrix}\{x\} & such that x ∈ M(p) and x ∈ c(p, t) & if p ∈ ^{•}t \\ ∅ & & otherwise \end{matrix}

C^{+}(t, p) = \{ \begin{matrix}\{0\} & if p ∈ t^{•} \\ ∅ & otherwise. \end{matrix}

Note that the tokens added to places t^{•} are of age 0. We define also timeelapsing transitions τ_{k}, k ∈ Σ, as follows: M[τ_{k}⟩M′ iff ∀p ∈ P. M′(p) = M(p) <+ k.

Let N = (P, T, F, c, L, λ, Σ) be a LTAPN. We define the corresponding labelled transition system T (N) = ([P → B], L∪{τ_{k} | k ∈ Σ}, ⟶, Eqv^{u}), where states are markings of N, actions are labels from L together with symbols for time-elapsing, and M ⟶^{a} M′ iff either M[t⟩M′ and a = λ(t), or M[τ_{k}⟩M′ and a = τ_{k} for some k ∈ Σ. For simplicity we define Eqv^{u} to be the universal relation.

Definition 2. A timed-arc BPP is a LTAPN (P, T, F, c, L, λ, Σ) such that |^{•}t| = 1 for all t ∈ T.

Example 4. Consider a timed-arc BPP net

N = ({p_{1}, p_{2}}, {t_{1}, t_{2}}, F, c, {a, b}, λ, {1})

where F, c and λ are defined in Figure 4. Names of places (circles) are p_{1} and p_{2} (from left to right) and names of transitions (squares) are t_{1} and t_{2} (from left to right) such that λ(t_{1}) = a and λ(t_{2}) = b. Notice that ^{•}t_{1} = {p_{1}} and ^{•}t_{2} = {p_{2}}, so the net is indeed a timed-arc BPP.

[figure: 0; [0,0]; a; [0,0]; b]

Fig. 4. A timed-arc BPP net N

Let ({0}, ∅) be an initial marking — since |P | = 2 we can identify any marking M : P → B with a pair (M(p_{1}), M(p_{2})). Now e.g.

({0}, ∅) ⟶^{a} ({0}, {0}) ⟶^{a} ({0}, {0, 0}) ⟶^{b}

({0}, {0}) ⟶^{τ_{1}} ({1}, {1}) ⟶^{τ_{1}} ({2}, {2}) ⟶^{τ_{1}} ….

Using similar arguments as in Example 2, there cannot be any BPP process bisimilar to the initial marking. On the other hand, for any BPP process there is a timed-arc BPP net bisimilar to it — we use the fact that any BPP process is essentially a Petri net where |^{•}t| = 1 for every transition t and then we define all the time constrains as [0, ∞] and set Σ = ∅. So the class of timed-arc BPP is strictly more expressive (w.r.t. bisimilarity) than the BPP class.

Assuming a fixed ordering on P = {p_{1}, …, p_{n}}, there is a natural one-to-one correspondence between [P → B] and B^{n}. Let M : P → B then we define (N_{1}, …, N_{n}) ∈ B^{n} by N_{i} = M(p_{i}) for 1 ≤ i ≤ n and vice versa. In what follows we freely interchange these equivalent notations.

The system T (N) is almost a commutative labelled transition system. There are only two problems: (i) states are not elements from B_{m}^{n} for some fixed m ∈ ℕ_{0} and (ii) the set of actions can be infinite. The following arguments show how to avoid these problems.

Definition 3. Let N = (P, T, F, c, L, λ, Σ) be a LTAPN. We define its maximal guard mg(N) ∈ ℕ_{0} as the maximal time constraint that appears in N, i.e.,

mg(N) = max ({t_{1}, t_{2} | ∃f ∈ F |_{P ×T} . c(f) = (t_{1}, t_{2})} ∖ {∞}).

Let M ∈ [P → B]. We define a compression of M, C_{M} ∈ [P → B_{mg(N)+1}], by

C_{M}(p)(k) = \begin{cases}M(p)(k) & if k < mg(N) + 1 \\ ∑_{i=mg(N)+1}^{∞} M(p)(i) & if k = mg(N) + 1 \\ 0 & if k > mg(N) + 1. \end{cases}

Lemma 6. Let N = (P, T, F, c, L, λ, Σ) be a LTAPN and M_{1}, M_{2} ∈ [P → B]. If C_{M_{1}} = C_{M_{2}} then M_{1} ∼_{T (N)} M_{2}.

Proof. It is a routine exercise to verify that R = {(M_{1}, M_{2}) ∈ [P → B] × [P → B] | C_{M_{1}} = C_{M_{2}}} is a bisimulation. ⊓ ⊔

Let N = (P, T, F, c, L, λ, Σ) be a LTAPN. By m we denote the number mg(N)+1. We define a commutative transition system T^{c}(N) = (B_{m}^{n}, L∪ {τ_{k} | k ∈ Σ ∧ k < m} ∪ T_{m}, ⟶, Eqv^{u}) where T_{m} = {τ_{m}} if there is k ∈ Σ such that k ≥ m, otherwise T_{m} = ∅ (note that the construction of T_{m} is effective since Σ is a recursive set). We define M ⟶^{a} M′ for M, M′ ∈ B_{m}^{n} iff either (i) M[t⟩M′ and a = λ(t), or (ii) M[τ_{k}⟩M′′ where m > k ∈ Σ or τ_{k} ∈ T_{m}, such that M′ = C_{M′′} and a = τ_{k}.

Proposition 3. Let N be a LTAPN and M_{1}, M_{2} a pair of markings on N. Then M_{1} ∼_{T (N)} M_{2} iff C_{M_{1}} ∼_{T^{c}(N)} C_{M_{2}}.

Proof. Immediately from Lemma 6. Also note that in T (N) for any k ≥ m = mg(N) + 1 holds that if M ⟶^{τ_{m}} M′ and M ⟶^{τ_{k}} M′′, then C_{M′} = C_{M′′}. ⊓ ⊔

We are now ready to show decidability of bisimilarity for timed-arc BPP.

Theorem 5. Given a timed-arc BPP net N = (P, T, F, c, L, λ, Σ) and a pair of markings M_{1}, M_{2} on N, it is decidable whether M_{1} ∼_{T (N)} M_{2}.

Proof. By Proposition 3 it is enough to prove that T^{c}(N) is an ECTS. To verify conditions (1) – (5) of Definition 1 is easy. Let us now examine the condition (6). We proceed by induction on k. Let α ∼_{k} β and γ ∈ B_{m}^{n}. We show that α ⊕ γ ∼_{k} β ⊕ γ. Base case: If k = 0 then it is enough to show that if (α, β) ∈ Eqv^{u} then also (α ⊕ γ, β ⊕ γ) ∈ Eqv^{u}. This is trivially true. Inductive step: Let k > 0 and α ∼_{k} β. Of course, (α ⊕ γ, β ⊕ γ) ∈ Eqv^{u}. We will analyse the transitions from α ⊕ γ only (the arguments for β ⊕ γ are symmetric).

Let α ⊕ γ ⟶^{a} κ such that a ≠ τ_{l} for l ∈ ℕ_{0}. Then either κ = α′ ⊕ γ and α ⟶^{a} α′, or κ = α ⊕ γ′ and γ ⟶^{a} γ′. (Note that there are not more possibilities since |^{•}t| = 1 for any t ∈ T.) In the first case, because of our assumption that α ∼_{k} β, also β ⟶^{a} β′ such that α′ ∼_{k−1} β′. Hence β ⊕γ ⟶^{a} β′⊕γ. Using the induction hypothesis we get α′⊕γ ∼_{k−1} β′⊕γ. The second case where κ = α ⊕ γ′ is similar.

Let α ⊕ γ ⟶^{τ_{l}} α′ ⊕ γ′ for some l, m ≥ l. Of course, α ⟶^{τ_{l}} α′ and since

α ∼_{k} β also β ⟶^{τ_{l}} β′ such that α′ ∼_{k−1} β′. Hence β ⊕ γ ⟶^{τ_{l}} β′ ⊕ γ′ and

using the induction hypothesis we get α′ ⊕ γ′ ∼_{k−1} β′ ⊕ γ′. ⊓ ⊔ Remark 3. It remains an open problem whether bisimilarity is decidable for timed-arc BPP with continuous time, i.e., if we allow e.g. Σ = ℝ_{0}^{+}.

On the other hand, if we keep the discrete time setting and consider distributed timed-arc BPP nets, bisimilarity remains decidable. For the definition of distributed timed-arc Petri nets see [NSS01].

4 Conclusion

We suggested a subclass of labelled transition systems called effective commutative transition systems (ECTS) where bisimilarity is decidable, and we showed that semantics of many extensions of BPP process algebra can be defined within the ECTS class. This approach seems to be feasible also for other natural extensions of BPP: the crucial condition to be satisfied is probably (6), saying that ∼_{k} are congruences. This condition fails e.g. for Petri nets, and indeed strong bisimilarity becomes undecidable here [Jan95].

Decidability of weak bisimilarity of BPP is still a well known open problem. Here the problematic condition is (5), stating that the transition system is image-finite, which is not the case for weak bisimilarity. Nevertheless, we can still instead of potentially infinite set of successors next(α, a) examine only its finite subset such that soundness and completeness of the tableau system is preserved. This possibility was exploited by Stirling in [Sti01] for weak bisimilarity of normed BPP, however, with additional technical restrictions. To design finite subsets of next(α, a) preserving soundness and completeness even in the general case might be a reasonable way to attack this problem.

Acknowledgement. I would like to thank my advisor Mogens Nielsen for his kind supervision. I also thank Daniel Polansky, Jan Strejcek and the referees for their comments and suggestions.

References

[AJ96] P.A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996.

[BB00] J.C.M. Baeten and J.A. Bergstra. Mode transfer in process algebra. Technical report CSR 00-01, Vakgroep Informatica, Technische Universiteit Eindhoven, 2000.

[BBK86] J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae, IX(2):127–168, 1986.

[BCMS01] O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, chapter 9, pages 545–623. Elsevier Science, 2001.

[Ber89] J. A. Bergstra. A mode transfer operator in process algebra. Technical report P8808b, University of Amsterdam, The Netherlands, 1989.

[BLS00] B. Berard, A. Labroue, and Ph. Schnoebelen. Verifying performance equivalence for timed basic parallel processes. In Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures (FOSSACS’2000), volume 1784 of LNCS, pages 35–47. Springer-Verlag, 2000.

[BLT90] T. Bolognesi, F. Lucidi, and S. Trigila. From timed Petri nets to timed LOTOS. In Proceedings of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verification (Ottawa 1990), pages 1–14. North-Holland, Amsterdam, 1990.

[BM99] A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. In Annual Symposium on Theoretical Aspects of Computer Science (STACS’99), volume 1563 of LNCS, pages 323–333. Springer-Verlag, 1999.

[BW90] J.C.M. Baeten and W.P. Weijland. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.

[CE98] T. Cobben and A. Engels. Disrupt and interrupt in MSC: Possibilities and problems. In Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC, number 104 in Informatik-Berichte, pages 75– 83. Humboldt-Universität zu Berlin, 1998.

[CHM93] S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation is decidable for basic parallel processes. In Proceedings of CONCUR’93, volume 715 of LNCS, pages 143–157. Springer-Verlag, 1993.

[Chr93] S. Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, The University of Edinburgh, 1993.

[Dic13] L.E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with distinct factors. American Journal of Mathematics, 35:413–422, 1913.

[Die94] B. Diertens. New features in PSF I: Interrupts, disrupts, and priorities. Technical report P9417, University of Amsterdam, The Netherlands, 1994.

[Han93] H.M. Hanisch. Analysis of place/transition nets with timed-arcs and its application to batch process control. In Application and Theory of Petri Nets, volume 691 of LNCS, pages 282–299, 1993.

[Jan95] P. Jancar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281–301, 1995.

[JM99] P. Jancar and F. Moller. Techniques for decidability and undecidability of bisimilarity – an invited tutorial. In CONCUR ’99: Concurrency Theory, 10th International Conference, volume 1664 of LNCS, pages 30–45. Springer-Verlag, 1999.

[May00a] R. Mayr. Process rewrite systems. Information and Computation, 156(1):264–286, 2000.

[May00b] R. Mayr. Undecidable problems in unreliable computations. In Latin American Theoretical Informatics (LATIN’2000), volume 1776 of LNCS. Springer-Verlag, 2000.

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

[NSS01] M. Nielsen, V. Sassone, and J. Srba. Properties of distributed timed-arc Petri nets. In Proceedings of 21nd International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’01), volume 2245 of LNCS, pages 280–291. Springer-Verlag, 2001.

[RdFEA00] V. Valero Ruiz, D. de Frutos Escrig, and O. Marroquin Alonso. Decidability of properties of timed-arc Petri nets. In ICATPN 2000, volume 1825 of LNCS, pages 187–206. Springer-Verlag, 2000.

[Srb01] J. Srba. Basic process algebra with deadlocking states. Theoretical Computer Science, 266(1–2):605–630, 2001.

[Srb02a] J. Srba. Note on the tableau technique for commutative transition systems. In Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’02), LNCS. Springer-Verlag, 2002. To appear.

[Srb02b] J. Srba. Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard. In Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science (STACS’02), LNCS. Springer-Verlag, 2002. To appear.

[Sti01] C. Stirling. Decidability of weak bisimilarity for a subset of basic parallel processes. In Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’01), volume 2030 of LNCS, pages 379–393. Springer-Verlag, 2001.

Recent BRICS Report Series Publications

RS-01-50 Jiří Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. 19 pp. To appear in the proceedings of FOSSACS ’02.

RS-01-49 Olivier Danvy and Lasse R. Nielsen. A First-Order One-Pass CPS Transformation. 2001. Extended version of a paper to appear in the proceedings of FOSSACS ’02.

RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. December 2001. 36 pp.

RS-01-47 Jesper Buus Nielsen. Non-Committing Encryption is Too Easy in the Random Oracle Model. December 2001. 20 pp.

RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.

RS-01-45 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001. 27 pp.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.

RS-01-42 Zoltán Ésik and Werner Kuich. Rationally Additive Semirings. November 2001. 11 pp.

RS-01-41 Ivan B. Damgård and Jesper Buus Nielsen. Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor. October 2001. 43 pp.

RS-01-40 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. October 2001. 9 pp.

RS-01-39 Olivier Danvy and Mayer Goldberg. There and Back Again. October 2001. 14 pp.