BRICS RS-98-6 K. Sunesen: Further Results on Partial Order Equivalences on Infinite Systems BRICS

Basic Research in Computer Science

Further Results on Partial Order Equivalences on Infinite Systems

Kim Sunesen

BRICS Report Series RS-98-6 ISSN 0909-0878 March 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, 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/98/6/

Further Results on Partial Order Equivalences on Infinite Systems

Kim Sunesen BRICS^{∗} Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C. ksunesen@daimi.aau.dk

Abstract

In [26], we investigated decidability issues for standard language equivalence for process description languages with two generalisations based on traditional approaches for capturing non-interleaving behaviour: pomset equivalence reflecting global causal dependency, and location equivalence reflecting spatial distribution of events.

In this paper, we continue by investigating the role played by TCSP-style renaming and hiding combinators with respect to decidability. One result of [26] was that in contrast to pomset equivalence, location equvialence remained decidable for a class of processes consisting of finite sets of BPP processes communicating in a TCSP manner. Here, we show that location equivalence becomes undecidable when either renaming or hiding is added to this class of processes.

Furthermore, we investigate the weak versions of location and pomset equivalences. We show that for BPP with τ prefixing, both weak pomset and weak location equivalence are decidable. Moreover, we show that weak location equivalence is undecidable for BPP semantically extended with CCS communication.

∗ Basic Research in Computer Science, Centre of the Danish National Research Foundation.

1 Introduction

In this paper, we investigate the decidability of non-interleaving linear-time behavioural equivalences on infinite-state systems described by process algebraic languages such as CCS [19] and TCSP [5].

Our results contribute to the ongoing and systematic investigation of decidability of problems about infinite-state systems. But, our results may also be seen as a contribution to the search for elucidating the sometimes delicate computational trade-offs involved in moving from the standard view of interleaving to more intentional non-interleaving views of behaviour.

Process algebraic languages, notably CCS [19], TCSP [5] and ACP [3], have proved a rich source of infinite-state systems, and moreover, an appropriate framework for a systematic study based on the choice of combinators. One of the most interesting suggestions is Basic Parallel Processes, BPP, introduced in [7]. BPPs are recursive expressions constructed from inaction, action, variables, and the standard operators prefixing, choice and parallel compositions. By removing the parallel operator one obtains a calculus with exactly the same expressive power as finite automata. BPPs can hence be seen as arising from a minimal concurrent extension of finite automata and therefore a natural starting point when exploring concurrent infinite-state systems.

The notion of behavioural equivalences is a cornerstone in the theory of process algebraic languages. It is common to classify behavioural equivalences into branching-time and linear-time equivalences depending on whether or not the branching structure of the behaviour is taken into account or not. Another central distinction is made between strong and weak equivalences. The distinction arises when actions are divided into visible and invisible actions. Often, there is just one invisible or silent action denoted τ. In the strong case, the invisible τ action is an action no different from the other actions whereas in the weak case equivalence is based on abstracting away from the invisible actions only requiring equivalent behaviour with respect to visible actions.

Many results about decidability are known for interleaving equivalences such as bisimulation and language equivalences on infinite-state systems, see [8, 11] for surveys. Also, for non-interleaving bisimulation equivalences results are known, see [6, 17].

In [26], we compared standard language equivalence with two generalisations based on traditional approaches capturing non-interleaving behaviour. The first known as pomset equivalence was based on pomsets representing global causal dependency [22], and the second known as location equivalence on locality [4] representing spatial distribution of events. The two notions of non-interleaving equivalences were shown to be decidable on BPP contrasting the result of Hirshfeld [10] that language equivalence is undecidable. Moreover, larger subclasses of CCS and TCSP obtained by adding different means for communication were studied. It was hence shown that when adding the parallel combinator of Milner’s CCS to BPP, BPP_{M}, we keep the decidability of both location and pomset equivalence whereas when adding the parallel combinator of Hoare’s TCSP both become undecidable. Also, for a non-trivial subclass of processes between BPP and TCSP, BPP_{S}, consisting of finite sets of communicating BPP processes, it was shown that location equivalence is decidable whereas pomset equivalence is not.

The work presented in this paper continues by investigating the role of the renaming and hiding combinators with respect to decidability, and by investigating the weak versions of pomset and location equivalence.

First, we look at BPP extended with renaming and hiding combinators, and show by a reduction to the same problem for BPP that both pomset and location equivalence remain decidable. Second, we turn to BPP_{S}. It follows from the undecidability for BPP_{S} that pomset equivalence for BPP_{S} extended with renaming or hiding combinators is undecidable. Here, we show that adding any of the combinators makes a significant difference for location equivalence which becomes undecidable. The result is shown by a reduction to the halting problem for two-counter machines base on weak encodings of counter machines. Our results are summarised in the table below where yes indicates decidability and no undecidability. The results of the first column are all direct consequences of Hirshfeld’s result on BPP [10]. The second and third show our results:

Language equiv. Pomset equiv. Location equiv.
BPP  no  yes  yes
BPP + renaming and/or hiding  no  yes  yes
BPP_{S}  no  no  yes
BPP_{S} + renaming and/or hiding  no  no  no

Furthermore, we turn to the weak case. We consider three extensions: BPP with τ prefixing BPP^{τ}, BPP with CCS-communication BPP_{M}, and BPP with both τ prefixing and CCS-communication BPP_{M}^{τ}. We show that for BPP^{τ}, both weak pomset and weak location equivalence are decidable. This points out a current contrast to the results in the interleaving world where there are currently no positive results on deciding weak equivalences for the full class of BPP^{τ}. In fact, one major open problem is the decidability of weak bisimulation on BPP^{τ}, see [9, 13]. In [17], a number of non-interleaving weak bisimulations were shown to be decidable for the class of so–called h-convergent BPP_{M}^{τ} processes which are processes that cannot evolve into a divergent process. Also, positive results are known for the asymmetric problem of deciding weak equivalences between a finite-state system and an infinite-state system such as BPP^{τ}, see [18, 14]. As a natural next step, we look at the class of processes BPP_{M}^{τ} obtained by semantically extending BPP^{τ} with the communication rule of Milner [19]. We show that for BPP_{M}^{τ}, (strong) location equivalence remains decidable whereas weak location equivalence becomes undecidable. The positive result is shown by a reduction to the same problem for BPP^{τ} and the negative result is shown by a reduction to the halting problem for two-counter machines. For the problem of deciding pomset equivalence on BPP_{M}^{τ}, we give and effective characterisation for the strong case in terms of a containment problem between finite tree automata and a family of finite tree automata. Our results are summarised in the table below where yes indicates decidability, no indicates undecidability, and ? means that the question is still open. The results of the first column are all direct consequences of Hirshfeld’s result on BPP [10]. The second and third show our results:

Weak

Language equiv. Pomset equiv. Location equiv.
BPP  no  yes  yes
BPP^{τ}  no  yes  yes
BPP_{M}  no  ?  no
BPP_{M}^{τ}  no  ?  no
CCS  no  no  no

The rest of the paper is organised as follows. In Section 2, we define fairly standard TCSP and CCS-style languages, and along the lines of [26] we augment the standard transitional semantics so that not only actions but also information of their locality is observed. Moreover, we define the subclasses studied in the following sections. Language, pomset and location equivalence as presented in [26] are defined in Section 3. Section 4 is devoted to the study of the renaming and hiding combinator. Weak versions of language, pomset and location equivalence are defined in Section 5. In Section 6, 7 and 8, we investigate BPP^{τ}, BPP_{M}, and BPP_{M}^{τ}, respectively. We conclude with discussions on some loose ends and suggestions for future work.

2 TCSP/CCS-style languages

We start by defining the abstract syntax and semantics of TCSP [12, 21] and CCS [19] – style a languages. The definitions are fairly standard. As usual, we fix a countably infinite set of actions Λ = \{α, β, … \}. Then, \overline{Λ} = \{ᾱ, β̄, … \} is the set of complement actions such that ¯ is a bijection between Λ and \overline{Λ}, mapping ¯ ᾱ to α. Let Act = Λ ∪ \overline{Λ} and let Act_{τ} = Act ∪ {τ} be the set of actions, where τ is a distinguished action not in Act. τ is known as the invisible action. Any other action is visible. Also, fix a countably infinite set of variables Var = {X, Y, Z, … }. A renaming f is an endofunction on Act_{τ} such that τ is preserved and reflected, that is, f^{−1}({τ}) = {τ}.

The set of process expressions of TCSP is defined by the abstract syntax

E ::= 0 | X | σ.E | E + E | E ∥_{A} E | E[f] | E\\L

where X is in Var, σ in Act_{τ}, A and L are subsets of Act and f is a renaming. All constructs are standard. 0 denotes inaction, X a process variable, σ. prefixing, + non-deterministic choice, ∥_{A} TCSP parallel composition of processes executing independently with forced synchronisation on actions in the synchronisation set, A, [f] renaming of actions according to the renaming f, \\L hiding of the actions in L. For convenience, we shall write ∥ for ∥_{∅}.

The set of CCS process expressions is defined by the abstract syntax

E ::= 0 | X | σ.E | E + E | E ∥ E | E\L | E[f]

where X is in Var, σ in Act_{τ}, L a subset of Λ and f is renaming. 0, X, σ., +, and [f] are as for TCSP. ∥ is CCS parallel composition of processes executing independently with the possibility of pairwise CCS-synchronisation and \L is CCS-restriction. Note that we do not put the usual requirement of preservation of complement [19] on the renaming (relabelling) function because our results go through with or without.

A process family is a family of recursive equations Δ = {X_{i} =^{def} E_{i} | i = 1, 2 …, n}, where X_{i} ∈ Var are distinct variables and E_{i} are process expressions containing at most variables in Var(Δ) = {X_{1}, …, X_{n}}. A process E is a process expression of with a process family Δ such that all variables occurring in E, Var(E), are contained in Var(Δ). We shall often assume the family of a process to be defined implicitly. Dually, a process family denotes the process defined by its leading variable X_{1}, if not mentioned explicitly. Let Act(E) denote the set of actions occurring in process E and its associated family. A process expression E is guarded if each variable in E occurs within some subexpression σ.F of E. Following [19], we also consider the more restricted kind of guarding where furthermore the “guard” cannot be a τ action, that is, σ ≠ τ, in this case we say that the process is Milner guarded. A process family is (Milner) guarded if for each equation the right side is (Milner) guarded. A process E with family Δ is (Milner) guarded if E and Δ are (Milner) guarded. Throughout the paper we shall only consider guarded processes and process families.

We enrich the standard operational semantics of TCSP [27] and CCS [19] by adding information to the transitions allowing us to observe an action together with its location. More precisely, the location of an action in a process P is the path from the root to the action in the concrete syntax tree represented by a string over {0, 1} labelling left and right branches of ∥_{A}-nodes with 0 and 1, respectively, and all other branches with the empty string ϵ.

Let L = P({0, 1}^{∗}), i.e. finite subsets of strings over {0, 1}^{∗}, and let l range over elements of L. We interpret prefixing a symbol to L as prefixing elementwise, i.e. 0l = {0s | s ∈ l}. With this convention, any process determines a (Act_{τ} × L)-labelled transition system with states the set of process expressions reachable from the leading variable and transitions given by the transitions rules of Table 1, 2, 3, and 4 for TCSP, and Table 1, 5, 6, and 3 for CCS. The set of computations of a process, E, is as usual defined as sequences of transitions, decorated by action and locality information:

c : E = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

We let loc(c) denote the set of locations occurring in c, i.e. loc(c) = ⋃_{1≤i≤n} l_{i}.

σ.E σ_{⟶} ; \{ϵ\} E (prefix)  \frac{E σ_{⟶} ; l E′}{X σ_{⟶} ; l E′}, (X =^{def} E) ∈ Δ (unfold)
\frac{E σ_{⟶} ; l E′}{E + F σ_{⟶} ; l E′} (sum_{l})  \frac{F σ_{⟶} ; l F′}{E + F σ_{⟶} ; l F′}  (sum_{r})
\frac{E σ_{⟶} ; l E′}{E∥_{A}F σ_{⟶} ; 0l E′∥_{A}F}, σ ∉ A (par_{l})  \frac{F σ_{⟶} ; l F′}{E∥_{A}F σ_{⟶} ; 1l E∥_{A}F′},σ ∉ A (par_{r})

Table 1: Transition rules for TCSP/CCS.

\frac{E σ_{⟶} ; l_{0} E′  F σ_{⟶} ; l_{1} F′}{E∥_{A}F σ_{⟶} ; 0l_{0}∪1l_{1} E′∥_{A}F′}, σ ∈ A (com)

Table 2: Transition rule for TCSP communication.

Example 1 Consider the process

p_{1} = a.b.c.0 ∥_{{b}} b.0.

The following is an example of an associated computation (representing the unique maximal run)

p_{1} \underrightarrow{a} ; \{0\} b.c.0 ∥_{\{b\}} b.0 \underrightarrow{b} ; \{0,1\} c.0 ∥_{\{b\}} 0 \underrightarrow{c} ; \{0\} 0 ∥_{\{b\}} 0.

Consider alternatively the process

p_{2} = a.b.0 ∥_{{b}} b.c.0

with computation

p_{2} \underrightarrow{a} ; \{0\} b.0 ∥_{\{b\}} b.c.0 \underrightarrow{b} ; \{0,1\} 0 ∥_{\{b\}} c.0 \underrightarrow{c} ; \{1\} 0 ∥_{\{b\}} 0.

■

\frac{E σ_{⟶} ; l F}{E[f] f(σ)_{⟶} ; l F [f]}, (ren)

Table 3: Transition rule for TCSP/CCS renaming.

\frac{E σ_{⟶} ; l F}{E\\L σ_{⟶} ; l F \\L}, σ ∉ L (hid_{1})  \frac{E σ_{⟶} ; l F}{E\\L τ_{⟶} ; l F \\L}, σ ∈ L (hid_{2})

Table 4: Transition rules for TCSP hiding.

\frac{E σ_{⟶} ; l_{0} E′  F σ̄_{⟶} ; l_{1} F′}{E ∥ F τ_{⟶} ; 0l_{0}∪1l_{1} E′ ∥ F′} (τ − com)

Table 5: Transition rule for CCS communication.

\frac{E σ_{⟶} ; l F}{E\L σ_{⟶} ; l F \L}, σ, σ̄ ∉ L (res)

Table 6: Transition rule for CCS restriction.

2.1 BPP, BPP^{τ}, BPP_{M}, and BPP_{M}^{τ}

We shall investigate a number of syntactic as well as semantic subsets of TCSP and CCS. The calculus known as Basic Parallel Processes [7] BPP is a syntactic subset of CCS and TCSP which can be seen as the largest common subset of these (except for the renaming combinator). The abstract syntax of BPP expressions is

E ::= 0 | X | σ.E | E + E | E ∥ E

where σ ∈ Act (note that τ prefixing is not allowed), and the semantics is given by the rules in Table 1, in particular there is no rule for communication.

BPP^{τ}, is the subset of CCS obtained by adding τ prefixing, that is, syntactically the prefixing combinator σ. is extended to all σ ∈ Act_{τ} the semantics is the same as for BPP

BPP_{M}, is the subset of CCS obtained by adding the transition rule τ-com of Table 5 to BPP and hence introducing CCS-synchronisation. Since there is no restriction operator in BPP_{M} communication cannot be forced. Whenever a communication occurs in a computation, also the computation with the communicating actions occurring separately is possible. Conversely, if there is a computation in which two complementing actions occur independently then the same computation except from the two actions now communicating exists.

BPP_{M}^{τ}, is the subset of CCS obtained by adding both τ prefixing and the transition rule τ-com of Table 5 to BPP.

In the following, we shall also consider the subsets of TCSP and CCS obtained by adding the renaming and the hiding combinator to the syntax, and the rules of Table 3 and 4 to the semantics of BPP, BPP^{τ}, BPP_{M}and BPP_{M}^{τ}, we called these classes BPP, BPP^{τ}, BPP_{M}and BPP_{M}^{τ} with renaming and hiding, respectively.

We shall make convenient use of the following structural congruence.

Definition 2 Let ≡ be the least congruence on BPP_{M}^{τ} expressions with respect to all operators such that the following laws hold.

Abelian monoid laws for +:

E + F ≡ F + E
E + (F + G) ≡ (E + F) + G
E + 0 ≡ E

Abelian monoid laws for ∥:

E ∥ F ≡ F ∥ E
E ∥ (F ∥ G) ≡ (E ∥ F) ∥ G
E ∥ 0 ≡ E

Idempotence law for +:

E + E ≡ E

Linear-time laws:

(E + F) ∥ G ≡ (E ∥ G) + (F ∥ G)
σ.(E + F) ≡ σ.E + σ.F
■

As parallel composition is commutative and associative, it is convenient to represent a parallel composition X_{0} ∥ … ∥ X_{k} by the multiset {|X_{0}, …, X_{k}|}. Inaction 0 is represented by the empty multiset. For a set Var, we denote by Var^{⊗} the set of all finite multisets over Var.

Definition 3 A BPP_{M}^{τ} family Δ = {X_{i} =^{def} E_{i} | i = 1, 2 …, n} is in (quasi) normal form if and only if each expression E_{i} is of the form

E_{i} ≡ ∑_{j=1}^{n_{i}} σ_{ij}α_{ij}

where σ_{ij} ∈ Act_{τ} and α_{ij} ∈ Var(Δ)^{⊗}. ■

For a BPP_{M}^{τ} family Δ = {X_{i} =^{def} E_{i} | i = 1, 2 …, n} in normal form the branching bound is the maximal cardinality of the multisets appearing in the sums, that is, max{|α_{ij}| | i ∈ [n], j ∈ [n_{i}]}. We sometimes write σα ∈ E_{i} to denote that there is a j ∈ [n_{i}] such that σ = σ_{ij} and α = α_{ij}.

2.2 BPP_{S}

A natural restriction when dealing with non-interleaving behaviours is to allow only parallel composition in a fixed static setup, see e.g. [2, 1]. This of course leads to finite-state systems. We generalise the idea to possibly infinite-state systems. Let BPP_{S} be the syntactic subset of TCSP obtained by allowing only synchronisation, i.e. the ∥_{A} operator with A ≠ ∅, at the top level and restricting the synchronisation sets to be the set of all actions possible in either of the components.

A BPP_{S} process can hence be seen as a fixed set of BPP processes synchronising on every action. Formally, a BPP_{S} expression is given by the abstract syntax

E ::= X_{1} ∥_{Σ} … ∥_{Σ} X_{l},

where Σ ⊇ Act. A BPP_{S} family is a process family Δ = {X =^{def} X_{1} ∥_{Σ} … ∥_{Σ} X_{l}} ∪ Δ′ with leading variable X such that the leading variable X does not occur on any right-side, the variables X_{1}, …, X_{l} are contained in Var(Δ′), the synchronisation set Σ is a superset of the actions Act(Δ′) in Δ′, and Δ′ is a BPP family in normal form. A BPP_{S} process E is a BPP_{S} expression with a process family Δ′ such that {X_{0} =^{def} E} ∪ Δ′ is a BPP_{S} family with leading variable X_{0}. We call l the arity of Δ.

BPP_{S} with renaming is all TCSP processes of the form Δ = {X =^{def} (X_{1} ∥_{Σ} … ∥_{Σ} X_{l})[f]}∪Δ′ such that {X =^{def} X_{1} ∥_{Σ} … ∥_{Σ} X_{l}}∪Δ′ is a BPP_{S} process and f is a renaming.

BPP_{S} with hiding is all TCSP processes of the form Δ = {X =^{def} (X_{1} ∥_{Σ} … ∥_{Σ} X_{l})\\L}∪ Δ′ such that {X =^{def} X_{1} ∥_{Σ} … ∥_{Σ} X_{l}} ∪ Δ′ is a BPP_{S} process.

3 Language, pomset, and location equivalence

Let ⊑ be the prefix ordering on {0, 1}^{∗}, extended to sets, i.e. for l, l′ ∈ L

l ⊑ l′ ⟺ ∃s ∈ l, s′ ∈ l′. s ⊑ s′.

As usual, we use [n] to denote the set {1, 2, …, n}. For a given computation

c : E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n},

we define the location dependency ordering over [n] as follows:

i ≤_{c} j ⟺ l_{i}⊑l_{j} ∧ i ≤ j.

As usual, let ≤_{c}^{∗} denote the transitive closure of ≤_{c}, let <_{c}^{∗} denote the strict version of ≤_{c}^{∗}, that is, i <_{c}^{∗} j iff i ≤_{c}^{∗} j and i ≠ j, and let ⋖_{c}^{∗} denote the covering relation i <_{c}^{∗} j, that is, i⋖_{c}^{∗}j iff i <_{c}^{∗} j and ∀k ∈ [n]. k <_{c}^{∗} j ⇒ k ≤_{c}^{∗} i.

Definition 4 Behavioural Equivalences. Processes E and E′ are said to be language equivalent, E ∼_{lan} E′, iff for every computation of E

c : E \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

there exists a computation of E′

c′ : E′ \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

and vice versa. E and E′ are said to be pomset equivalent, E ∼_{pom} E′, iff the above condition for language equivalence is satisfied, and c′ is further required to satisfy i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j. E and E′ are said to be location equivalent, E ∼_{loc} E′, iff the above condition for language equivalence is satisfied, and c′ is further required to satisfy that there exists a relation R ⊆ loc(c) × loc(c′) satisfying that for each 1 ≤ i ≤ n, R restricts to a bijection on l_{i} × l′_{i}, and for each i ≤ j, s_{0}(R ∩ l_{i} × l′_{i})s′_{0} and s_{1}(R ∩ l_{j} × l′_{j})s′_{1}, s_{0} ⊑ s_{1} ⟺ s′_{0} ⊑ s′_{1}.

In each case, we say that c′ is a match of c with respect to ∼_{lan}, ∼_{pom} and ∼_{loc}, respectively. □

Notice that the condition in the definition of pomset equivalence requires identical global causal relationship between the events of c and c′, whereas the condition in the definition of location equivalence requires the same set of local causal relationships (up to renaming of locations). Also, notice that our notion of pomset equivalence is consistent with formal definitions from e.g. [15], and that location equivalence is a natural application of the concepts from [4] to the setting of language equivalence.

Example 5 It follows immediate from the definition that for our process language considered so far, location equivalence is included in pomset equivalence, which in turn is included in language equivalence. The standard example of processes a.0 ∥ b.0 and a.b.0 + b.a.0 shows that the inclusion in language equivalence is strict. The different intuitions behind our two non-interleaving equivalences may be illustrated by the two processes from Example 1. Formally, the reader may verify that p_{1} and p_{2} are pomset equivalent but not location equivalent. Intuitively, both processes may perform actions a,b, and c in sequence, i.e. same set pomsets, but in p_{1} one location is responsible for both a and c, whereas in p_{2} two different locations are responsible for these actions. □

4 Renaming and hiding

In this section, we investigate the role of renaming and hiding with respect to the decidability. First we show that for BPP, the decidability of both pomset and location equivalence is preserved when adding renaming and hiding. Second, we show that adding renaming or hiding to BPP_{S} makes location equivalence undecidable.

Theorem 6 For BPP with renaming and hiding, ∼_{loc} = ∼_{pom} ⊂∼_{lan}.

Proof: That ∼_{pom} and ∼_{lan} coincide follows from the proof of Theorem 7 below. The inclusion into ∼_{lan} follows from the definition and the strictness follows from Example 5. □

Theorem 7 For BPP with renaming and hiding, ∼_{loc} and ∼_{pom} are decidable.

Proof: It is not hard to check the following equalities:

(σ.E)[f] ∼_{pom} f(σ).E[f],

(σ.E)\\L ∼_{pom} σ.(E\\L), if σ ∉ L,

(σ.E)\\L ∼_{pom} τ.(E\\L), if σ ∈ L,
E[f]\\L ∼_{pom} (E\\f^{−1}(L))[f], and

(E\\L)[f] ∼_{pom} (E[f′])\\\{μ_{E}^{new}\}, f′(σ) = \{ \begin{matrix}μ_{E}^{new} & if σ ∈ L, \\ f(σ) & otherwise \end{matrix}

where μ_{E}^{new} is a new action not present in the process E.

Because no communication is possible, it is straightforward using such equalities to check that renaming and hiding combinators can be eliminated by pushing them inwards while renaming and hiding actions in the prefixing combinator explicitly such that the obtained process is an ordinary BPP process which is pomset and location equivalent to the orignal process. □

Theorem 8 For BPP_{S} with renaming and hiding, ∼_{loc} ⊂ ∼_{pom} ⊂∼_{lan}.

Proof: The inclusions follow by the definition, and the strictness from simple modifications of Example 1 and 5. □

We spend the rest of the section showing that location equivalence is undecidable for BPP_{S} with renaming or hiding. The proof is by a reduction from the halting problem for two-counter machines. A (Minsky) two-counter machine [20] consists of a finite program

l_{1} : com_{1}
⋮
l_{n−1} : com_{n−1}
l_{n} : HALT

and unbounded counters c_{0} and c_{1}. The l_{i}s and the com_{i}s are called labels and commands, respectively. Commands are of one of two different types: commands of type I are of the form c_{j} := c_{j} +1;goto l (unconditional increment) and commands of type II are of the form if c_{j} = 0 then goto l else c_{j} := c_{j} − 1;goto l′ (conditional decrement), where j is either 0 or 1, and l and l′ are labels.

A two-counter machine M executes on a given input (contents of the counters (c_{0}, c_{1})) (m_{0}, m_{1}) by first executing com_{1}, then com_{2}, and so forth. Stopping if and only if the HALT command is reached. M halts on input (m_{0}, m_{1}) if it reaches label l_{n} and hence the HALT command in finitely many steps. It is well-known that the halting problem for two-counter machines is undecidable.

Theorem 9 [20] It is undecidable whether a two-counter machine M halts on input (0, 0). □

Given a two-counter machine M the idea is to encode the state of M by a BPP_{S} process of the form

X ∥_{Σ} (C_{0} ∥ d_{0}^{m_{0}} ∥ C_{1} ∥ d_{1}^{m_{1}})

where the variable X encodes the state of the finite-state program of M, m_{0} and m_{1} are the values of the counters, and C_{0} and C_{1} controls in interaction with X the incrementing, decrementing and zero-testing of the counters. We exhibit two different encodings which are both weak in the sense that they allow computations which do not correspond to any execution of the encoded machine. For convenience, we work with TCSP processes and not BPP_{S} with renaming for starters. Later, we transform the setting appropriately.

Definition 10 First weak encoding Given a two-counter machine M let Δ_{M} be the TCSP family with leading variable X_{0} given by the following definitions where k ranges over 1, …, n − 1 and j ranges over 0, 1:

X_{0} =^{def} X_{1} ∥_{A} ((GC_{0} ∥ GC_{1}) ∥_{B} S),

where A = {i_{j}, z_{j}, d_{j} | j = 0, 1} and B = {z_{j}, d_{j} | j = 0, 1}. If com_{k} is c_{j} := c_{j} + 1;goto l_{p} then

X_{k} =^{def} i_{j}.X_{p},

and if com_{k} is if c_{j} = 0 then goto l_{p} else c_{j} := c_{j} − 1; goto l_{q} then

X_{k} =^{def} z_{j}.X_{p} + d_{j}.X_{q},

X_{n} =^{def} h.0,

GC_{j} =^{def} i_{j}.(GC_{j} ∥ C_{j}) + z_{j}.GC_{j},
C_{j}  =^{def} d_{j}.0,
S  =^{def} ∑_{j} z_{j}.S + d_{j}.S.
■

Let M be a two-counter machine M and let Δ_{M} be the TCSP family given by Definition 10. It is clear from the definition that for any computation

c : X_{1} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{M} and for each i ∈ [n] there is k_{i}, j_{i}, m_{0}^{i} and m_{1}^{i} such that either

E_{i} ≡ X_{k_{i}} ∥_{A} (GC_{0} ∥ C_{0}^{m_{0}} ∥ GC_{1} ∥ C_{1}^{m_{1}}) ∥_{B} S

or

E_{i} ≡ 0 ∥_{A} (GC_{0} ∥ C_{0}^{m_{0}} ∥ GC_{1} ∥ C_{1}^{m_{1}}) ∥_{B} S

in the latter case E_{i} is called a halting state. The computation c is a halting computation if it reaches a halting state. For each i ∈ [n] and j = 0, 1, let count_{j}(E_{i}) = m_{j}. The computations of the encoding above always increment and decrement counters properly but they may take the zero branch eventhough the corresponding counter is not zero.

Definition 11 Proper transitions and computations Let

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

be a computation of Δ_{M}. For each i ∈ [n] and j = 0, 1, the ith transition of c is a proper transition if and only if the zero-branch is only chosen on a zero-counter, that is, if σ_{i} = z_{j} then count_{j}(E_{i−1}) = 0. The computation c is a proper computation if and only if for each i ∈ [n] the ith transition is a proper transition. Dually, an improper transition (computation) is a transition (computation) that is not proper. If c is an improper computation, the ith transition is the first improper transition in c and σ_{i} = z_{j}, c is said to cheat on counter j at the ith transition, and furthermore, k is said to be the witness iff the kth transition in c is the first transition to enable a d_{j} still enabled in E_{i}. ■

The following lemma shows that the encoding is correct in the sense that the execution of M can be uniquely simulated by Δ_{M}. It is however only weakly correct in the sense that there may be computations of Δ_{M} which do not correspond to executions of M.

Lemma 12 “Weak” correctness of simulation

• If M halts on input (0, 0) then Δ_{M} has a unique maximal proper computation reaching a halting state.

• If M does not halt on input (0, 0) then all proper computations of Δ_{M} are prefixes of a single infinite proper computation which never reaches a halting state

Proof: Both properties are not hard to verify: each execution step of M is matched by a unique transitions of Δ_{M}. Matching for each j = 0, 1, a test for zero, an increment and a decrement of the jth counter by z_{j}, i_{j} and d_{j}, respectively. □

Definition 13 Second weak encoding Given a two-counter machine M let Δ′_{M} be the TCSP family with leading variable Y_{0} given by the following definitions where k ranges over 1, …, n − 1 and j ranges over 0, 1:

Y_{0} =^{def} Y_{1} ∥_{A} (GD_{0} ∥ GD_{1}) ∥_{B} T,

where A = {i_{j}, z_{j}, d_{j} | j = 0, 1} and B = {z_{j}, z′_{j}, d_{j}, d′_{j} | j = 0, 1}. If com_{k} is c_{j} := c_{j}+1;goto l_{p} then

Y_{k} =^{def} i_{j}.Y_{p},

and if com_{k} is if c_{j} = 0 then goto l_{p} else c_{j} := c_{j} − 1;goto l_{q} then

Y_{k} =^{def} z_{j}.Y_{p} + d_{j}.Y_{q} + z′_{j}.Y^{H},

Y_{n} =^{def} 0

and

GD_{j} =^{def} i_{j}.(GD_{j} ∥ D_{j}) + i_{j}.(GD′_{j} ∥ D′_{j}) + z_{j}.GD_{j},
GD′_{j} =^{def} i_{j}.(GD′_{j} ∥ D_{j}) + z_{j}.GD′_{j} + z′_{j}.GD′_{j}.
D_{j}  =^{def} d_{j}.0,
D′_{j}  =^{def} d′_{j}.0,
T  =^{def} ∑_{j} z_{j}.T + d_{j}.T + z′_{j}.T^{H}
T^{H}  =^{def} ∑_{j} z_{j}.T^{H} + d_{j}.T^{H} + d′_{j}.T^{H}.

Furthermore, for each k over 1, …, n − 1 and each j over 0, 1. If com_{k} is c_{j} := c_{j} + 1;goto l_{p} then

Y_{k}^{H} =^{def} i_{j}.Y_{p}^{H}

and if com_{k} is if c_{j} = 0 then goto l_{p} else c_{j} := c_{j} − 1;goto l_{q} then

Y_{k}^{H} =^{def} z_{j}.Y_{p}^{H} + d_{j}.Y_{q}^{H} + d′_{j}.Y_{q}^{H},

and

Y_{n}^{H} =^{def} h.0.

■

Let f be the renaming function given by

f(σ) = \{ \begin{matrix}z_{j} & if σ = z′_{j} \\ d_{j} & if σ = d′_{j} \\ σ & otherwise \end{matrix}

We call a state of a computation of Δ′_{M} containing a variable labeled by superscript H an H-labeled state. The idea is that any proper computation of Δ_{M} can and can only be matched by a computation of Δ′_{M} using only states which are not H-labeled. Whereas an improper computation of Δ_{M} can and can only be matched by a computation of Δ′_{M} using only states which are not H-labeled up to the first improper transition and from then on using only states which are H-labeled.

Lemma 14 M does not halt on input (0, 0) ⟺ X_{0} ∼_{loc} Y_{0}[f]

Proof: To see the only if direction, assume that M does not halt. We show that X_{0} ≲_{loc} Y_{0}[f] and that Y_{0}[f] ≲_{loc} X_{0}. The second case is easy. Let h be the variable-relabeling homomorphism on syntactic trees of Proc induced by letting h(Y_{k}) = X_{k}, h(GD_{j}) = h(GD′_{j}) = GC_{j}, h(D_{j}) = h(D′_{j}) = C_{j} and h(T) = h(T^{H}) = S. Then, it is routine to check that for each computation

d : F_{0} \underrightarrow{f(σ_{1})} ; l_{1} F_{1} … \underrightarrow{f(σ_{n})} ; l_{n} F_{n}

of Y_{0}[f],

c : h(F_{0}) \underrightarrow{σ_{1}} ; l_{1} h(F_{1}) … \underrightarrow{σ_{n}} ; l_{n} h(F_{n})

is a computation of X_{0}.

To show the first case, it suffices by Lemma 12 to consider only every non-halting proper computation and every improper computation of X_{0}. We split the proof into two. Let

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

be a proper and non-halting computation of X_{0}, and let g be the variable-relabeling homomorphism on syntactic trees of Proc induced by letting g(X_{k}) = Y_{k}, g(GC_{j}) = GD_{j}, g(C_{j}) = D_{j} and g(S) = T. Again, it is routine to check that

d : g(F_{0}) \underrightarrow{σ_{1}} ; l_{1} g(F_{1}) … \underrightarrow{σ_{n}} ; l_{n} g(F_{n})

is a computation of Y_{0}[f]. Next, let

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

be an improper computation of X_{0}. Observe that it is straightforward to show by induction in the length of the computation that for any computation

d : F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

of Y_{0}[f] with matching transition labelling, also the counters match, that is, for each i ∈ [n] and j = 0, 1, count_{j}(E_{i}) = count_{j}(F_{i}). Now, assume that c is improper because it cheats on J at I with witness K. By the above the (proper) computation up to the Ith transition can be matched by Y [f]. Clearly, this match may be assumed to generate CD′_{J} ∥ D′_{J} by the K transition, and hence the improper Ith transition of c may be match by a z′_{J} transition. Since a z′_{J} transition leads to an H-labelled state it is easy to see that any continuation can be matched.

Conversely to see the if direction, assume that M does halt. We show that X_{0} ≴_{loc} Y_{0}[f]. By Lemma 12, X_{0} has a unique maximal proper computation reaching a halting state. We show that this computation cannot be matched by Y_{0}[f]. Assume that there were a match. It is easy to check that Y_{0}[f] can only perform h in a H-labelled state and that the only way to enter such a state is by jperforming a z′_{j} which again can only be performed after a D′_{j} has been generated. Moreover, since also a d′_{j} can only be performed in an H-labelled state, we get that D′_{j} must be present in the state performing the first z′_{j}. Now, this is a contradiction by the fact that f(z′_{j}) = z_{j} and the above observation on counters in matching computations. □

Let

U_{L} =^{def} ∑_{σ∈L} σ.U_{L}.

The follwing lemma makes it straightforward to make the reduction to BPP_{S} processes with renaming.

Lemma 15 Let L_{1} and L_{2} be the sets {h} and {i_{0}, i_{1}, h}, respectively, s an action in Act,

X′_{0} =^{def} s.X_{1} ∥_{Σ} (s.(GC_{0} ∥ GC_{1} ∥ U_{L_{1}}) ∥_{Σ} s.(S ∥ U_{L_{2}})), and

Y′_{0} =^{def} s.Y_{1} ∥_{Σ} (s.(GD_{0} ∥ GD_{1} ∥ U_{L_{1}}) ∥_{Σ} s.(T ∥ U_{L_{2}})).

Then,

X_{0} ∼_{loc} Y_{0}[f] ⟺ X′_{0} ∼_{loc} Y′_{0}[f].

Proof: Straightforward because the computations are the same except from the involvement of every component in every transition and because the new locations observed are exactly the same in both processes. □

Theorem 16 For BPP_{S} with renaming, ∼_{loc} and ∼_{pom} are undecidable.

Proof: Immediate consequence of Lemma 15 and 14. □

Lemma 17 Let L be the set of actions {d_{j}, d′_{j}, z_{j}, z′_{j} | j = 0, 1}.

M does not halt on input (0, 0) ⟺ X_{0}\\L ∼_{loc} Y_{0}\\L

Proof: The proof is a routine adaption of the Lemma 14. □

Lemma 18 Let L, L_{1} and L_{2} be the sets {d_{j}, d′_{j}, z_{j}, z′_{j} | j = 0, 1}, {h} and {i_{0}, i_{1}, h}, respectively, and let

X′_{0} =^{def} s.X_{1} ∥_{Σ} (s.(GC_{0} ∥ GC_{1} ∥ U_{L_{1}}) ∥_{Σ} s.(S ∥ U_{L_{2}})), and

Y′_{0} =^{def} s.Y_{1} ∥_{Σ} (s.(GD_{0} ∥ GD_{1} ∥ U_{L_{1}}) ∥_{Σ} s.(T ∥ U_{L_{2}})).

Then,

X_{0}\\L ∼_{loc} Y_{0}\\L ⟺ X′_{0}\\L ∼_{loc} Y′_{0}\\L

Proof: Straightforward. □

Theorem 19 For BPP_{S} with hiding, ∼_{loc} and ∼_{pom} are undecidable.

Proof: Immediate consequence of Lemma 17 and 18. □

5 Weak language, pomset, and location equivalence

All the undecidability results for the strong case extend immediately to the weak case. In the following we show that for BPP^{τ} the decidability results for pomset and location equivalence extent to the weak case.

With each computation c we associate a partial function v^{c} : ℕ ↪ ℕ yielding on i the index of the ith visible action in c if it exists and undefined otherwise, and the function ∥ c ∥ yielding the number of occurrences of visible actions in c.

Definition 20 Processes E and E′ are said to be weak language preordered, E ⪅_{lan} E′, iff for every computation of E

c : E \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

there exists a computation of E′

c′ : E′ \underrightarrow{σ′_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ′_{m}} ; l′_{m} E′_{m}

such that there ∥ c ∥ = ∥ c′ ∥, for each i ∈ [∥ c ∥], σ_{v^{c}(i)} = σ′_{v^{c′}(i)}. E and E′ are said to be weak pomset preordered, E ⪅_{pom} E′, iff c′ is further required to satisfy that for each i, j ∈ [∥ c ∥], v^{c}(i) ≤_{c}^{∗} v^{c}(j) ⟺ v^{c′}(i) ≤_{c′}^{∗} v^{c′}(j). E and E′ are said to be weak location preordered, E ⪅_{loc} E′, iff c′ is further required to satisfy that there exists a relation R ⊆ loc(c)×loc(c′) satisfying that for each 1 ≤ i ≤∥ c ∥, R restricts to a bijection on l_{i} ×l′_{i}, and for each i, j ∈ [∥ c ∥] such that i ≤ j, s_{0}(R∩l_{i} ×l′_{i})s′_{0} and s_{1}(R ∩ l_{j} × l′_{j})s′_{1}, s_{0} ⊑ s_{1} ⟺ s′_{0} ⊑ s′_{1}. In each case, we say that c′ is a match of c with respect to ≈_{lan}, ≈_{pom} and ≈_{loc}, respectively.

Moreover, E and E′ are said to be weak language equivalent, E ≈_{lan} E′, iff E ⪅_{lan} E′ and E′ ⪅_{lan} E. E and E′ are said to be weak pomset equivalent, E ≈_{pom} E′, if and only if E ⪅_{pom} E′ and E′ ⪅_{pom} E. E and E′ are said to be weak location equivalent, E ≈_{loc} E′, if and only if E ⪅_{loc} E′ and E′ ⪅_{loc} E. ■

We write E ⟹^{ϵ} E′, if E = E′, or if there exists a computation

E \underrightarrow{τ} ; l_{1} E_{1} … \underrightarrow{τ} ; l_{n} E_{n} = E′,

from E to E′ with only τ transition, E σ_{⟹} ; l E′, if there exists processes E_{1} and E_{2} such that

E ⟹^{ϵ} E_{1} \underrightarrow{σ} ; l E_{2} ⟹^{ϵ} E′,

and E ⟶^{σ}⟹^{ϵ} E′, if there exists a process E′′ such that

E ⟶^{σ} E′′ ⟹^{ϵ} E′.

Example 21 Consider the process

p_{3} = (a.b.0 ∥ b̄.c.0)\{b}

The following is an example of an associated computation (representing the unique maximal run)

c : p_{3} \underrightarrow{a} ; \{0\} (b.0 ∥ b̄.c.0)\\{b\} \underrightarrow{τ} ; \{0,1\} (0 ∥ c.0)\\{b\} \underrightarrow{c} ; \{1\} (0 ∥ 0)\\{b\}.

Consider alternatively the process

p_{4} = τ.a.τ.c.0

with computation

d : p_{4} \underrightarrow{τ} ; \{ϵ\} a.τ.c.0 \underrightarrow{a} ; \{ϵ\} τ.c.0 \underrightarrow{τ} ; \{ϵ\} c.0 \underrightarrow{c} ; \{ϵ\} 0.

The computation d is a match of c with respect to ≈_{lan} and ≈_{pom} but not with respect to ≈_{loc}. ■

6 BPP^{τ}

In the strong case, τ is just another action no different than the others. Hence, all results of decidablility on BPP transfers to BPP^{τ}.

Theorem 22 For BPP^{τ}, ≈_{loc} = ≈_{pom} ⊂≈_{lan}.

Proof: That ≈_{pom} and ≈_{lan} coincide is an easy consequence of the definition because no communication is possible. The inclusion into ≈_{lan} follows immediate from the definition and the strictness follows from Example 5. □

It is easy to see that a Milner guarded BPP^{τ} family Δ can effectively be transformed into a guarded BPP family Δ′ by systematically getting rid of τ.E subexpressions by appropriate substitutions of E in such a way that Δ ≈_{pom} Δ′ (Δ ≈_{loc} Δ′).

For the general case, this elimination procedure cannot be applied due to the possibility of τ cycles. Instead, we introduce a closure operation performing combined elimination and bounded saturation of τs as explained below.

To appriciate the difference in the underlying “τ-structure” of computations which correspond to matching computations with respect to ≈_{pom}, consider the pomsets in Figure 1, as pomsets they clearly do not match but as weak pomset they match. The pomset to the left (right) is a pomset of Δ_{1} (Δ_{2}) in Example 23 below. In fact, Δ_{1} ≈_{pom} Δ_{2} but clearly Δ_{1} ≁_{pom} Δ_{2}. Moreover, Δ_{1} and Δ_{2} can match any BPP^{τ} computation over a and b with respect to ≈_{pom}.

[figure: τ; τ; a; τ; τ; τ; b; τ; τ; τ; a; b; a; τ; a; b; a; b; b; τ; a; τ; b]

Figure 1: Distinct strong pomsets whose weak versions match.

Example 23

Δ_{1} = { X_{1} =^{def} τ.{X_{2}, X_{3}},

X_{2} =^{def} a.{X_{1}},

X_{3} =^{def} τ.{X_{1}, X_{4}},

X_{4} =^{def} b.{X_{1}}  }

Δ_{2} = { Y_{1} =^{def} τ.{Y_{1}, Y_{1}} + τ.{Y_{2}, Y_{3}},

Y_{2} =^{def} a.{Y_{1}},

Y_{3} =^{def} b.{Y_{1}}}

■

In the following, we show how to reduce the decidability of ⪅_{pom} to the decidability of ≲_{pom}. The main observation used is that whereas a BPP^{τ} family may allow computations of arbitrary large branching degrees when restricting to visible transitions, the underlying dependency ordering is a tree of a branching degree uniformly bounded over all computations of the family. Hence, if Δ and Δ′ are BPP^{τ} families then based on the branching bound B of Δ, we seek to effectively compute a family S_{B}(Δ′) such that Δ ⪅_{pom} Δ′ iff Δ ≲_{pom} S_{B}(Δ′). Intuitively, S_{B}(Δ′) will do all computations whose underlying dependency ordering is a tree with branching bounded by B and which can be match by a computation of Δ′ with respect to ≈_{pom}. The first step is to compute for each variable X a finite representation of the set of all states reachable from X by doing any number of τ actions, that is, the set

{β | X ⟹^{ϵ} β}

and for each action σ ∈ Act(Δ)∪{τ} a finite representation of the set of all states reachable from X by doing a σ action and then doing any number of τ actions, that is,

{β | X ⟶^{σ}⟹^{ϵ} β}.

For this purpose, it is convenient to assume that the families are of the following form.

Definition 24 A BPP^{τ} family Δ = {X_{i} =^{def} E_{i} | i = 1, 2 …, n} is in subset closed normal form if and only if it is in normal form and furthermore for each expression

E_{i} ≡ ∑_{j=1}^{n_{i}} σ_{ij}α_{ij}

the set Γ_{ij} = {α_{ij} | j ∈ [n_{i}]} is subset closed, that is, for every α_{1}, α_{2} ∈ Var(Δ)^{⊗} such that α_{1} ⊆ α_{2}, if α_{2} ∈ Γ_{ij} then α_{1} ∈ Γ_{ij}. ■

As shown next, we can safely restrict ourselves to families in subset closed normal form in the following.

Proposition 25 Let Δ be a BPP^{τ} family with leading variable X_{1}. Then a BPP^{τ} family in subset closed normal form Δ′ can be effectively constructed such that Δ′′ ∼_{pom} Δ′, where Δ′′ is Δ extended with a new leading variable X′_{1} = s.X_{1}, for some s ∈ Act and X′_{1} ∉ Var(Δ).

Proof: Straightforward extension of the normal form result in [26]. □

Note that for example the process (a.0 ∥ b.0) + c.0 can not be brought on normal form while preserving pomset equivalence whereas the process s.((a.0 ∥ b.0) + c.0) can. Hence, the point of the slightly technical normal form result is that prefixing the leading equation of two BPP processes by the same action respects and reflects pomset equivalence.

We base the computation of the set reachable states discussed above on a “weak” version of the standard Karp-Miller tree, see e.g. [23, 24]. For this purpose, we need a bunch of fairly standard definitions.

Definition 26 The set IN ∪{ω} of the natural numbers IN extended with a special (limit) symbol ω is denoted by IN_{ω}. As usual, the operations + and −, and the relation ≤ over IN are extended to IN_{ω} by stipulating that for all n ∈ IN, ω + ω = ω + n = n + ω = ω and n ≤ ω. The set of all n-tuples over IN (IN_{ω}) is denoted IN^{n} (IN_{ω}^{n}), elements of IN (IN_{ω}^{n}) are denoted m̄, and the components are for each i ∈ [n] denoted by m̄_{i}. For each i ∈ [n], we denote by ē_{i} the ith unit n-tuple, that is, the n-tuple with 1 in the ith entry and 0 in all other entries. For any k ∈ IN, the n-tuple with k in all entries is denoted by k̄. Operations and relations on IN_{ω} extend componentwise to IN_{ω}^{n}. The downwards closure of a subset M ⊆ IN_{ω}^{n} is the set M̂ = {m̄ ∈ IN^{n} | ∃m̄′ ∈ M. m̄ ≤ m̄′}. Let α a finite multiset over a finite set of variables {X_{1}, …, X_{n}}, then we denote by m̄(α) the n-tuple over IN defined by taking the ith entry to be the number of copies of the variable X_{i} in α. For any BPP^{τ} family Δ, let |⟩_{Δ} ⊆ IN_{ω}^{n} × (Act(Δ) ∪ {τ}) × IN_{ω}^{n} be the relation defined by for each m̄, m̄′ ∈ IN_{ω}^{n} and σ ∈ Act(Δ) ∪ {τ}, (m̄, σ, m̄′) ∈ |⟩_{Δ} iff there exists X_{i} ∈ Var(Δ) and α ∈ Var(Δ)^{⊗} such that m̄ ≥ ē_{i}, X ⟶^{σ} α and (m̄ − ē_{i}) + m̄(α) = m̄′. Often, we use the more convenient infix notionation m̄|σ⟩_{Δ}m̄′ instead of (m̄, σ, m̄′) ∈ |⟩_{Δ} and whenever Δ is clear from the context we drop the Δ subscript. ■

Keeping in mind that BPP^{τ} processes in normal form may be viewed as communicationfree nets, the weak Karp-Miller tree defined next are essentially the Karp-Miller trees on nets but restricted to τ actions.

Definition 27 Let Δ be a BPP^{τ} family in normal form. The weak Karp-Miller tree associated with the process α ⊆ Var(Δ)^{⊗} is a node labelled tree T_{α} in which each node is labelled with an n-tuple over IN_{ω}. The tree T_{α} is inductively defined as follows

(i) the root of T_{α} is labelled by m̄(α), and

whenever v is a node in T_{α} labelled m̄, then

(ii) if m̄ is also the label of an ancestor of v then v has no sons, and

(iii) otherwise, for each m̄′ ∈ IN_{ω}^{n} such that t = m̄|τ⟩m̄′, v has a son v^{t} with label m̄^{t} where

(a) if there is an ancestor v′′ of v with label m̄′′ such that m̄′′ ≤ m̄′ then for each i ∈ [n],

m̄_{i}^{t} = \{ \begin{matrix}ω, & if m̄′′_{i} < m̄′_{i}, \\ m̄′_{i}, & else \end{matrix}

(b) otherwise, m̄^{t} = m̄′.

For each σ ∈ Act(Δ) ∪ {τ}, the σ-weak Karp-Miller tree associated with the process α ⊆ Var(Δ)^{⊗} is a node labelled tree T_{α}^{σ} in which each node is labelled with an n-tuple over IN_{ω} such that (i) the root of T_{α}^{σ} is labelled by m̄(α), and

(ii) for each β ⊆ Var(Δ)^{⊗} such that α →^{σ} β_{t}, the root has the weak Karp-Miller tree T_{β_{t}} as a subtree.

The set of all labels in T_{α} and T_{α}^{σ} is denoted by E(α) and E^{σ}(α), respectively. Moreover,

E(Δ) = ⋃_{X∈Var(Δ)} E(X) ∪ ⋃_{σ∈Act(Δ)∪{τ}} E^{σ}(X)

■

Lemma 28 Let Δ be a BPP^{τ} family in normal form. Then for any process α ⊆ Var(Δ)^{⊗}, the weak Karp-Miller tree T_{α} is finite and effectively constructible, and moreover, for any σ ∈ Act(Δ) ∪ {τ}, the σ-weak Karp-Miller tree T_{α}^{σ} is finite and effectively constructible. In particular, the set E(α) of all labels in T_{α}, the set E^{σ}(α), of all labels in T_{α}^{σ}, and the set E(Δ) are finite and effectively computable.

Proof: Standard Karp-Miller trees for vector addition systems and Petri nets are wellknown to be finite and effectively constructible, see e.g. [23, 24], and it is routine to transfer the proof to (σ-) weak Karp-Miller trees. The rest follows easily. □

Lemma 29 Let Δ be a BPP^{τ} family in subset closed normal form. Then,

{ \atop E(X)} = \{m̄(β) | X ⟹^{ϵ} β\}, and

{ \atop E^{σ}(X)} = \{m̄(β) | X ⟶^{σ}⟹^{ϵ} β\}.

Proof: Straightforward from the construction of the (σ-) weak Karp-Miller tree and downwards closure ensure by the subset closedness. □

Definition 30 Let BPP^{τ} be a family Δ = {X_{i} =^{def} E_{i} | i = 1, 2 …, n} in subset closed normal form such that for each i ∈ [n], E_{i} ≡ ∑_{j=1}^{n_{i}} σ_{ij}α_{ij} and let B ∈ ℕ. Define the τ-saturation of Δ up-to branching bound B,

S_{B}(Δ) = {Y_{i} =^{def} F_{i} | i ∈ [n]} ∪ {Zσ ; m̄ =^{def} Gσ ; m̄ | m̄ ∈ E(Δ) ∧ σ ∈ Act(Δ) ∪ {τ}},

where for each m̄ ∈ E(Δ), the set Cm̄ consists of all submultisets γ for which there exist subsets m̄_{1}, …, m̄_{k} ∈ E(Δ), α ⊆ Var(Δ)^{⊗}, such that

γ = {|Zτ ; m̄_{1}, …, Zτ ; m̄_{k}|} ∪ α ∧ |γ| ≤ B ∧ ∑_{1≤i≤k} m̄_{i} + m̄(α) ≤ m̄,

and

Gσ ; m̄ ≡ ∑_{β∈Cm̄} σ.β,

and for each i ∈ [n],

F′_{i} ≡ ∑_{j=1}^{n_{i}} ∑_{m̄∈E^{σ_{ij}} (X_{i})} Zσ_{ij} ; m̄ + ∑_{m̄∈E(X_{i})} Zτ ; m̄, and  (1)

F_{i} ≡ F′_{i} + ∑_{k∈[n], k≠i, ē_{k}∈E(X_{i})} F′_{k}.  (2)

■

Lemma 31 For any BPP^{τ} family Δ in subset closed normal form and any natural number B

Δ ≈_{pom} S_{B}(Δ), in fact, Δ ≲_{pom} S_{B}(Δ) and S_{B}(Δ) ⪅_{pom} Δ.

Proof: Straightforward from Definition 30. □

Lemma 32 Let Δ_{1} and Δ_{2} be BPP^{τ} families in subset closed normal form such that B is the branching bound of Δ_{1}. Then,

Δ_{1} ⪅_{pom} Δ_{2} ⟺ Δ_{1} ≲_{pom} S_{B}(Δ_{2}).

Proof: The if direction follows from Lemma 31, because

Δ_{1} ≲_{pom} S_{B}(Δ_{2}) ≈_{pom} Δ_{2}.

To see the only if direction assume that Δ_{1} ⪅_{pom} Δ_{2}. We show a slightly stronger result. For any X ∈ Var(Δ) and any computation

c : X \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{1}, if there is a computation

d′ : Y \underrightarrow{σ′_{1}} ; l′_{1} F_{1} … \underrightarrow{σ′_{m}} ; l′_{m} F_{m}

such that d′ is a match of c with respect to ≈_{pom} then there is a computation

d′′ : Y \underrightarrow{σ_{1}} ; l′′_{1} F′′_{1} … \underrightarrow{σ′′_{n}} ; l′′_{n} F′′_{n}

such that d′′ is a match of c with respect to ∼_{pom}. We proceed by induction in the length n of the computation c, The base case (n = 1) is obvious. In the step (n > 1) there are three cases σ_{1} = σ′_{1}, σ_{1} = τ ∧ σ′_{1} ≠ τ, and σ_{1} ≠ τ ∧ σ′_{1} = τ each of which follows by induction and use of, respectively, the first and second clause in the sum (1) and the second clause in the sum (2) of Definition 30. □

Theorem 33 For BPP^{τ}, ≈_{pom} and ≈_{loc} are decidable.

Proof: The decidability of weak pomset equivalence follows from Lemma 32 and the decidability of BPP^{τ} in the strong case. The decidability of weak location equivalence follows since by Theorem 22 ≈_{pom} and ≈_{loc} coincide on BPP^{τ}. □

7 BPP_{M}

We settled the strong case in [26] by showing that pomset and location equivalence conicide and remain decidable for BPP_{M}. In the weak setting, ≈_{pom} and ≈_{loc} still conicide for BPP^{τ} but when moving to BPP_{M} this changes. In fact, they become incomparable which contrast the strong case where location equivalence is always finer then pomset. We have borrowed the following example from Kiehn [16] to show this.

Example 34 For the BPP_{M} processes

r_{1} = a.b.0 ∥ b̄.c.0 + a.c.0 and r_{2} = a.b.0 ∥ b̄.c.0,

we have that r_{1}≈_{pom}r_{2} and r_{1}≉_{loc}r_{2}, and for BPP_{M} processes

s_{1} = a.b.0 ∥ b̄.c.0 + c.b.0 ∥ b̄.a.0 + a.0∥c.0 and s_{2} = a.b.0 ∥ b̄.c.0 + c.b.0 ∥ b̄.a.0,

we have that s_{1}≈_{loc}s_{2} and s_{1}≉_{pom}s_{2}. ■

Theorem 35 For BPP_{M}, ≈_{loc} and ≈_{pom} incomparable and both strictly finer than ≈_{lan}.

Proof: Immediate from the definition and Example 34. □

7.1 Weak location equivalence

In this section, we settle the weak case by showing that ⪅_{loc} and ≈_{loc} are undecidable for BPP_{M}. Again, the proof is by a reduction from the halting problem for two-counter machines. The encodings used are considerably weaker than those used for BPP_{S} with renaming in the sense that those encodings could only cheat on zero testing whereas these can additionally cheat on decrement leaving only increment behaving properly.

Clearly, the decidability of ⪅_{loc} would imply decidability of ≈_{loc}. The following lemma observes that in fact ⪅_{loc} and ≈_{loc} are equivalent with respect to decidability.

Lemma 36 Let E and F be BPP_{M} processes.

E ⪅_{loc} F ⇔ E + F ≈_{loc} F

Proof: Immediate from the definition. □

We spend the rest of this section showing that ⪅_{loc} and hence ≈_{loc} are undecidable for BPP_{M}. The proof is by a reduction from the Halting problem for Minsky two-counter machines to the ⪅_{loc} problem using weak encodings of two-counter machines into BPP_{M} processes.

Given a two-counter machine M the idea is to encode the state of M by a BPP process of the form

X ∥ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}}

where the variable X encodes the state of the finite-state program of M and m_{0} and m_{1} are the values of the counters.

Definition 37 First weak encoding Given a two-counter machine M let Δ_{M} be the BPP_{M} family with leading variable X_{1} given by the following definitions where k ranges over 1, …, n − 1 and j ranges over 0, 1. If com_{k} is c_{j} := c_{j} + 1;goto l_{p} then

X_{k} =^{def} i_{j}.(X_{p} ∥ C_{j}),

and if com_{k} is if c_{j} = 0 then goto l_{p} else c_{j} := c_{j} − 1;goto l_{q} then

X_{k} =^{def} z_{j}.X_{p} + g_{j}.P_{kj}

and

P_{kj} =^{def} g′_{j}.X_{q},

X_{n} =^{def} h.0

and

C_{j} =^{def} d_{j}.0

■

Let M be a two-counter machine M and let Δ_{M} be the BPP_{M}^{τ} family given by Definition 37. It is clear from the definition that for any computation

c : X_{1} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{M}, for each i ∈ [n] there is k ∈ [n], j ∈ {0, 1}, and m_{0}, m_{1} ∈ IN such that either

E_{i} ≡ X_{k} ∥ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}},  E_{i} ≡ P_{kj} ∥ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}},  or E_{i} ≡ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}}

in the latter case E_{i} is called a halting state. The computation c is a halting computation if it reaches a halting state. For each i ∈ [n] and j = 0, 1, let count_{j}(E_{i}) = m_{j}. The computations of the encoding above always increment counters properly but they may take the zero branch eventhough the corresponding counter is not zero and they may decrement a non-zero counter at any point.

Definition 38 Proper transitions and computations Let

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

be a computation of Δ_{M}. For each i ∈ [n] and j = 0, 1, the ith transition of c is a proper transition if and only if

1. (The zero-branch is only chosen on a zero-counter) If σ_{i} = z_{j} then count_{j}(E_{i−1}) = 0.

2. (A decrement is performed: g_{j}d_{j}g′_{j})

(a) If σ_{i} = d_{j} then i > 1 and σ_{i−1} = g_{j}, and

(b) if σ_{i} = g′_{j} then i > 1 and σ_{i−1} = d_{j}.

The computation c is a proper computation if and only if for each i ∈ [n] the ith transition is a proper transition. ■

Lemma 39 “Weak” correctness of simulation

• If M halts on input (0, 0) then Δ_{M} has a unique maximal proper computation reaching for some m_{0}, m_{1} ∈ ℕ a halting state.

• If M does not halt on input (0, 0) then all proper computations of Δ_{M} are prefixes of a single infinite proper computation which never reaches a halting state

Proof: Both properties are not hard to verify: each execution step of M is matched by a unique sequence of one or more transitions of Δ_{M}. Matching for each j = 0, 1, a test for zero, an increment and a decrement of the jth counter by z_{j}, i_{j} and g_{j}d_{j}g′_{j}, respectively. □

The second encoding is more complicated than the first. Its task is to match any computation of Δ_{M} except for a possible proper halting computation.

Definition 40 Second weak encoding Given a two-counter machine M let Δ′_{M} be the BPP_{M} family with leading variable Y_{1} given by the following definitions where k ranges over 1, …, n − 1 and j over 0, 1. If com_{k} is c_{j} := c_{j} + 1;goto l_{p} then

Y_{k} =^{def} i_{j}.(Y_{p} ∥ D_{j})+
t_{j}.t′_{j}.Y_{k}^{H} + t_{j⊕1}.t′_{j⊕1}.Y_{k}^{H} (wrong decrement of a counter)

and if com_{k} is if c_{j} = 0 then goto l_{p} else c_{j} := c_{j} − 1;goto l_{q} then

Y_{k}  =^{def} z_{j}.Y_{p} + g_{j}.Q_{kj}+
s_{j}.z_{j}.Y_{p}^{H} + (choosing zero-branch on non-zero counter)
t_{j}.t′_{j}.Y_{k}^{H} + t_{j⊕1}.t′_{j⊕1}.Y_{k}^{H}, (wrong decrement of a counter)
Q_{kj} =^{def} t_{j}.t′_{j}.R_{kj}+
g′_{j}.Y_{q}^{H} + (leaving out decrement)
t_{j⊕1}.t′_{j⊕1}.Q_{kj}^{H}, (decrement of the wrong counter)
R_{kj} =^{def} g′_{j}.Y_{q}+
t_{j}.t′_{j}.R_{kj}^{H} + t_{j⊕1}.t′_{j⊕1}.Q_{kj}^{H}, (wrong decrement of a counter)

Y_{n} =^{def} 0

and

D_{j} =^{def} t̄_{j}.d_{j}.t̄′_{j}.0 + s̄_{j}.D_{j}.

Furthermore, If com_{k} is c_{j} := c_{j} + 1;goto l_{p} then

Y_{k}^{H} =^{def} i_{j}.(Y_{p}^{H} ∥ D_{j}) + t_{j}.t′_{j}.Y_{k}^{H} + t_{j⊕1}.t′_{j⊕1}.Y_{k}^{H}

and if com_{k} is if c_{j} = 0 then goto l_{p} else c_{j} := c_{j} − 1;goto l_{q} then

Y_{k}^{H} =^{def} z_{j}.Y_{p}^{H} + g_{j}.Q_{kj}^{H} + s_{j}.z_{j}.Y_{p}^{H} + t_{j}.t′_{j}.Y_{k}^{H} + t_{j⊕1}.t′_{j⊕1}.Y_{k}^{H},
Q_{kj}^{H} =^{def} t_{j}.t′_{j}.R_{kj}^{H} + g′_{j}.Y_{q}^{H} + t_{j⊕1}.t′_{j⊕1}.Q_{kj}^{H},
R_{kj}^{H} =^{def} g′_{j}.Y_{q}^{H} + t_{j}.t′_{j}.R_{kj}^{H} + t_{j⊕1}.t′_{j⊕1}.Q_{kj}^{H},

Y_{n}^{H} =^{def} h.0

■

We call a state of a computation of Δ′_{M} containing a variable labelled by superscript H an H-labelled state. The idea is that any proper computation of Δ_{M} can and can only be matched by a computation of Δ′_{M} using only states which are not H-labelled. Whereas an improper computation of Δ_{M} can and can only be matched by a computation of Δ′_{M} using only states which are not H-labelled up to the first improper transition and from then on using only states which are H-labelled.

Also for the second encoding, it is clear from the definition that for any computation

d : Y_{1} \underrightarrow{σ_{1}} ; l_{1} F_{1} … \underrightarrow{σ_{n}} ; l_{n} F_{n}

of Δ′_{M}, for each i ∈ [n] there is k ∈ [n], j ∈ {0, 1}, and m_{0}, m_{1} ∈ IN such that F_{i} is of the form

F_{i} ≡ Z ∥ D_{0}^{m_{0}} ∥ D_{1}^{m_{1}}, or F_{i} ≡ D_{0}^{m_{0}} ∥ D_{1}^{m_{1}}

where Z is either Y_{k}, Q_{kj}, R_{kj}, Y_{k}^{H}, Q_{kj}^{H}, or R_{kj}^{H}. For each i ∈ [n] and j = 0, 1, let count_{j}(F_{i}) = m_{j} and in the first case, let control(F_{i}) = Z. In fact, there is a close relationship between the states of the encodings. The following definition gives a way of mapping states of Δ_{M} to states of Δ′_{M} which will be useful in the next lemma. Definition 41 For each computation

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{M} for each i ∈ [n], let f_{i}^{c} be the variable-relabelling homomorphism on syntactic trees of Proc induced by letting f_{i}^{c}(C_{j}) = D_{j}, and whenever the computation from E_{0} to E_{i} is a proper computation, f_{i}^{c}(X_{k}) = Y_{k} and

f_{i}^{c}(P_{kj}) = \{ \begin{matrix}R_{kj} & if i > 0 and σ_{i} = d_{j} \\ Q_{kj} & otherwise \end{matrix}

and whenever the computation from E_{0} to E_{i} is not a proper computation, f_{i}^{c}(X_{k}^{H}) = Y_{k}^{H} and

f_{i}^{c}(P_{kj}^{H}) = \{ \begin{matrix}R_{kj}^{H} & if i > 0 and σ_{i} = d_{j} \\ Q_{kj}^{H} & otherwise \end{matrix}

■

Lemma 42 Any proper non-halting computation and any improper computation of Δ_{M} can be matched with respect to ⪅_{loc} by a computation of Δ′_{M}, i.e. for each proper and non-halting or improper (possibly halting) computation

c : X_{1} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{M} there exists a computation

d : Y_{1} \underrightarrow{σ_{1}} ; l_{1} F_{1} … \underrightarrow{σ_{n}} ; l_{n} F_{n}

of Δ′_{M} such that for each i ∈ [n], F_{i} = f_{i}^{c}(E_{i}). Moreover, the case where c proper nonhalting computation the match d is unique.

Proof: Let f_{0}^{c}(E_{0}) = f_{0}^{c}(X_{1}) = Y_{1} = F_{0}. Given a computation

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{M}, we construct a unique computation

d : Y_{1} = F_{0} \underrightarrow{σ_{1}} ; l_{1} F_{1} … \underrightarrow{σ_{n}} ; l_{n} F_{n}

of Δ′_{M} such that for each i ∈ {0, …, n}, F_{i} = f_{i}^{c}(E_{i}). We show that for each i ∈ [n − 1] and j = 0, 1,

E_{i} σ_{i+1}_{⟶} ; l_{i+1} E_{i+1} implies F_{i} σ_{i+1}_{⟹} ; l_{i+1} F_{i+1}

from which the result follows by induction in the length n of c. Let j range over 0, 1. Given i = 0, …, n − 1, we divide the proof into three cases:

1. The computation E_{0} to E_{i} a proper non-halting computation and the (i + 1)th transition is proper.

(a) for σ_{i+1} = i_{j}, z_{j}, g_{j}, g′_{j},

E_{i} σ_{i+1}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} σ_{i+1}_{⟶} ; l_{i+1} F_{i+1}, and

(b) for σ_{i+1} = d_{j},

E_{i} d_{j}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} τ_{⟶} ; l′_{i+1} F′_{i} d_{j}_{⟶} ; l_{i+1} F′′_{i} τ_{⟶} ; l′_{i+1} F_{i+1}

where for some m_{0}, m_{1} ∈ IN (m_{j} > 0),

\begin{aligned}F′_{i} & ≡ & t′_{j}.R_{k_{i}j} ∥ d_{j}.t̄′_{j}.0 ∥ D_{0}^{m_{j}−1} ∥ D_{1}^{m_{j⊕1}}, \\ F′′_{i} & ≡ & t′_{j}.R_{k_{i}j} ∥ t̄′_{j}.0 ∥ D_{0}^{m_{j}−1} ∥ D_{1}^{m_{j⊕1}}, \end{aligned}

and l′_{i+1} = l_{i+1}∪{l} where l is the location of control(F_{i}) in F_{i} (and in particular,

of R_{k_{i}j} in F′_{i} and F′′_{i}.)

2. The computation E_{0} to E_{i} a proper non-halting computation and the (i + 1)th transition is improper.

(a) (leaving out decrement)

E_{i} g′_{j}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} g′_{j}_{⟶} ; l_{i+1} F_{i+1}

(b) (choosing zero-branch on non-zero counter)

E_{i} z_{j}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} τ_{⟶} ; l′_{i+1} F′_{i} z_{j}_{⟶} ; l_{i+1} F_{i+1},

where for some label p and m_{0}, m_{1} ∈ IN,

F′_{i} ≡ z_{j}.Y_{p}^{H} ∥ D_{0}^{m_{0}} ∥ D_{1}^{m_{1}},

and l′_{i+1} = l_{i+1} ∪ {l} where l is the location of some C_{j} in E_{i} (and in particular, of some D_{j} in F_{i}.)

(c) (decrement of the wrong counter or wrong decrement of a counter) For some label k and m_{0}, m_{1} ∈ IN, let E_{i} ≡ P_{kj} ∥ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}}, then note that necessarily i > 0 and that the state of F_{i} dependent on whether or not σ_{i} = d_{j} in any case though

E_{i} d_{j⊕1}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} τ_{⟶} ; l′_{i+1} F′_{i} d_{j⊕1}_{⟶} ; l_{i+1} F′′_{i} τ_{⟶} ; l′_{i+1} F_{i+1}

where for some label k and m_{0}, m_{1} ∈ IN,

\begin{aligned}F′_{i} & ≡ & t′_{j⊕1}.Q_{kj⊕1} ∥ d_{j⊕1}.t̄′_{j⊕1}.0 ∥ D_{0}^{m_{j⊕1}−1} ∥ D_{1}^{m_{j}}, \\ F′′_{i} & ≡ & t′_{j⊕1}.Q_{kj⊕1} ∥ t̄′_{j⊕1}.0 ∥ D_{0}^{m_{j⊕1}−1} ∥ D_{1}^{m_{j}}, \end{aligned}

and l′_{i+1} = l_{i+1} ∪ {l} where l is the location of P_{kj} in E_{i} (and in particular, of Q_{kj} in F_{i}.)

(d) (wrong decrement of a counter)

For some label k and m_{0}, m_{1} ∈ IN, let E_{i} ≡ P_{kj} ∥ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}}, and let σ_{i} = d_{j} (note that necessarily i > 0)

E_{i} d_{j}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} τ_{⟶} ; l′_{i+1} F′_{i} d_{j}_{⟶} ; l_{i+1} F′′_{i} τ_{⟶} ; l′_{i+1} F_{i+1}

where for some label k and m_{0}, m_{1} ∈ IN,

\begin{aligned}F′_{i} & ≡ & t′_{j⊕1}.R_{kj⊕1} ∥ d_{j⊕1}.t̄′_{j⊕1}.0 ∥ D_{0}^{m_{j⊕1}−1} ∥ D_{1}^{m_{j}}, \\ F′′_{i} & ≡ & t′_{j⊕1}.R_{kj⊕1} ∥ t̄′_{j⊕1}.0 ∥ D_{0}^{m_{j⊕1}−1} ∥ D_{1}^{m_{j}}, \end{aligned}

and l′_{i+1} = l_{i+1} ∪ {l} where l is the location of P_{kj} in E_{i} (and in particular, of R_{kj} in F_{i}.)

(e) (wrong decrement of a counter) For some label k and m_{0}, m_{1} ∈ IN, E_{i} ≡ X_{k} ∥ C_{0}^{m_{0}} ∥ C_{1}^{m_{1}},

E_{i} d_{j}_{⟶} ; l_{i+1} E_{i+1} is matched by F_{i} τ_{⟶} ; l′_{i+1} F′_{i} d_{j}_{⟶} ; l_{i+1} F′′_{i} τ_{⟶} ; l′_{i+1} F_{i+1}

where

\begin{aligned}F′_{i} & ≡ & t′_{j}.Y_{k}^{H} ∥ d_{j}.t̄′_{j}.0 ∥ D_{0}^{m_{j}−1} ∥ D_{1}^{m_{j}}, \\ F′′_{i} & ≡ & t′_{j}.Y_{k}^{H} ∥ t̄′_{j}.0 ∥ D_{0}^{m_{j}−1} ∥ D_{1}^{m_{j}}, \end{aligned}

and l′_{i+1} = l_{i+1} ∪ {l} where l is the location of X_{k} in E_{i} (and in particular, of Y_{k} in F_{i}.)

3. The computation from E_{0} to E_{i} an improper computation. In this case, it easy to see that once in an H-labelled state the matching is straightforward.

□

Lemma 43 Δ_{M} ⪅_{loc} Δ′_{M} if and only if M does not halt

Proof: Assume that M does not halt (0, 0). Then by Lemma 39, Δ_{M} has no proper halting computation. Hence, Δ_{M} ⪅_{loc} Δ′_{M} by Lemma 42.

Conversely, assume that M does halt on input (0, 0). Then by Lemma 39, there is a unique proper halting computation of Δ_{M}

c : X_{1} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n} \underrightarrow{h} ; l_{n+1} E_{n+1}.

The by Lemma 42, unique matching computation of

c′ : X_{1} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ′_{M} is

d : Y_{1} \underrightarrow{σ_{1}} ; l_{1} F_{1} … \underrightarrow{σ_{n}} ; l_{n} F_{n}.

Since c is proper the final state of d is f_{n}(E_{n}) = F_{n} ≡ Y_{m} ∥ D_{0}^{m_{0}} ∥ D_{1}^{m_{1}} which does not enable h. Hence by the uniqueness of the match, we conclude that

Δ_{M} ⪅̸_{loc} Δ′_{M}.
□

Theorem 44 For BPP_{M}, ⪅_{loc} and ≈_{loc} are undecidable.

Proof: Immediate consequence of Lemma 43, Theorem 9 and Lemma 36. □

The result is in fact slightly stronger since the first encoding is only a BPP process.

7.2 Weak pomset equivalence

Next, we turn to weak pomset equivalence for BPP_{M}. We leave the decidability of unsettled. Instead, we give two characterisations which might be helpful in settling the question.

Definition 45 Processes E and E′ are said to be weak tree-pomset preordered, E ⪅_{pom}^{tree} E′, iff for every computation of E

c : E \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

without communication there exists a computation of E′

c′ : E′ \underrightarrow{σ′_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ′_{m}} ; l′_{m} E′_{m}

(possibly with communication) such that ∥ c ∥ = ∥ c′ ∥, for each i ∈ [∥ c ∥], σ_{v^{c}(i)} = σ′_{v^{c′}(i)} and furthermore for each i, j ∈ [∥ c ∥], v^{c}(i) ≤_{c}^{∗} v^{c}(j) ⟺ v^{c′}(i) ≤_{c′}^{∗} v^{c′}(j). ■

Proposition 46 Let E and F be BPP_{M} processes.

E ⪅_{pom} F if and only if E + F ≈_{pom} F.

Proof: Straightforward. □

Proposition 47 Let E and F be BPP_{M} processes.

E ⪅_{pom} F if and only if E ⪅_{pom}^{tree} F.

Proof: The only if direction is obvious. To see the other direction, observe that a computation with communication can be split into one without communication - a tree - which can be matched by assumption, and clearly the match composes to a match for the original computation with communication. Following this argument it is easy to do an induction proof in the number of communications occuring in a computation.

Assume that E ⪅_{pom}^{tree} F. We show by induction in the number of communications that for every computation

c : E = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of E there exists a computation

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

of F such that d is a match of c with respect to ≈_{pom}.

In the base case, no communications occur in c and hence the existence of d follows from the assumption.

In the induction step, assume that σ_{k} = τ (1 ≤ k ≤ n). By Lemma 59,

c′ : E = E_{0} \underrightarrow{σ′_{1}} ; l_{1} E_{1} … \underrightarrow{σ′_{k−1}} ; l_{k−1} E_{k−1} \underrightarrow{μ} ; u_{1} E′_{k} \underrightarrow{μ̄} ; u_{2} E_{k} \underrightarrow{σ′_{k+1}} ; l_{k+1} E_{k+1} … \underrightarrow{σ′_{m}} ; l_{m} E_{m}

is a computation of E such that u_{1} ⋢ u_{2} and μ ≠ τ. Then by induction, there exists a computation

d′ : F = F_{0} \underrightarrow{σ′_{1}} ; l′_{1} F_{1} … \underrightarrow{σ′_{k−1}} ; l′_{k−1} F_{k−1} \underrightarrow{μ} ; v_{1} F′_{k} \underrightarrow{μ̄} ; v_{2} F_{k} \underrightarrow{σ′_{k+1}} ; l′_{k+1} F_{k+1} … \underrightarrow{σ′_{m}} ; l′_{m} F_{m}

such that ∥ c′ ∥ = ∥ d′ ∥ and σ_{v^{c′}(i)} = σ′_{v^{d′}(i)} for i ∈ [∥ c′ ∥], and c′ furthermore satisfies that v^{c′}(i) ≤_{c′}^{∗} v^{c′}(j) ⟺ v^{d′}(i) ≤_{d′}^{∗} v^{d′}(j). Since u_{1} ⋢ u_{2} and

u_{1} ⋢ u_{2} ⟹ k ≰_{c′}^{∗} k + 1 ⟹ k ≰_{d′}^{∗} k + 1 ⟹ v_{1} ⋢ v_{2},

it is not hard using Lemma 60 to verify that

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

is a computation of F with l′_{m} = v_{1} ∪ v_{2} and such that d is a match of c with respect to ≈_{pom}.

By induction and a symmetric argument, we conclude that E ⪅_{pom} F. □

Let Δ_{1} and Δ_{2} be BPP_{M} processes, we can summarise the results of Proposition 46 and 47 as follows. The following problems are equivalent with respect to decidability:

(i) Δ_{1} ≈_{pom} Δ_{2},

(ii) Δ_{1} ⪅_{pom} Δ_{2}, and

(iii) Δ_{1} ⪅_{pom}^{tree} Δ_{2}.

8 BPP_{M}^{τ}

In this section, we are able to complete the picture for location equivalence.

The following example shows that with τ prefixing the characterization no longer holds for pomset equivalence.

Example 48 Let

s_{1} = a.b.0 ∥ b̄.c.0 + a.τ.c.0 and s_{2} = a.b.0 ∥ b̄.c.0.

Then, s_{1} and s_{2} are pomset equivalent when communication is allowed, that is, as BPP_{M}^{τ} processes, and not when it is disallowed, that is, as BPP^{τ} processes. Moreover as BPP_{M}^{τ} processes, s_{1} ∼_{pom} s_{2} but s_{1} ≁_{loc} s_{2}. ■

Theorem 49 For BPP_{M}^{τ}, ∼_{loc}⊂∼_{pom}⊂∼_{lan}.

Proof: The inclusions follow by definition and the properness from Example 48 and 5. □

8.1 Location equivalence

For location equivalence, the decidability proof of BPP_{M} straightforwardly extends to the case with τ prefixing, since τ-actions stemming from prefixing and those stemming from communications cannot be confused.

Lemma 50 The BPP_{M}^{τ} processes E and F are location equivalent if and only if the BPP^{τ} processes E and F are location equivalent.

Proof: For the only if direction, assume that E and F are location equivalent as BPP_{M}^{τ} processes. Let

c : E = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

be a BPP^{τ} computation of E, since any BPP^{τ} computation is also a BPP_{M}^{τ} computation there exists a BPP^{τ} computation

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

of F such that there exists a relation R ⊆ loc(c) × loc(d) satisfying that for each 1 ≤ i ≤ n, R restricts to a bijection on l_{i} × l′_{i}, and for each i ≤ j, s_{0}(R ∩ l_{i} × l′_{i})s′_{0} and s_{1}(R ∩ l_{j} × l′_{j})s′_{1}, s_{0} ⊑ s_{1} ⟺ s′_{0} ⊑ s′_{1}

Since R restricts to a bijection on l_{i} × l′_{i}, l_{i} and l′_{i} have the same cardinality. But, c is a BPP^{τ} computation and thus each l_{i} is a singleton and thus there cannot be communications in d. Therefore, d is a BPP^{τ} computation which matches c with respect to ∼_{loc}.

For the if direction, assume that E ∼_{loc} F when E and F are considered as BPP^{τ} processes. We show by induction in the number of communications that for every computation

c : E = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of E there exists a computation

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

of F such that there exists a relation R ⊆ loc(c) × loc(d) satisfying that for each 1 ≤ i ≤ n, R restricts to a bijection on l_{i} × l′_{i}, and for each i ≤ j, s_{0}(R ∩ l_{i} × l′_{i})s′_{0} and s_{1}(R ∩ l_{j} × l′_{j})s′_{1}, s_{0} ⊑ s_{1} ⟺ s′_{0} ⊑ s′_{1}.

In the base case, no communications occur in c and hence the existence of d follows from the assumption.

In the induction step, assume that σ_{m} = τ (m ∈ [n]) such that σ_{n} stems from a communication By Lemma 59,

c′ : E = E_{0} \underrightarrow{σ_{1}} ; l_{1}^{1} E_{1} … \underrightarrow{σ_{m−1}} ; l_{m−1}^{1} E_{m−1} \underrightarrow{μ} ; l_{m}^{1} E′_{m} \underrightarrow{μ̄} ; l_{m+1}^{1} E_{m} \underrightarrow{σ_{m+1}} ; l_{m+2}^{1} E_{m+1} … \underrightarrow{σ_{n}} ; l_{n+1}^{1} E_{n}

is a computation of E such that u_{1} ⋢ u_{2}, μ ≠ τ and for each i ∈ [n + 1],

l_{i}^{1} = \{ \begin{matrix}l_{i} & if i < m \\ \{u_{1}\} & if i = m \\ \{u_{2}\} & if i = m + 1 \\ l_{i−1} & if i > m + 1. \end{matrix}

Then by induction, there exists a computation

d′ : F = F_{0} \underrightarrow{σ_{1}} ; l_{1}^{2} F_{1} … \underrightarrow{σ_{m−1}} ; l_{m−1}^{2} F_{m−1} \underrightarrow{μ} ; l_{m}^{2} F′_{m} \underrightarrow{μ̄} ; l_{m+1} F_{m} \underrightarrow{σ_{m+1}} ; l_{m+2}^{2} F_{m+1} … \underrightarrow{σ_{n}} ; l_{n+1}^{2} F_{n}

of F such that there exists a relation R ⊆ loc(c′)×loc(d′) satisfying that for each i ∈ [n+1], R restricts to a bijection on l_{i}^{1} ×l_{i}^{2}, and for each i ≤ j, s_{0}(R∩l_{i}^{1} ×l_{i}^{2})s′_{0} and s_{1}(R∩l_{j}^{1} ×l_{j}^{2})s′_{1}, s_{0} ⊑ s_{1} ⟺ s′_{0} ⊑ s′_{1}.

By a cardinality argument, there exist v_{1} and v_{2} such that l_{m}^{2} = {v_{1}} and l_{m+1}^{2} = {v_{2}}. Since u_{1} ⋢ u_{2}, we hence get that v_{1} ⋢ v_{2}. By Lemma 60, it follows that

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

is a computation of F, where for each i ∈ [n],

l′_{i} = \{ \begin{matrix}l_{i}^{2} & if i < m \\ \{v_{1}, v_{2}\} & if i = m \\ l_{i+1}^{2} & if i ≥ m + 1 \end{matrix}

Moreover, loc(c) = loc(c′), loc(d) = loc(d′) and for each i ∈ [n], R restricts to a bijection on l_{i} × l′_{i}, and for each i ≤ j, s_{0}(R ∩ l_{i} × l′_{i})s′_{0} and s_{1}(R ∩ l_{j} × l′_{j})s′_{1}, s_{0} ⊑ s_{1} ⟺ s′_{0} ⊑ s′_{1}.

By induction and a symmetric argument, we conclude that E ∼_{loc} F. □

Theorem 51 For BPP_{M}^{τ}, ∼_{loc} is decidable whereas ≈_{loc} is undecidable.

Proof: In the strong case, the results follows from Lemma 50 and the decidability of location equivalence on BPP [26]. The weak case is a straightforward consequence of Lemma 44. □

8.2 Pomset equivalence

The positive decidability results in [26] rely on reductions to problems about automata on trees. In this section, we follow the same strategy in investigate the decidability of pomset equivalence of BPP_{M}^{τ} and give a characterisation in terms a containment problem between finite tree automata and a family of finite tree automata. The characterisation does not settle the question of decidability but we hope that the rephrasing might be a step towards establishing decidability.

8.2.1 Finite Tree Automata

In [26], we showed how to effectively construct a finite tree automaton A_{Δ} from a BPP family Δ in normal form. Building on this result, we exhibit a similar construction for BPP_{M}^{τ} families. The construction is however more complex and involves tree languages which are not recognisable.

Let Σ = Σ_{0} ∪ … ∪ Σ_{n} be a ranked finite alphabet. The set of all trees over Σ, T_{Σ} is the free term algebra over Σ, that is, T_{Σ}, is the least set such that Σ_{0} ⊆ T_{Σ} and such that if a ∈ Σ_{k} and for i = 1, …, k, t_{i}∈ T_{Σ}, then a[t_{1}, …, t_{k}]∈ T_{Σ}. For convenience, we use a and a[] interchangeably to denote members of Σ_{0}.

Definition 52 A non-deterministic top-down finite tree automaton, NTA, is a four-tuple A = (Σ, Q, S, δ), where Σ is a ranked finite alphabet, Q a finite set of states, S ⊆ Q is a set of initial states, and δ is a ranked family of labelled transition relations associating with each k ≥ 0, a relation δ_{k} ⊆ Q×Σ_{k}×Q^{k} such that δ_{k} is non-empty for only finitely many k. ■

Definition 53 Let A = (Σ, Q, S, δ) be a NTA and let t ∈ T_{Σ}. A configuration of A, is a multiset of pairs from Q × T_{Σ}. Denote by conf_{A} the set of all configurations of A. For σ ∈ Σ, let →^{σ}⊆ conf_{A}× conf_{A} be the labelled transition relation between configurations defined by

{|(q, t)|} ∪ c →^{σ} {|(q_{1}, t_{1}), …, (q_{k}, t_{k})|} ∪ c,

if and only if σ ∈ Σ_{k}, t = σ[t_{1}, …, t_{k}], (q, σ, q_{1}, …, q_{k}) ∈ δ_{k} and c ∈ conf_{A}. We write → for the union over all σ ∈ Σ of →^{σ}, and →^{∗} for the reflexive and transitive closure of →. A (successful) run of A on input t is a derivation {|(q_{0}, t)|}→^{∗}∅, where q_{0} ∈ S. The tree language, L(A), recognised by A consists of all trees t, for which there is a successful run of A on t. ■

Definition 54 Given a BPP family Δ in normal form with leading variable X_{1}, define the NTA A_{Δ} = (Act(Δ), Var(Δ), {X_{1}}, δ) such that for every (X =^{def} ∑_{i=1}^{n} σ_{i}α_{i}) ∈ Δ, every index 1 ≤ j ≤ n and for every {|Y_{1}, …, Y_{k}|} ⊆ α_{j},

(X, σ_{j}, Y_{1}, …, Y_{k}) ∈ δ_{k}.

The ranking of the alphabet Act(Δ) is induced by the definition of δ. ■

In [26], the following characterisation was shown.

Proposition 55 [26] Given BPP families Δ_{1} and Δ_{2} in normal form. Then

Δ_{1} ∼_{pom} Δ_{2} ⟺ L(A_{Δ_{1}}) = L(A_{Δ_{2}})
□

The proposition above does not hold for BPP_{M} families as shown by Example 48. Here, the first characterisation is given in terms of the obvious pomset preorder.

Definition 56 Let E and E′ be BPP_{M}^{τ} processes. E ≲_{pom} E′ iff for every computation of E

c : E \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

there exists a computation of E′

c′ : E′ \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

such that i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j. ■

Proposition 57 Let E and F be BPP_{M}^{τ} processes.

E ≲_{pom} F if and only if E + F ∼_{pom} F.

Proof: Straightforward. □

Definition 58 Let E and E′ be BPP_{M}^{τ} processes. E ≲_{pom}^{tree} E′ iff for every computation of E

c : E \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

without communication there exists a computation of E′

c′ : E′ \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

(possibly with communication) such that i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j. We say that E and E′ are pomset tree equivalent, E ∼_{pom}^{tree} E′, iff E ≲_{pom}^{tree} E′ and E′ ≲_{pom}^{tree} E. ■

It is an easy exercise to show the following lemmas.

Lemma 59 If E τ_{⟶} ; l G and τ stems from a communication then there exist an expression F ∈ Proc, an action σ ∈ Act and locations l_{1} and l_{2} such that l = l_{1} ∪ l_{2}, ¬(l_{1} ⊑ l_{2}) and

E σ_{⟶} ; l_{1} F σ̄_{⟶} ; l_{2} G. □

Lemma 60 If E σ_{⟶} ; l_{1} F σ̄_{⟶} ; l_{2} G and ¬(l_{1} ⊑ l_{2}) then E τ_{⟶} ; l_{1}∪l_{2} G . □

Proposition 61 Let E and F be BPP_{M}^{τ} processes.

E ≲_{pom} F if and only if E ≲_{pom}^{tree} F.

Proof: The only if direction is obvious. To see the other direction, observe that a computation with communication can be split into one without communication - a tree - which can be matched by assumption, and clearly the match composes to a match for the original computation with communication. Following this argument it is easy to do an induction proof in the number of communications occurring in a computation.

Assume that E ≲_{pom}^{tree} F. We show by induction in the number of communications that for every computation

c : E = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of E there exists a computation

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

of F such that i ≤_{c}^{∗} j ⟺ i ≤_{d}^{∗} j.

In the base case, no communications occur in c and hence the existence of d follows from the assumption.

In the induction step, assume that σ_{m} = τ (m ∈ [n]) and σ_{m} stems from a communication. By Lemma 59,

c′ : E = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{m−1}} ; l_{m−1} E_{m−1} \underrightarrow{μ} ; u_{1} E′_{m} \underrightarrow{μ̄} ; u_{2} E_{m} \underrightarrow{σ_{m+1}} ; l_{m+1} E_{m+1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

is a computation of E such that u_{1} ⋢ u_{2} and μ ≠ τ. Then by induction, there exists a computation

d′ : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{m−1}} ; l′_{m−1} F_{m−1} \underrightarrow{μ} ; v_{1} F′_{m} \underrightarrow{μ̄} ; v_{2} F_{m} \underrightarrow{σ_{m+1}} ; l′_{m+1} F_{m+1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

such that i ≤_{c′}^{∗} j ⟺ i ≤_{d′}^{∗} j. Since u_{1} ⋢ u_{2} and

u_{1} ⋢ u_{2} ⟹ m ≰_{c′}^{∗} m + 1 ⟹ m ≰_{d′}^{∗} m + 1 ⟹ v_{1} ⋢ v_{2},

it follows from Lemma 60, that

d : F = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

is a computation of F, where l′_{m} = v_{1} ∪ v_{2}. Moreover, it is not hard to check that i ≤_{c}^{∗} j ⟺ i ≤_{d}^{∗} j. By induction and a symmetric argument, we conclude that E ≲_{pom} F. □

By Proposition 61, it suffices to match tree-ordered pomsets. Because tree-ordered pomsets are obviously only matched by tree-ordered pomsets, we next move to explicitly compute the tree-ordered pomsets arising through communication and then to forget about communication. The idea is to approximate a BPP_{M}^{τ} family Δ by a family of BPP^{τ} families {Δ^{τK} | K ∈ IN} in such a way that any tree-ordered pomset of Δ is also a pomset of Δ^{τK} for some K ∈ IN. The construction is based on augmenting variables with a memory used to remember processes available for communication. The memory is decreased when communicating and increased by non-deterministically picking up “brothers”. The main observation is that when only tree-ordered pomsets are considered, the “brothers” are in fact the only possible candidates for communications “later on”.

Example 62 Consider the BPP_{M}^{τ} family

Δ = { X_{1} =^{def} a.{X_{1}, X_{2}} + a.{X_{2}, X_{3}},

X_{2} =^{def} c̄.∅,

X_{3} =^{def} c.{X_{4}},

X_{4} =^{def} b.{X_{3}}  }.

For each natural number K, define the BPP^{τ} family

Δ^{τK} = { X_{1}(m̄) =^{def} a.∅+
a. ∑{{X_{1}(m̄′)} | ¯0 ≤ m̄′ − m̄ ≤ ē_{2}}+
a. ∑{{X_{2}(m̄′)} | ¯0 ≤ m̄′ − m̄ ≤ ē_{1}}+
a. ∑{{X_{2}(m̄′)} | ¯0 ≤ m̄′ − m̄ ≤ ē_{3}}+
a. ∑{{X_{3}(m̄′)} | ¯0 ≤ m̄′ − m̄ ≤ ē_{2}}+
a. ∑{{X_{1}(m̄_{1}), X_{2}(m̄_{2})} | m̄_{1} + m̄_{2} ≤ m̄}+
a. ∑{{X_{2}(m̄_{1}), X_{3}(m̄_{2})} | m̄_{1} + m̄_{2} ≤ m̄},
X_{2}(m̄) =^{def} c̄.∅ + τ.∅,  if 0 ≤ m̄ − ē_{3},
X_{2}(m̄) =^{def} c̄.∅,  if not 0 ≤ m̄ − ē_{3},
X_{3}(m̄) =^{def} c.∅ + c.{X_{4}(m̄)}+
τ.∅ + τ.{X_{4}(m̄ − ē_{2})},  if 0 ≤ m̄ − ē_{2},
X_{3}(m̄) =^{def} c.∅ + c.{X_{4}(m̄)},  if not 0 ≤ m̄ − ē_{2},
X_{4}(m̄) =^{def} b.∅ + b.{X_{3}(m̄)} | ¯0 ≤ m̄ ≤ K̄}.
■

Note that the constructed families approximate Δ from below in the sense that for each K ∈ IN, Δ^{τK} ≲_{pom} Δ.

Next, we formally define the approximations but first a convenient technical definition.

Definition 63 Let Δ = {X_{i} =^{def} E_{i} | i ∈ [n]} be a BPP_{M}^{τ} family, Let m̄_{i} range over ℕ^{n} For convenience, we denote by {|X_{i_{1}}, …, X_{i_{k}}|}⟨m̄_{1}, …, m̄_{k}⟩ (i_{1} ≤ i_{2} ≤ … ≤ i_{k}) the set {|X_{i_{1}}(m̄_{1}), …, X_{i_{k}}(m̄_{k})|}. For each m̄ ∈ ℕ^{n}, and subset α of Var(Δ), let

α⟨⟨m̄⟩⟩ = ∑{β⟨m̄_{1}, …, m̄_{|β|}⟩ | β ⊆ α, ¯0 ≤ ∑_{i} m̄_{i} − m̄ ≤ m̄(α − β)}.

■

Definition 64 Let Δ = {X_{i} =^{def} E_{i} | i ∈ [n]} be a BPP_{M}^{τ} family in normal form with E_{i} ≡ ∑_{j=1}^{n_{i}} σ_{ij}α_{ij} Define for each K ∈ ℕ the K –approximations BPP^{τ} family,

Δ^{τK} = {X_{i}(m̄) =^{def} F_{i}(m̄) | i ∈ [n] ∧ ¯0 ≤ m̄ ≤ K̄},

with leading variable X_{1}(¯0) where for each i ∈ [n] and m̄ ≤ K̄,

F_{i}(m̄) ≡ ∑_{j=1}^{n_{i}} σ_{ij}α_{ij}⟨⟨m̄⟩⟩ + ∑_{j=1}^{n_{i}} ∑{τ(α_{ij} ∪ β)⟨⟨m̄ − ē_{k}⟩⟩ | ē_{k} ≤ m̄ ∧ σ̄_{ij}γ ∈ E_{k} ∧ β ⊆ γ}.

■

The next lemma captures the use of approximation families in making communication dispensable when checking for ≲_{pom}^{tree}-containment. Lemma 65 Let Δ a BPP_{M}^{τ} family in normal form with leading variable X_{1}. Then

(i) for every computation

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ such that ≤_{c}^{∗} is a tree ordering there exists a K ∈ ℕ and a computation

c′ : X_{1}(¯0) = E′_{0} \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

without communication of Δ^{τK} such that i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j.

(ii) for every K ∈ ℕ and every computation

c : X_{1}(¯0) = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ^{τK} without communication there exists a computation

c′ : X_{1} = E′_{0} \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

(possibly with communication) of Δ such that i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j.

Proof:

(i) Given a computation

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ such that ≤_{c}^{∗} is a tree ordering. We proceed by induction in the number of communications K occuring in c.

In the base case, no communications occur in c and it is easy to check that

c′ : X_{1}(¯0) = E′_{0} \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

is a computation of Δ^{τK} such that i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j, and E′_{i} = η(E_{i}) where η is the relabeling homomorphism induced by taking for each X ∈ Var(Δ), η(X) = X(¯0).

In the induction step, K > 0, assume that σ_{m} = τ (m ∈ [n]) and that σ_{m} stems from a communication. By Lemma 59, there is a computation

d : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{m−1}} ; l_{m−1} E_{m−1} \underrightarrow{μ} ; u_{1} E′_{m} \underrightarrow{μ̄} ; u_{2} E_{m} \underrightarrow{σ_{m+1}} ; l_{m+1} E_{m+1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ such that u_{1} ⋢ u_{2} and μ ≠ τ. Then by induction, since ≤_{d}^{∗} is a tree ordering, there exists a computation

d′ : X_{1}(¯0) = F_{0} \underrightarrow{σ_{1}} ; l′_{1} F_{1} … \underrightarrow{σ_{m−1}} ; l′_{m−1} F_{m−1} \underrightarrow{μ} ; v_{1} F′_{m} \underrightarrow{μ̄} ; v_{2} F_{m} \underrightarrow{σ_{m+1}} ; l′_{m+1} F_{m+1} … \underrightarrow{σ_{n}} ; l′_{n} F_{n}

of Δ^{τK} such that i ≤_{d}^{∗} j ⟺ i ≤_{d′}^{∗} j.

Let k be the greatest common predecessor of m and m + 1 with respect to ≤_{d}^{∗}. Such a k exists since Δ is in normal form and ≤_{d}^{∗} is a tree ordering.

The important observation is now that either m or m + 1 is a son (immediate successor) of k since otherwise there exist k_{1} and k_{2} such that k_{1} ≰_{d}^{∗} k_{2}, k_{2} ≰_{d}^{∗} k_{1}, k <_{d}^{∗} k_{1} <_{d}^{∗} m and k <_{d}^{∗} k_{2} <_{d}^{∗} m + 1 which contradicts the assumption that ≤_{c}^{∗} is a tree ordering.

Assume without loss of generality that m is a son of k. From this it is not hard to verify that d′ can be modified so that the kth transition picks up the appropriate son into memory sends it along the appriate path while performing the transitions as in d′, and when reaching the mth transition performs the communication between μ and μ̄ reaching F_{m} modulo ≡. Also, it is clear that the obtained computation is a match of c with respect to ∼_{pom}.

(ii) Let ι be the homomorphism on induced by letting ι(X_{i}((m_{1}, …, m_{n}))) = X_{i} ∥ X_{1}^{m_{1}} ∥ … ∥ X_{n}^{m_{n}}. Given a K ∈ ℕ and a computation

c : X_{1}(¯0) = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ^{τK} without communication it is not hard to verify that there exists a computation

c′ : X_{1} = E′_{0} \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

(possibly with communication) of Δ such that for each i ∈ [n], E′_{i} ≡ ι(E_{i}) and for each i, j ∈ [n], i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j.

□

Lemma 66 Given BPP_{M}^{τ} families Δ_{1} and Δ_{2} in normal form with leading variables X_{1} and Y_{1}, respectively. Then Δ_{1} ≲_{pom}^{tree} Δ_{2} if and only if for every computation

c : X_{1} = E_{0} \underrightarrow{σ_{1}} ; l_{1} E_{1} … \underrightarrow{σ_{n}} ; l_{n} E_{n}

of Δ_{1} without communication there exists a K ∈ ℕ and a computation

c′ : Y_{1}(¯0) = E′_{0} \underrightarrow{σ_{1}} ; l′_{1} E′_{1} … \underrightarrow{σ_{n}} ; l′_{n} E′_{n}

without communication of Δ_{2}^{τK} such that i ≤_{c}^{∗} j ⟺ i ≤_{c′}^{∗} j.

Proof: Straightforward from Lemma 65. □

Definition 67 For each BPP_{M}^{τ} family Δ define

L_{Δ}^{τ} = ⋃_{K∈ℕ}L(A_{Δ^{τK}})

■

As expected and illustrated by the following example the language accepted by a family of approximation automata is not necessarily a recognisable set of trees.

Example 68 Consider the BPP_{M}^{τ} family Δ of Example 62. The language L_{Δ}^{τ} contains for each M ∈ ℕ the tree

\underbrace{a − a − ⋯ − a}_{M} − \underbrace{τ − b − τ − ⋯ − τ − b}_{2M},

whereas for each M, N ∈ ℕ such that M < N the tree

\underbrace{a − a − ⋯ − a}_{M} − \underbrace{τ − b − τ − ⋯ − τ − b}_{2N}

is not contained in L_{Δ}^{τ}. It follows from a standard pumping argument that the tree language L_{Δ}^{τ} cannot be recognisable. ■

Lemma 69 Given BPP_{M}^{τ} families Δ_{1} and Δ_{2} in normal form. Then

Δ_{1} ≲_{pom}^{tree} Δ_{2} ⟺ L(A_{Δ_{1}}) ⊆ L_{Δ_{2}}^{τ}

Proof: Follows from Lemma 66 and the lemmas of Appendix A of [25]. □

Let Δ_{1} and Δ_{2} be BPP_{M}^{τ} processes, we can then summarise the consequences of Proposition 57 and 61, and Lemma 69 as follows. The following problems are equivalent with respect to decidability:

(i) Δ_{1} ∼_{pom} Δ_{2},

(ii) Δ_{1} ≲_{pom} Δ_{2},

(iii) Δ_{1} ≲_{pom}^{tree} Δ_{2}, and

(iv) L(A_{Δ_{1}}) ⊆ L_{Δ_{2}}^{τ}.

9 Conclusion

Continuing the systematic study initiated in [26], we have presented results illuminating the sometimes delicate bounds between the decidable and the undecidable in the setting of behavioural equivalences for infinite-state concurrent systems. In particular, we have shown that renaming and hiding may make a difference with respect to decidability and given the – to our best knowledge – first positive decidability result for a natural weak behavioural equivalence on the full class of BPP^{τ} processes.

Many other non-interleaving equivalences exist besides our chosen pomset and location equivalences, and which deserve to be explored. For instance, the augmentation closure of Pratt [22] is an obvious candidate. Also we would like to emphasise that we do not claim that our notion of location equivalence is the only natural capture of spatial distribution, other possibilities exist.

We showed that pomset and location equivalence are decidable on BPP (BPP^{τ}) with renaming and hiding. The natual next step is to look at BPP_{M} with renaming and hiding. We know that both equivalences are decidable on BPP_{M}. But, renaming seems to be considerably more intricate in the presence of communication. In particular, pushing the renaming combinator inwards does not work. For instance, consider the BPP_{M} processes

p = (a.0 ∥ b̄.0)[f] and p′ = (a.0)[f] ∥ (b̄.0)[f]

with f(a) = b and the identity elsewhere, clearly p and p′ are not even language equivalent because p′ can do a τ-action whereas p cannot. Similarly for the hiding combinator: consider the BPP_{M} processes

q = (a.b.0 ∥ ā.c.0)\\{a, ā} and q′ = (a.b.0)\\{a, ā} ∥ (ā.c.0)\\{a, ā}

clearly q and q′ are not even language equivalent because q can do a single τ-action and then a b-action followed by a c-action whereas q′ need to do two τ-actions in order to do a b-action followed by a c-transition.

The automata characterisation, we gave in Section 8.2 was phrased in terms of a family of finite tree automata. The family which we are interested in of course has much more structure, and we could equally well have phrased the characterisation in terms of finite tree automata with weak counters, that is, counters that can only be partially tested for zero. Such counter machines have been intensively studied over words in terms of Petri nets and vector addition systems but we do not know of any generalisation to trees.

References

[1] S. Abramsky. Eliminating local non-determinism: Semantics for ccs. Technical Report Report no. 290, Computer Systems Laboratory, Queen Mary College, 1981.

[2] L. Aceto. A static view of localities. Formal Aspects of Computing, 6(2):202–222, 1994.

[3] J.A. Bergstra and J.W. Klop. Process Algebra for Synchronous Communication. Information and Control, 60:109–137, 1984.

[4] G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. Observing localities. Theoretical Computer Science, 114, 31–61, 114:31–61, 1993.

[5] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, July 1984.

[6] S. Christensen. Distributed bisimilarity is decidable for a class of infinite-state systems. In W.R. Cleaveland, editor, CONCUR 92, pages 148–161. Springer-Verlag, 1992. Lecture Notes in Computer Science, Vol. 630.

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

[8] S. Christensen and H. Hüttel. Decidability issues for infinite-state processes - a survey. EATCS Bulletin, 51:156–166, 1993.

[9] J. Esparza. Petri nets, commutative context-free grammars and basic parallel processes. In Proceedings of Fundamentals of Computation Theory, (FCT’95). Springer-Verlag, Lecture notes vol. 965, 1995.

[10] Y Hirshfeld. Petri nets and the equivalence problem. In E. Börger, Y. Gurevich, and K. Meinke, editors, Computer Science Logic: 7th Workshop, CSL ’93 Selected Papers, pages 165–174. Springer-Verlag, 1994. Lecture Notes in Computer Science, Vol. 832.

[11] Y. Hirshfeld and F. Moller. Decidability results in automata and process theory. In G. Birtwistle and F. Moller, editors, Proceedings of Logics for Concurrency: Automata vs Structure. The VIII Banff Higher Order Workshop, Lecture Notes in Computer Science. Springer-Verlag, 1994. To appear.

[12] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

[13] P. Jancar. High undecidability of weak bisimilarity for Petri nets. Lecture Notes in Computer Science, 915:349–363, 1995.

[14] P. Jancar, A. Kucera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state processes. Technical report, Institut für Informatik, Technische Universitt München, 1998.

[15] L. Jategaonkar and A. Meyer. Deciding true concurrency equivalences on finite safe nets. In ICALP ’93, pages 519–531. Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 700.

[16] A. Kiehn. Comparing locality and causality based equivalences. Acta Informatica, 31:697–718, 1994.

[17] A. Kiehn and M. Hennessy. On the decidability of non-interleaving process equivalences. In B. Jonsson and J. Parrow, editors, Concur ’94: Concurrency Theory 5th International conference Proceedings. Springer-Verlag, 1994. Lecture Notes in Computer Science, Vol.836.

[18] R. Mayr. Weak bisimulation and model checking for basic parallel processes. In Proceedings of FSTTCS: Foundations of Software Technology and Theoretical Computer Science, volume 1180. Lecture Notes in Computer Science, Springer–Verlag, 1996.

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

[20] M.L. Minsky. Computation - Finite and Infinite Machines. Prentice Hall, 1967.

[21] E.R. Olderog and C.A.R. Hoare. Specification- oriented semantics for communicating processes. Acta Informatica, 23:9–66, 1986.

[22] V.R. Pratt. Modelling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33–71, 1986.

[23] W Reisig. Petri Nets - an Introduction. EATCS Monograph in Computer Science, Springer, 1985.

[24] C. Reutenauer. Mathematics of Petri Nets. Masson and Prentice-Hall, 1990.

[25] K. Sunesen and M. Nielsen. Behavioural equivalence for infinite systems – partially decidable! BRICS Report Series RS-95-55, Aarhus University, 1995.

[26] K. Sunesen and M. Nielsen. Behavioural equivalence for infinite systems — partially decidable! Lecture Notes in Computer Science, 1091:460–479, 1996.

[27] D. Taubner. Finite Representations of CCS and CSP programs by Automata and Petri Nets. Springer-Verlag, 1989. Lecture Notes in Computer Science, Vol. 369.

Recent BRICS Report Series Publications

RS-98-6 Kim Sunesen. Further Results on Partial Order Equivalences on Infinite Systems. March 1998. 48 pp.

RS-98-5 Olivier Danvy. Formatting Strings in ML. March 1998. 3 pp. This report is superseded by the later report BRICS RS-98-12.

RS-98-4 Mogens Nielsen and Thomas S. Hune. Deciding Timed Bisimulation through Open Maps. February 1998.

RS-98-3 Christian N. S. Pedersen, Rune B. Lyngsø, and Jotun Hein. Comparison of Coding DNA. January 1998. 20 pp. To appear in Combinatorial Pattern Matching: 9th Annual Symposium, CPM ’98 Proceedings, LNCS, 1998.

RS-98-2 Olivier Danvy. An Extensional Characterization of Lambda-Lifting and Lambda-Dropping. January 1998.

RS-98-1 Olivier Danvy. A Simple Solution to Type Specialization (Extended Abstract). January 1998. 7 pp.

RS-97-53 Olivier Danvy. Online Type-Directed Partial Evaluation. December 1997. 31 pp. Extended version of an article to appear in Third Fuji International Symposium on Functional and Logic Programming, FLOPS ’98 Proceedings (Kyoto, Japan, April 2– 4, 1998), pages 271–295, World Scientific, 1998.

RS-97-52 Paola Quaglia. On the Finitary Characterization of π-Congruences. December 1997. 59 pp.

RS-97-51 James McKinna and Robert Pollack. Some Lambda Calculus and Type Theory Formalized. December 1997. 43 pp.

RS-97-50 Ivan B. Damgård and Birgit Pfitzmann. Sequential Iteration of Interactive Arguments and an Efficient Zero-Knowledge Argument for NP. December 1997. 19 pp. To appear in 25th International Colloquium on Automata, Languages, and Programming, ICALP ’98 Proceedings, LNCS, 1998.

RS-97-49 Peter D. Mosses. CASL for ASF+SDF Users. December 1997. 22 pp. Appears in Sellink, Editor, 2nd International Workshop on the Theory and Practice of Algebraic Specifications, Electronic Workshops in Computing, ASF+SDF ’97 Proceedings, Springer-Verlag, 1997.