The Linear Time - Branching Time Spectrum I^{∗}

The Semantics of Concrete, Sequential Processes

R.J. van Glabbeek

Computer Science Department, Stanford University Stanford, CA 94305-9045, USA

                                     rvg@cs.stanford.edu
                               http://theory.stanford.edu/~rvg

In this paper various semantics in the linear time – branching time spectrum are presented in a uniform, model-independent way. Restricted to the class of finitely branching, concrete, sequential processes, only fifteen of them turn out to be different, and most semantics found in the literature that can be defined uniformly in terms of action relations coincide with one of these fifteen. Several testing scenarios, motivating these semantics, are presented, phrased in terms of ‘button pushing experiments’ on generative and reactive machines. Finally twelve of these semantics are applied to a simple language for finite, concrete, sequential, nondeterministic processes, and for each of them a complete axiomatization is provided.

Keywords: Concurrency, Labelled transition systems, Nondeterminism, Semantic equivalences, Linear time, Branching time, Generative and reactive systems, Modal logic, Trace semantics, Failures semantics, Failure trace, Ready trace, Simulation, Ready simulation, Bisimulation, Complete axiomatizations.

Table of contents

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1 Labelled transition systems and process graphs . . . . . . . . . . . . . . . . . . . . . 6 2 Trace semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3 Completed trace semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4 Failures semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5 Failure trace semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6 Ready trace semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 7 Readiness semantics and possible-futures semantics . . . . . . . . . . . . . . . . . . . 25 8 Simulation semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 9 Ready simulation semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 10 Reactive versus generative testing scenarios . . . . . . . . . . . . . . . . . . . . . . . 36 11 2-nested simulation semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 12 Bisimulation semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 13 Tree semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 14 Possible worlds semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 15 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 16 Deterministic and saturated processes . . . . . . . . . . . . . . . . . . . . . . . . . . 54 17 Complete axiomatizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 18 Criteria for selecting a semantics for particular applications . . . . . . . . . . . . . . 72 19 Distinguishing deadlock and successful termination . . . . . . . . . . . . . . . . . . . 77 Concluding remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80

∗This is an extension of [20]. The research reported in this paper has been initiated at CWI in Amsterdam, continued at the Technical University of Munich, and finalized at Stanford University. It has been supported by Sonderforschungsbereich 342 of the TU München and by ONR under grant number N00014-92-J-1974. Part of it was carried out in the preparation of a course Comparative Concurrency Semantics, given at the University of Amsterdam, spring 1988. A coloured version of this paper is available at http://boole.stanford.edu/pub/spectrum1.ps.gz.

Introduction

Process theory A process is the behaviour of a system. The system can be a machine, an elementary particle, a communication protocol, a network of falling dominoes, a chess player, or any other system. Process theory is the study of processes. Two main activities of process theory are modelling and verification. Modelling is the activity of representing processes, mostly by mathematical structures or by expressions in a system description language. Verification is the activity of proving statements about processes, for instance that the actual behaviour of a system is equal to its intended behaviour. Of course, this is only possible if a criterion has been defined, determining whether or not two processes are equal, i.e. two systems behave similarly. Such a criterion constitutes the semantics of a process theory. (To be precise, it constitutes the semantics of the equality concept employed in a process theory.) Which aspects of the behaviour of a system are of importance to a certain user depends on the environment in which the system will be running, and on the interests of the particular user. Therefore it is not a task of process theory to find the ‘true’ semantics of processes, but rather to determine which process semantics is suitable for which applications.

Comparative concurrency semantics This paper aims at the classification of process semantics.^{1} The set of possible process semantics can be partially ordered by the relation ‘makes strictly more identifications on processes than’, thereby becoming a complete lattice^{3}. Now the classification of some useful process semantics can be facilitated by drawing parts of this lattice and locating the positions of some interesting process semantics, found in the literature. Furthermore the ideas involved in the construction of these semantics can be unravelled and combined in new compositions, thereby creating an abundance of new process semantics. These semantics will, by their intermediate positions in the semantic lattice, shed light on the differences and similarities of the established ones. Sometimes they also turn out to be interesting in their own right. Finally the semantic lattice serves as a map on which it can be indicated which semantics satisfy certain desirable properties, and are suited for a particular class of applications.

Most semantic notions encountered in contemporary process theory can be classified along four different lines, corresponding with four different kinds of identifications. First there is the dichotomy of linear time versus branching time: to what extent should one identify processes differing only in the branching structure of their execution paths? Secondly there is the dichotomy of interleaving semantics versus partial order semantics: to what extent should one identify processes differing only in the causal dependencies between their actions (while agreeing on the possible orders of execution)? Thirdly one encounters different treatments of abstraction from internal actions in a process: to what extent should one identify processes differing only in their internal or silent actions? And fourthly there are different approaches to infinity: to what extent should one identify processes differing only in their infinite behaviour? These considerations give rise to a four dimensional representation of the proposed semantic lattice.

1This field of research is called comparative concurrency^{2}semantics, a terminology first used by Meyer in [36].

2Here concurrency is taken to be synonymous with process theory, although strictly speaking it is only the study of parallel (as opposed to sequential) processes. These are the behaviours of systems capable of performing different actions at the same time. In this paper the term concurrency is considered to include sequential process theory. This may be justified since much work on sequential processes is intended to facilitate later studies involving parallelism.

3The supremum of a set of process semantics is the semantics identifying two processes whenever they are identified by every semantics in this set.

However, at least three more dimensions can be distinguished. In this paper, stochastic and realtime aspects of processes are completely neglected. Furthermore it deals with uniform concurrency^{4} only. This means that processes are studied, performing actions^{5} a, b, c, ... which are not subject to further investigations. So it remains unspecified if these actions are in fact assignments to variables or the falling of dominoes or other actions. If also the options are considered of modelling (to a certain degree) the stochastic and real-time aspects of processes and the operational behaviour of the elementary actions, three more parameters in the classification emerge.

Process domains In order to be able to reason about processes in a mathematical way, it is common practice to represent processes as elements of a mathematical domain^{6}. Such a domain is called a process domain. The relation between the domain and the world of real processes is mostly stated informally. The semantics of a process theory can be modelled as an equivalence on a process domain, called a semantic equivalence. In the literature one finds among others:

• graph domains, in which a process is represented as a process graph, or state transition diagram,

• net domains, in which a process is represented as a (labelled) Petri net,

• event structure domains, in which a process is represented as a (labelled) event structure,

• explicit domains, where a process is represented as a mathematically coded set of its properties,

• projective limit domains, which are obtained as projective limits of series of finite term domains,

• and term domains, in which a process is represented as a term in a system description language.

Action relations Write p ⟶^{a} q if the process p can evolve into the process q, while performing the action a. The binary predicates ⟶^{a} are called action relations. The semantic equivalences which are treated in this paper will be defined entirely in terms of action relations. Hence these definitions apply to any process domain on which action relations are defined. Such a domain is called a labelled transition system. Furthermore they will be defined uniformly in terms of action relations, meaning that all actions are treated in the same way. For reasons of convenience, even the usual distinction between internal and external actions is dropped in this paper.

Finitely branching, concrete, sequential processes Being a first step, this paper limits itself to a very simple class of processes. First of all only sequential processes are investigated: processes capable of performing at most one action at a time. Furthermore, instead of dropping the usual distinction between internal and external actions, one can equivalently maintain to study concrete processes: processes in which no internal actions occur. For this simple class of processes the announced semantic lattice collapses in two out of four dimensions and covers only the infinitary linear time – branching time spectrum.

Moreover, the main interest is in finitely branching processes: processes having in each state only finitely many possible ways to proceed. The material pertaining to infinitely branching processes— coloured brown in the electronic version of this paper—can easily be omitted in first reading.

4The term uniform concurrency is employed by De Bakker et al [8].

5Strictly speaking processes do not perform actions, but systems do. However, for reasons of convenience, this paper sometimes uses the word process, when actually referring to a system of which the process is the behaviour.

6I use the word domain in the sense of universal algebra; it can be any class of mathematical objects—typically the first component of an algebra; the other component being a collection of operators defined on this domain. Without further adjectives I do not refer to the more restrictive domains employed in domain theory.

Literature In the literature on uniform concurrency 12 semantics can be found, which are uniformly definable in terms of action relations and different on the domain of finitely branching, sequential processes (see Figure 1). The coarsest one (i.e. the semantics making the most identifi-

trace semantics completed trace semantics failures semantics readiness semantics failure trace semantics ready trace semantics possible worlds semantics ready simulation semantics 2-nested simulation semantics bisimulation semantics simulation semantics  possible-futures semantics (tree semantics)

Figure 1: The linear time – branching time spectrum

cations) is trace semantics, as presented in Hoare [30]. In trace semantics only partial traces are employed. The finest one (making less identifications than any of the others) is bisimulation semantics, as presented in Milner [39]. Bisimulation semantics is the standard semantics for the system description language CCS (Milner [37]). The notion of bisimulation was introduced in Park [41]. Bisimulation equivalence is a refinement of observational equivalence, as introduced by Hennessy & Milner in [27]. On the domain of finitely branching, concrete, sequential processes, both equivalences coincide. Also the semantics of De Bakker & Zucker, presented in [9], coincides with bisimulation semantics on this domain. Then there are ten semantics in between. First of all a variant of trace semantics can be obtained by using complete traces besides partial ones. In this paper it is called completed trace semantics. Failures semantics is introduced in Brookes, Hoare & Roscoe [13], and used in the construction of a model for the system description language CSP (Hoare [29, 31]). It is finer than completed trace semantics. The semantics based on testing equivalences, as developed in De Nicola & Hennessy [17], coincides with failures semantics on the domain of finitely branching, concrete, sequential processes, as do the semantics of Kennaway [34] and Darondeau [15]. This has been established in De Nicola [16]. In Olderog & Hoare [40] readiness semantics is presented, which is slightly finer than failures semantics. Between readiness and bisimulation semantics one finds ready trace semantics, as introduced independently in Pnueli [43] (there called barbed semantics), Baeten, Bergstra & Klop [6] and Pomello [44] (under the name exhibited behaviour semantics). The natural completion of the square, suggested by failures, readiness and ready trace semantics yields failure trace semantics. For finitely branching processes this is the same as refusal semantics, introduced in Phillips [42]. Simulation semantics, based on the classical notion of simulation (see e.g. Park [41]), is independent of the last five semantics. Ready simulation semantics was introduced in Bloom, Istrail & Meyer [12] under the name GSOS trace congruence. It is finer than ready trace as well as simulation semantics. In Larsen & Skou [35] a more operational characterization of this equivalence was given under the name \frac{2}{3}-bisimulation equivalence. The (denotational) notion of possible worlds semantics of Veglioni & De Nicola [49] fits between ready trace and ready simulation semantics. Finally 2-nested simulation semantics, introduced in Groote & Vaandrager [25], is located between ready simulation and bisimulation semantics, and possible-futures semantics, as proposed in Rounds & Brookes [46], can be positioned between 2-nested simulation and readiness semantics.

Tree semantics, employed in Winskel [50], is even finer than bisimulation semantics. However, a proper treatment requires more than mere action relations.

About the contents The first section of this paper introduces labelled transition systems and process graphs. A labelled transition system is any process domain that is equipped with action relations. The domain of process graphs or state transition diagrams is one of the most popular labelled transition systems. In Sections 2–14 all semantic equivalences mentioned above are defined on arbitrary labelled transition systems. In particular these definitions apply to the domain of process graphs. Most of the equivalences can be motivated by the observable behaviour of processes, according to some testing scenario. (Two processes are equivalent if they allow the same set of possible observations, possibly in response to certain experiments.) I will try to capture these motivations in terms of button pushing experiments (cf. Milner [37], pp. 10-12). Furthermore the semantics will be partially ordered by the relation ‘makes at least as many identifications as’. This yields the linear time – branching time spectrum. Counterexamples are provided, showing that on the graph domain this ordering cannot be further expanded. However, for deterministic processes the spectrum collapses, as was first observed by Park [41]. Section 16 describes various other classes of processes on which parts of the spectrum collapse. In Section 17, the semantics are applied to a simple language for finite, concrete, sequential, nondeterministic processes, and for twelve of them a complete axiomatization is provided. Section 18 applies a few criteria indicating which semantics are suitable for which applications. Finally, in Section 19 the work of this paper is extended to labelled transition systems that distinguish between deadlock and successful termination.

With each of the semantic equivalences treated in this paper (except for tree semantics) a preorder is associated that may serve as an implementation relation between processes. The results obtained for the equivalences are extended to the associated preorders as well.

Acknowledgment My thanks to Tony Hoare for suggesting that the axioms of Table 2 could be simplified along the lines of Table 5.

1 Labelled transition systems and process graphs

1.1 Labelled transition systems

In this paper processes will be investigated that are capable of performing actions from a given set Act. By an action any activity is understood that is considered as a conceptual entity on a chosen level of abstraction. Actions may be instantaneous or durational and are not required to terminate, but in a finite time only finitely many actions can be carried out. Any activity of an investigated process should be part of some action a ∈ Act performed by the process. Different activities that are indistinguishable on the chosen level of abstraction are interpreted as occurrences of the same action a ∈ Act.

A process is sequential if it can perform at most one action at the same time. In this paper only sequential processes will be considered. A class of sequential processes can often be conveniently represented as a labelled transition system. This is a domain IP on which infix written binary predicates ⟶^{a} are defined for each action a ∈ Act. The elements of IP represent processes, and p ⟶^{a} q means that p can start performing the action a and after completion of this action reach a state where q is its remaining behaviour. In a labelled transition system it may happen that p ⟶^{a} q and p ⟶^{b} r for different actions a and b or different processes q and r. This phenomenon is called branching. It need not be specified how the choice between the alternatives is made, or whether a probability distribution can be attached to it.

Certain actions may be synchronizations of a process with its environment, or the receipt of a signal sent by the environment. Naturally, these actions can only occur if the environment cooperates. In the labelled transition system representation of processes all these potential actions are included, so p ⟶^{a} q merely means that there is an environment in which the action a can occur.

Notation: For any alphabet Σ, let Σ^{∗} be the set of finite sequences and Σ^{∞} the set of infinite sequences over Σ. Σ^{ω} := Σ^{∗} ∪ Σ^{∞}. Write ε for the empty sequence, σρ for the concatenation of σ ∈ Σ^{∗} and ρ ∈ Σ^{ω}, and a for the sequence consisting of the single symbol a ∈ Σ.

Definition 1.1 A labelled transition system is a pair (IP, →) with IP a class and → ⊆ IP×Act×IP, such that for p ∈ IP and a ∈ Act the class {q ∈ IP | (p, a, q) ∈ →} is a set.

Most of this paper should be read in the context of a given labelled transition system (IP, →), ranged over by p, q, r, .... Write p ⟶^{a} q for (p, a, q) ∈ →. The binary predicates ⟶^{a} are called action relations.

Definition 1.2 (Remark that the following concepts are defined in terms of action relations only)

• The generalized action relations ⟶^{σ} for σ ∈ Act^{∗} are defined recursively by:

1. p ⟶^{ε} p, for any process p.

2. (p, a, q) ∈ → with a ∈ Act implies p ⟶^{a} q with a ∈ Act^{∗}.

3. p ⟶^{σ} q ⟶^{ρ} r implies p ⟶^{σρ} r.

In words: the generalized action relations ⟶^{σ} are the reflexive and transitive closure of the ordinary action relations ⟶^{a}. p ⟶^{σ} q means that p can evolve into q, while performing the sequence σ of actions. Remark that the overloading of the notion p ⟶^{a} q is quite harmless.

• A process q ∈ IP is reachable from p ∈ IP if p ⟶^{σ} q for some σ ∈ Act^{∗}.

• The set of initial actions of a process p is defined by: I(p) = {a ∈ Act | ∃q : p ⟶^{a} q}.

• A process p ∈ IP is finite if the set {(σ, q) ∈ (Act^{∗} × IP) | p ⟶^{σ} q} is finite.

• p is image finite if for each σ ∈ Act^{∗} the set {q ∈ IP | p ⟶^{σ} q} is finite.

• p is deterministic if p ⟶^{σ} q ∧ p ⟶^{σ} r ⇒ q = r.

• p is well-founded if there is no infinite sequence p ⟶^{a_{1}} p_{1} ⟶^{a_{2}} p_{2} ⟶^{a_{3}} · · ·.

• p is finitely branching if for each q reachable from p, the set {(a, r)∈Act × IP | q ⟶^{a} r} is finite.

Note that a process p ∈ IP is image finite iff for each q ∈ IP reachable from p and each a ∈ Act, the set {r ∈ IP | q ⟶^{a} r} is finite. Hence finitely branching processes are image finite. Moreover, by König’s lemma a process is finite iff it is well-founded and finitely branching.

1.2 Process graphs

Definition 1.3 A process graph over an alphabet Act is a rooted, directed graph whose edges are labelled by elements of Act. Formally, a process graph g is a triple (nodes(g), root(g), edges(g)), where

• nodes(g) is a set, of which the elements are called the nodes or states of g,

• root(g) ∈ nodes(g) is a special node: the root or initial state of g,

• and edges(g) ⊆ nodes(g) × Act × nodes(g) is a set of triples (s, a, t) with s, t ∈ nodes(g) and a ∈ Act: the edges or transitions of g.

If e = (s, a, t) ∈ edges(g), one says that e goes from s to t. A (finite) path π in a process graph is an alternating sequence of nodes and edges, starting and ending with a node, such that each edge goes from the node before it to the node after it. If π = s_{0}(s_{0}, a_{1}, s_{1})s_{1}(s_{1}, a_{2}, s_{2}) ⋯ (s_{n−1}, a_{n}, s_{n})s_{n}, also denoted as π : s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s_{n}, one says that π goes from s_{0} to s_{n}; it starts in s_{0} and ends in end(π) = s_{n}. Let paths(g) be the set of paths in g starting from the root. If s and t are nodes in a process graph then t can be reached from s if there is a path going from s to t. A process graph is said to be connected if all its nodes can be reached from the root; it is a phrase-tree if each node can be reached from the root by exactly one path. Let ^{|}G be the domain of connected process graphs over a given alphabet Act.

Definition 1.4 Let g, h ∈ ^{|}G. A graph isomorphism between g and h is a bijective function f : nodes(g) → nodes(h) satisfying

• f(root(g)) = root(g) and

• (s, a, t) ∈ edges(g) ⇔ (f(s), a, f(t)) ∈ edges(h).

Graphs g and h are isomorphic, notation g ≅ h, if there exists a graph isomorphism between them.

In this case g and h differ only in the identity of their nodes. Remark that graph isomorphism is an equivalence relation on ^{|}G.

Connected process graphs can be pictured by using open dots (∘) to denote nodes, and labelled arrows to denote edges, as can be seen further on. There is no need to mark the root of such a process graph if it can be recognized as the unique node without incoming edges, as is the case in all my examples. These pictures determine process graphs only up to graph isomorphism, but usually this suffices since it is virtually never needed to distinguish between isomorphic graphs.

Definition 1.5 For g ∈ ^{|}G and s ∈ nodes(g), let g_{s} be the process graph defined by

• nodes(g_{s}) = {t ∈ nodes(g) | there is a path going from s to t},

• root(g_{s}) = s ∈ nodes(g_{s}),

• and (t, a, u) ∈ edges(g_{s}) iff t, u ∈ nodes(g_{s}) and (t, a, u) ∈ edges(g).

Of course g_{s} ∈ ^{|}G. Note that g_{root(g)} = g. Now on ^{|}G action relations ⟶^{a} for a ∈ Act are defined by g ⟶^{a} h iff (root(g), a, s) ∈ edges(g) and h = g_{s}. This makes ^{|}G into a labelled transition system.

1.3 Embedding labelled transition systems in ^{|}G

Let (IP, →) be an arbitrary labelled transition system and let p ∈ IP. The canonical graph G(p) of p is defined as follows:

• nodes(G(p)) = {q ∈ IP | ∃σ ∈ Act^{∗} : p ⟶^{σ} q},

• root(G(p)) = p ∈ nodes(G(p)),

• and (q, a, r) ∈ edges(G(p)) iff q, r ∈ nodes(G(p)) and q ⟶^{a} r.

Of course G(p) ∈ ^{|}G. This means G is a function from IP to ^{|}G.

Proposition 1.1 G : IP → ^{|}G is injective and satisfies, for a ∈ Act: G(p) ⟶^{a} G(q) ⇔ p ⟶^{a} q. Moreover, G(p) ⟶^{a} h only if h has the form G(q) for some q ∈ IP (with p ⟶^{a} q). Proof: Trivial. □

Proposition 1.1 says that G is an embedding of IP in ^{|}G. It implies that any labelled transition system over Act can be represented as a subclass G(IP) = {G(p) ∈ ^{|}G | p ∈ IP} of ^{|}G.

Since ^{|}G is also a labelled transition system, G can be applied to ^{|}G itself. The following proposition says that the function G : ^{|}G → ^{|}G leaves its arguments intact up to graph isomorphism.

Proposition 1.2 For g ∈ ^{|}G, G(g) ≅ g. Proof: Remark that nodes(G(g)) = {g_{s} | s ∈ nodes(g)}. Now the function f : nodes(G(g)) → nodes(g) defined by f(g_{s}) = s is a graph isomorphism. □

1.4 Equivalences relations and preorders on labelled transition systems

This paper studies semantics on labelled transition systems. Each of the semantics examined here (except for tree semantics) is defined or characterized in terms of a function O that associates with every process p ∈ IP a set O(p). In most cases the elements of O(p) can be regarded as the possible observations one could make while interacting with the process p in the context of a particular testing scenario. The set O(p) then constitutes the observable behaviour of p. For every such O, the equivalence relation =_{O} ∈ IP×IP is given by p =_{O} q ⇔ O(p) = O(q), and the preorder ⊑_{O} ∈ IP×IP by p ⊑_{O} q ⇔ O(p) ⊆ O(q). Obviously p =_{O} q ⇔ p ⊑_{O} q ∧ q ⊑_{O} p. The semantic equivalence =_{O} partitions IP into equivalence classes of processes that are indistinguishable by observation (using observations of type O). The preorder ⊑_{O} moreover provides a partial order between these equivalence classes; one that could be taken to constitute an “implementation” relation. The associated semantics, also called O, is the criterion that identifies two processes whenever they are O-equivalent. Two semantics are considered the same if the associated equivalence relations are the same.

As the definitions of O are given entirely in terms of action relations, they apply to any labelled transition system IP. Moreover, the definitions of O(p) involve only action relations between processes reachable from p. Thus Proposition 1.1 implies that O(G(p)) = O(p). This in turn yields

Corollary 1.1 p ⊑_{O} q iff G(p) ⊑_{O} G(q) and p =_{O} q iff G(p) =_{O} G(q). □

Write O ⪯IP N if semantics O makes at least as much identifications as semantics N. This is the case if the equivalence corresponding with O is equal to or coarser than the one corresponding with N, i.e. if p =_{N} q ⇒ p =_{O} q for all p, q ∈ IP. Let ⪯ abbreviate ⪯_{|}G. The following is then immediate by Corollary 1.1.

Corollary 1.2 O ⪯ N iff O ⪯IP N for each labelled transition system IP. On the other hand, O ⪯̸ N iff O ⪯̸IP N for some labelled transition system IP. □

Write O ⪯IP^{∗} N if p ⊑_{N} q ⇒ p ⊑_{O} q for all p, q ∈ IP, and let ⪯^{∗} abbreviate ⪯^{|}G^{∗}. By definition O ⪯^{∗} N ⇒ O ⪯ N for all semantics O and N. The reverse does not hold by definition, but it will be shown to hold for all semantics discussed in this paper (cf. Section 15).

1.5 Initial nondeterminism

In a process graph it need not be determined in which state one ends after performing a nonempty sequence of actions. This phenomenon is called nondeterminism. However, process graphs as defined above are not capable of modelling initial nondeterminism, as there is only one initial state. This can be rectified by considering process graphs with multiple roots, in which roots(g) may be any nonempty subset of nodes(g)—let ^{|}G^{mr} be the class of such connected process graphs. A process graph with multiple roots can also be regarded as a nonempty set of process graphs with single roots. More generally, initial nondeterminism can be modelled in any labelled transition system IP by regarding the nonempty subsets of IP (rather than merely its elements) to be processes. The elements of a process P ⊆ IP then represent the possible initial states of P.

Now any notion of observability O on IP extends to processes with initial nondeterminism by defining O(P) = ⋃_{p∈P} O(p) for P ⊆ IP. Thus also the equivalences =_{O} and preorders ⊑_{O} are defined on such processes. Write O ⪯IP^{′} N if P =_{N} Q ⇒ P =_{O} Q for all nonempty P, Q ⊆ IP, and let ⪯′ abbreviate ⪯^{|}G^{′}. Clearly, one has O ⪯′ N ⇒ O ⪯ N for all semantics O and N.

Let g be a process graph over Act with multiple roots. Let i be an action (initialize) which is not in Act. Define ρ(g) as the process graph over Act∪{i} obtained from g by adding a new state ∗, which will be the root of ρ(g), and adding a transition (∗, i, r) for every r ∈ roots(g). Now for every semantics O to be discussed in this paper it will be the case that g ⊑_{O} h ⇔ ρ(g) ⊑_{O} ρ(h), as the reader may easily verify for each such O. From this it follows that we have in fact O ⪯′ N ⇔ O ⪯ N for all semantics O and N treated in this paper. This justifies focusing henceforth on process graphs with single roots and processes as mere elements of labelled transition systems.

2 Trace semantics

Definition 2 σ ∈ Act^{∗} is a trace of a process p if there is a process q such that p ⟶^{σ} q. Let T (p) denote the set of traces of p. Two processes p and q are trace equivalent, notation p =_{T} q, if T (p) = T (q). In trace semantics (T) two processes are identified iff they are trace equivalent.

Testing scenario Trace semantics is based on the idea that two processes are to be identified if they allow the same set of observations, where an observation simply consists of a sequence of actions performed by the process in succession.

Modal characterization

Definition 2.1 The set L_{T} of trace formulas over Act is defined recursively by:

• ⊤ ∈ L_{T}.

• If φ ∈ L_{T} and a ∈ Act then aφ ∈ L_{T}.

The satisfaction relation ⊧ ⊆ IP × L_{T} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

Note that a trace formula satisfied by a process p represents nothing more or less than a trace of p. Hence one has

Proposition 2.1 p =_{T} q ⇔ ∀φ ∈ L_{T} (p ⊧ φ ⇔ q ⊧ φ). □

Process graph characterization Let g ∈ ^{|}G^{mr} and π : s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s_{n} ∈ paths(g). Then T (π) := a_{1}a_{2} ⋯ a_{n} ∈ Act^{∗} is the trace of π. As ^{|}G is a labelled transition system, T (g) is defined above. Alternatively, it could be defined as the set of traces of paths of g. It is easy to see that these definitions are equivalent:

Proposition 2.2 T (g) = {T (π) | π ∈ paths(g)}. □

Explicit model In trace semantics a process can be represented by a trace equivalence class of process graphs, or equivalently by the set of its traces. Such a trace set is always nonempty and prefix-closed. The next proposition shows that the domain T T of trace sets is in bijective correspondence with the domain ^{|}G/_{=_{T}} of process graphs modulo trace equivalence, as well as with the domain ^{|}G^{mr}/_{=_{T}} of process graphs with multiple roots modulo trace equivalence. Models of concurrency like T T, in which a process is not represented as an equivalence class but rather as a mathematically coded set of its properties, are sometimes referred to as explicit models.

Definition 2.2 The trace domain T T is the set of subsets T of Act^{∗} satisfying

\begin{matrix}T1 & ε ∈ T, \\ T2 & σρ ∈ T ⇒ σ ∈ T. \end{matrix}

Proposition 2.3 T ∈ T T ⇔ ∃g ∈ ^{|}G : T (g) = T ⇔ ∃g ∈ ^{|}G^{mr} : T (g) = T. Proof: Let T ∈ T T. Define the canonical graph G(T) of T by nodes(G(T)) = T, root(G(T)) = ε and (σ, a, ρ) ∈ edges(G(T)) iff ρ = σa. As T satisfies T2, G(T) is connected, i.e. G(T) ∈ ^{|}G. In fact, G(T) is a tree. Moreover, for every path π ∈ paths(G(T)) one has T (π) = end(π). Hence, using Proposition 2.2, T (G(T)) = T.

For the remaining two implication, note that ^{|}G ⊆ ^{|}G^{mr}, and the trace set T (g) of any graph g ∈ ^{|}G^{mr} satisfies T1 and T2. □

T T was used as a model of concurrency in Hoare [30].

Infinite processes For infinite processes one distinguishes two variants of trace semantics: (finitary) trace semantics as defined above, and infinitary trace semantics (T^{∞}), obtained by taking infinite runs into account.

Definition 2.3 a_{1}a_{2} ⋯ ∈ Act^{∞} is an infinite trace of a process p ∈ IP if there are processes p_{1}, p_{2}, ... such that p ⟶^{a_{1}} p_{1} ⟶^{a_{2}} · · ·. Let T^{∞}(p) denote the set of infinite traces of p. Two processes p and q are infinitary trace equivalent, notation p =_{T}^{∞} q, if T (p) = T (q) and T^{∞}(p) = T^{∞}(q).

Clearly p =_{T}^{∞} q ⇒ p =_{T} q. That on ^{|}G the reverse does not hold follows from Counterexample 1:

a  a a a a  a  a  ⋯ a  a a  a  a a a a  a  a  ⋯ a a  a  a a =_{B}^{ω} ≠_{T}^{∞} ≠_{PF}

Counterexample 1: Finitary equivalent but not infinitary equivalent

one has T (left) = T (right) = {a^{n} | n ∈ IN}, but T^{∞}(left) ≠ T^{∞}(right), as only the graph at the right has an infinite trace.

However, with König’s lemma one easily proves that for image finite processes finitary and infinitary trace equivalence coincide:

Proposition 2.4 Let p and q be image finite processes with p =_{T} q. Then p =_{T}^{∞} q. Proof: It is sufficient to show that T^{∞}(p) can be expressed in terms of T (p) for any image finite process p. In fact, T^{∞}(p) consists of all those infinite traces for which all finite prefixes are in T (p). One direction of this statement is trivial: if σ ∈ T^{∞}(p), all finite prefixes of σ must be in T (p). For the other direction suppose that, for i ∈ IN, a_{i} ∈ Act and a_{1}a_{2} ⋯ a_{i} ∈ T (p). With induction on i ∈ IN one can show that there exists processes p_{i} such that i = 0 and p_{0} = p, or p_{i−1} ⟶^{a_{i}} p_{i}, and for every j ≥ i one has a_{i+1}a_{i+2} ⋯ a_{j} ∈ T (p_{i}). The existence of these p_{i}’s immediately entails that a_{1}a_{2}a_{3} ⋯ ∈ T^{∞}(p). The base case (i = 0) is trivial. Suppose the claim holds for certain i. For every j ≥ i + 1 there must be a process q with p_{i} − −^{a_{i+1}} → q and a_{i+2}a_{i+3} ⋯ a_{j} ∈ T (q). As there are only finitely many processes q with p_{i} − −^{a_{i+1}} → q, there must be one choice of q for which a_{i+2}a_{i+3} ⋯ a_{j} ∈ T (q) for infinitely many values of j. Take this q to be p_{i+1}. As T (p_{i+1}) is prefixclosed, one has a_{i+2}a_{i+3} ⋯ a_{j} ∈ T (p_{i+1}) for all j ≥ i + 1. □

An explicit representation of infinitary trace semantics is obtained by taking the subsets T of Act^{ω} satisfying T1 and T2.

3 Completed trace semantics

Definition 3 σ ∈ Act^{∗} is a complete trace of a process p, if there is a process q such that p ⟶^{σ} q and I(q) = ∅. Let CT (p) denote the set of complete traces of p. Two processes p and q are completed trace equivalent, notation p =_{CT} q, if T (p) = T (q) and CT (p) = CT (q). In completed trace semantics (CT) two processes are identified iff they are completed trace equivalent.

Testing scenario Completed trace semantics can be explained with the following (rather trivial) completed trace machine. The process is modelled as a black box that contains as its interface to

b

Figure 2: The completed trace machine

the outside world a display on which the name of the action is shown that is currently carried out by the process. The process autonomously chooses an execution path that is consistent with its position in the labelled transition system (IP, →). During this execution always an action name is visible on the display. As soon as no further action can be carried out, the process reaches a state of deadlock and the display becomes empty. Now the existence of an observer is assumed that watches the display and records the sequence of actions displayed during a run of the process, possibly followed by deadlock. It is assumed that an observation takes only a finite amount of time and may be terminated before the process stagnates. Hence the observer records either a sequence of actions performed in succession—a trace of the process—or such a sequence followed by deadlock— a completed trace. Two processes are identified if they allow the same set of observations in this sense.

The trace machine can be regarded as a simpler version of the completed trace machine, were the last action name remains visible in the display if deadlock occurs (unless deadlock occurs in the beginning already). On this machine traces can be recorded, but stagnation can not be detected, since in case of deadlock the observer may think that the last action is still continuing.

Modal characterization

Definition 3.1 The set L_{CT} of completed trace formulas over Act is defined recursively by:

• ⊤ ∈ L_{CT}.

• 0 ∈ L_{CT}.

• If φ ∈ L_{CT} and a ∈ Act then aφ ∈ L_{CT}.

The satisfaction relation ⊧ ⊆ IP × L_{CT} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ 0 if I(p) = ∅.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

Note that a completed trace formula satisfied by a process p represents either a trace (if it has the form a_{1}a_{2} ⋯ a_{n}⊤) or a completed trace (if it has the form a_{1}a_{2} ⋯ a_{n}0). Hence one has

Proposition 3.1 p =_{CT} q ⇔ ∀φ ∈ L_{CT} (p ⊧ φ ⇔ q ⊧ φ). □

Also note the close link between the constructors of the modal formulas (corresponding to the three clauses in Definition 3.1) and the types of observations according to the testing scenario: ⊤ represents the act of the observer of terminating the observation, regardless of whether the observed process has terminated, 0 represents the observation of deadlock (the display becomes empty), and aφ represents the observation of a being displayed, followed by the observation φ.

Process graph characterization Let g ∈ ^{|}G^{mr} and s ∈ nodes(g). Then I(s) := {a ∈ Act | ∃t : (s, a, t) ∈ edges(g)} is the menu of s. CT (g) can now be characterized as follows.

Proposition 3.2 CT (g) = {T (π) | π ∈ paths(g) ∧ I(end(π)) = ∅}. □

Classification Trivially T ⪯ CT (as in Figure 1). Counterexample 2 shows that the reverse

a  a b ab + a  =_{T} ≠_{CT} =_{S} ≠_{F}^{1}  abab

Counterexample 2: Trace and simulation equivalent, but not completed trace equivalent

does not hold: one has T (left) = T (right) = {ε, a, ab}, whereas CT (left) ≠ CT (right) (since a ∈ CT (left) − CT (right)). Hence the two process graphs are identified in trace semantics but distinguished in completed trace semantics. Thus T ≺ CT: on ^{|}G completed trace semantics makes strictly less identifications than trace semantics.

Explicit model In completed trace semantics a process can be represented by a completed trace equivalence class of process graphs, or equivalently by the pair (T, CT) of its sets of traces and complete traces. The next proposition gives an explicit characterization of the domain ^{|}CT T of pairs of sets of traces and complete traces of process graphs with multiple roots.

Definition 3.2 The completed trace domain ^{|}CT T is the set of pairs (T, CT) ∈ Act^{∗}×Act^{∗} satisfying

T ∈ T T and CT ⊆ T, σ ∈ T − CT ⇒ ∃a ∈ Act : σa ∈ T.

Proposition 3.3 (T, CT) ∈ ^{|}CT T ⇔ ∃g ∈ ^{|}G^{mr} : T (g) = T ∧ CT (g) = T. Proof: Let (T, CT) ∈ ^{|}CT T. Define the canonical graph G(T, CT) of (T, CT) by

• nodes(G(T, CT)) = T ∪ {σδ | σ ∈ CT},

• roots(G(T, CT)) = {ε} ∪ {δ | ε ∈ CT} and

• (σ, a, ρ) ∈ edges(G(T)) iff ρ = σa ∨ ρ = σaδ.

As T satisfies T2, G(T, CT) is connected, i.e. G(T, CT) ∈ ^{|}G^{mr}. In fact, G(T, CT) is a tree, except that it may have two roots. Using Propositions 2.2 and 3.2 it is easy to see that T (G(T, CT)) = T and CT (G(T, CT)) = CT. □

The pairs obtained from process graphs with single roots are the ones moreover satisfying

ε ∈ CT ⇔ T = {ε}.

Infinite processes Also for completed trace semantics one can distinguish a finitary and an infinitary variant. In terms of the testing scenario, the latter (CT^{∞}) postulates that observations may take an infinite amount of time.

Definition 3.3 Two processes p and q are infinitary completed trace equivalent, notation p =_{CT}^{∞} q, if CT (p) = CT (q) and T^{∞}(p) = T^{∞}(q). Note that in this case also T (p) = T (q).

Proposition 2.4 implies that for image finite processes CT and CT^{∞} coincide, whereas Counterexample 1 shows that in general the two are different. In fact, T ≺ T^{∞} ≺ CT^{∞} and T ≺ CT ≺ CT^{∞}, and the two preceding counterexamples show that there are no further inclusions.

4 Failures semantics

Testing scenario The failures machine contains as its interface to the outside world not only the display of the completed trace machine, but also a switch for each action a ∈ Act (as in Figure 3). By means of these switches the observer may determine which actions are free and which are

a· _{b}· _{⋯} _{z}·  _{a}

Figure 3: The failure trace machine

blocked. This situation may be changed any time during a run of the process. As before, the process autonomously chooses an execution path that fits with its position in (IP, →), but this time the process may only start the execution of free actions. If the process reaches a state where all initial actions of its remaining behaviour are blocked, it can not proceed and the machine stagnates, which can be recognized from the empty display. In this case the observer may record that after a certain sequence of actions σ, the set X of free actions is refused by the process. X is therefore called a refusal set and ^{/} \σ, X^{\} / a failure pair. The set of all failure pairs of a process is called its failure set, and constitutes its observable behaviour.

Definition 4 ^{/} \σ, X^{\} / ∈ Act^{∗} × P(Act) is a failure pair of a process p if there is a process q such that p ⟶^{σ} q and I(q) ∩ X = ∅. Let F (p) denote the set of failure pairs of p. Two processes p and q are failures equivalent, notation p =_{F} q, if F (p) = F (q). In failures semantics (F) two processes are identified iff they are failures equivalent.

Note that T (p) can be expressed in terms of F (p): T (p) = {σ ∈ Act^{∗} | ^{/} \σ, ∅^{\} / ∈ F (p)}; hence p =_{F} q implies T (p) = T (q).

Definition 4.1 For p ∈ IP and σ ∈ T (p), let Cont_{p}(σ) = {a ∈ Act | σa ∈ T (p)}, the set of possible continuations of σ.

The following proposition says that the failure set F (p) of a process p is completely determined by the set of failure pairs ^{/} \σ, X^{\} / with X ⊆ Cont_{p}(σ).

Proposition 4.1 Let p∈IP, σ ∈T (p) and X ⊆Act. Then ^{/} \σ, X^{\} /∈F (p) ⇔ ^{/} \σ, X ∩ Cont_{p}(σ)^{\} /∈F (p). Proof: If p ⟶^{σ} q then I(q) ⊆ Cont_{p}(σ). □

Modal characterization

Definition 4.2 The set L_{F} of failure formulas over Act is defined recursively by:

• ⊤ ∈ L_{F}.

• X̃ ∈ L_{F} for X ⊆ Act.

• If φ ∈ L_{F} and a ∈ Act then aφ ∈ L_{F}.

The satisfaction relation ⊧ ⊆ IP × L_{F} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ X̃ if I(p) ∩ X = ∅.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

X̃ represents the observation that the process refuses the set of actions X, i.e. that stagnation occurs in a situation where X is the set of actions allowed by the environment. Note that a failure formula satisfied by a process p represents either a trace (if it has the form a_{1}a_{2} ⋯ a_{n}⊤) or a failure pair (if it has the form a_{1}a_{2} ⋯ a_{n}X̃). Hence one has

Proposition 4.2 p =_{F} q ⇔ ∀φ ∈ L_{F} (p ⊧ φ ⇔ q ⊧ φ). □

Process graph characterization Let g ∈ ^{|}G^{mr} and π ∈ paths(g). Then

F (π) := {^{/} \T (π), X^{\} / | I(end(π)) ∩ X = ∅}

is the failure set of π. F (g) can now be characterized as follows.

Proposition 4.3 F (g) = ⋃_{π∈paths(g)} F (π). □

Classification CT ≺ F. Proof: For “CT ⪯ F ” it suffices to show that also CT (p) can be expressed in terms of F (p):

CT (p) = {σ ∈ Act^{∗} | ^{/} \σ, Act^{\} / ∈ F (p)}.

It also suffices to show that the modal language L_{CT} is a sublanguage of L_{F}: p ⊧ 0 ⇔ p ⊧ Ãct. “CT ⪰̸ F ” follows from Counterexample 3: one has CT (left) = CT (right) = {ab, ac}, whereas F (left) ≠ F (right) (since ^{/} \a, {c}^{\} / ∈ F (left) − F (right)). □

a  a b  b  c ab + a(b + c)  =_{CT} ≠_{F} =_{CS} ≠_{F}^{1}  a b  c a(b + c)

Counterexample 3: Completed trace and completed simulation equivalent, but not failures equivalent or even singleton-failures equivalent

Explicit model In failures semantics a process can be represented by a failures equivalence class of process graphs, or equivalently by its failure set. The next proposition gives an explicit characterization of the domain IF of failure sets of process graphs with multiple roots.

Definition 4.3 The failures domain IF is the set of subsets F of Act^{∗} × P(Act) satisfying

F1 ^{/} \ε, ∅^{\} / ∈ F,
F2 ^{/} \σρ, ∅^{\} / ∈ F ⇒ ^{/} \σ, ∅^{\} / ∈ F,
F3 ^{/} \σ, Y ^{\} / ∈ F ∧ X ⊆ Y ⇒ ^{/} \σ, X^{\} / ∈ F,
F4 ^{/} \σ, X^{\} / ∈ F ∧ ∀a ∈ Y (^{/} \σa, ∅^{\} / ∉ F) ⇒ ^{/} \σ, X ∪ Y ^{\} / ∈ F.

Proposition 4.4 F ∈ IF ⇔ ∃g ∈ ^{|}G^{mr} : F (g) = F. Proof: “⇐”: F1 and F2 follow from T1 and T2 in Section 2, as one has ^{/} \σ, ∅^{\} / ∈ F (g) ⇔ σ ∈ T (g). F3 follows immediately from the definitions, as I(q) ∩ Y = ∅ ∧ X ⊆ Y ⇒ I(q) ∩ X = ∅. F4 follows immediately from Proposition 4.1, as ∀a ∈ Y (^{/} \σa, ∅^{\} / ∉ F (g)) iff Y ∩ Cont_{g}(σ) = ∅.

For “⇒” let F ∈ IF. For σ ∈ Act^{∗} write Cont_{F}(σ) for {a ∈ Act | ^{/} \σa, ∅^{\} / ∈ F}. Define the canonical graph G(F) of F by

• nodes(G(F)) = {^{/} \σ, X^{\} / ∈ F | X ⊆ Cont_{F}(σ)},

• roots(G(F)) = {^{/} \ε, X^{\} / | ^{/} \ε, X^{\} / ∈ F},

• edges(G(F)) = {(^{/} \σ, X^{\} /, a, ^{/} \σa, Y ^{\} /) | ^{/} \σ, X^{\} /, ^{/} \σa, Y ^{\} / ∈ nodes(G(F)) ∧ a ∉ X}.

By F1, roots(G(F)) ≠ ∅. Using F3 and F2, any node s = ^{/} \a_{1} ⋯ a_{n}, X^{\} / of G(F) is reachable from

a root by the path π_{s} : ^{/} \ε, ∅^{\} / ⟶^{a_{1}} ^{/} \a_{1}, ∅^{\} / ⟶^{a_{2}} ⋯ ⟶^{a_{n−1}} ^{/} \a_{1} ⋯ a_{n−1}, ∅^{\} / ⟶^{a_{n}} ^{/} \a_{1} ⋯ a_{n}, X^{\} /; hence G(F) is

connected. So G(F) ∈ ^{|}G^{mr}. I have to show that F (G(F)) = F.

“⊇”: Suppose ^{/} \σ, X^{\} / ∈ F. Then, by F3, s := ^{/} \σ, X ∩ Cont_{F}(σ)^{\} / ∈ nodes(G(F)). By construction one has T (π_{s}) = σ and I(s) ∩ X = ∅. Hence ^{/} \σ, X^{\} / ∈ F (π_{s}) ⊆ F (G(F)).

“⊆”: With induction on the length of paths, it follows immediately from the definition of G(F) that for π ∈ paths(G(F)), if end(π) = ^{/} \ρ, Y ^{\} / then ρ = T (π) and I(end(π)) = Cont_{F}(ρ) − Y. (*) Suppose ^{/} \σ, X^{\} / ∈ F (G(F)). Then, by Proposition 4.3, there must be a path π ∈ paths(G(F)) with / \σ, X^{\} / ∈ F (π). So T (π) = σ and I(end(π)) ∩ X = ∅. Let end(π) := ^{/} \ρ, Y ^{\} / ∈ F. By (*), ρ = σ and X ∩ Cont_{F}(σ) ⊆ Y. By F3 it follows that ^{/} \σ, X ∩ Cont_{F}(σ)^{\} / ∈ F, and F4 yields ^{/} \σ, X^{\} / ∈ F. □

A variant of IF was used as a model of concurrency in Hoare [31].^{7}

7There a process is given as a triple (A, F, D) with A ⊆ Act a set of actions that may occur in the process, F ∈ IF and D a set of so-called divergencies, traces that can lead along a state where an infinite sequence of internal actions is possible. As this paper considers only concrete, and hence divergence-free, processes, D is always empty here.

If roots(g) would be allowed to be empty, a characterization is obtained by dropping requirement F1. A characterization of the domain of failure sets of process graphs with single roots is given by adding to F1–4 the requirement

F5 ^{/} \ε, X^{\} / ∈ F ⇒ ∀a ∈ X : ^{/} \a, ∅^{\} / ∉ F.

That F5 holds follows from the observation that I(root(g)) = {a ∈ Act | ^{/} \a, ∅^{\} / ∈ F (g)} for g ∈ ^{|}G.

Alternative characterizations In De Nicola [16] several equivalences, that were proposed in Kennaway [34], Darondeau [15] and De Nicola & Hennessy [17], are shown to coincide with failures semantics on the domain of finitely branching transition systems without internal moves. For this purpose he uses the following alternative characterization of failures equivalence.

Definition 4.4 Write p after σ MUST X if for each q ∈ IP with p ⟶^{σ} q there is an a ∈ I(q) with a ∈ X. Put p ≃ q if for all σ ∈ Act^{∗} and X ⊆ Act: p after σ MUST X ⇔ q after σ MUST X.

Proposition 4.5 Let p, q ∈ IP. Then p ≃ q ⇔ p =_{F} q. Proof: p after σ MUST X ⇔ ^{/} \σ, X^{\} / ∉ F (p) [16]. □

Instead of the complement of the failure set of a process p, one can also take the complement Cont_{p}(σ)−X of every refusal set X within a failure pair ^{/} \σ, X^{\} / of p. In view of Proposition 4.1, the same information stored in F (p) is given by the set of all pairs ^{/} \σ, X^{\} / ∈ Act^{∗} × P(Act) for which there is a process q such that p ⟶^{σ} q and I(q) ⊆ X ⊆ Cont_{p}(σ). In Hennessy [26], a model for nondeterministic behaviours is proposed in which a process is represented as an acceptance tree. An acceptance tree of a finitely branching process without internal moves is essentially the set of pairs described above, conveniently represented as a finitely branching, deterministic process tree, of which the nodes are labelled by collections of sets of actions. Thus acceptance trees constitute an explicit model of failures semantics.

Infinite processes For infinite processes, three versions of failures semantics can be distinguished.

Definition 4.5 Two processes p and q are (finitary) failures equivalent if F (p) = F (q). p and q are infinitary failures equivalent, notation p =_{F}^{∞} q, if F (p) = F (q) and T^{∞}(p) = T^{∞}(q). They are finite-failures equivalent, notation p =_{F}^{−} q, if F^{−}(p) = F^{−}(q), where F^{−}(p) denotes the set of failure pairs ^{/} \σ, X^{\} / of p with X finite.

The original failures semantics of Brookes, Hoare & Roscoe [13] is F^{−}, i.e. what I call finitefailures semantics. They “adopt this view of distinguishability because [they] consider a realistic environment to be one that is at any time capable of performing only a finite number of events.” In terms of the failures machine this means that at any time only finitely many switches can be set on free. Finitary failures semantics is the default version introduced at the beginning of this section. This can be regarded to be the semantics employed in Brookes & Roscoe [14] and Hoare [31]. Infinitary failures semantics was first discussed in Bergstra, Klop & Olderog [10]; it was proposed as a semantics for CSP in Roscoe [45]. The difference between the testing scenarios for F and F^{∞} is that only the latter allows observations of infinite duration. Obviously, F^{−} ⪯ F ⪯ F^{∞}. That the latter inclusion is strict follows from Counterexample 1; Counterexample 4 shows that also the former is strict: one has F^{−}(left) = F^{−}(right), whereas F (left) ≠ F (right). In fact even

a  a a a b_{1} b_{2} b_{3}  ...  a a a b_{1} b_{2} b_{3}  ... =_{B}^{−} ≠_{CT}

Counterexample 4: HML- and finite-failures equivalent, but not completed trace equivalent

CT (left) ≠ CT (right), as a ∈ CT (left) − CT (right). Thus, although T ≺ F^{−}, CT ≺ F and CT^{∞} ≺ F^{∞}, CT and F^{−} are independent, as are CT^{∞} and F.

In addition to the three variants of Definition 4.5 one could also define a version of failures semantics based on infinite traces and finite refusal sets. Such a semantics would distinguish the two graphs of Counterexample 1, but identify the ones of Counterexample 4. As this semantics does not occur in the literature, and has no clear advantages over the other variants, I will not further consider it here.

Proposition 4.6 Let p en q be image finite processes. Then p =_{F}^{−} q ⇔ p =_{F} q ⇔ p =_{F}^{∞} q. Proof: “⇐” has been established for all processes, and the second “⇒” follows immediately from Proposition 2.4 (as p =_{F} q ⇒ p =_{T} q ⇒ p =_{T}^{∞} q). So it remains to show that p ≠_{F} q ⇒ p ≠_{F}^{−} q. Suppose F (p) ≠ F (q), say there is a failure pair ^{/} \σ, X^{\} / ∈ F (p) − F (q). By the image finiteness of q there are only finitely many processes r_{i} with q ⟶^{σ} r_{i}, and for each of them there is an action a_{i} ∈ I(r_{i}) ∩ X (as otherwise ^{/} \σ, X^{\} / would be a failure pair of q). Let Y be the set of all those a_{i}’s. Then Y is a finite subset of X, so ^{/} \σ, Y ^{\} / ∈ F^{−}(p). On the other hand, a_{i} ∈ I(r_{i}) ∩ Y for all r_{i}, so / \σ, Y ^{\} / ∉ F^{−}(q). □

It is not hard to change the leftmost process in Counterexample 4 to an image finite one with the same failure pairs. Thus, in the first statement of Proposition 4.6 it is necessary that both processes are image finite. For the subclass of finitely branching processes a stronger result can be obtained.

Proposition 4.7 Let p, q ∈ IP and p is finitely branching. Then p =_{F}^{−} q ⇔ p =_{F} q. Proof: Suppose p =_{F}^{−} q. As p is finitely branching, Cont_{p}(σ) is finite for all σ ∈ T (p). And as T (q) = T (p), Cont_{q}(σ) = Cont_{p}(σ), which is finite, for all σ ∈ T (q). Now for processes p with this property, F (p) is completely determined by F^{−}(p), as follows from Proposition 4.1. □

The second statement of Proposition 4.6 does not allow such a strengthening, as will follow from Counterexample 12.

5 Failure trace semantics

Testing scenario The failure trace machine has the same layout as the failures machine, but is does not stagnate permanently if the process cannot proceed due to the circumstance that all actions it is prepared to continue with are blocked by the observer. Instead it idles—recognizable from the empty display—until the observer changes its mind and allows one of the actions the process is ready to perform. What can be observed are traces with idle periods in between, and for each such period the set of actions that are not blocked by the observer. Such observations can be coded as sequences of members and subsets of Act.

Example: The sequence {a, b}cdb{b, c}{b, c, d}a(Act) is the account of the following observation: At the beginning of the execution of the process p, only the actions a and b were allowed by the observer. Apparently, these actions were not on the menu of p, for p started with an idle period. Suddenly the observer canceled its veto on c, and this resulted in the execution of c, followed by d and b. Then again an idle period occurred, this time when b and c were the actions not being blocked by the observer. After a while the observer decided to allow d as well, but the process ignored this gesture and remained idle. Only when the observer gave the green light for the action a, it happened immediately. Finally, the process became idle once more, but this time not even one action was blocked. This made the observer realize that a state of eternal stagnation had been reached, and disappointed he terminated the observation.

A set X ⊆ Act, occurring in such a sequence, can be regarded as an offer from the environment, that is refused by the process. Therefore such a set is called a refusal set. The occurrence of a refusal set may be interpreted as a ‘failure’ of the environment to create a situation in which the process can proceed without being disturbed. Hence a sequence over Act ∪ P(Act), resulting from an observation of a process p may be called a failure trace of p. The observable behaviour of a process, according to this testing scenario, is given by the set of its failure traces, its failure trace set. The semantics in which processes are identified iff their failure trace sets coincide, is called failure trace semantics (F T).

For image finite processes failure trace semantics is exactly the equivalence that originates from Phillips notion of refusal testing [42]. (Image infinite processes are not considered in [42].) There it is called refusal equivalence.

Definition 5

• The refusal relations ⟶^{X} for X ⊆ Act are defined by: p ⟶^{X} q iff p = q and I(p) ∩ X = ∅. p ⟶^{X} q means that p can evolve into q, while being idle during a period in which X is the set of actions allowed by the environment.

• The failure trace relations ⟶^{σ} for σ ∈ (Act∪P(Act))^{∗} are defined as the reflexive and transitive closure of both the action and the refusal relations. Again the overloading of notation is harmless.

• σ ∈ (Act ∪ P(Act))^{∗} is a failure trace of a process p if there is a process q such that p ⟶^{σ} q. Let F T (p) denote the set of failure traces of p. Two processes p and q are failure trace equivalent, notation p =_{F T} q, if F T (p) = F T (q).

Modal characterization

Definition 5.1 The set L_{F T} of failure trace formulas over Act is defined recursively by:

• ⊤ ∈ L_{F T}.

• If φ ∈ L_{F T} and X ⊆ Act then X̃φ ∈ L_{F T}.

• If φ ∈ L_{F T} and a ∈ Act then aφ ∈ L_{F T}.

The satisfaction relation ⊧ ⊆ IP × L_{F T} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ X̃φ if I(p) ∩ X = ∅ and p ⊧ φ.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

X̃φ represents the observation that the process refuses the set of actions X, followed by the observation φ. A modal failure trace formula satisfied by a process p represents exactly a failure trace as defined above. Hence one has

Proposition 5.1 p =_{F T} q ⇔ ∀φ ∈ L_{F T} (p ⊧ φ ⇔ q ⊧ φ). □

Process graph characterization Let g ∈ ^{|}G^{mr} and π : s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s_{n} ∈ paths(g). Then the failure trace set of π, F T (π), is the smallest subset of (Act ∪ P(Act))^{∗} satisfying

• (Act − I(s_{0}))a_{1}(Act − I(s_{1}))a_{2} ⋯ a_{n}(Act − I(s_{n})) ∈ F T (π),

• σXρ ∈ F T (π) ⇒ σρ ∈ F T (π),

• σXρ ∈ F T (π) ⇒ σXXρ ∈ F T (π),

• σXρ ∈ F T (π) ∧ Y ⊂ X ⇒ σY ρ ∈ F T (π).

F T (g) can now be characterized as follows.

Proposition 5.2 F T (g) = ⋃_{π∈paths(g)} F T (π). □

Proposition 5.2 yields a technique for deciding that two process graphs are failure trace equivalent, without calculating their entire failure trace set.

Let g, h∈ ^{|}G^{mr}, π: s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s_{n} ∈ paths(g) and π′: t_{0} ⟶^{b_{1}} t_{1} ⟶^{b_{2}} ⋯ ⟶^{b_{m}} t_{m} ∈ paths(h).

Path π′ is a failure trace augmentation of π, notation π ≤_{F T} π′, if F T (π) ⊆ F T (π′). This is the case exactly when n = m, a_{i} = b_{i} and I(t_{i}) ⊆ I(s_{i}) for i = 1, ..., n. From this the following can be concluded.

Corollary 5.1 Two process graphs g, h ∈ ^{|}G^{mr} are failure trace equivalent iff

• for any path π ∈ paths(g) in g there is a π′ ∈ paths(h) such that π ≤_{F T} π′

• and for any path π ∈ paths(g) in h there is a π′ ∈ paths(g) such that π ≤_{F T} π′.

If g and h are moreover without infinite paths, then it suffices to check the requirements above for maximal paths. □

Classification F ≺ F T. Proof: For “F ⪯ F T ” it suffices to show that F (p) can be expressed in terms of F T (p):

/ \σ, X^{\} / ∈ F (p) ⇔ σX ∈ F T (p).

“F ⪰̸ F T ” follows from Counterexample 5; see Section 7 for details. □

Infinite processes As for failures semantics, three variants of failure trace semantics for infinite processes can be defined. Besides the default version (F T) there is an infinitary version (F T^{∞}), motivated by observations that may last forever, and a finite version (F T^{−}), motivated by an observer that may only set finitely many switches on free at any time.

Definition 5.2 σ_{1}σ_{2} ⋯ ∈ (Act ∪ P(Act))^{∞} is an infinite failure trace of a process p ∈ IP if there are processes p_{1}, p_{2}, ... such that p ⟶^{σ_{1}} p_{1} ⟶^{σ_{2}} · · ·. Let F T^{∞}(p) denote the set of infinite failure traces of p. Two processes p and q are infinitary failure trace equivalent, notation p =_{F T}^{∞} q, if

a  a c  c b  f d  e a(b + cd) + a(f + ce)  =_{F} ≠_{F T} =_{R} ≠_{RT}  a a  c c  f b  d e a(b + ce) + a(f + cd)

Counterexample 5: Failures and ready equivalent, but not failure trace or ready trace equivalent

F T^{∞}(p) = F T^{∞}(q) and F T (p) = F T (q). They are finite-failure trace equivalent, notation p =_{F T}^{−} q, if F T^{−}(p) = F T^{−}(q), where F T^{−}(p) denotes the set of failure traces of p in which all refusal sets are finite.

Clearly, F T^{−} ≺ F T ≺ F T^{∞}; Counterexamples 1 and 4 show that the inclusions and strict. One also has F^{−} ≺ F T^{−}, F ≺ F T and F^{∞} ≺ F T^{∞}; here strictness follows from Counterexample 5.

Proposition 5.3 Let p en q be image finite processes. Then p =_{F T}^{−} q ⇔ p =_{F T} q ⇔ p =_{F T}^{∞} q. Proof: “p =_{F T}^{−} q ⇐ p =_{F T} q ⇐ p =_{F T}^{∞} q” holds for all processes. Note that the definition of F T (p) is exactly like the definition of T (p), except that the failure trace relations are used instead of the generalized action relations; the same relation exists between F T^{∞}(p) and T^{∞}(p). Moreover, a process p ∈ IP is image finite in terms of the failure trace relations on IP iff it is image finite in terms of terms of the (generalized) action relations on IP, as defined in Definition 1.2. Hence “p =_{F T} q ⇒ p =_{F T}^{∞} q” follows immediately from Proposition 2.4. “p =_{F T}^{−} q ⇒ p =_{F T} q”: Suppose F T (p) ≠ F T (q), say F T (p) − F T (q) ≠ ∅. Let σ be a failure trace in F T (p) − F T (q) with at least one infinite refusal set. I will show that there must be a failure trace in F T (p) − F T (q) with strictly fewer infinite refusal sets than σ. By applying this result a finite number of times, a failure trace ρ ∈ F T (p) − F T (q) is found without infinite refusal sets, showing that F T^{−}(p) ≠ F T^{−}(q).

So let σ = σ_{1}Xσ_{2} ∈ F T (p) − F T (q) with X an infinite refusal set. Clearly σ_{1}σ_{2} ∈ F T (p). By the image finiteness of q there are only finitely many pairs of processes r_{i}, s_{i} with q ⟶^{σ_{1}} r_{i} ⟶^{σ_{2}} s_{i}, and for each of them there is an action a_{i} ∈ I(r_{i}) ∩ X (as otherwise σ_{1}Xσ_{2} would be a failure trace of q). Let Y be the set of all those a_{i}’s. Then Y is finite. As Y is a subset of X, one has σ_{1}Y σ_{2} ∈ F T (p). On the other hand, a_{i} ∈ I(r_{i}) ∩ Y for all r_{i}, so σ_{1}Y σ_{2} ∉ F T (q). □

Unlike the situation for failures semantics, in the first statement of Proposition 5.3 it is not necessary that both processes are image finite.

Proposition 5.4 Let p, q ∈ IP and p is image finite. Then p =_{F T}^{−} q ⇔ p =_{F T} q. Proof: More difficult, and omitted here. □

The second statement of Proposition 5.3 does not allow such a strengthening, as will follow from Counterexample 12.

6 Ready trace semantics

Testing scenario The ready trace machine is a variant of the failure trace machine that is equipped with a lamp for each action a ∈ Act. Each time the process idles, the lamps of all actions

a· _{b}· _{⋯}  _{z}·  _{b}

Figure 4: The ready trace machine

the process is ready to engage in are lit. Of course all these actions are blocked by the observer, otherwise the process wouldn’t idle. Now the observer can see which actions could be released in order to let the process proceed. During the execution of an action no lamps are lit. An observation now consists of a sequence of members and subsets of Act, the actions representing information obtained from the display, and the sets of actions representing information obtained from the lights. Such a sequence is called a ready trace of the process, and the subsets occurring in a ready trace are referred to as menus. The information about the free and blocked actions is now redundant. The set of all ready traces of a process is called its ready trace set, and constitutes its observable behaviour.

Definition 6

• The ready trace relations × +⟶^{σ} for σ ∈ (Act ∪ P(Act))^{∗} are defined recursively by:

1. p × +⟶^{ε} p, for any process p.

2. p ⟶^{a} q implies p × +⟶^{a} q.

3. p × +⟶^{X} q with X ⊆ Act whenever p = q and I(p) = X.

4. p × +⟶^{σ} q × +⟶^{ρ} r implies p × +⟶^{σρ} r.

The special arrow × +⟶^{σ} had to be used, since further overloading of ⟶^{σ} would cause confusion with the failure trace relations.

• σ ∈ (Act∪P(Act))^{∗} is a ready trace of a process p if there is a process q such that p × +⟶^{σ} q. Let RT (p) denote the set of ready traces of p. Two processes p and q are ready trace equivalent, notation p =_{RT} q, if RT (p) = RT (q). In ready trace semantics (RT) two processes are identified iff they are ready trace equivalent.

In Baeten, Bergstra & Klop [6], Pnueli [43] and Pomello [44] ready trace semantics was defined slightly differently. By Proposition 6.1 below, their definition yields the same equivalence as mine.

a  b  a  c

Definition 6.1 X_{0}a_{1}X_{1}a_{2} ⋯ a_{n}X_{n} ∈ P(Act)×(Act×P(Act))^{∗} is a normal ready trace of a process

p if there are processes p_{1}, ..., p_{n} such that p ⟶^{a_{1}} p_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} p_{n} and I(p_{i}) = X_{i} for i = 1, ..., n.

Let RT_{N}(p) denote the set of normal ready traces of p. Two processes p and q are ready trace equivalent in the sense of [6, 43, 44] if RT_{N}(p) = RT_{N}(q).

Proposition 6.1 Let p, q ∈ IP. Then RT_{N}(p) = RT_{N}(q) ⇔ RT (p) = RT (q). Proof: The normal ready traces of a process are just the ready traces which are an alternating sequence of sets and actions, and vice versa the set of all ready traces can be constructed form the set of normal ready traces by means of doubling and leaving out menus. □

Modal characterization

Definition 6.2 The set L_{RT} of ready trace formulas over Act is defined recursively by:

• ⊤ ∈ L_{RT}.

• If φ ∈ L_{RT} and X ⊆ Act then Xφ ∈ L_{RT}.

• If φ ∈ L_{RT} and a ∈ Act then aφ ∈ L_{RT}.

The satisfaction relation ⊧ ⊆ IP × L_{RT} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ Xφ if I(p) = X and p ⊧ φ.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

Xφ represents the observation of a menu, followed by the observation φ. A ready trace formula satisfied by a process p represents exactly a ready trace in Definition 6. Hence one has

Proposition 6.2 p =_{RT} q ⇔ ∀φ ∈ L_{RT} (p ⊧ φ ⇔ q ⊧ φ). □

Process graph characterization Let g ∈ ^{|}G^{mr} and π : s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} s_{n} ∈ paths(g). The ready trace of π is given by RT_{N}(π) := I(s_{0})a_{1}I(s_{1})a_{2} ⋯ a_{n}I(s_{n}). RT_{N}(g) can now be characterized by:

Proposition 6.3 RT_{N}(g) = {RT_{N}(π) | π ∈ paths(g)}. □

Moreover, RT (g) is the smallest subset of (Act ∪ P(Act))^{∗} containing RT_{N}(g) and satisfying

σXρ ∈ RT (g) ⇒ σρ ∈ RT (g) ∧ σXXρ ∈ RT (g).

Classification F T ≺ RT. Proof: For “F T ⪯ RT ” it suffices to show that F T (p) can be expressed in terms of RT (p):

σ = σ_{1}σ_{2} ⋯ σ_{n} ∈ F T (p) (σ_{i} ∈ Act ∪ P(Act)) ⇔
∃ρ = ρ_{1}ρ_{2} ⋯ ρ_{n} ∈ RT (p) (ρ_{i} ∈ Act ∪ P(Act)) such that for i = 1, ..., n either
σ_{i} = ρ_{i} ∈ Act or σ_{i}, ρ_{i} ⊆ Act and σ_{i} ∩ ρ_{i} = ∅.

“F T ⪰̸ RT ” follows from Counterexample 6; see Section 7 for details. □

a  a b  c ab + ac  =_{F} ≠_{R} =_{F T} ≠_{RT}  a b  c a  a b  c ab + a(b + c) + ac

Counterexample 6: Failures and failure trace equivalent, but not ready or ready trace equivalent

Explicit model In ready trace semantics a process can be represented by a ready trace equivalence class of process graphs, or equivalently by its ready trace set, possibly in the normal form of Definition 6.1. The next proposition gives an explicit characterization of the domain IRT T of ready trace sets in this form of process graphs with multiple roots.

Definition 6.3 The ready trace domain IRT T is the set of subsets RT of P(Act) × (Act × P(Act))^{∗} satisfying

RT1 ∃X(X ∈ RT),
RT2 σX ∈ RT ∧ a ∈ X ⇔ ∃Y (σXaY ∈ RT).

Proposition 6.4 RT ∈ IRT T ⇔ ∃g ∈ ^{|}G^{mr} : RT_{N}(g) = RT. Proof: “⇐” is evident. For “⇒” let RT ∈ IRT T. Define the canonical graph G(RT) of RT by

• nodes(G(RT)) = RT,

• roots(G(RT)) = {X ⊆ Act | X ∈ RT},

• edges(G(RT)) = {(σ, a, σaY) | σ, σaY ∈ nodes(G(RT))}.

By RT1, roots(G(RT)) ≠ ∅. Using R2, G(RT) is connected. So G(RT) ∈ ^{|}G^{mr}. Moreover, for every path π ∈ paths(G(RT)) one has RT_{N}(π) = end(π). Hence RT_{N}(G(RT)) = RT. □

If roots(g) would be allowed to be empty, a characterization is obtained by dropping requirement RT1. A characterization of the domain of ready trace sets of process graphs with single roots is given by strengthening RT1 to ∃!X(X ∈ RT), where ∃!X means “there is exactly one X such that”.

Infinite processes An infinitary version of ready trace semantics (RT^{∞}) is defined analogously to infinitary failure trace semantics. A finite version is not so straightforward; a definition will be proposed in the next section.

Definition 6.4 σ_{1}σ_{2} ⋯ ∈ (Act ∪ P(Act))^{∞} is an infinite ready trace of a process p ∈ IP if there are processes p_{1}, p_{2}, ... such that p × +⟶^{σ_{1}} p_{1} × +⟶^{σ_{2}} · · ·. Let RT^{∞}(p) denote the set of infinite ready traces of p. Two processes p and q are infinitary ready trace equivalent, notation p =_{RT}^{∞} q, if RT^{∞}(p) = RT^{∞}(q) and RT (p) = RT (q).

Clearly, RT ≺ RT^{∞}; Counterexample 1 shows that the inclusion is strict. Moreover F T^{∞} ≺ RT^{∞}.

Proposition 6.5 Let p en q be image finite processes. Then p =_{RT} q ⇔ p =_{RT}^{∞} q. Proof: Exactly as the corresponding part of Proposition 5.3. □

Counterexample 12 will show that in Proposition 6.5 both p and q need to be image finite.

7 Readiness semantics and possible-futures semantics

Testing scenario The readiness machine has the same layout as the ready trace machine, but, like the failures machine, can not recover from an idle period. By means of the lights the menu of initial actions of the remaining behaviour of an idle process can be recorded, but this happens at most once during an observation of a process, namely at the end. An observation either results in a trace of the process, or in a pair of a trace and a menu of actions by which the observation could have been extended if the observer wouldn’t have blocked them. Such a pair is called a ready pair of the process, and the set of all ready pairs of a process is its ready set.

Definition 7 ^{/} \σ, X^{\} / ∈ Act^{∗} × P(Act) is a ready pair of a process p if there is a process q such that p ⟶^{σ} q and I(q) = X. Let R(p) denote the set of ready pairs of p. Two processes p and q are ready equivalent, notation p =_{R} q, if R(p) = R(q). In readiness semantics (R) two processes are identified iff they are ready equivalent.

Modal characterization

Definition 7.1 The set L_{R} of readiness formulas over Act is defined recursively by:

• ⊤ ∈ L_{R}.

• X ∈ L_{R} for X ⊆ Act.

• If φ ∈ L_{R} and a ∈ Act then aφ ∈ L_{R}.

The satisfaction relation ⊧ ⊆ IP × L_{R} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ X if I(p) = X.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

X represents the observation of a menu. A readiness formula satisfied by a process p represents either a trace (if it has the form a_{1}a_{2} ⋯ a_{n}⊤) or a ready pair (if it has the form a_{1}a_{2} ⋯ a_{n}X). Hence one has

Proposition 7.1 p =_{R} q ⇔ ∀φ ∈ L_{R}(p ⊧ φ ⇔ q ⊧ φ). □

Process graph characterization Let g ∈ ^{|}G^{mr} and π ∈ paths(g). The ready pair of π is given by R(π) := ^{/} \T (π), I(end(π))^{\} /. R(g) can now be characterized by:

Proposition 7.2 R(g) = {R(π) | π ∈ paths(g)}. □

Classification F ≺ R ≺ RT, but R and F T are independent. Proof: For “F ⪯ R” it suffices to show that F (p) can be expressed in terms of R(p):

/ \σ, X^{\} / ∈ F (p) ⇔ ∃Y ⊆ Act : ^{/} \σ, Y ^{\} / ∈ R(p) ∧ X ∩ Y = ∅.

For “R ⪯ RT ” it suffices to show that R(p) can be expressed in terms of RT (p):

/ \σ, X^{\} / ∈ R(p) ⇔ σX ∈ RT (p).

“R ⪰̸ F T ” (and hence “R ⪰̸ RT ” and “F ⪰̸ F T ”) follows from Counterexample 5, in which R(left) = R(right) but F T (left) ≠ F T (right). The first statement follows with Proposition 7.2. Both graphs have 9 paths starting from the root, and hence 9 ready pairs. These are easily seen to be the same at both sides; in the second graph only 4 ready pairs swapped places. The second statement follows since a{b}ce ∈ F T (left) − F T (right).

“R ⪯̸ F T ” (and hence “R ⪯̸ F ” and “RT ⪯̸ F T ”) follows from Counterexample 6, in which F T (left) = F T (right) but R(left) ≠ R(right). The first statement follows from Corollary 5.1, since the new maximal paths at the right-hand side are both failure trace augmented by the two maximal paths both sides have in common. The second one follows since ^{/} \a, {b, c}^{\} / ∈ R(right) − R(left). □

Explicit model In readiness semantics a process can be represented by a ready equivalence class of process graphs, or equivalently by its ready set. The next proposition gives an explicit characterization of the domain IR of ready sets of process graphs with multiple roots.

Definition 7.2 The readiness domain IR is the set of subsets R of Act^{∗} × P(Act) satisfying

\begin{matrix}R1 & ∃X(^{/} \ε, X^{\} / ∈ R), \\ R2 & ∃X(^{/} \σ, X ∪ \{a\}^{\} / ∈ R) ⇔ ∃Y(^{/} \σa, Y ^{\} / ∈ R). \end{matrix}

Proposition 7.3 R ∈ IR ⇔ ∃g ∈ ^{|}G^{mr} : R(g) = R. Proof: “⇐” is evident. For “⇒” let R ∈ IR. Define the canonical graph G(R) of R by

• nodes(G(R)) = R,

• roots(G(R)) = {^{/} \ε, X^{\} / | ^{/} \ε, X^{\} / ∈ R},

• edges(G(R)) = {(^{/} \σ, X^{\} /, a, ^{/} \σa, Y ^{\} /) | ^{/} \σ, X^{\} /, ^{/} \σa, Y ^{\} / ∈ nodes(G(R)) ∧ a ∈ X}.

By R1, roots(G(R)) ≠ ∅. Using R2, G(R) is connected. Hence G(R) ∈ ^{|}G^{mr}. Moreover, for every path π ∈ paths(G(R)) one has R(π) = end(π). From this it follows that R(G(R)) = R. □

If roots(g) would be allowed to be empty, a characterization is obtained by dropping requirement R1. A characterization of the domain of ready sets of process graphs with single roots is given by strengthening R1 to ∃!X(^{/} \ε, X^{\} / ∈ R), where ∃!X means “there is exactly one X such that”.

Possible-futures and acceptance-refusal semantics Readiness semantics was proposed by Olderog & Hoare [40]. Two preliminary versions stem from Rounds & Brookes [46]: in possible-futures semantics (PF ) the menu consists of the entire trace set of the remaining behaviour of an idle process, instead of only the set of its initial actions; in acceptance-refusal semantics a menu may be any finite subset of initial actions, while also the finite refusal sets of Section 4 are observable.

Definition 7.3 ^{/} \σ, X^{\} / ∈ Act^{∗} × P(Act^{∗}) is a possible future of a process p if there is a process q such that p ⟶^{σ} q and T (q) = X. Let PF (p) denote the set of possible futures of p. Two processes p and q are possible-futures equivalent, notation p =_{PF} q, if PF (p) = PF (q).

The modal and process graph characterizations of possible-future semantics are straightforward, but a plausible testing scenario has not been proposed. Trivially R ⪯ PF . That the reverse does not hold, and even that PF ⪯̸ RT, will follow from Counterexample 10. Counterexample 7 shows that F T ⪯̸ PF . There PF (left) = PF (right) but F T (left) ≠ F T (right). As for the first statement, both graphs have 18 paths starting from the root, and hence 18 possible futures. These are easily seen to be the same at both sides; in the second graph only 2 possible futures swapped places. The second statement follows since a{b}a{b}cd ∈ F T (left) − F T (right). Thus possible-future semantics is incomparable with failure trace and ready trace semantics.

a b a a c c b d e  a a a c c b d e a(b + a(b + cd) + ace) + a(acd + a(ce + b)) =_{PF} ≠_{FT} ≠_{S}  a a a c c b d e a(a(b + cd) + ace) + a(acd + a(ce + b) + b) a  b a a c c b d e

Counterexample 7: Possible-futures equivalent, but not failure trace or simulation equivalent

Definition 7.4 ^{/} \σ, X, Y ^{\} / ∈ Act^{∗} × P(Act) × P(Act) is an acceptance-refusal triple of a process p if X and Y are finite and there is a process q such that p ⟶^{σ} q, X ⊆ I(q) and Y ∩ I(q) = ∅. Let AR(p) denote the set of acceptance-refusal triples of p. Two processes p and q are acceptance-refusal equivalent, notation p =_{AR} q, if AR(p) = AR(q).

The modal and process graph characterizations are again straightforward. A motivating testing scenario would be the same as for readiness semantics, except that at any time only finitely many switches can be set on free, and only finitely many lamps can be investigated in a finite amount of time. Clearly p =_{R} q ⇒ p =_{AR} q, for

AR(p) = {^{/} \σ, X, Y ^{\} / | ∃^{/} \σ, Z^{\} / ∈ R(p) | X, Y finite ∧ X ⊆ Z ∧ Y ∩ Z = ∅}.

That this implication is strict follows from Counterexample 4. It is not difficult to see that for finitely branching processes acceptance-refusal equivalence coincides with ready equivalence: ^{/} \σ, X^{\} / is a ready pair of a process p iff p has an acceptance-refusal triple ^{/} \σ, X, Y ^{\} / with X ∪ Y = Cont_{p}(σ) (cf. Definition 4.1).

Infinite processes Note that if in Definition 7.4 the sets X and Y are allowed to be infinite the resulting equivalence would be ready equivalence again. Namely ^{/} \σ, X^{\} / is a ready pair of a process p iff p has such an acceptance-refusal triple ^{/} \σ, X, Act − Y ^{\} /. Thus acceptance-refusal semantics can be regarded as the finite variant of readiness semantics, and will therefore be denoted R^{−}. The infinitary variant of readiness semantics (R^{∞}), motivated by observations that may last forever, is defined analogously to F^{∞}:

Definition 7.5 p and q are infinitary ready equivalent if R(p) = R(q) and T^{∞}(p) = T^{∞}(q).

Clearly, R ≺ R^{∞}; by Counterexample 1 the inclusion is strict. Moreover, F^{∞} ≺ R^{∞} ≺ RT^{∞}.

Proposition 7.4 Let p en q be image finite processes. Then p =_{R} q ⇔ p =_{R}^{∞} q. Proof: “⇐” has been established for all processes, and the second “⇒” follows immediately from Proposition 2.4 (as p =_{R} q ⇒ p =_{T} q ⇒ p =_{T}^{∞} q). □

Proposition 7.5 Let p, q ∈ IP and p is image finite. Then p =_{AR} q ⇔ p =_{R} q. Proof: “⇐” holds for all process. I will prove “⇒” assuming that p has the property that for any σ ∈ Act^{∗} there are only finitely many ready pairs ^{/} \σ, X^{\} / ∈ R(p). This property (call it RIF ) is clearly implied by image finiteness. So suppose p has the RIF property and AR(p) = AR(q). I will show that R(p) = R(q).

Suppose ^{/} \σ, Y ^{\} / ∉ R(p). By RIF there are only finitely many ready pairs ^{/} \σ, X_{i}^{\} / ∈ R(p). For each of them choose an action a_{i} ∈ Y − X_{i} or b_{i} ∈ X_{i} − Y. Let U be the set of all those a_{i}’s, and V the set of the b_{i}’s. Then ^{/} \σ, U, V ^{\} / ∉ AR(p) = AR(q) and hence ^{/} \σ, Y ^{\} / ∉ R(q).

It follows that R(q) ⊆ R(p), and thus q has the property RIF as well. Now the same argument applies in the other direction, yielding R(p) ⊆ R(q). □

Inspired by the definition of R^{−}, a finite version of ready trace semantics (RT^{−}) can be defined likewise. Here I will just give its modal characterization.

Definition 7.6 The set L_{RT}^{−} of finite ready trace formulas over Act is given by:

• ⊤ ∈ L_{RT}^{−}.

• If φ ∈ L_{RT}^{−} and X ⊆_{fin} Act then Xφ ∈ L_{RT}^{−} and X̃φ ∈ L_{RT}^{−}.

• If φ ∈ L_{RT}^{−} and a ∈ Act then aφ ∈ L_{RT}^{−}.

The satisfaction relation ⊧ ⊆ IP × L_{RT}^{−} is given by the usual clauses for ⊤ and aφ, and:

• p ⊧ Xφ if X ⊆ I(p) and p ⊧ φ.

• p ⊧ X̃φ if I(p) ∩ X = ∅ and p ⊧ φ.

Processes p and q are finite-ready trace equivalent, notation p =_{RT}^{−} q, if ∀φ ∈ L_{RT}^{−} (p ⊧ φ ⇔ q ⊧ φ).

As these formulas are expressible in terms of the ones of Definition 6.2, one has RT^{−} ≺ RT; Counterexample 4 shows that the inclusion is strict. Also F T^{−} ≺ RT^{−} and F^{−} ≺ R^{−} ≺ RT^{−}.

Proposition 7.6 Let p, q ∈ IP and p is image finite. Then p =_{RT}^{−} q ⇔ p =_{RT} q. Proof: “⇐” holds for all process. “⇒” follows just as in Proposition 7.5, using the property that for any a_{1}a_{2} ⋯ a_{n} ∈ Act^{ω} there are only finitely many normal ready traces X_{0}a_{1}X_{1}a_{2} ⋯ a_{n}X_{n} ∈ RT_{N}(p). □

Unlike the semantics T to RT, possible-futures semantics distinguishes between the two processes of Counterexample 1: ^{/} \a, a^{∗}^{\} / ∈ PF (right) − PF (left). Still, T^{∞} ⊀ PF , as can be seen from the variant of Counterexample 1 in which the left-hand process is appended to the endnodes of both processes. The so obtained systems have the same possible futures, including {^{/} \a^{n}, a^{∗}^{\} / | n ∈ IN}, but only the right-hand side has an infinite trace.

For the sake of completeness I include a definition of infinitary possible-futures semantics (PF^{∞}), such that PF ≺ PF^{∞} and R^{∞} ≺ PF^{∞}. A finite variant of PF has not been explored.

Definition 7.7 ^{/} \σ, X^{\} / ∈ Act^{∗} × P(Act^{∗}) is an infinitary possible future of a process p if there is a process q such that p ⟶^{σ} q and T (q)∪T^{∞}(q) = X. Let PF^{∞}(p) denote the set of infinitary possible futures of p. Two processes p and q are infinitary possible-futures equivalent, notation p =_{PF}^{∞} q, if PF^{∞}(p) = PF^{∞}(q).

8 Simulation semantics

The following concept of simulation occurs frequently in the literature (see e.g. Park [41]).

Definition 8 A simulation is a binary relation R on processes, satisfying, for a ∈ Act:

• if pRq and p ⟶^{a} p′, then ∃q′ : q ⟶^{a} q′ and p′Rq′.

Process p can be simulated by q, notation p \underrightarrow{⊂} q, if there is a simulation R with pRq. p and q are similar, notation p \overrightarrow{←} q, if p \underrightarrow{⊂} q and q \underrightarrow{⊂} p.

Proposition 8.1 Similarity is an equivalence relation on the domain of processes. Proof: Symmetry is immediate, so it has to be checked that p \underrightarrow{⊂} p, and p \underrightarrow{⊂} q ∧ q \underrightarrow{⊂} r ⇒ p \underrightarrow{⊂} r.

• The identity relation is a simulation with pRp.

• If R is a simulation with pRq and S is a simulation with qSr, then the relation R;S, defined by x(R;S)z iff ∃y : xRy ∧ ySz, is a simulation with p(R;S)r. □

Hence the relation will be called simulation equivalence. In simulation semantics (S) two processes are identified iff they are simulation equivalent.

Testing scenario and modal characterization The testing scenario for simulation semantics resembles that for trace semantics, but in addition the observer is, at any time during a run of the investigated process, capable of making arbitrary many copies of the process in its present state and observe them independently. Thus an observation yields a tree rather than a sequence of actions. Such a tree can be coded as an expression in a simple modal language.

Definition 8.1 The class L_{S} of simulation formulas over Act is defined recursively by:

• If I is a set and φ_{i} ∈ L_{S} for i ∈ I then ⋀_{i∈I} φ_{i} ∈ L_{S}.

• If φ ∈ L_{S} and a ∈ Act then aφ ∈ L_{S}.

The satisfaction relation ⊧ ⊆ IP × L_{S} is defined recursively by:

• p ⊧ ⋀_{i∈I} φ_{i} if p ⊧ φ_{i} for all i ∈ I.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

Let S(p) denote the class of simulation formulas satisfied by the process p: S(p) = {φ ∈ L_{S} | p ⊧ φ}. Write p ⊑_{S} q if S(p) ⊆ S(q) and p =_{S} q if S(p) = S(q).

Write ⊤ for ⋀_{i∈∅} φ_{i}, and φ_{1} ∧ φ_{2} for ⋀_{i∈{1,2}} φ_{i}. It turns out that L_{T} is a sublanguage of L_{S}.

Proposition 8.2 p \underrightarrow{⊂} q ⇔ p ⊑_{S} q. Hence p \overrightarrow{←} q ⇔ p =_{S} q. Proof: For “⇒” I have to prove that for any simulation R and for all φ ∈ L_{S} one has

pRq ⇒ (p ⊧ φ ⇒ q ⊧ φ).

I will do so with structural induction on φ. Suppose pRq.

– Let p ⊧ aφ. Then there is a p′ ∈ IP with p ⟶^{a} p′ and p′ ⊧ φ. As R is a simulation, there must be a q′ ∈ IP with q ⟶^{a} q′ and p′Rq′. So by induction q′ ⊧ φ, and hence q ⊧ aφ.

– p ⊧ ⋀_{i∈I} φ_{i} ⇔ ∀i∈I(p ⊧ φ_{i}) ⟹^{ind.} ∀i∈I(q ⊧ φ_{i}) ⇔ q ⊧ ⋀_{i∈I} φ_{i}.

For “⇐” it suffices to establish that ⊑_{S} is a simulation. Suppose p ⊑_{S} q and p ⟶^{a} p′. I have to show that ∃q′ ∈ IP with q ⟶^{a} q′ and p′ ⊑_{S} q′. Let Q′ be

{q′ ∈ IP | q ⟶^{a} q′ ∧ p′ ⋢_{S} q′}.

By Definition 1.1 Q′ is a set. For every q′ ∈ Q′ there is a formula φ_{q′} ∈ S(p′) − S(q′). Now

a ⋀_{q′∈Q′} φ_{q′} ∈ S(p) ⊆ S(q),

so there must be a q′ ∈ IP with q ⟶^{a} q′ and q′ ∉ Q′, which had to be shown. □

Process graph characterization Simulation equivalence can also be characterized by means of relations between the nodes of two process graphs, rather than between process graphs themselves.

Definition 8.2 Let g, h ∈ ^{|}G. A simulation of g by h is a binary relation R ⊆ nodes(g)×nodes(h), satisfying:

• root(g)Rroot(h).

• If sRt and (s, a, s′) ∈ edges(g), then there is an edge (t, a, t′) ∈ edges(h) such that s′Rt′.

This definition is illustrated in Figure 5. Solid lines indicates what is assumed, dashed lines what is required. It follows easily that g \underrightarrow{⊂} h iff there exists a simulation of g by h.

a  a

Figure 5: A simulation

For process graphs with multiple roots, the first requirement of Definition 8.2 generalizes to

• ∀s ∈ roots(g) ∃t ∈ roots(h) : sRt.

Classification Simulation semantics (S) is finer than trace semantics (T ≺ S), but independent of CT, F, R, F T, RT and PF . Proof: “T ⪯ S” follows since L_{T} is a sublanguage of L_{S}. “S ⪰̸ CT ” (and hence “S ⪰̸ RT ”, “S ⪰̸ PF ” etc.) follows from Counterexample 2. There left ≠_{CT} right, although left \overrightarrow{←} right; the construction of the two simulations is left to the reader. “S ⪯̸ RT ” (and hence “S ⪯̸ T ” etc.) follows from Counterexample 8. There RT (left) = RT (left), but S(left) ≠ S(left). The first statement follows from Proposition 6.3 and the insight that it suffices to check the two ready traces contributed by the maximal paths; these are the same for both graphs. The second statement follows since a(bc⊤ ∧ bd⊤) ∈ S(right) − S(left). “S ⪯̸ PF ” follows from Counterexample 7, where PF (left) = PF (right) but S(left) ≠ S(left). The latter statement follows since a(b⊤ ∧ a(b⊤ ∧ cd⊤)) ∈ S(left) − S(right). □

a  a b  b c  d abc + abd  =_{PW} =_{RT} ≠_{S}  a b  b c  d a(bc + bd)

Counterexample 8: Possible worlds and ready trace equivalent, but not simulation equivalent

Infinite processes In order to make the testing scenario match its formalization in terms of the modal language L_{S} even for infinite processes, one has to assume that the amount of copies one can make at any time is infinite. Moreover, although no single copy can be tested forever, due to its infinite branching there may be no upperbound upon the duration of an observation.

One might consider an even more infinitary testing scenario by allowing observations to go on forever on some or all of the copies. However, this would not give rise to a more discriminating equivalence; ordinary simulation equivalences already preserves infinite traces.

Proposition 8.3 If p \underrightarrow{⊂} q then T^{∞}(p) ⊆ T^{∞}(q). Hence T^{∞} ≺ S. Proof: Suppose R is a simulation with p_{0}Rq_{0} and a_{1}a_{2} ⋯ ∈ T^{∞}(p_{0}). Then there are p_{1}, p_{2}, ... such that p_{0} ⟶^{a_{1}} p_{1} ⟶^{a_{2}} · · ·. With induction on i ∈ IN it follows that there are processes q_{i+1} such that

q_{i} − −^{a_{i+1}} → q_{i+1} and p_{i+1}Rq_{i+1}. Hence a_{1}a_{2} ⋯ ∈ T^{∞}(q_{0}). □

The most radical way to make the testing scenario finitary, is to allow only finitely many copies to be made in any state of the process. This also puts an upperbound on the duration of any observation. Observations can now be modelled with simulation formulas in which the index sets I of the first clause of Definition 8.1 are always finite. The modal language containing such simulation formulas can equivalently be defined by splitting the construction ⋀_{i∈I} into ⊤ and ∧.

Definition 8.3 The set L_{S}^{∗} of finitary simulation formulas over Act is defined recursively by:

• ⊤ ∈ L_{S}^{∗}.

• If φ, ψ ∈ L_{S}^{∗} then φ ∧ ψ ∈ L_{S}^{∗}.

• If φ ∈ L_{S}^{∗} and a ∈ Act then aφ ∈ L_{S}^{∗}.

The satisfaction relation ⊧ ⊆ IP × L_{S}^{∗} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ φ ∧ ψ if p ⊧ φ and p ⊧ ψ.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

Let S^{∗}(p) denote the set of all finitary simulation formulas that are satisfied by the process p: S^{∗}(p) = {φ ∈ L_{S}^{∗} | p ⊧ φ}. Two processes p and q are finitary simulation equivalent, notation p =_{S}^{∗} q, if S^{∗}(p) = S^{∗}(q).

In contrast, the equivalence \overrightarrow{←} of Definition 8 is then infinitary simulation equivalence. Note however, that contrary to the previous equivalences surveyed, the default version (the one meant when leaving out the adjective “finitary” or “infinitary”) is the infinitary one. In general, I use the superscript ∗ for finitary versions and ∞ for infinitary versions. However, for the trace oriented equivalences (Sections 2–7) I leave out the ∗, and for the simulation oriented equivalences (Sections 8–12) I leave out the ∞.

The next proposition, and hence also the essence of Proposition 8.2, stems from in Hennessy & Milner [28]. It states that for image finite processes finitary and infinitary simulation equivalence coincide.

Proposition 8.4 Let p, q ∈ IP be image finite processes. Then p \overrightarrow{←} q ⇔ p =_{S}^{∗} q. Proof: Exactly as the proof of Proposition 8.2, but for “⇐” one shows that the relation ⊑_{S}^{i.f.} given by p ⊑_{S}^{i.f.} q iff p ⊑_{S} q and q is image finite is a simulation, using that, as q is image finite, Q′ must be finite. □

In fact, this proposition is a special case of the following one, which is proved likewise.

Proposition 8.5 Let S_{κ}(p) denote the set of all simulation formulas satisfied by p in which all index sets have cardinality less than κ. Let p, q ∈ IP and assume |{q′ | q ⟶^{σ} q′}| < κ for each σ ∈ Act^{∗}. Then p \underrightarrow{⊂} q ⇔ S_{κ}(p) ⊆ S_{κ}(q). □

Although only q needs to be image finite in order to obtain p \underrightarrow{⊂} q ⇔ p ⊑_{S}^{∗} q, Counterexample 12 will show that both p and q need to be image finite in the statement of Proposition 8.4.

A less radical way to finitize the testing scenario for simulation semantics is to allow infinitely many copies to be made in any state of the process, but put a finite upperbound on the duration of any observation. Observations can then be modelled with simulation formulas in which the index sets can be arbitrary, but there is a finite upperbound on the nesting of the construction aφ of the second clause of Definition 8.1.

Definition 8.4 Let L_{S}^{ω} = ⋃_{n=0}^{∞} L_{S}^{n}, where L_{S}^{n} is given by:

• If I is a set and φ_{i} ∈ L_{S}^{n} for i ∈ I then ⋀_{i∈I} φ_{i} ∈ L_{S}^{n}.

• If φ ∈ L_{S}^{n} and a ∈ Act then aφ ∈ L_{S}^{n+1}.

Let S^{ω}(p) = {φ ∈ L_{S}^{ω} | p ⊧ φ} and write p =_{S}^{ω} q if S^{ω}(p) = S^{ω}(q).

Now p =_{S} q ⇒ p =_{S}^{ω} q ⇒ p =_{S}^{∗} q, and for image finite processes all three equivalences coincide. For image infinite processes both implications are strict, as illustrated by Counterexamples 9 and 1.

compare the processes with and without the left branch a b 1  b 2 b 3b 4 ⋯  =_{RB}^{∗} ≠_{S}^{ω}  a b 2 b 3b 4 ⋯  a b 1  b 3b 4 ⋯ a  b 1  b 2 b 4 ⋯  · · · . . .

Counterexample 9: Finitary equivalent, but not S^{ω}-equivalent

In Counterexample 9 S^{∗}(with) = S^{∗}(without), yet a ⋀_{i=1}^{∞} bi⊤ ∈ S^{ω}(with) − S^{ω}(without). In Counterexample 1 S^{ω}(left) = S^{ω}(right), yet right \underrightarrow{⊄} left. For the first statement, let φ ∈ L_{S}^{ω}. Then there is an n such that φ ∈ L_{S}^{n}. Now parts of trees that are further than n edges away from the root play no rôle in the satisfaction relation for φ. Thus, the validity of φ remains unchanged if in both trees all paths are cut off after n steps. However, the cut versions of both trees are isomorphic, and hence satisfy the same formulas (cf. Corollary 12.1). The second statement follows immediately from Proposition 8.3.

It follows that T ≺ S^{∗} ≺ S^{ω} ≺ S and T ≺ T^{∞} ≺ S, whereas T^{∞} is incomparable with S^{∗} and S^{ω}. Moreover, S^{∗}, S^{ω} and S are incomparable with the semantics ranging from CT or F^{−} to RT^{∞}.

9 Ready simulation semantics

Testing scenario Of course one can also combine the copying facility with any of the other testing scenarios. The observer can then plan experiments on one of the machines from the Sections 3 to 7 together with a replicator, an ingenious device by which one can replicate the machine whenever and as often as one wants. In order to represent observations, the modal languages from Sections 3 to 7 need to be combined with the one from Section 8.

Definition 9 The language L_{CS} and the corresponding satisfaction relation is defined recursively by combining the clauses of Definition 3.1 (for L_{CT} ) with those of Definition 8.1 (for L_{S} ). Likewise, L_{FS} is obtained by combining L_{F} and L_{S} ; L_{FTS} by combining L_{FT} and L_{S} ; L_{RS} by combining L_{R} and L_{S} ; and L_{RTS} by combining L_{RT} and L_{S} . For p ∈ IP and O ∈ {CS, FS, FTS, RS, RTS} let O(p) = {φ ∈ L_{O} | p ⊧ φ}. Two processes p, q ∈ IP are

• completed simulation equivalent, notation p =_{CS} q, if CS(p) = CS(q);

• failure simulation equivalent, notation p =_{FS} q, if FS(p) = FS(q);

• failure trace simulation equivalent, notation p =_{FTS} q, if FTS(p) = FTS(q);

• ready simulation equivalent, notation p =_{RS} q, if RS(p) = RS(q);

• ready trace simulation equivalent, notation p =_{RTS} q, if RTS(p) = RTS(q).

It is obvious that failure trace simulation equivalence coincides with failure simulation equivalence and ready trace simulation equivalence with ready simulation equivalence (p ⊧ Xφ ⇔ p ⊧ X ∧ φ). Also it is not difficult to see that failure simulation equivalence and ready simulation equivalence coincide (p ⊧ X ⇔ p ⊧ Ỹ ∧ ⋀_{a∈X} a⊤, where Y = Act − X). So one has

Proposition 9.1 p =_{FS} q ⇔ p =_{FTS} q ⇔ p =_{RTS} q ⇔ p =_{RS} q. □

Relational characterizations The two remaining equivalences can be characterized as follows:

Definition 9.1 A complete simulation is a binary relation R on processes, satisfying, for a ∈ Act:

• if pRq and p ⟶^{a} p′, then ∃q′ : q ⟶^{a} q′ and p′Rq′;

• if pRq then I(p) = ∅ ⇔ I(q) = ∅.

Proposition 9.2 Two processes p and q are completed simulation equivalent if there exists a complete simulation R with pRq and a complete simulation S with qSp. Proof: A trivial modification of the proof of Proposition 8.2. □

Definition 9.2 A ready simulation is a binary relation R on processes, satisfying, for a ∈ Act:

• if pRq and p ⟶^{a} p′, then ∃q′ : q ⟶^{a} q′ and p′Rq′;

• if pRq then I(p) = I(q).

Proposition 9.3 Two processes p and q are ready simulation equivalent if there exists a ready simulation R with pRq and a ready simulation S with qSp. Proof: A trivial modification of the proof of Proposition 8.2. □

A variant of ready simulation equivalence was originally proposed by Bloom, Istrail & Meyer [12] under the name GSOS trace congruence; they provided a modal characterization, to be discussed in Section 10. A relational characterization was first given by Larsen & Skou [35] under the name \frac{2}{3}-bisimulation equivalence. A \frac{2}{3}-bisimulation is defined just like a ready simulation, except that the second clause reads “if pRq and ∃q′ : q ⟶^{a} q′ then ∃p′ : p ⟶^{a} p′”. This is clearly equivalent.

Classification RT ≺ RS, CT ≺ CS and S ≺ CS ≺ RS. CS is independent of F to RT. Proof: “RT ⪯ RS” follows since L_{RT} is a sublanguage of L_{RTS} , using Proposition 9.1. “CT ⪯ CS” and “S ⪯ CS ⪯ RS” follow since L_{CT} and L_{S} are sublanguages of L_{CS} , which is a sublanguage of L_{FS} . “RT ⪰̸ RS” follows from Counterexample 8, using “RS ⪰ S”; similarly RT ⪰̸ CS and CT ⪰̸ CS. “S ⪰̸ CS” follows from Counterexample 2, using “CS ⪰ CT ”. “CS ⪰̸ F ” (and hence “CS ⪰̸ RS”) follows from Counterexample 3, in which F (left) ≠ F (right) but left =_{CS} right; the construction of the two complete simulations is left to the reader. □

Proposition 9.4 PF is incomparable with CS and RS. Proof: “CS ⪯̸ PF ” (and hence “RS ⪯̸ PF ”) follows from Counterexample 7, using “CS ⪰ S”.

• a  a b  b  b c  c  d abc + a(bc + bd)  =_{RS} ≠_{PF}  • a b  b c  d a(bc + bd)

Counterexample 10: Ready simulation equivalent, but not possible-futures equivalent

“RS ⪰̸ PF ” (and hence “CS ⪰̸ PF ”) follows from Counterexample 10, which shows two graphs that are ready simulation equivalent but not possible-futures equivalent. Concerning the first claim, note that there exists exactly one simulation of right by left, namely the one mapping right on the right-hand side of left. There also exists exactly one simulation of left by right, which relates the red (or shaded) node on the left to the red (or shaded) shaded node on the right. Both simulations are ready simulations, as related nodes have the same menu of initial actions. The second claim follows since ^{/} \a, {ε, b, bc}^{\} / ∈ PF (left) − PF (right). □

Infinite processes For each of the semantics CS, FS, FTS, RS and RTS a finitary variant (superscripted with a *), motivated by allowing finite replication only, is defined by combining the modal languages L_{CT} , L_{F} , L_{FT} , L_{R} and L_{RT} , respectively, with L_{S}^{∗}. Likewise, an intermediate variant (superscripted with an ω), motivated by requiring any observation to be over within a finite amount of time, is defined by combining these languages with L_{S}^{ω}. Finally, a finite variant (superscripted with a −), motivated by observers that can only engage in finite replication, can only set finitely many switches on free, and can only inspect finitely many lamps in a finite time, is obtained by combining the (obvious) modal languages L_{F}^{−}, L_{FT}^{−}, L_{R}^{−} and L_{RT}^{−} with L_{S}^{∗} (there is no CS^{−}). Exactly as in the case of Proposition 9.1 one finds:

Proposition 9.5 FS^{ω} = FTS^{ω} = RTS^{ω} = RS^{ω} and FS^{−} = FTS^{−} = RTS^{−} = RS^{−}. Moreover, FS^{∗} = FTS^{∗} and RTS^{∗} = RS^{∗}. □

However, as pointed out in Schnoebelen [47], FS^{∗} and RS^{∗} are different: in Counterexample 11

compare the processes with and without the left branch a 1 2 3 4  ...  =_{FB}^{∗} ≠_{R}  a 2 3 4  ...  a 1 3 4  ... a  1 2 4  ...  ... . . .

Counterexample 11: Finitary failure simulation equivalent, but not ready equivalent

one has FS^{∗}(with) = FS^{∗}(without), but ^{/} \a, {1, 2, ...}^{\} / ∈ R(with) − R(without).

Clearly one has CS^{∗} ≺ CS^{ω} ≺ CS and RS^{−} ≺ FS^{∗} ≺ RS^{∗} ≺ RS^{ω} ≺ RS. The strictness of these inclusions is given by Counterexamples 4, 11, 9 and 1. In addition one has RT^{−} ≺ RS^{−}, S^{∗} ≺ RS^{−}, RT ≺ RS^{∗}, FT ≺ FS^{∗}, CT ≺ CS^{∗} and S^{∗} ≺ CS^{∗} ≺ FS^{∗}; as well as RT^{∞} ≺ RS, CT^{∞} ≺ CS, S^{ω} ≺ CS^{ω} ≺ RS^{ω} and S ≺ CS ≺ RS. Counterexamples against further inclusions have already been provided.

Proposition 9.6 Let p, q ∈ IP be image finite. Then p =_{CS} q ⇔ p =_{CS}^{∗} q and p =_{RS} q ⇔ p =_{RS}^{−} q. Proof: Two trivial modifications of the proof of Proposition 8.4. In the second one, one uses that if ∀φ ∈ L_{RS}^{−}(p ⊧ φ ⇒ q ⊧ φ) then surely I(p) = I(q). □

In fact, if it is merely known that only q is image finite it follows already that p ⊑_{CS} q ⇔ p ⊑_{CS}^{∗} q and p ⊑_{RS} q ⇔ p ⊑_{RS}^{−} q. However, the following variant of Counterexample 1 shows that in the statement of Proposition 9.6 it is essential that both p and q are image finite. In Counterexample 12 right is image finite—in fact, it is even finitely branching—but left is not. It turns out that left =_{RS}^{ω} right (and hence left =_{RS}^{−} right, left =_{CS}^{∗} right, left =_{RT} right, left =_{F} right, etc.) but left ≠_{T}^{∞} right (and hence left ≠_{F}^{∞} right, left ≠_{RT}^{∞} right, left ≠_{CS} right, left ≠_{RS} right, etc.).

a  a a a a a a a  a  a  ...  a aa  a =_{RS}^{ω} ≠_{T}^{∞}

Counterexample 12: Finitary ready simulation equivalent but not infinitary equivalent

For general (non-image-finite) processes, no relational characterizations of the finite, finitary and intermediate equivalences are known.

Testing scenario An alternative and maybe more natural testing scenario for finitary ready simulation semantics (or simulation semantics) can be obtained by exchanging the replicator for an undo-button on the (ready) trace machine (Figure 6). It is assumed that all intermediate states

a· _{b}· _{⋯}  _{z}·  _{c}  _{•}_{undo}

Figure 6: The ready simulation machine

that are past through during a run of a process are stored in a memory inside the black box. Now pressing the undo-button causes the machine to shift one state backwards. In the initial state pressing the button has no effect. An observation now consists of a (ready) trace, enriched with undo-actions. Such observations can easily be translated into finitary (ready) simulation formulas.

10 Reactive versus generative testing scenarios

In the testing scenarios presented so far, a process is considered to perform actions and make choices autonomously. The investigated behaviours can therefore be classified as generative processes. The observer merely restricts the spontaneous behaviour of the generative machine by cutting off some possible courses of action. An alternative view of the investigated processes can be obtained by considering them to react on stimuli from the environment and be passive otherwise. Reactive machines can be obtained out of the generative machines presented so far by replacing the switches by buttons and the display by a green light. Initially the process waits patiently until the observer

a •  b•  ⋯  z•  • undo

Figure 7: The reactive ready simulation machine

tries to press one of the buttons. If the observer tries to press an a-button, the machine can react in two different ways: if the process can not start with an a-action the button will not go down and the observer may try another one; if the process can start with an a-action it will do so and the button goes down. Furthermore the green light switches on. During the execution of a no buttons can be pressed. As soon as the execution of a is completed the light switches off, so that the observer knows that the process is ready for a new trial. Reactive machines as described above originate from Milner [37, 38].

One family of testing scenarios with reactive machines can be obtained by allowing the observer to try to depress more than one button at a time. In order to influence a particular choice, the observer could already start exercising pressure on buttons during the execution of the preceding action (when no button can go down). When this preceding action is finished, at most one of the buttons will go down. These testing scenarios are equipotent with the generative ones: putting pressure on a button is equivalent to setting the corresponding switch on ‘free’; moreover an action a appearing in the display is mimicked by the a-button going down, and the disappearance of a from the display by the green light going off.

Another family of testing scenarios is obtained by allowing the user to try only one button at a time. They are equipotent with those generative testing scenarios in which at any time only one switch can be set on ‘free’. Next I will discuss the equivalences that originate from these scenarios.

First consider the reactive machine that resembles the failure trace machine, thus without menulights and undo-button. An observation on such a machine consists of a sequence of accepted and refused actions, indicating which buttons went down in a sequence of trials of the user. Such a sequence can be seen as a failure trace where all refusal sets are singletons. Call the resulting semantics F T^{1}. Clearly, the failure trace set of any process p satisfies

σ(X ∪ Y)ρ ∈ F T (p) ⇔ σXY ρ ∈ F T (p).

Thus, any failure trace σ{a_{1}, …, a_{n}}ρ can be rewritten as (contains the same information as) σ{a_{1}}{a_{2}} ⋯ {a_{n}}ρ. It follows that the singleton-failure trace set F T^{1}(p) of a process p contains as much information as its finite-failure trace set F T^{−}(p), so the semantics F T^{1} coincides with F T^{−}.

In order to arrive at a reactive counterpart to failures semantics, one could suppose that an observer continues an experiment only as long as all buttons he tries to depress actually go down; when a button refuses to go down, he will not try another one. This testing scenario gives rise to the variant F^{1} of failures semantics in which all refusal sets are singletons.

Definition 10 ^{/} \σ, a^{\} / ∈ Act^{∗} × Act is a singleton-failure pair of a process p if there is a process q such that p ⟶^{σ} q and a ∉ I(q). Let F^{1}(p) denote the set of singleton-failure pairs of p. Two processes p and q are singleton-failures equivalent, p =_{F}^{1} q, if T (p) = T (q) and F^{1}(p) = F^{1}(q).

Unlike for F and F^{−}, F^{1}(p) = F^{1}(q) does not always imply that T (p) = T (q), so one has to keep track of traces explicitly. These model observations ended by the observer before stagnation occurs.

Singleton-failures semantics (F^{1}) is situated strictly between trace (T) and finite-failures semantics (F^{−}). For Counterexample 2 shows two processes with T (left) = T (right) but ^{/} \a, b^{\} / ∈ F^{1}(left) − F^{1}(right), and Counterexample 13 shows two processes with F^{1}(left) = F^{1}(right) (both contain ^{/} \a, b^{\} / and ^{/} \a, c^{\} /), but ^{/} \a, {b, c}^{\} / ∈ F (left) − F (right). Furthermore, F^{1} is independent of CT, S and CS, for in Counterexample 13 one has CT (left) ≠ CT (right), in Counterexample 8 one has left =_{F}^{1} right but left ≠_{S} right, and in Counterexample 3 one has left =_{CS} right but / \a, c^{\} / ∈ F^{1}(left) − F^{1}(right).

Adding the undo-button to the reactive failure trace machine gives a semantics FS^{1} characterized by the modal language L_{S}^{∗} to which has been added a modality “Can’t(a)”, with p ⊧ Can’t(a) iff a ∉ I(p). This modality denotes a failed attempt to depress the a-button. If fact, Bloom, Istrail & Meyer studied the coarsest equivalence finer than trace equivalence that is a congruence

a  a a b  c ab + a + ac  =_{F}^{1} ≠_{CT} ≠_{F}^{−}  a b  a c ab + ac

Counterexample 13: Singleton-failures equivalent, but not completed trace or failures equivalent

for the class of so-called GSOS-operators, and characterized this GSOS trace congruence by the modal language above; its formulas were called denial formulas. As in the modal language L_{FS}^{−} one has p ⊧ X̃ ∪ Y ⇔ p ⊧ X̃ ∧ Ỹ, and Can’t(a) is the same as ˜{a}, it follows that the language of denial formulas is equally expressive as L_{FS}^{−}, and hence FS^{1} coincides with FS^{−} and RS^{−}.

If the menu-lights are added to the reactive failure trace machine considered above one can observe ready trace sets, and the green light is redundant. Likewise, adding menu-lights to the reactive failure scenario would give readiness semantics, and adding them to the reactive failure simulation machine would yield ready simulation. If the green light (as well as the menu-lights) are removed from the reactive failure trace machine, one can only test trace equivalence, since any refusal may be caused by the last action not being ready yet. Likewise, removing the green light from the reactive failure simulation machine (with undo-button) yields (finitary) simulation semantics. Reactive machines on which only one button at a time is depressed appear to be unsuited for testing completed trace, completed simulation and failures equivalence.

11 2-nested simulation semantics

2-nested simulation equivalence popped up naturally in Groote & Vaandrager [25] as the coarsest congruence with respect to a large and general class of operators that is finer than completed trace equivalence.

Definition 11 A 2-nested simulation is a simulation contained in simulation equivalence (\overrightarrow{←}). Two processes p and q are 2-nested simulation equivalent, notation p =_{2S} q, if there exists a 2-nested simulation R with pRq and a 2-nested simulation S with qSp.

Modal characterization A modal characterization of this notion is obtained by the fragment of the infinitary Hennessy-Milner logic (cf. Definition 12.1) without nested negations.

Definition 11.1 The class L_{2S} of 2-nested simulation formulas over Act is defined recursively by:

• If I is a set and φ_{i} ∈ L_{2S} for i ∈ I then ⋀_{i∈I} φ_{i} ∈ L_{2S} .

• If φ ∈ L_{2S} and a ∈ Act then aφ ∈ L_{2S} .

• If φ ∈ L_{S} then ¬φ ∈ L_{2S} .

Note that L_{S} ⊆ L_{2S} . The satisfaction relation ⊧ ⊆ IP × L_{2S} is defined recursively by:

• p ⊧ ⋀_{i∈I} φ_{i} if p ⊧ φ_{i} for all i ∈ I.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

• p ⊧ ¬φ if p |̸= φ.

Proposition 11.1 p =_{2S} q ⇔ ∀φ ∈ L_{2S} (p ⊧ φ ⇔ q ⊧ φ). Proof: A trivial modification of the proof of Proposition 8.2. □

Testing scenario In order to obtain a testing scenario for this equivalence one has to introduce the rather unnatural notion of a lookahead [25]: The 2-nested simulation machine is a variant of the ready trace machine with replicator, where in an idle state the machine not only tells which actions are on the menu, but even which simulation formulas are (not) satisfied in the current state.

Classification RS ≺ 2S and PF ≺ 2S. Proof: For “RS ⪯ 2S” it suffices to show that each 2-nested simulation is a ready simulation. This follows since p \overrightarrow{←} q ⇒ I(p) = I(q). PF ≺ 2S is easily established using that T ≺ S. That both inclusions are strict follows immediately from the fact that RS and PF are incomparable (Proposition 9.4). □

Infinite processes Exactly as for ready simulations semantics, 5 versions of 2-nested simulation semantics can be defined that differ for infinite processes. 2S^{−} is the semantics whose modal characterization has the constructs ⊤, ∧, aφ and ¬φ′ with φ′ ∈ L_{S}^{∗}. The constructs X̃ and X for X ⊆_{fin} Act are expressible in this logic. F2S^{∗} additionally has the construct X̃, and R2S^{∗} the construct X, for X ⊆ Act. Finally 2S^{ω} is characterized by the class of 2-nested simulation formulas with a finite upperbound on the nesting of the aφ construct. The constructs X̃ and X for X ⊆ Act are expressible in L_{2S}^{ω}, and hence also in L_{2S} .

We have 2S^{−} ≺ F2S^{∗} ≺ R2S^{∗} ≺ 2S^{ω} ≺ 2S. The strictness of these inclusions is given by Counterexamples 4, 11, 9 and 1. In addition one has RS^{−} ≺ 2S^{−}, FS^{∗} ≺ F2S^{∗}, RS^{∗} ≺ R2S^{∗}, RS^{ω} ≺ 2S^{ω} and RS ≺ 2S; as well as PF^{∞} ≺ 2S. Counterexample 1 shows that PF ⊀ 2S^{ω}: 2S^{ω}(left) = 2S^{ω}(right) (cf. Proposition 12.10), but ^{/} \a, a^{∗}^{\} / ∈ PF (right) − PF (left).

Proposition 11.2 Let p, q ∈ IP be image finite. Then p =_{2S} q ⇔ p =_{2S}^{−} q. Proof: An easy modification of the proof of Proposition 8.4, also using its result. □

12 Bisimulation semantics

The concept of bisimulation equivalence stems from Milner [37]. Its formulation below is due to Park [41].

Definition 12 A bisimulation is a binary relation R on processes, satisfying, for a ∈ Act:

• if pRq and p ⟶^{a} p′, then ∃q′ : q ⟶^{a} q′ and p′Rq′;

• if pRq and q ⟶^{a} q′, then ∃p′ : p ⟶^{a} p′ and p′Rq′.

Two processes p and q are bisimilar, notation p\underline{↔} q, if there exists a bisimulation R with pRq.

The relation \underline{↔} is again a bisimulation. As for similarity, one easily checks that bisimilarity is an equivalence relation on IP. Hence the relation will be called bisimulation equivalence. In bisimulation semantics (B) two processes are identified iff they are bisimulation equivalent. Note that the concept of bisimulation does not change if in the definition above the action relations ⟶^{a} were replaced by generalized action relations ⟶^{σ}.

Modal characterization

Definition 12.1 The class L_{B} of infinitary Hennessy-Milner formulas over Act is defined by:

• If I is a set and φ_{i} ∈ L_{B} for i ∈ I then ⋀_{i∈I} φ_{i} ∈ L_{B}.

• If φ ∈ L_{B} and a ∈ Act then aφ ∈ L_{B}.

• If φ ∈ L_{B} then ¬φ ∈ L_{B}.

The satisfaction relation ⊧ ⊆ IP × L_{B} is defined recursively by:

• p ⊧ ⋀_{i∈I} φ_{i} if p ⊧ φ_{i} for all i ∈ I.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

• p ⊧ ¬φ if p |̸= φ.

Let B(p) denote the class of all infinitary Hennessy-Milner formulas satisfied by the process p: B(p) = {φ ∈ L_{B} | p ⊧ φ}. Write p ⊑_{B} q if B(p) ⊆ B(q) and p =_{B} q if B(p) = B(q).

Proposition 12.1 p ⊑_{B} q ⇔ p =_{B} q. Proof: If φ ∈ B(q) − B(p) then ¬φ ∈ B(p) − B(q). □

Proposition 12.2 p\underline{↔} q ⇔ p =_{B} q. Proof: For “⇒” I have to prove that for any bisimulation R and for all φ ∈ L_{B} one has

pRq ⇒ (p ⊧ φ ⇔ q ⊧ φ).

I will do so with structural induction on φ. Suppose pRq.

– Let p ⊧ aφ. Then there is a p′ ∈ IP with p ⟶^{a} p′ and p′ ⊧ φ. As R is a bisimulation, there must be a q′ ∈ IP with q ⟶^{a} q′ and p′Rq′. So by induction q′ ⊧ φ, and hence q ⊧ aφ. By symmetry one also obtains q ⊧ aφ ⇒ p ⊧ aφ.

– p ⊧ ⋀_{i∈I} φ_{i} ⇔ ∀i∈I(p ⊧ φ_{i}) ⟺^{ind.} ∀i∈I(q ⊧ φ_{i}) ⇔ q ⊧ ⋀_{i∈I} φ_{i}.

– p ⊧ ¬φ ⇔ p |̸= φ ⟺^{ind.} q |̸= φ ⇔ q ⊧ ¬φ.

For “⇐” it suffices to establish that ⊑_{B} is a simulation (Proposition 12.1 then implies that =_{B} = ⊑_{B} = ⊑_{B}^{−1} is a bisimulation). This goes exactly as in the proof of Proposition 8.2. □

Testing scenario The testing scenario for bisimulation semantics, as presented in Milner [37], is the oldest and most powerful testing scenario, from which most others have been derived by omitting some of its features. It was based on a reactive failure trace machine with replicator, but additionally the observer is equipped with the capacity of global testing. Global testing is described in Abramsky [1] as: “the ability to enumerate all (of finitely many) possible ‘operating environments’ at each stage of the test, so as to guarantee that all nondeterministic branches will be pursued by various copies of the subject process”. Milner [37] implemented global testing by assuming that

“(i) It is the weather at any moment which determines the choice of transition (in case of ambiguity [...]);

(ii) The weather has only finitely many states—at least as far as choice-resolution is concerned;

(iii) We can control the weather.”

Now it can be ensured that all possible moves a process can perform in reaction on a given a-experiment will be investigated by simply performing the experiment in all possible weather conditions. Unfortunately, as remarked in Milner [38], the second assumption implies that the amount of different moves an investigated process can perform in response to any given experiment is bounded by the number of possible weather conditions (i.e. ∃n ∈ IN ∀p ∈ IP ∀a ∈ Act : |{q ∈ IP | p ⟶^{a} q}| < n). So for general application this condition has to be dropped, thereby losing the possibility of effective implementation of the testing scenario.

An observation in the global testing scenario can be represented as an infinitary Hennessy-Milner formula φ ∈ L_{B}. This is essentially a simulation formula in which it is possible to indicate that certain branches are not present. A formula ¬φ says that by making sufficiently many copies of the investigated process, and exposing them to all possible weather conditions, it can be observed that none of these copies permits the observation φ.

Remark: Let [a]φ denote ¬a¬φ. Now the negation in L_{B} can be eliminated in favour of the modalities [a] and infinitary disjunction ⋁_{i∈I}. A formula [a]φ says that in all possible weather conditions, after an a-move it is always possible to make the observation φ.

In order to justify the observations of L_{B} in a generative testing scenario no switches or menulights are needed; the architecture of the completed trace machine suffices. However, in order to warrant negative observations, one has to assume that actions take only a finite amount of time, and idling can be detected (either by observations that last forever, or by means of the display becoming empty). Adding switches and or menu-lights does not increase the discriminating power of the observers. It would give rise to observations that can be modelled as formulas in languages L_{FB}, L_{RTB}, etc., obtained by combining L_{F}, L_{RT}, etc. with L_{B}. These observations can already be expressed in L_{B}: p ⊧ X̃ ⇔ p ⊧ ⋀_{a∈X} ¬a⊤ and p ⊧ Xφ ⇔ p ⊧ (⋀_{a∉X} ¬a⊤) ∧ (⋀_{a∈X} a⊤) ∧ φ.

A different implementation of global testing is given in Larsen & Skou [35]. They assumed that every transition in a transition system has a certain probability of being taken. Therefore an observer can with an arbitrary high degree of confidence assume that all transitions have been examined, simply by repeating an experiment many times.

As argued among others in Bloom, Istrail & Meyer [12], global testing in the above sense is a rather unrealistic testing ability. Once you assume that the observer is really as powerful as in the described scenarios, in fact more can be tested then only bisimulation equivalence: in the testing scenario of Milner also the correlation between weather conditions and transitions being taken by the investigated process can be recovered, and in that of Larsen & Skou one can determine the relative probabilities of the various transitions.

Process graph characterization Also bisimulation equivalence can be characterized by means of relations between the nodes of two process graphs.

Definition 12.2 Let g, h ∈ ^{|}G. A bisimulation between g and h is a binary relation R ⊆ nodes(g)× nodes(h), satisfying:

• root(g)Rroot(h).

• If sRt and (s, a, s′) ∈ edges(g), then there is an edge (t, a, t′) ∈ edges(h) such that s′Rt′.

• If sRt and (t, a, t′) ∈ edges(h), then there is an edge (s, a, s′) ∈ edges(g) such that s′Rt′.

This definition is illustrated in Figure 8. Solid lines indicates what is assumed, dashed lines what is required. It follows easily that g \underline{↔} h iff there exists a bisimulation between g and h.

a a  a a

Figure 8: A bisimulation

For process graphs with multiple roots, the first requirement of Definition 12.2 generalizes to

• ∀s ∈ roots(g) ∃t ∈ roots(h) : sRt.

• ∀t ∈ roots(h) ∃s ∈ roots(g) : sRt.

Classification 2S ≺ B. Proof: “2S ⪯ B” follows since L_{2S} is a sublanguage of L_{B}. “2S ⪰̸ B” follows from Counterexample 14, which shows two graphs that are 2-nested simulation equivalent, but not bisimulation equivalent. Concerning the first claim, as in Counterexample 10 there exists exactly one simulation of left by right, which relates the red (or shaded) node on the left to the red (or shaded) node on the right. Unlike in Counterexample 10, this simulation is 2-nested, for the two subgraphs originating from the two red (or shaded) nodes are simulation equivalent, as are the graphs left and right themselves. Likewise, the simulation mapping right on the right-hand side of left is also 2-nested. The second claim follows since a¬b¬c⊤ ∈ B(left) − B(right). □

• a  a b  b  b c  c abc + a(bc + b)  =_{2S} ≠_{B}  • a b  b c a(bc + b)

Counterexample 14: 2-nested simulation equivalent, but not bisimulation equivalent

Thus bisimulation equivalence is the finest semantic equivalence treated so far. The following shows however that on ^{|}G graph isomorphism is even finer, i.e. isomorphic graphs are always bisimilar. In fact, a graph isomorphism can be seen as a bijective bisimulation. That not all bisimilar graphs are isomorphic will follow from Counterexample 15.

Proposition 12.3 For g, h ∈ ^{|}G, g ≅ h iff there exists a bisimulation R between g and h, satisfying

• If sRt and uRv then s = u ⇔ t = v. (*)

Proof: Suppose g ≅ h. Let f : nodes(g) → nodes(h) be a graph isomorphism. Define R ⊆ nodes(g) × nodes(h) by sRt iff f(s) = t. Then it is routine to check that R satisfies all clauses of Definition 12.2 and (*). Now suppose R is a bisimulation between g and h satisfying (*). Define f : nodes(g) → nodes(h) by f(s) = t iff sRt. Since g is connected it follows from the definition of a bisimulation that for each s such a t can be found. Furthermore direction “⇒” of (*) implies that f(s) is uniquely determined. Hence f is well-defined. Now direction “⇐” of (*) implies that f is injective. From the connectedness of h if follows that f is also surjective, and hence a bijection. Finally, the clauses of Definition 12.2 imply that f is a graph isomorphism. □

Corollary 12.1 If g ≅ h then g and h are equivalent according to all semantic equivalences encountered so far. □

Non-well-founded sets Another characterization of bisimulation semantics can be given by means of Aczel’s universe V of non-well-founded sets [4]. This universe is an extension of the Von Neumann universe of well-founded sets, where the axiom of foundation (every chain x_{0} ∋ x_{1} ∋ ⋯ terminates) is replaced by an anti-foundation axiom.

Definition 12.3 Let B denote the unique function M : IP → V satisfying

M(p) = {^{/} \a, M(q)^{\} / | p ⟶^{a} q}

for all p ∈ IP. Two processes p and q are branching equivalent (my terminology) if B(p) = B(q).

It follows from Aczel’s anti-foundation axiom that such a function exists. In fact the axiom amounts to saying that systems of equations like the one above have unique solutions. In [4] there is also a section on communicating systems. There two processes are identified iff they are branching equivalent.

A similar idea underlies the semantics of De Bakker & Zucker [9], but there the domain of processes is a complete metric space and the definition of B above only works for finitely branching processes, and only if = is interpreted as isometry, rather then equality, in order to stay in wellfounded set theory. For finitely branching processes the semantics of De Bakker and Zucker coincides with the one of Aczel and also with bisimulation semantics. This is observed in Van Glabbeek & Rutten [22], where also a proof can be found of the next proposition, saying that bisimulation equivalence coincides with branching equivalence.

Proposition 12.4 Let p, q ∈ IP. Then p\underline{↔} q ⇔ B(p) = B(q). Proof: “⇐”: Let B be the relation defined by pBq iff B(p) = B(q); then it suffices to prove that B is a bisimulation. Suppose pBq and p ⟶^{a} p′. Then ^{/} \a, B(p′)^{\} / ∈ B(p) = B(q). So by the definition of B(q) there must be a process q′ with B(p′) = B(q′) and q ⟶^{a} q′. Hence p′Bq′, which had to be proved. The second requirement for B being a bisimulation follows by symmetry.

“⇒”: Let B^{∗} denote the unique solution of M^{∗}(p) = \{^{/} \a, M^{∗}(r′)^{\} / | ∃r : r \underline{↔} p ∧ r ⟶^{a} r′\}. As for B it follows from the anti-foundation axiom that such a unique solution exists. From the symmetry and transitivity of \underline{↔} it follows that

p\underline{↔} q ⇒ B^{∗}(p) = B^{∗}(q).  (1)

Hence it remains to be proven that B^{∗} = B. This can be done by showing that B^{∗} satisfies the equations M(p) = {^{/} \a, M(q)^{\} / | p ⟶^{a} q}, which have B as unique solution. So it has to be established that B^{∗}(p) = {^{/} \a, B^{∗}(q)^{\} / | p ⟶^{a} q}. The direction “⊇” follows directly from the reflexivity of \underline{↔}. For “⊆”, suppose ^{/} \a, X^{\} / ∈ B^{∗}(p). Then ∃r : r \underline{↔} p, r ⟶^{a} r′ and X = B^{∗}(r′). Since \underline{↔} is a bisimulation, ∃p′ : p ⟶^{a} p′ and r′ \underline{↔} p′. From (1) it follows that X = B^{∗}(r′) = B^{∗}(p′). Therefore ^{/} \a, X^{\} / ∈ {^{/} \a, B^{∗}(q)^{\} / | p ⟶^{a} q}, which had to be established. □

Infinite processes The following predecessor of bisimulation equivalence was proposed in Hennessy & Milner [27, 28].

Definition 12.4 Let p, q ∈ IP. Then:

• p ∼_{0} q is always true.

• p ∼_{n+1} q if for all a ∈ Act:

• p ⟶^{a} p′ implies ∃q′ : q ⟶^{a} q′ and p′ ∼_{n} q′;

• q ⟶^{a} q′ implies ∃p′ : p ⟶^{a} p′ and p′ ∼_{n} q′.

• p and q are observationally equivalent, notation p ∼ q, if p ∼_{n} q for every n ∈ IN.

Hennessy and Milner provided the following modal characterization of observational equivalence on image finite processes.

Definition 12.5 The set L_{HM} of Hennessy-Milner formulas over Act is defined recursively by:

• ⊤ ∈ L_{HM}.

• If φ, ψ ∈ L_{HM} then φ ∧ ψ ∈ L_{HM}.

• If φ ∈ L_{HM} and a ∈ Act then aφ ∈ L_{HM}.

• If φ ∈ L_{HM} then ¬φ ∈ L_{HM}.

The satisfaction relation ⊧ ⊆ IP × L_{HM} is defined recursively by:

• p ⊧ ⊤ for all p ∈ IP.

• p ⊧ φ ∧ ψ if p ⊧ φ and p ⊧ ψ.

• p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q and q ⊧ φ.

• p ⊧ ¬φ if p |̸= φ.

The modal logic above is now known as the Hennessy-Milner logic (HML). Let HM (p) denote the set of all Hennessy-Milner formulas that are satisfied by the process p: HM (p) = {φ ∈ L_{HM} | p ⊧ φ}. Two processes p and q are HML-equivalent, notation p =_{B}^{−} q, if HM (p) = HM (q).

Theorem 2.2 in Hennessy & Milner [27, 28] says that ∼ and =_{B}^{−} coincide for image finite processes. This result will be strengthened by Proposition 12.6. Below I provide a modal characterization of ∼ that is valid for arbitrary processes.

Definition 12.6 Let L_{B}^{ω} = ⋃_{n=0}^{∞} L_{B}^{n}, where L_{B}^{n} is given by:

• If I is a set and φ_{i} ∈ L_{B}^{n} for i ∈ I then ⋀_{i∈I} φ_{i} ∈ L_{B}^{n}.

• If φ ∈ L_{B}^{n} and a ∈ Act then aφ ∈ L_{B}^{n+1}.

• If φ ∈ L_{B}^{n} then ¬φ ∈ L_{B}^{n}.

Let B^{ω}(p) = {φ ∈ L_{B}^{ω} | p ⊧ φ} and write p =_{B}^{ω} q if B^{ω}(p) = B^{ω}(q).

Proposition 12.5 p ∼_{n} q ⇔ ∀φ ∈ L_{B}^{n}(p ⊧ φ ⇔ q ⊧ φ) for all n ∈ IN. Hence p ∼ q ⇔ p =_{B}^{ω} q. Proof: Induction Base: Formulas in L_{B}^{0} do not contain the construct aφ. Hence for such formulas ψ the statement p ⊧ ψ is independent of p. Thus ∀p, q ∈ IP : ∀φ ∈ L_{B}^{0}(p ⊧ φ ⇔ q ⊧ φ). Induction Step: Suppose p ∼_{n+1} q. I now use structural induction on φ.

– Let p ⊧ aφ with aφ ∈ L_{B}^{n+1}. Then there is a p′ ∈ IP with p ⟶^{a} p′ and p′ ⊧ φ ∈ L_{B}^{n}. As p ∼_{n+1} q, there must be a q′ ∈ IP with q ⟶^{a} q′ and p′ ∼_{n} q′. So by induction q′ ⊧ φ, and hence q ⊧ aφ. By symmetry one also obtains q ⊧ aφ ⇒ p ⊧ aφ.

– p ⊧ ⋀_{i∈I} φ_{i} ⇔ ∀i∈I(p ⊧ φ_{i}) ⟺^{ind.} ∀i∈I(q ⊧ φ_{i}) ⇔ q ⊧ ⋀_{i∈I} φ_{i}.

– p ⊧ ¬φ ⇔ p |̸= φ ⟺^{ind.} q |̸= φ ⇔ q ⊧ ¬φ.

Now suppose ∀φ ∈ L_{B}^{n+1}(p ⊧ φ ⇔ q ⊧ φ) and p ⟶^{a} p′. Considering the symmetry in the definitions involved, all I have to show is that ∃q′ ∈ IP with q ⟶^{a} q′ and p′ ∼_{n} q′. Let Q′ be

{q′ ∈ IP | q ⟶^{a} q′ ∧ p′ ≁_{n} q′}.

By Definition 1.1 Q′ is a set. For every q′ ∈ Q′ there must, by induction, be a formula φ_{q′} ∈ L_{B}^{n} with p′ ⊧ φ_{q′} but q′ |̸= φ_{q′} (use negation if necessary). Now p ⊧ a ⋀_{q′∈Q′} φ_{q′} ∈ L_{B}^{n+1} and therefore q ⊧ a ⋀_{q′∈Q′} φ_{q′}. So there must be a q′ ∈ IP with q ⟶^{a} q′ and q′ ∉ Q′, which had to be shown. □

Comparing their modal characterizations (=_{B} of \underline{↔} and =_{B}^{ω} of ∼) one finds

p\underline{↔} q ⇒ p ∼ q ⇒ p =_{B}^{−} q.

Theorem 2.1 in Hennessy & Milner [27, 28] says, essentially, that for image finite processes the relation ∼ satisfies the defining properties of a bisimulation (cf. Definition 12). Inspired by this insight, Park [41] proposed the concise formulation of bisimulation equivalence employed in Definition 12. It follows immediately that if p, q ∈ IP are image finite, then p \underline{↔} q ⇔ p ∼ q. The following strengthening of this result is due to Hollenberg [32].

Proposition 12.6 Let p, q ∈ IP and p is image finite. Then p\underline{↔} q ⇔ p =_{B}^{−} q. Proof: Write pBq iff p =_{B}^{−} q and p is image finite. It suffices to establish that B is a bisimulation.

– Suppose pBq and q ⟶^{a} q′. I have to show that ∃r ∈ IP with p ⟶^{a} r and HM (r) = HM (q′).

Let R be

{r ∈ IP | p ⟶^{a} r ∧ HM (r) ≠ HM (q′)}.

As p is image finite, R is finite. For every r ∈ R take a formula φ_{r} ∈ HM (q′) − HM (r) (note that if ψ ∈ HM (r) − HM (q′) then ¬ψ ∈ HM (q′) − HM (r)). Now

a ⋀_{r∈R} φ_{r} ∈ HM (q) = HM (p),

so there must be a r ∈ IP with p ⟶^{a} r and r ⊧ ⋀_{r∈R} φ_{r}. The latter implies r ∉ R, i.e. HM (r) = HM (q′), which had to be shown.

– Suppose pBq and p ⟶^{a} p′. I have to show that ∃q′ ∈ IP with q ⟶^{a} q′ and HM (p′) = HM (q′).

Let S be

{s ∈ IP | p ⟶^{a} s ∧ HM (s) ≠ HM (p′)}.

As p is image finite, S is finite. For every s ∈ S take a formula φ_{s} ∈ HM (p′) − HM (s). Now

a ⋀_{s∈S} φ_{s} ∈ HM (p) = HM (q),

so there must be a q′ ∈ IP with q ⟶^{a} q′ and q′ ⊧ ⋀_{s∈S} φ_{s}. By the previous item in this proof, ∃r ∈ IP with p ⟶^{a} r and HM (r) = HM (q′), hence r ⊧ ⋀_{s∈S} φ_{s}. The latter implies r ∉ S, so HM (r) = HM (p′). Thus HM (p′) = HM (q′), which had to be shown. □

By Counterexample 12, a result like the one above does not hold for (ready) simulation semantics.

For the sake of completeness, two more variants of bisimulation equivalence can be considered. Let FB^{∗} be characterized by the Hennessy-Milner logic augmented with formulas X̃, and RB^{∗} by the Hennessy-Milner logic augmented with formulas X, for X ⊆ Act.

Then B^{−} ≺ FB^{∗} ≺ RB^{∗} ≺ B^{ω} ≺ B, and for image finite processes all five equivalences coincide. The strictness of these inclusions is given by Counterexamples 4, 11, 9 and 1:

Proposition 12.7 CT ⪯̸ B^{−}, and hence FB^{∗} ⪯̸ B^{−}. Proof: Counterexample 4 shows two processes with CT (left) ≠ CT (right). It remains to be shown that HM (left) = HM (right), i.e. that for all φ ∈ L_{HM}: left ⊧ φ ⇔ right ⊧ φ. Using Definition 12.5 it is sufficient to restrict attention to formulas φ which are of the form a(⋀_{i∈I} b_{i}⊤ ∧ ⋀_{j∈J} ¬b_{j}⊤) with I and J finite sets of indices. It is not difficult to see that each such formula that is satisfied on one side is also satisfied on the other side. □

Proposition 12.8 R ⪯̸ FB^{∗}, and hence RB^{∗} ⪯̸ FB^{∗}. Proof: Counterexample 11, shows two processes with R(with) ≠ R(without). It remains to be shown that FB^{∗}(with) = FB^{∗}(without). The argument is the same as in the previous proof, but this time focusing on formulas of the form a(X̃ ∧ ⋀_{i∈I} i⊤ ∧ ⋀_{j∈J} ¬j⊤) with I and J finite sets of numbers and X a possibly infinite set of numbers (= actions). □

Proposition 12.9 S^{ω} ⪯̸ RB^{∗}, and hence RB^{ω} ⪯̸ RB^{∗}. Proof: Counterexample 9 shows two processes with S^{ω}(with) ≠ S^{ω}(without). It remains to be shown that RB^{∗}(with) = RB^{∗}(without). The argument is the same as in the previous proofs—this time using formulas a({b} ∧ ⋀_{i∈I} bi⊤ ∧ ⋀_{j∈J} ¬bj⊤) with I and J finite sets of numbers. □

Proposition 12.10 T^{∞} ⪯̸ B^{ω}, and hence B ⪯̸ B^{ω}. In addition, PF ⪯̸ B^{ω}. Proof: Counterexample 1 shows two processes with T^{∞}(left) ≠ T^{∞}(right). As remarked at the end of Section 7, also PF (left) ≠ PF (right). It remains to be shown that left =_{B}^{ω} right, i.e. that for all n ∈ IN: left ∼_{n} right. In order to establish p ∼_{n} q for two trees p and q, the parts of p and q that are further than n edges away from the root play no rôle, and can just as well be omitted. As the cut versions of left and right are isomorphic, by Corollary 12.1 surely left ∼_{n} right. □

In addition one has 2S^{−} ≺ B^{−}, F2S^{∗} ≺ FB^{∗}, R2S^{∗} ≺ RB^{∗}, 2S^{ω} ≺ B^{ω} and 2S ≺ B.

13 Tree semantics

Definition 13 Let g ∈ ^{|}G. The unfolding of g is the graph U(g) ∈ ^{|}G defined by

• nodes(U(g)) = paths(g),

• root(U(g)) = root(g), i.e. the empty path, starting and ending at the root of g,

• (π, a, π′) ∈ edges(U(g)) iff π′ extends π by one edge, which is labelled a.

Two processes p and q are tree equivalent, notation p =_{U} q, if their unfoldings are isomorphic, i.e. if U(G(p)) ≅ U(G(p)). In tree semantics (U) two processes are identified iff they are tree equivalent.

It is easy to see that the unfolding of any process graph is a tree, and the unfolding of a tree is isomorphic to itself. It follows that up to isomorphism every tree equivalence class of process graphs contains exactly one tree, which can be obtained from an arbitrary member of the class by means of unfolding.

Proposition 13.1 Let g ∈ ^{|}G. Then U(g)\underline{↔} g. Hence g =_{U} h ⇒ g \underline{↔} h. Proof: As is easily verified, {(π, end(π)) | π ∈ paths(g)} is a bisimulation between U(g) and g. □

Tree semantics is employed in Winskel [50]. No plausible testing scenario or modal characterization is known for it. Proposition 13.1 shows that B ⪯ U. That B ⪰̸ U follows from Counterexample 15.

a  a a + a  =_{B} ≠_{U}  aa

Counterexample 15: Bisimulation equivalent, but not tree equivalent

Although above tree equivalence is defined entirely in terms of action relations, such a definition is in fact misleading, as action relations abstract from an aspect of system behaviour that tree

semantics tries to capture. The problem can best be explained by considering the process \begin{matrix}a \\ a \end{matrix}

that can proceed from its initial to its final state by performing one of two different a-transitions. In tree semantics, such a process should be considered equivalent to the leftmost process of Counterexample 15, and hence different from the rightmost one. However, action relations only tell whether a process p can evolve into q by performing an a-action; they do not tell in how many ways this can happen. So in labelled transition systems as defined in this paper the mentioned process is represented as a and hence considered tree equivalent to the rightmost process of Counterexample 15. The mishap that ensues this way will be illustrated in Section 17.

Tree semantics on labelled transitions systems as in Section 1.1 is a sensible notion only if one knows that each transition in the system can be taken in only one way. In general, more satisfactory domains for defining tree equivalence are labelled transition systems in which the transitions (p, a, q) are equipped with a multiplicity, telling in how many different ways this transition can be taken, or process graphs g = (nodes(g), root(g), edges(g), begin, end, label) in which nodes(g) and edges(g) are sets, root(g) ∈ nodes(g), begin, end : edges(g) → nodes(g) and label : edges(g) → Act. The functions begin, end and label associate with every edge a triple (s, a, t) ∈ nodes(g)×Act×nodes(g), but contrary to the situation in Definition 1.3 the identity of an edge is not completely determined by such a triple. On such process graphs, the notions paths, unfolding and tree equivalence are defined exactly as for the process graphs of Definition 1.3.

14 Possible worlds semantics

In Veglioni & De Nicola [49], a nondeterministic process is viewed as a set of deterministic ones: its possible worlds. Two processes are said to be possible worlds equivalent iff they have the same possible worlds. Two different approaches by which a nondeterministic process can be resolved into a set of deterministic ones need to be distinguished; I call them the state-based and the path-based approach. In the state-based approach a deterministic process h is obtained out of a nondeterministic process g ∈ ^{|}G by choosing, for every state s of g and every action a ∈ I(s) a single edge s ⟶^{a} s′. Now h is the reachable part of the subgraph of g consisting of the chosen edges. In the path-based approach on the other hand, one chooses for every path π ∈ paths(g) and every action a ∈ I(end(π)) a single edge end(π) ⟶^{a} s′ to continue with. The chosen edges may now be different for different paths ending in the same state. The difference between the two approaches is illustrated in Counterexample 16. In the state-based approach, the process in the middle has

abc b b b  =_{PW}^{state} ≠_{PW}^{path} ≠_{T}  a b b c  ≠_{PW}^{state} =_{PW}^{path} =_{U}  abc b bc b bc b

Counterexample 16: State-based versus path-based possible worlds equivalence

two possible worlds, depending on which of the two b-edges is chosen. These worlds are essentially abc and ab^{∞}. In the path-based approach, the process in the middle has countably many possible worlds, namely ab^{n}c for n ≥ 1 and ab^{∞}.

In [49], Veglioni & De Nicola take the state-based approach: “once we have resolved the underspecification present in a state s by saying, for example, s ⟶^{a} s, then, we cannot choose s ⟶^{a} 0 in the same possible world.” However, they provide a denotational characterization of possible worlds semantics on finite processes, namely by inductively allocating sets of deterministic trees to BCCSP expressions (cf. Section 17), which can be regarded as path-based. In addition, they give an operational characterization of possible world semantics, essentially following the state-based approach outlined above. They claim that both characterizations agree. This, however, is not the case, as Counterexample 17 reveals a difference between the two approaches even on finite processes. In the path-based approach the process displayed has a possible world acd + bce (i.e. a process with branches acd and bce), which it has not in the state-based approach. As it turns out, the complete axiomatization they provide w.r.t. BCCSP is correct for the path-based, denotational characterization, but is unsound for the state-based, operational characterization. To be precise: their operational semantics fails to be compositional w.r.t. BCCSP.

a  b c  c d  e

Counterexample 17: State-based versus path-based possible worlds equivalence for finite processes

Counterexample 16 shows that a suitable formulation^{8} of the state-based approach to possible worlds semantics is incomparable with any of the semantics encountered so far. The processes left and middle are state-based possible worlds equivalent, yet abbc ∈ T (middle)−T (left). Furthermore, the processes right and middle are tree equivalent, yet in the state-based approach one has abbc ∈ PW (right) − PW (middle).

Below I propose a formalization of the path-based approach to possible worlds semantics that, on finite processes, agrees with the denotational characterization of [49].

Definition 14 A process p is a possible world of a process q if p is deterministic and p ⊑_{RS} q. Let PW (q) denote the class of possible worlds of q. Two processes q and r are possible worlds equivalent, notation q =_{PW} r, if PW (q) = PW (r). In possible worlds semantics (PW ) two processes are identified iff they are possible worlds equivalent. Write q ⊑_{PW} r iff PW (q) ⊆ PW (r).

It can be argued that the philosophy underlying possible worlds semantics is incompatible with the view on labelled transition systems taken in this paper. The informal explanation of the action relations in Section 1.1 implies for instance that the right-hand process graph of Counterexample 8 has a state in which a has happened already and both bc and bd are possible continuations. In the possible worlds philosophy on the other hand, this process graph is just a compact representation of the set of deterministic processes {abc, abd}. None of the two processes in this set has such a state.

This could be a reason not to treat possible worlds semantics on the same footing as the other semantics of this paper. However, one can give up on thinking of non-deterministic processes as sets of deterministic ones, and justify possible worlds semantics—at least the path-based version of Definition 14—by an appropriate testing scenario. This makes it fit in the present paper.

Testing scenario A testing scenario for possible worlds semantics can be obtained by making one change in the reactive testing scenario of failure simulation semantics. Namely in each state only as many copies of the process can be made as there are actions in Act, and, for a ∈ Act, the first test on copy p_{a} of p is pressing the a-button. If it goes down, one goes on testing that copy, but is has already changed its state; if it does not go down, the test on p_{a} ends.

Modal characterization On well-founded processes, a modal characterization of possible worlds semantics can be obtained out of the modal characterization of ready simulation semantics by changing the modality ⋀_{i∈I} φ_{i} into ⋀_{a∈X} aφ_{a} with X ⊆ Act. Possible worlds of a well-founded process p can be simply encoded as modal formulas in the resulting language. Probably, this modal characterization applies to image finite processes as well. For processes that are neither well-founded nor image finite this characterization is not exact, as it fails to distinguish the two processes of Counterexample 1.

8Let two processes be possible worlds equivalent iff each possible world of the one is ∼-equivalent to a possible world of the other, where ∼ is any of the equivalences treated in this paper. Theorem 6 will imply that the choice of ∼ is immaterial.

Classification RT ≺ PW ≺ RS. PW is independent of S, CS and P F. Proof: “PW ⪯ RS”^{9} follows by the transitivity of ⊑_{RS}. “RT ⪯ PW ” holds as σ is a ready trace of p ∈ IP iff it is a ready trace of a possible world of p. “S ⪯̸ PW ” (and hence “RS ⪯̸ PW ”) follows from Counterexample 8. There S(left) ≠ S(right), but PW (left) = PW (right) = {abc, abd}. “PF ⪯̸ PW ” follows since PF ⪯̸ RS. “CS ⪰̸ PW ” follows since CS ⪰̸ RT, and “P F ⪰̸ PW ” since PF ⪰̸ RT . Finally, “RT ⪰̸ PW ” follows from Counterexample 18, taken from [49]. There the first process denotes two possible worlds, whereas the second one denotes four. □

b d  b g a  a c  c e  f a(bd + ce) + a(cf + bg)  =_{RT} ≠_{PW}  b d  b  g a c c e  f a(bd + ce + cf + bg)

Counterexample 18: Ready trace equivalent, but not possible worlds equivalent

Infinite processes The version of possible worlds semantics defined above is the infinitary one. Note that RT^{∞} ≺ PW . Exactly as above one even establishes p ⊑_{RS} q ⇒ p ⊑_{PW} q ⇒ p ⊑_{RT}^{∞} q, i.e. RT^{∞} ⪯^{∗} PW ⪯^{∗} RS. Finitary versions could be defined by means of the modal characterization given above. I will not pursue this here.

15 Summary

In Sections 2–14 fifteen semantics were defined that are different for finitely branching processes. These are abbreviated by T, CT, F^{1}, F, R, FT, RT, PF, S, CS, RS, PW, 2S, B and U. For each of these semantics O, except U, a modal language L_{O} (a set of modal formulas φ) has been defined: L_{T} φ ::= ⊤ | aφ′ (φ′ ∈ L_{T}) the (partial) trace formulas L_{CT} φ ::= ⊤ | aφ′ (φ′ ∈ L_{CT}) | 0 the completed trace formulas L_{F^{1}} φ ::= ⊤ | aφ′ (φ′ ∈ L_{F^{1}}) | ã (a ∈ Act) the singleton-failure formulas L_{F} φ ::= ⊤ | aφ′ (φ′ ∈ L_{F}) | X̃ (X ⊆ Act) the failure formulas L_{R} φ ::= ⊤ | aφ′ (φ′ ∈ L_{R}) | X (X ⊆ Act) the readiness formulas L_{F T} φ ::= ⊤ | aφ′ (φ′ ∈ L_{F T}) | X̃φ′ (X ⊆ Act, φ′ ∈ L_{F T}) the failure trace formulas L_{RT} φ ::= ⊤ | aφ′ (φ′ ∈ L_{RT}) | Xφ′ (X ⊆ Act, φ′ ∈ L_{RT}) the ready trace formulas L_{PF} φ ::= aφ′ (φ′ ∈ L_{PF} ) | ⋀_{i∈I} φ_{i} ∧ ⋀_{j∈J} ¬φ′_{j} (φ_{i}, φ′_{j} ∈ L_{T}) the possible-futures formulas L_{S} φ ::= aφ′ (φ′ ∈ L_{S}) | ⋀_{i∈I} φ_{i} (φ_{i} ∈ L_{S}) the simulation formulas L_{CS} φ ::= aφ′ (φ′ ∈ L_{CS}) | ⋀_{i∈I} φ_{i} (φ_{i} ∈ L_{CS}) | 0 the completed simulation formulas L_{RS} φ ::= aφ′ (φ′ ∈ L_{RS}) | ⋀_{i∈I} φ_{i} (φ_{i} ∈ L_{RS}) | X (X ⊆ Act) the ready simulation formulas L_{PW} ⋀_{a∈X} aφ_{a} (φ_{a} ∈ L_{PW} , X ⊆ Act) | X (X ⊆ Act) the possible worlds formulas L_{2S} φ ::= aφ′ (φ′ ∈ L_{2S} ) | ⋀_{i∈I} φ_{i} (φ_{i} ∈ L_{2S} ) | ¬φ′ (φ′ ∈ L_{S}) the 2-nested simulation formulas L_{B} φ ::= aφ′ (φ′ ∈ L_{B}) | ⋀_{i∈I} φ_{i} (φ_{i} ∈ L_{B}) | ¬φ′ (φ′ ∈ L_{B}) the bisimulation formulas. All these languages can be regarded as sublanguages of L_{B}, the infinitary Hennessy-Milner logic, namely by considering the constructs not in L_{B} as abbreviations:

9The counterexample against “PW ⪯ RS” given in [49] is incorrect. The two processes displayed there are not ready simulation equivalent.

\begin{matrix}⊤ := ⋀_{i∈∅} φ_{i} & X̃ := ⋀_{a∈X} ¬a⊤ & X̃φ′ := X̃ ∧ φ′ & 0 := Ãct \\ φ_{1} ∧ φ_{2} := ⋀_{i∈\{1,2\}} φ_{i} & X := ⋀_{a∈X} a⊤ ∧ ⋀_{a∉X} ¬a⊤ & Xφ′ := X ∧ φ′ & ã := ¬a⊤ \end{matrix}

On any labelled transition system IP, the satisfaction relation ⊧ ⊆ IP × L_{B} is given by:

p ⊧ aφ if for some q ∈ IP: p ⟶^{a} q ∧ q ⊧ φ; p ⊧ ⋀_{i∈I} φ_{i} if ∀i ∈ I : p ⊧ φ_{i}; p ⊧ ¬φ if p |̸= φ.

For each semantics O ∈ {T , CT ,F^{1}, F , R, FT , RT , PF , S, CS, RS, PW , 2S, B} this definition specializes to the sublanguage L_{O}. Now a modal characterization of O-equivalence^{10} is given by:

p =_{O} q ⇔ ∀φ ∈ L_{O}(p ⊧ φ ⇔ q ⊧ φ).

In the cases O ∈ {T , CT ,F^{1}, F , R, FT , RT } O-equivalence was defined by p =_{O} q ⇔ O(p) = O(q). Writing O_{modal}(p) for {φ ∈ L_{O} | p ⊧ φ}, it can be observed that the formulas in O_{modal}(p) are mild syntactic variations of the elements in O(p). Thus, the modal characterization is a rather trivial restatement of the original definition of the equivalence. The modal characterization of PF is fairly easy to check. This is left to the reader. In the cases O ∈ {S, CS, RS, 2S, B} the modal characterization of =_{O} has been proven equivalent to a relational characterization in Propositions 8.2, 9.2, 9.3, 11.1 and 12.2. It is a matter of taste which one is taken to be the official definition.

The same applies to the modal characterizations of the O-preorders^{10}, given by

p ⊑_{O} q ⇔ ∀φ ∈ L_{O}(p ⊧ φ ⇒ q ⊧ φ).

For each of the semantics T , CT ,F^{1}, F , R, FT , RT , S, CS, RS, PW , B a testing scenario has been proposed in which the modal formulas satisfied by a process p are interpreted as the possible observations that can be made on a suitable machine interacting with p. In particular, the formula aφ represents the observation of “a” appearing in the display of a generative machine (or the abutton going down on a reactive machine) followed by the observation φ. The formula X̃ represents the display of the generative machine becoming empty, while X is the set of actions that are allowed to happen by the environment/observer, i.e. the ones whose switches are set “free”. In particular, 0 represents the display becoming empty while all actions are free (in the absence of switches). On a reactive machine, ã represents the a-button refusing to go down, and X̃ means that none of the a-buttons for a ∈ X go down when they all receive pressure. X represents the menu lights for the actions in X being lit while the machine is idling. ⊤ represents the act of the observer terminating his observations, and ⋀_{i∈I} φ_{i} represents the observations that can be made on |I| copies of the investigated process in its current state, obtained by means of a replication facility. Finally ¬φ represents the observation that φ cannot be observed—an observation which occurs when copies of the investigated process are exposed to all possible weather conditions, and in none of them the observation φ is made. A testing scenario for a particular semantics is obtained by allowing machines that are equipped with (only) those features corresponding with its modal characterization.

10In case O = PW the modal characterization is known to be valid for well-founded processes only.

I write O ⪯ N if semantics O makes at least as much identifications as semantics N, i.e. if =_{O} ⊇ =_{N}. Clearly, if L_{O} is a sublanguage of L_{N} it must be that O ⪯ N. This immediately yields^{11} the following theorem, whose proof has also appeared in the various subsections entitled “classification”.

Theorem 1 T ⪯ CT ⪯ F ⪯ R ⪯ RT, T ⪯ F^{1} ⪯ F ⪯ F T ⪯ RT ⪯ PW ⪯ RS ⪯ 2S ⪯ B ⪯ U , R ⪯ PF ⪯ 2S, T ⪯ S ⪯ CS ⪯ RS and CT ⪯ CS.

Theorem 1 is illustrated in Figure 1. There, however, singleton-failures semantics and completed simulation semantics are missing, since they did not occur in the literature, and appear to be of minor interest. The theorem applies to any labelled transition system (IP, →). Whether the inclusions are strict depends on the choice of (IP, →). In the subsections “classification” a number of counterexamples have been presented, showing that on ^{|}G all semantic notions mentioned in Theorem 1 are different and O ⪯ N holds only if this follows from that theorem. Moreover, all relevant examples use finite processes only.

Let IH be the set of finite connected process graphs. Here finite is used in the sense of Definition 1.2; a process graph g ∈ ^{|}G is finite iff paths(g) is finite, which is the case iff g is acyclic and has only finitely many nodes and edges. Now the next theorem follows.

Theorem 2 Let O, N ∈ {T , CT ,F^{1}, F , R, FT , RT , PF , S, CS, RS, PW , 2S, B, U }. Then O ⪯̸ N, and even O ⪯̸IH N, unless O ⪯ N follows from Theorem 1 (and the fact that ⪯ is a partial order).

The following theorem says that the inclusion hierarchy of the preorders T, CT, F^{1}, F, R, FT, RT, PF, S, CS, RS, PW, 2S and B is the same as the inclusion hierarchy of the corresponding equivalences (there is no preorder for U).

Theorem 3 Let O, N ∈ {T , CT ,F^{1}, F , R, FT , RT , PF , S, CS, RS, PW , 2S, B}. Then O ⪯^{∗} N iff O ⪯ N.

Proof: Clearly, if L_{O} is a sublanguage of L_{N} it must be that p ⊑_{N} q ⇒ p ⊑_{O} q, i.e. O ⪯^{∗} N. This yields “if” (except for RT ⪯^{∗} PW ⪯^{∗} RS, which have been established in Section 14). “Only if” is immediate (cf. Section 1.4). □

When the restriction to finitely branching processes is dropped, there exists a finitary and an infinitary variant of each of these semantics, depending on whether or not infinite observations are taken into account (I do not consider the finitary version of PW or the infinitary version of F^{1} though). These versions are notationally distinguished by means of superscripts “*” and “∞”, respectively; the unsubscripted abbreviation will refer to the infinitary versions in case of simulation-like semantics (treated in Sections 8–12) and to the finitary versions for the decorated Summary 53

11The statements involving PW and U do not follow this way, but have been established in Sections 13 and 14.

T CT F  R F T RT RS^{∗}_{FS_{∗}} _{R2S^{∗}}_{F2S^{∗}} RB^{∗} FB^{∗} S^{∗} CS^{∗}  PF  T^{∞} CT^{∞} F^{∞} R^{∞} F T^{∞} RT^{∞}_{PW} RS 2S B U S CS  _{PF_{∞}} RS^{ω} 2S^{ω} B^{ω} S^{ω} CS^{ω} F^{1} F^{−} R^{−} F T^{−} RT^{−} RS^{−} 2S^{−} B^{−}

Figure 9: The infinitary linear time – branching time spectrum

trace semantics (treated in Section 2–7). The modal characterizations summarized above apply to the default (= unsubscripted) versions. Modal characterizations of T^{∞}, CT^{∞}, F^{∞}, R^{∞}, resp. F T^{∞} and RT^{∞}, are obtained by allowing traces, resp. failure traces or ready traces, of infinite length as modal formulas; a modal characterization of PF^{∞} is obtained by replacing the reference to T by one to T^{∞}. Modal characterizations of S^{∗}, CS^{∗}, etc. are obtained by requiring the index sets I to be finite. For the simulation-like semantics also an intermediate variant is considered—superscripted with “ω”—based on the assumption that observers can investigate arbitrary many copies of a process in parallel, but have only a finite amount of time to do so. Modally, this corresponds to the restriction to modal formulas with a finite upperbound on the number of nestings of the aφ construct. For the semantics that incorporate refusal sets, the finitary versions come in two variants, depending on whether the refusal sets are required to be finite (superscript “−”) or not (the default assumption). A similar distinction is made for semantics where menus of actions can be observed: in R^{−}, RT^{−} and RS^{−} the modal formula X is replaced by ⋀_{a∈Y} ¬a⊤ ∧ ⋀_{a∈Z} a⊤, where the sets of actions Y and Z are required to be finite. Finally, whereas failure simulation semantics, modally characterized by L_{FS} φ ::= aφ′ (φ′ ∈ L_{FS} ) | ⋀_{i∈I} φ_{i} (φ_{i} ∈ L_{FS} ) | X̃ (X ⊆ Act) the failure simulation formulas, coincides with ready simulation semantics, its finitary version (FS^{∗}) can be distinguished from RS^{∗}. The intermediate notions FS^{ω} and RS^{ω} coincide again, as do FS^{−} and RS^{−}. By analogy, new semantics FB^{∗} and RB^{∗} can be defined by adding the modality X̃ resp. X to L_{B}^{−}. These modalities would be redundant on top of L_{B}^{ω} or L_{B}. A similar situation occurs for 2-nested simulation.

All semantics encountered are displayed in Figure 9, in which the ⪯-relation is represented by solid and dotted arrows.

Theorem 4 For all semantics O and N defined so far, the formula O ⪯ N holds iff there is a path O → ⋯ → N (consisting of solid and dotted arrows alike) in Figure 9. Furthermore, semantics connected by dotted arrows coincide for image finite processes.

Proof: That T^{∞} ⪯ S has been established in Proposition 8.3; that CT^{∞} ⪯ CS, RT^{∞} ⪯ RS and PF^{∞} ⪯ 2S follows in the same way. R^{∞} ⪯ PW ⪯ RS has been established in Section 14. All other implications O ⪯ N follow from the observation that the modal language L_{O} is included in L_{N}. The latter statement has been established in Propositions 2.4, 4.6, 5.3, 6.5, 7.4, 7.5, 7.6, 8.4, 9.6, 11.2 and 12.6 (except that the case of possible-futures semantics is left to the reader). In order to show that on ^{|}G there are no inclusions that are not indicated in Figure 9, is suffices, in view of Theorem 2, the already established parts of Theorem 4, and the fact that ⪯ is a partial order, to show that CT ⪯̸ B^{−}, R ⪯̸ FB^{∗}, S^{ω} ⪯̸ RB^{∗}, T^{∞} ⪯̸ B^{ω}, PF ⪯̸ B^{ω} and T^{∞} ⪯̸ PF . This has been done in Propositions 12.7, 12.8, 12.9 and 12.10, and at the end of Section 7. □

Again, the inclusion hierarchy for the preorders is the same as for the equivalences.

Theorem 5 For all semantics O and N defined so far, the formula O ⪯^{∗} N holds iff there is a path O → ⋯ → N (consisting of solid and dotted arrows alike) in Figure 9.

Proof: That p ⊑_{S} q ⇒ p ⊑_{T}^{∞} q has been established in Proposition 8.3; that p ⊑_{CS} q ⇒ p ⊑_{CT}^{∞} q, p ⊑_{RS} q ⇒ p ⊑_{RT}^{∞} q and p ⊑_{2S} q ⇒ p ⊑_{PF}^{∞} q follows in the same way. In Section 14 it has been established that p ⊑_{RS} q ⇒ p ⊑_{PW} q ⇒ p ⊑_{RT}^{∞} q. All other implications p ⊑_{O} q ⇒ p ⊑_{N} q follow from the observation that the modal language L_{O} is included in L_{N}. The “only if” part is an immediate consequence of Theorem 4. □

16 Deterministic and saturated processes

If the labelled transition system IP on which the semantic equivalences of Section 15 are defined is large enough, then they are all different and O ⪯IP N holds only if this is indicated in Figure 9. However, for certain labelled transition systems much more identifications can be made. Is has been remarked already that for image finite processes all semantics that are connected by dotted arrows coincide. In this section various other classes of processes are examined on which parts of the linear time – branching time spectrum collapse. All results of this section, expect for Propositions 16.1 and 16.2, will be used in the completeness proofs in Section 17.

Recall that a process p is deterministic iff p ⟶^{σ} q ∧ p ⟶^{σ} r ⇒ q = r.

Remark: If p is deterministic and p ⟶^{σ} p′ then also p′ is deterministic. Hence any domain of processes on which action relations are defined, has a subdomain of deterministic processes with the inherited action relations. (A similar remark can be made for image finite processes.) Proof: Suppose p′ ⟶^{ρ} q and p′ ⟶^{ρ} r. Then p ⟶^{σρ} q and p ⟶^{σρ} r, so q = r. □

Theorem 6 (Park [41]) On a domain of deterministic processes all semantics in the infinitary linear time – branching time spectrum coincide.

Proof: Because of Theorem 4 it suffices to show that g =_{T} h ⇒ g =_{U} h for any two deterministic process graphs g, h ∈ ^{|}G. Note that a process graph g ∈ ^{|}G is deterministic iff for every trace σ ∈ T (g) there is exactly one path π ∈ paths(g) with T (π) = σ. Now let g and h be deterministic process graphs with g =_{T} h. Then the relation i ⊆ paths(g) × paths(h) that relates π ∈ paths(g) with π′ ∈ paths(h) iff T (π) = T (π′) clearly is an isomorphism between U(g) and U(h). □

Thus, if two processes p and q are both deterministic, then p =_{T} q ⇔ p =_{F}^{1} q ⇔ p \underline{↔} q ⇔ p =_{U} q. In case only one of them is deterministic, this cannot be concluded, for in Counterexamples 2 and 15 the right-hand processes are deterministic. However, in such cases one still has p =_{F}^{1} q ⇔ p\underline{↔} q. In fact, a stronger statement holds: if q is deterministic, then p ⊑_{F}^{1} q ⇔ p\underline{↔} q.

Lemma 16.1 If p ⊑_{F}^{1} q then I(p) = I(q). Proof: Let p ⊑_{F}^{1} q, i.e. T (p) ⊆ T (q) and F^{1}(p) ⊆ F^{1}(q). Then a ∈ I(p) ⇔ a ∈ T (p) ⇒ a ∈ T (q) ⇔ a ∈ I(q) and a ∉ I(p) ⇔ ^{/} \ε, a^{\} / ∈ F^{1}(p) ⇒ ^{/} \ε, a^{\} / ∈ F^{1}(q) ⇔ a ∉ I(q). □

Proposition 16.1 If q is deterministic then p ⊑_{F}^{1} q ⇔ p\underline{↔} q. Proof: Let R be the binary relation on IP defined by pRq iff q is deterministic and p ⊑_{F}^{1} q, then it suffices to prove that R is a bisimulation. Suppose pRq and p ⟶^{a} p′. Then a ∈ I(p) = I(q). So there is a process q′ ∈ IP with q ⟶^{a} q′. As q is deterministic, so is q′. Now let ^{/} \σ, b^{\} / ∈ F^{1}(p′). Then ∃r : p′ ⟶^{σ} r ∧ b ∉ I(r). Hence p ⟶^{aσ} r and ^{/} \aσ, b^{\} / ∈ F^{1}(p) ⊆ F^{1}(q). So there must be a process s with q ⟶^{aσ} s ∧ b ∉ I(s). By the definition of the generalized action relations ∃t : q ⟶^{a} t ⟶^{σ} s, and since q is deterministic, t = q′. Thus ^{/} \σ, b^{\} / ∈ F^{1}(q′). From this it follows that F^{1}(p′) ⊆ F^{1}(q′). Similarly one finds T (p′) ⊆ T (q′), hence p′ ⊑_{F}^{1} q′.

Now suppose pRq and q ⟶^{a} q′. Then a ∈ I(q) = I(p). So there is a process p′ ∈ IP with p ⟶^{a} p′. Exactly as above it follows that q′ is deterministic and p′ ⊑_{F}^{1} q′. □

Call a process p deterministic up to ≡, for ≡ an equivalence relation or preorder, if there exists a deterministic process p′ with p ≡ p′. Now the above proposition implies that determinism up to \underline{↔} coincides with determinism up to =_{F}^{1} , and even with determinism up to ⊑_{F}^{1} . In contrast, any process is deterministic up to =_{T}, as the canonical graphs constructed in the proof of Proposition 2.3 are deterministic. Furthermore, determinism up to =_{U} is just determinism, for g ∈ ^{|}G is deterministic iff U(g) is, and determinism is preserved under isomorphism.

The following notion of determinacy was proposed in Engelfriet [18].

Definition 16.1 Let ≡ be an equivalence relation on IP. A process p ∈ IP is ≡-determinate if

p ⟶^{σ} q ∧ p ⟶^{σ} r ⇒ q ≡ r.

Note that =-determinacy is determinism. Furthermore, if O ≤ N then =_{O}-determinacy is implied by =_{N} -determinacy. Besides =_{T} -determinacy, =_{F} -determinacy and \underline{↔} -determinacy, Engelfriet also considers =_{I}-determinacy, where =_{I} is given by p =_{I} q iff I(p) = I(q). Clearly =_{I} is coarser than any of the equivalences of Section 15: p =_{T} q ⇒ p =_{I} q. Moreover, =_{I} is even coarser than most of the preorders: p ⊑_{F}^{1} q ⇒ p =_{I} q, as established in Lemma 16.1.

Engelfriet established the following three results:

(1) \underline{↔} -determinacy and =_{I}-determinacy are the same. Hence ≡-determinacy is the same for all equivalences ≡ of Section 15, except U. Therefore, he just calls this determinacy.

(2) For determinate processes, bisimulation equivalence and trace equivalence (and hence all equivalences in between) are the same.

(3) Determinacy is preserved under failures equivalence (and hence under \underline{↔}). Even stronger, if q is determinate and p ⊑_{F} q, then p is determinate and p\underline{↔} q. (In [18], ⊒_{F} is written ⊆_{f}.)

Using Proposition 16.1 I show that both =_{I}-determinacy and \underline{↔} -determinacy coincide with determinism up to \underline{↔}, from which (1), (2) and (3) follow.

Proposition 16.2 Let p ∈ IP. The following are equivalent:

(a) p is \underline{↔} -determinate

(b) p is =_{I}-determinate

(c) p is deterministic up to =_{R}

(d) p is deterministic up to \underline{↔}. Proof: “(a) ⇒ (b)” is immediate as =_{I} is coarser than \underline{↔}.

“(b) ⇒ (c)”: Suppose p is =_{I}-determinate. Let G(T (p)) be the canonical graph of the trace set of p as defined in the proof of Proposition 2.3. By construction, G(T (p)) is deterministic and T (p) = T (G(T (p))). It remains to be shown that p =_{R} G(T (p)).

As p is =_{I}-determinate, one has ^{/} \σ, X^{\} /, ^{/} \σ, Y ^{\} / ∈ R(p) ⇒ X = Y. Hence ^{/} \σ, X^{\} / ∈ R(p) iff σ ∈ T (p) ∧ X = {a ∈ Act | σa ∈ T (p)}, i.e. R(p) is completely determined by T (p). As also G(T (p)) is =_{I}-determinate (for it is even deterministic), also R(G(T (p))) is completely determined by T (G(T (p))): ^{/} \σ, X^{\} / ∈ R(G(T (p))) iff σ ∈ T (G(T (p))) ∧ X = {a ∈ Act | σa ∈ T (G(T (p)))}. It follows that R(p) = R(G(T (p))).

“(c) ⇒ (d)” has been established in Proposition 16.1.

“(d) ⇒ (a)”: Suppose p \underline{↔} q and q is deterministic. Let p ⟶^{σ} p′ and p ⟶^{σ} p′′. Then

∃q′ : q ⟶^{σ} q′ ∧ p′ \underline{↔} q′ and ∃q′′ : q ⟶^{σ} q′′ ∧ p′′ \underline{↔} q′′. As q is deterministic, q′ = q′′. Hence p′ \underline{↔} p′′.

It follows that p is \underline{↔} -determinate. □

Now (1) is part of Proposition 16.2. (2) is a generalization of Theorem 6, that is now implied by it: Suppose p and q are determinate and p =_{T} q. By Proposition 16.2 there are deterministic processes p′ with p\underline{↔} p′ and q′ with q \underline{↔} q′. Hence p′ =_{T} q′, so by Theorem 6 p′ \underline{↔} q′. Thus p\underline{↔} q, yielding (2).

(3) holds even for F^{1} instead of F. For let q be determinate and p ⊑_{F}^{1} q. Then there is a deterministic process q′ with q \underline{↔} q′. Hence p ⊑_{F}^{1} q′. By Proposition 16.1 p\underline{↔} q′, so p is determinate and p\underline{↔} q.

Note that a process p is deterministic iff for π, π′ ∈ paths(G(p)) one has T (π) = T (π′) ⇒ π = π′. For this reason, determinism could have been called trace determinism, and the notions of ready trace determinism and completed trace determinism can be defined analogously.

Definition 16.2 A process p is ready trace deterministic if for π, π′ ∈ paths(G(p)) one has RT (π) = RT (π′) ⇒ π = π′. It is completed trace deterministic if for π, π′ ∈ paths(G(p)) one has T (π) = T (π′) ∧ (I(end(π)) = ∅ ⇔ I(end(π′)) = ∅) ⇒ π = π′.

A process p ∈ IP is ready trace deterministic iff there is are no p′, q, r ∈ IP and a ∈ Act such that p′ is reachable from p, p′ ⟶^{a} q, p′ ⟶^{a} r, I(q) = I(r) and q ≠ r. For trace determinism the condition I(q) = I(r) is dropped, and for completed trace determinism it is weakened to I(q) = ∅ ⇔ I(r) = ∅. Note that if p is ready (or completed) trace deterministic and p ⟶^{σ} p′ then so is p′. Now the following variants of Theorem 6 can be established.

Proposition 16.3 If g and h ∈ ^{|}G are ready trace deterministic then g =_{RT} h ⇔ g =_{U} h. Likewise, if g and h ∈ ^{|}G are completed trace deterministic then g =_{CT} h ⇔ g =_{U} h. Proof: Let g and h be ready trace deterministic process graphs with g =_{RT} h. Then the relation i ⊆ paths(g) × paths(h) that relates π ∈ paths(g) with π′ ∈ paths(h) iff RT (π) = RT (π′) clearly is an isomorphism between U(g) and U(h). The proof of the second statement goes likewise. □

For completed trace deterministic processes, the equivalences =_{T} and =_{CT} are different, as can be seen from Counterexample 2. For ready trace deterministic processes, the equivalences =_{T}, =_{CT}, =_{F}^{1} , =_{F}, =_{F T}, =_{R}, =_{RT}, =_{S} and =_{CS} are all different, as can be seen from Counterexamples 2, 3, 5, 6 and 13. Theorem 6 and Proposition 16.3 do not generalize to the corresponding preorders, for in Counterexample 19 one finds two deterministic processes middle and right with middle ⊑_{CT} right but middle ⋢_{B} right, and in Counterexample 3 one finds two ready trace deterministic processes right and left with right ⊑_{RT} left but right ⋢_{B} left. However, the following variants of these results can be obtained.

Proposition 16.4 If q is ready trace deterministic then p ⊑_{RT} q ⇔ p ⊑_{RS} q. Likewise, if q is completed trace deterministic then p ⊑_{CT} q ⇔ p ⊑_{CS} q, and if q is (trace) deterministic then p ⊑_{T} q ⇔ p ⊑_{S} q. Proof: Let R be the binary relation on IP given by pRq if q is ready trace deterministic and p ⊑_{RT} q. For the first statement it suffices to prove that R is a ready simulation. Clearly pRq implies I(p) = I(q). Now suppose pRq and p ⟶^{a} p′. Let X be I(p′). Then aX ∈ RT (p) ⊆ RT (q). So there is a process q′ ∈ IP with q ⟶^{a} q′ and I(q′) = X. Now let σ ∈ RT (p′). Then ∃r : p′ × +⟶^{σ} r.

Hence p × +⟶^{aXσ} r and aXσ ∈ RT (p) ⊆ RT (q). So there must be a process s with q × +⟶^{aXσ} s. By the definition of the ready trace relations ∃t : q ⟶^{a} t × +⟶^{σ} s ∧ I(t) = X, and since q is ready trace deterministic, t = q′. Thus σ ∈ RT (q′). From this it follows that RT (p′) ⊆ RT (q′), implying p′Rq′.

This finishes the proof of the first statement. The proofs of the other two statements go the same way (but involving a trivial case distinction for the completed trace deterministic one). □

Together, Propositions 16.1 and 16.4 imply that on a domain of deterministic processes only three of the preorders of Section 15 are different, namely ⊑_{T}, ⊑_{CT} and ⊑_{F}^{1} , coinciding with ⊑_{S}, ⊑_{CS} and ⊑_{B}, respectively. That these three are indeed different is shown in Counterexample 19.

0  ⊑_{T} ⋢_{CT}  aa  ⊑_{CT} ⋢_{F}  a  b a + b

Counterexample 19: The trace, completed trace, and failures preorders are all different on deterministic processes

Definition 16.3 A process p is cross saturated if p ⟶^{σ} q ⟶^{a} r ∧ p ⟶^{σ} s ⟶^{a} t ⇒ q ⟶^{a} t.

Thus a process graph g ∈ ^{|}G is cross saturated iff for any π, π′ ∈ paths(g) and a ∈ Act such that a ∈ I(end(π)) and T (π′) = T (π)a one has (end(π), a, end(π′)) ∈ edges(g).

Proposition 16.5 If g and h ∈ ^{|}G are cross saturated then g =_{R} h ⇔ g \underline{↔} h. Proof: Let g and h ∈ ^{|}G be cross saturated and suppose that R(g) = R(h). Define the relation R ⊆ nodes(g) × nodes(h) by sRt iff there are π ∈ paths(g) and ρ ∈ paths(h) with end(π) = s, end(ρ) = t and R(π) = R(ρ). It suffices to show that R is a bisimulation between g and h. As I(root(g)) = I(root(h)) one clearly has root(g)Rroot(h). Now suppose sRt and (s, a, s′) ∈ edges(g). Let π and ρ be such that end(π) = s, end(ρ) = t and R(π) = R(ρ), and let π′ be the extension of π with (s, a, s′). Now a ∈ I(end(π)) = I(end(ρ)). Choose ρ′ ∈ paths(h) with R(ρ′) = R(π′) (using that R(g) = R(h)). Then T (ρ′) = T (π′) = T (π)a = T (ρ)a, so (t, a, end(ρ′)) ∈ edges(h). Moreover, s′R end(ρ′). The remaining requirement of Definition 12.2 follows by symmetry. □

Proposition 16.6 If h ∈ ^{|}G is cross saturated then g ⊑_{R} h ⇔ g ⊑_{RS} h. Proof: Exactly as above. □

Definition 16.4 A process p is saturated if ^{/} \σ, X^{\} / ∈ R(p)∧^{/} \σ, Y ∪ Z^{\} / ∈ R(p) ⇒ ^{/} \σ, X ∪ Y ^{\} / ∈ R(p).

Proposition 16.7 If p is finitely branching and q is saturated then p ⊑_{F} q ⇔ p ⊑_{R} q. Thus if both p and q are finitely branching and saturated then p =_{F} q ⇔ p =_{R} q. Proof: Suppose p is finitely branching, q is saturated and p ⊑_{F} q. Let ^{/} \σ, Y ^{\} / ∈ R(p). Then Y is finite. In case Y = ∅ one has ^{/} \σ, Act^{\} / ∈ F (p) ⊆ F (q), implying ^{/} \σ, ∅^{\} / ∈ R(q), as desired. So assume Y ≠ ∅. Then, for all a ∈ Y, ^{/} \σa, ∅^{\} / ∈ F (p) ⊆ F (q) so ∃Z_{a} ⊆ Act with ^{/} \σ, {a} ∪ Z_{a}^{\} / ∈ R(q). Hence, using Definition 16.4 with Z = ∅, one obtains ^{/} \σ, Y ∪ ⋃_{a∈Y} Z_{a}^{\} / ∈ R(q). As ^{/} \σ, Act − Y ^{\} / ∈ F (p) ⊆ F (q) it must be that ^{/} \σ, X^{\} / ∈ R(q) for some X ⊆ Y. Now Definition 16.4 gives ^{/} \σ, Y ^{\} / ∈ R(q). □

Definition 16.5 A process p is RT-saturated if

σXρ ∈ RT_{N}(p) ∧ σY ∈ RT_{N}(p) ⇒ σ(X ∪ Y)ρ ∈ RT_{N}(p).

Proposition 16.8 If p is finitely branching and q is RT-saturated then p ⊑_{F T} q ⇔ p ⊑_{RT} q. Thus if both p and q are finitely branching and RT-saturated then p =_{F T} q ⇔ p =_{RT} q. Proof: Suppose p is finitely branching, q is RT-saturated and p ⊑_{F T} q. With induction on k ∈ IN I will show that whenever X_{0}a_{1}X_{1}a_{2} ⋯ a_{n}X_{n} ∈ RT (p) then there are Y_{i} ⊆ X_{i} for i = k + 1, …, n such that X_{0}a_{1}X_{1}a_{2} ⋯ a_{k}X_{k}a_{k+1}Y_{k+1}a_{k+2} ⋯ a_{n}Y_{n} ∈ RT (q). The case k = n, together with Proposition 6.1, completes the proof of the proposition. Induction base (k = 0): Let X_{0}a_{1}X_{1}a_{2} ⋯ a_{n}X_{n} ∈ RT (p). Write \overline{X} for Act − X. Then \overline{X_{0}}a_{1}\overline{X_{1}}a_{2} ⋯ a_{n}\overline{X_{n}} ∈ F T (p) ⊆ F T (q). Hence there are Y_{i} ⊆ X_{i} for i = 0, ..., n such that Y_{0}a_{1}Y_{1}a_{2} ⋯ a_{n}Y_{n} ∈ RT (q). As p ⊑_{F T} q ⇒ p ⊑_{T} q ⇒ I(p) ⊆ I(q), we have Y_{0} = X_{0}. Induction step: Take k > 0 and suppose the statement has been established for k − 1. Let X_{0}a_{1}X_{1}a_{2} ⋯ a_{n}X_{n} ∈ RT (p). Then, by induction, there are Y_{i} ⊆ X_{i} for i = k, ..., n such that X_{0}a_{1}X_{1}a_{2} ⋯ a_{k−1}X_{k−1}a_{k}Y_{k}a_{k+1}Y_{k+1}a_{k+2} ⋯ a_{n}Y_{n} ∈ RT (q). Moreover, for every b ∈ X_{k}, X_{0}a_{1}X_{1}a_{2} ⋯ a_{k}X_{k}b ∈ RT (p), so, again using the induction hypothesis, there must be a Z_{b} ⊆ X_{k} such that X_{0}a_{1}X_{1} ⋯ X_{k−1}a_{k}Z_{b}b ∈ RT (q), and hence X_{0}a_{1}X_{1} ⋯ X_{k−1}a_{k}(Z_{b} ∪ {b}) ∈ RT (q). As X_{k} is finite and Y_{k} ∪ ⋃_{b∈X_{k}}(Z_{b} ∪ {b}) = X_{k}, the RT-saturation of q gives X_{0}a_{1} ⋯ a_{k}X_{k}a_{k+1}Y_{k+1}a_{k+2} ⋯ a_{n}Y_{n} ∈ RT (q), which had to be established. □

17 Complete axiomatizations

17.1 A language for finite, concrete, sequential processes

Consider the following basic CCS- and CSP-like language BCCSP for finite, concrete, sequential processes over a given alphabet Act:

inaction : 0 (called nil or stop) is a constant, representing a process that refuses to do any action.

action : a is a unary operator for any action a ∈ Act. The expression ap represents a process, starting with an a-action and proceeding with p.

choice : + is a binary operator. p + q represents a process, first being involved in a choice between its summands p and q, and then proceeding as the chosen process.

The set T(BCCSP) of (closed) process expressions or terms over this language is defined as usual:

• 0 ∈ T(BCCSP),

• ap ∈ T(BCCSP) for any a ∈ Act and p ∈ T(BCCSP),

• p + q ∈ T(BCCSP) for any p, q ∈ T(BCCSP).

Subterms a0 may be abbreviated by a. Brackets are used for disambiguation only, assuming associativity of +, and letting a bind stronger than +. If P = {p_{1}, ..., p_{n}} is a finite nonempty multiset of BCCSP expressions, then ΣP abbreviates p_{1} + ⋯ + p_{n}. This expression is determined only up to associativity and commutativity of +. Let Σ∅ := 0. An expression ap′ is called a summand of p if, up to associativity and commutativity of +, p can be written as ΣP with ap′ ∈ P.

On T(BCCSP) action relations ⟶^{a} for a ∈ Act are defined as the predicates on T(BCCSP) generated by the action rules of Table 1. Here a ranges over Act and p and q over T(BCCSP).

ap ⟶^{a} p  \frac{p ⟶^{a} p′}{p + q ⟶^{a} p′}  \frac{q ⟶^{a} q′}{p + q ⟶^{a} q′}

Table 1: Action rules for BCCSP

A trivial structural induction shows that p ⟶^{a} p′ iff ap′ is a summand of p. Now all semantic equivalences of Sections 2–14 are well-defined on T(BCCSP), and for each of the semantics it is determined when two process expressions denote the same process.

The following theorem says that, apart from U, all these semantics are compositional w.r.t. BCCSP, i.e. all semantic equivalences are congruences for BCCSP.

Theorem 7 Let p, q, r, s ∈ T(BCCSP) and let O be any of the semantics of Section 15 except U. Then

p =_{O} q ∧ r =_{O} s ⇒ ap =_{O} aq ∧ p + r =_{O} q + s.

Proof: Each of the semantics O has a modal characterization, given by p =_{O} q ⇔ O(p) = O(q), where O(p) is the set of modal formulas of the appropriate form satisfied by p. Let O^{+}(p) := {aφ | aφ ∈ O(p)} be the set of such formulas which are of the form aφ. For each choice of O one easily verifies that O(p) is completely determined by O^{+}(p), i.e. O(p) = O(q) ⇔ O^{+}(p) = O^{+}(q). One also verifies easily that O^{+}(0) = ∅, O^{+}(ap) = {aφ | φ ∈ O(p)} and O^{+}(p+q) = O^{+}(p)∪O^{+}(q). From this the theorem follows immediately. □

For each such choice of O one easily verifies that moreover O(p) ⊆ O(q) ⇔ O^{+}(p) ⊆ O^{+}(q). From this it follows that all the preorders of Section 15 are precongruences for BCCSP:

Theorem 7b Let p, q, r, s ∈ T(BCCSP) and let O be any of the semantics of Section 15 but U. Then

p ⊑_{O} q ∧ r =_{O} s ⇒ ap ⊑_{O} aq ∧ p + r ⊑_{O} q + s. □

Tree semantics, when defined merely in terms of the action relations on T(BCCSP), fails to be compositional w.r.t. BCCSP. The expression a0 + a0 has only a single outgoing a-transition, namely to the expression 0. Thus, by Definition 13, a0 + a0 =_{U} a0. Likewise b(a0 + a0) =_{U} ba0. However, b(a0 + a0) + b0 ≠_{U} ba0 + ba0, as the first process has two outgoing b-transitions and the second process only one. If follows that tree equivalence as defined above is not compositional w.r.t. +.

T(BCCSP) can be turned into a labelled transition system with multiplicities by assuming a different transition p ⟶^{a} q for every different proof of p ⟶^{a} q from the action rules of Table 1. On such a transition system tree equivalence is compositional w.r.t. BCCSP.

A straightforward structural induction shows that any process p ∈ T(BCCSP) is finite in the sense of Definition 1.2. Hence the process graph G(p) is finite as well. The next proposition establishes that moreover, up to bisimulation equivalence, any finite process graph can be represented by a BCCSP expression. In fact, all finite process graphs displayed in this paper have been annotated by their representing BCCSP expressions.

Definition 17.1 Let {// \atop \\}·{\\ \atop //} : IH → T(BCCSP) be a mapping satisfying {// \atop \\}g{\\ \atop //} = Σ\{a{// \atop \\}h{\\ \atop //} | g ⟶^{a} h\}.

A straightforward induction on the length of the longest path of finite process graphs teaches that such a mapping exists and is completely determined up to associativity and commutativity of +.

Proposition 17.1 Let g ∈ IH. Then there is a p ∈ T(BCCSP) with G(p)\underline{↔} g. In fact, G({// \atop \\}g{\\ \atop //})\underline{↔} g. Proof: It suffices to show that the relation \{h, G({// \atop \\}h{\\ \atop //}) | h ∈ IH\} is a bisimulation. Suppose h ⟶^{a} h′.

Then a{// \atop \\}h′{\\ \atop //} is a summand of {// \atop \\}h{\\ \atop //}, so {// \atop \\}h{\\ \atop //} ⟶^{a} {// \atop \\}h′{\\ \atop //}, and by Proposition 1.1 G({// \atop \\}h{\\ \atop //}) ⟶^{a} G({// \atop \\}h′{\\ \atop //}).

Vice versa, let G({// \atop \\}h{\\ \atop //}) ⟶^{a} h′′. Then, by Proposition 1.1, h′′ = G(p′) for some p′ ∈ T(BCCSP) with {// \atop \\}h{\\ \atop //} ⟶^{a} p′. Thus ap′ must be a summand of {// \atop \\}h{\\ \atop //}. By Definition 17.1 p′ = {// \atop \\}h′{\\ \atop //} for some h′ ∈ IH with h ⟶^{a} h′. As h′ is related to h′′ = G({// \atop \\}h′{\\ \atop //}), also this requirement is satisfied. □

Corollary 17.1 Let p ∈ T(BCCSP). Then p\underline{↔} {// \atop \\}G(p){\\ \atop //}. Proof: By the above G({// \atop \\}G(p){\\ \atop //})\underline{↔} G(p). Now apply Corollary 1.1. □

Corollary 17.2 Let g, h ∈ IH and let O be any of the semantics of Section 15. Then

g ⊑_{O} h ⇔ {// \atop \\}g{\\ \atop //} ⊑_{O} {// \atop \\}h{\\ \atop //} and g =_{O} h ⇔ {// \atop \\}g{\\ \atop //} =_{O} {// \atop \\}h{\\ \atop //}.

Proof: Let g ⊑_{O} h. By the above G({// \atop \\}g{\\ \atop //})\underline{↔} g ⊑_{O} h\underline{↔} G({// \atop \\}h{\\ \atop //}). Now apply Corollary 1.1. For “⇐” let {// \atop \\}g{\\ \atop //} ⊑_{O} {// \atop \\}h{\\ \atop //}. By Corollary 1.1 and Proposition 17.1 g \underline{↔} G({// \atop \\}g{\\ \atop //}) ⊑_{O} G({// \atop \\}h{\\ \atop //})\underline{↔} h. □

17.2 Axiomatizing the equivalences

In Table 2, complete axiomatizations can be found for twelve of the fifteen semantic equivalences of this paper that differ on BCCSP. Axioms for singleton-failures, 2-nested simulation and possiblefutures semantics are more cumbersome, and the corresponding testing notions are less plausible. Therefore they have been omitted. The axiomatization of tree semantics (U) requires action relations with multiplicities. Although rather trivial, I will not formally establish its soundness and completeness here. In order to formulate the axioms, variables have to be added to the language as usual. In the axioms they are supposed to be universally quantified. Most of the axioms are axiom schemes, in the sense that there is one axiom for each substitution of actions from Act for the parameters a, b, c. Some of the axioms are conditional equations, using an auxiliary operator I. Thus provability is defined according to the standards of either first-order logic with equality or conditional equational logic. I is a unary operator that calculates the set of initial actions of a process expression, coded as a process expression again.

Theorem 8 For each of the semantics O ∈ {T, S, CT, CS, F, R, F T, RT, P W, RS, B} two process expressions p, q ∈ T(BCCSP) are O-equivalent iff they can be proved equal from the axioms marked with “+” in the column for O in Table 2. The axioms marked with “v” or “ω” are valid in O-semantics but not needed for the proof.

U B RS PW RT FT R F CS CT S T
(x + y) + z = x + (y + z)  + + + + + + + + + + + +
x + y = y + x  + + + + + + + + + + + +
x + 0 = x  + + + + + + + + + + + +
x + x = x  + + + + + + + + + + +
I(x) = I(y) ⇒ a(x + y) = a(x + y) + ay  + v v v v v v v v v
a(bx + by + z) = a(bx + z) + a(by + z)  + v v v v  v  v
I(x) = I(y) ⇒ ax + ay = a(x + y)  + + v v  v  v
ax + ay = ax + ay + a(x + y)  +  v  v  v
a(bx+u) + a(by+v) = a(bx+by+u) + a(by+v)  + +  v  v
ax + a(y + z) = ax + a(x + y) + a(y + z)  +  ω  v
a(x + by + z) = a(x + by + z) + a(by + z)  + v v v
a(bx + u) + a(cy + v) = a(bx + cy + u + v) + v
a(x + y) = a(x + y) + ay  + v
ax + ay = a(x + y)  +
I(0) = 0  + + + + + + + + + + + +
I(ax) = a0  + + + + + + + + + + + +
I(x + y) = I(x) + I(y)  + + + + + + + + + + + +

Table 2: Complete axiomatizations for the equivalences

Proof: “If” (soundness): In the light of Theorem 7 it suffices to show that the closed instances of the indicated axioms are valid in the corresponding semantics. This is straightforward.

“Only if” (completeness): Let T_{O} be the set of axioms marked with “+” in the column for O. Write T_{O} ⊢ p = q if the equation p = q is provable from T_{O}. I have to show that

p =_{O} q ⇒ T_{O} ⊢ p = q  (2)

for any p, q ∈ T(BCCSP). For the cases O ∈ {B, S, RS, CS} I will show that

p ⊑_{O} q ⇒ T_{O} ⊢ q = q + p  (3)

for any p, q ∈ T(BCCSP), from which (2) follows immediately. This will be done with structural induction on p and q. So assume p ⊑_{O} q and (3) has been proven for all pairs of smaller expressions p′, q′ ∈ T(BCCSP). Provided T_{O} contains at least the first four axioms of Table 2, one has T_{O} ⊢ q = q + p iff T_{O} ⊢ q = q + ap′ for every summand ap′ of p.

Take O = B, so p ⊑_{B} q. Let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ =_{B} q′. By induction T_{B} ⊢ p′ = p′ + q′ = q′, using Proposition 12.1. Furthermore, aq′ must be a summand of q, so T_{B} ⊢ q = q + aq′ = q + ap′ and therefore T_{B} ⊢ q = q + p.

Take O = S, so p ⊑_{S} q. Let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ ⊑_{S} q′. By induction T_{S} ⊢ q′ = q′ + p′, so T_{S} ⊢ aq′ = a(q′ + p′) = a(q′ + p′) + ap′ = aq′ + ap′. Furthermore, aq′ must be a summand of q, so T_{S} ⊢ q = q + aq′ = q + ap′ and thus T_{S} ⊢ q = q + p.

Take O = RS, so p ⊑_{RS} q. Let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ ⊑_{RS} q′. Now I(p′) = I(q′) and hence T_{RS} ⊢ I(p′) = I(q′). By induction T_{RS} ⊢ q′ = q′ + p′, so T_{RS} ⊢ aq′ = a(q′ + p′) = a(q′ + p′) + ap′ = aq′ + ap′. Furthermore, aq′ must be a summand of q, so T_{RS} ⊢ q = q + aq′ = q + ap′ and thus T_{RS} ⊢ q = q + p.

Take O = CS, so p ⊑_{CS} q. Let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ ⊑_{CS} q′. In case I(p′) = ∅ it must be that I(q′) = ∅ as well, and hence T_{CS} ⊢ p′ = q′ = 0. Otherwise, T_{CS} ⊢ p′ = bp′′ + r and by induction T_{CS} ⊢ q′ = q′ + p′, so T_{CS} ⊢ aq′ = a(q′ + p′) = a(q′ + bp′′ + r) = a(q′ + bp′′ + r) + a(bp′′ + r) = a(q′ + p′) + ap′ = aq′ + ap′. Furthermore, aq′ must be a summand of q, so in both cases T_{CS} ⊢ q = q + aq′ = q + ap′ and thus T_{CS} ⊢ q = q + p.

Take O = P W. Suppose p =_{P W} q. The axiom a(bx + by + z) = a(bx + z) + a(by + z) allows to rewrite p and q to BCCSP expressions p′ = Σ_{i∈I}a_{i}p_{i} and q′ = Σ_{j∈J}a_{j}q_{j} with p_{i} and q_{j} deterministic. For expressions of this form it is easy to establish that p′ =_{P W} q′ ⇔ p′ \underline{↔} q′. Using the soundness of the axiom employed, and the completeness of T_{B} ⊆ T_{P W} for \underline{↔}, it follows that T_{P W} ⊢ p = p′ = q′ = q.

For F and R (as well as B) a proof is given in Bergstra, Klop & Olderog [11] by means of graph transformations. A similar proof for RT can be found in Baeten, Bergstra & Klop [6]. This method, applied to semantics O, requires the definition of a class IH^{∗} of finite process graphs that contains at least all finite process trees, and a binary relation ⇝^{O} ⊆ IH^{∗} × IH^{∗} — a system of graph transformations—such that the following can be established:

1. ⇝^{O}, used as a rewriting system, is terminating on IH^{∗}, i.e. any reduction sequence g_{0} ⇝^{O} g_{1} ⇝^{O} ⋯ leads (in finitely many steps) to a normal form, a graph that cannot be further transformed,

2. if g ⇝^{O} h then (a) g =_{O} h and (b) T_{O} ⊢ {// \atop \\}g{\\ \atop //} = {// \atop \\}h{\\ \atop //}

3. and two normal forms are bisimilar iff they are O-equivalent. Now the completeness proof goes as follows: Suppose p =_{O} q. As paths(G(p)) and paths(G(q)) are finite, U(G(p)) and U(G(q)) belong to IH^{∗}, and by requirement 1 they can be rewritten to normal forms g and h. Using Corollary 1.1, Proposition 13.1 and requirement 2(a) above

g =_{O} U(G(p))\underline{↔} G(p) =_{O} G(q)\underline{↔} U(G(q)) =_{O} h.

Thus, with requirement 3, g \underline{↔} h; and Corollaries 17.1 and 17.2 yield

p\underline{↔} {// \atop \\}G(p){\\ \atop //} \underline{↔} {// \atop \\}U(G(p)){\\ \atop //},  {// \atop \\}g{\\ \atop //} \underline{↔} {// \atop \\}h{\\ \atop //},  {// \atop \\}U(G(q)){\\ \atop //} \underline{↔} {// \atop \\}G(q){\\ \atop //} \underline{↔} q.

Requirement 2(b) and the completeness result for bisimulation semantics proved above finally give

T_{O} ⊢ p = {// \atop \\}U(G(p)){\\ \atop //} = {// \atop \\}g{\\ \atop //} = {// \atop \\}h{\\ \atop //} = {// \atop \\}U(G(q)){\\ \atop //} = q.

I will now apply this method to T, RT, CT, R, F and F T. In the cases of T, RT and CT, IH^{∗} is taken to be IH^{tree}, the class of finite process trees.

Take O = T. Let ⇝^{T} be the graph transformation that converts g into h, notation g ⇝^{T} h, iff g is a finite tree with edges (s, a, t) and (s, a, u) with t ≠ u, and h is obtained by identifying t and u. Formally speaking, the nodes of h are those of g, except that t and u are omitted and a fresh node v has been added instead. Often v is taken to be the (equivalence) class {t, u}. Define the function ′ : nodes(g) → nodes(h) by t′ = v, u′ = v and w′ = w for w ≠ t, u. Now edges(h) = {(p′, a, q′) | (p, a, q) ∈ edges(g)} and root(h) = root(g)′. This graph transformation is illustrated in Figure 10.

⋯  ⋯ s t  u a  a b_{1} b_{n} c_{1} c_{m}  ⇝^{T} ⋯  ⋯ sva b_{1} b_{n} c_{1}c_{m}  ⋯ tu  v w a_{1}  a_{n} a_{1} a_{n} b  b ⇝^{R}  ⋯ tu  v w a_{1}  a_{n} a_{1} a_{n} b  b b b

Figure 10: Graph transformations

If g is a finite tree and g ⇝^{T} h then so is h. Moreover, h has fewer nodes than g. Hence ⇝^{T} is terminating on IH^{tree}. The normal forms are exactly the finite deterministic trees. Now requirement 3 has been established by Theorem 6. Requirement 2(a) is trivial, and for 2(b) observe that any application of ⇝^{T} corresponds to an application of the axiom ax + ay = a(x + y).

Take O = RT . Let ⇝^{RT} be the same graph transformation as ⇝^{T}, except that it only applies if I(t) = I(u). This time the normal forms are the ready trace deterministic trees, and requirement 3 has been established by Proposition 16.3. Again requirement 2(a) is easy to check, and for 2(b) it suffice to observe that any application of ⇝^{RT} corresponds to an application of the axiom I(x) = I(y) ⇒ ax + ay = a(x + y).

Take O = CT . Let ⇝^{CT} be the same graph transformation as ⇝^{T}, except that it only applies if I(t) = ∅ ⇔ I(u) = ∅. This time the normal forms are the completed trace deterministic trees, and again requirement 3 has been established by Proposition 16.3. Once more requirement 2(a) is easy to check, and for 2(b) observe that any application of ⇝^{CT} corresponds to an application of the law (I(x) = 0 ⇔ I(y) = 0) ⇒ ax + ay = a(x + y). This law falls outside conditional equational logic, but it can be reformulated equationally by considering the two cases I(x) = 0 = I(y) and I(x) ≠ 0 ≠ I(y). In the first case it must be that T_{B} ⊢ x = 0 = y and hence the law follows from the third and fourth axiom of Table 2. In the second, observe that I(p) ≠ 0 iff p has the form bq +r with b ∈ Act. Hence the law can be reformulated as a(bx + u) + a(cy + v) = a(bx + cy + u + v).

A process graph g ∈ ^{|}G is called history unambiguous [11] if any two paths from the root to the same node give rise to the same trace, i.e. if for π, π′ ∈ paths(g) one has end(π) = end(π′) ⇒ T (π) = T (π′). The history or trace T (s) of a node s in such a graph g is defined as T (π) for π an arbitrary path from the root of g to s. Observe that trees are history unambiguous. In the next two completeness proofs (the cases R and F) IH^{∗} is taken to be the class IH^{hu} of finite, history unambiguous, connected process graphs. For g ∈ IH^{hu} and t, v ∈ nodes(g) let t ∼ v abbreviate

∀s ∈ nodes(g), a ∈ Act : (s, a, t) ∈ edges(g) ⇔ (s, a, v) ∈ edges(g).

Take O = R. Let ⇝^{R} be the graph transformation with g ⇝^{R} h iff g has edges (t, b, u) and (v, b, w) with t ∼ v, and h is obtained by adding a new edge (t, b, w). This graph transformation is illustrated in Figure 10. Note that by applying ⇝^{R} twice, one can also add the edge (v, b, u) (indicated with a dashed arrow in Figure 10) if it isn’t there already. If g is a finite, history unambiguous process graph and g ⇝^{R} h then so is h. Moreover, h has more edges than g. As there is an upperbound to the number of edges of graphs that can be obtained from a given graph g ∈ IH^{hu} by applying ⇝^{R} (namely n × l × n, where n is the number of nodes in g, and l the number of different edge-labels occurring in g), ⇝^{R} is terminating on IH^{hu} (requirement 1). It is easy to see that ⇝^{R} does not add new ready pairs. This gives requirement 2(a). For 2(b) observe that an application of ⇝^{R} corresponds to a number of applications of a(bx+u)+a(by +v) = a(bx+by +u)+a(by +v). Finally, requirement 3 follows from Proposition 16.5 and the following Claim: The normal forms w.r.t. ⇝^{R} are cross saturated. Proof of the claim: Let g ∈ IH^{hu} be a normal form w.r.t. ⇝^{R}. With induction to the length of T (u) I will show that, for u, w ∈ nodes(g),

if T (u) = T (w) then u ∼ w.  (4)

This implies that g is cross saturated, for if π, π′ and a are as in the remark below Definition 16.3, there must be an edge (end(π), a, u) in g. Now T (u) = T (π)a = T (end(π′)), so also (end(π), a, end(π′)) ∈ edges(g). Induction base: If length(T (u)) = 0, one has u = w = root(g) and the statement is trivial. Induction step: Let T (u) = T (w) ≠ ε, and let (t, b, u) ∈ edges(g). By symmetry, it suffices to show that (t, b, w) ∈ edges(g). As g is connected and history unambiguous, there must be an edge (v, b, w) with T (t) = T (v). By induction t∼v. As g is in normal form it must have an edge (t, b, w).

⋯  ⋯  ⋯ b_{1}  b_{n}  c_{1} c_{k} d_{1} d_{m} s t  a  u a  ⇝^{fork}  ⋯  ⋯  ⋯ a b_{1}b_{n} c_{1} c_{k} b_{1} b_{n}  c_{1} c_{k} d_{1} d_{m} s t  a  u v a

Figure 11: Fork

Take O = F . Let ⇝^{fork} be the graph transformation with g ⇝^{fork} h iff g has edges (s, a, t) and (s, a, u), ∃Y ⊆ I(u) such that h is given by

• nodes(h) = nodes(g) ._{∪} {v}

• root(h) = root(g)

• edges(h) = edges(g) ∪ {(s, a, v)} ∪{(v, b, w) | (t, b, w) ∈ edges(g)} ∪ {(v, b, w) | (u, b, w) ∈ edges(g) ∧ b ∈ Y } and |R(h)| > |R(g)|. This graph transformation is illustrated in Figure 11. Note that for any path π ∈ paths(h) not ending in v, a path π′ ∈ edges(g) can be found with T (π′) = T (π) and end(π′) = end(π), namely by circumventing the possible portion through v along t or u. Thus, such paths do not give rise to new ready or failure pairs. For any path π ∈ paths(h) ending in v there is a path π′ ∈ edges(g) with T (π′) = T (π) and end(π′) = t. As I(t) ⊆ I(v), also such paths do not give rise to new failure pairs. Hence one has R(h) = R(g) ∪ {^{/} \T (t), I(t) ∪ Y ^{\} /} and F (h) = F (g). Note that if g ∈ IH^{hu} and g ⇝^{fork} h, then also h ∈ IH^{hu}. Let ⇝^{F} be ⇝^{R} ∪ ⇝^{fork}. As g ⇝^{fork} h ⇒ g =_{F} h and g ⇝^{R} h ⇒ g =_{R} h ⇒ g =_{F} h, requirement 2(a) is satisfied. For 2(b) observe that an application of ⇝^{fork} corresponds to an application of the axiom ax + a(y + z) = ax + a(x + y) + a(y + z).

The requirement |R(h)| > |R(g)| says that the transformation may only take place if it actually increases the ready set of the transformed graph. Note that if g ⇝^{F} h then T (g) = T (h). As there is an upperbound to the number of ready pairs of graphs g with a given trace set (namely |T (g)| × 2^{l}, where l is the number of different edge-labels occurring in g), a reduction sequence g_{0} ⇝^{F} g_{1} ⇝^{F} ⋯ on IH^{hu} can contain only finitely many occurrences of ⇝^{fork}. After the last such occurrence it leads in finitely many steps to a normal form, because ⇝^{R} is terminating on IH^{hu}. Hence also ⇝^{F} is terminating on IH^{hu} (requirement 1).

Suppose g is a normal form w.r.t. ⇝^{F} and ^{/} \σ, X^{\} / ∈ R(g) ∧ ^{/} \σ, Y ∪ Z^{\} / ∈ R(g). Then g has nodes t and u with T (t) = T (u) = σ, I(t) = X and Y ⊆ I(u). As g must be a normal form w.r.t. ⇝^{R}, it satisfies (4) and hence t ∼ u. As g is connected, there are edges (s, a, t) and (s, a, u) in g. As g must also be a normal form w.r.t. ⇝^{fork}, ^{/} \σ, X ∪ Y ^{\} / ∈ R(g). Thus normal forms w.r.t. ⇝^{F} are saturated as well as cross saturated, and hence requirement 3 follows by Propositions 16.7 and 16.5.

Take O = FT . Let ⇝^{sf} (symmetric fork) be the graph transformation consisting of those instances of ⇝^{fork} where Y = I(u), but with the requirement |R(h)| > |R(g)| relaxed to |RT_{N}(h)| > |RT_{N}(g)|. Let IH^{∗} be IH^{tree}, and define ⇝^{sfu} by g ⇝^{sfu} h if g ⇝^{sf} h′ and h = U(h′). Thus ⇝^{sfu} is the variant of ⇝^{sf} in which the target is unfolded into a tree. Let ⇝^{FT} be ⇝^{RT} ∪ ⇝^{sfu}. As there is an upperbound to the number of normal ready traces of graphs with a given finite trace set, ⇝^{FT} is terminating on IH^{∗} (requirement 1). The normal forms are exactly the finite RT -saturated ready trace deterministic process trees, so requirement 3 follows from Propositions 16.3 and 16.8. It follows immediately from Corollary 5.1 that g ⇝^{sf} h ⇒ g =_{FT} h. Hence Proposition 13.1 gives g ⇝^{sfu} h ⇒ g =_{FT} h. Moreover, g ⇝^{RT} h ⇒ g =_{RT} h ⇒ g =_{FT} h, which yields requirement 2(a). For 2(b) observe that an application of ⇝^{sf} corresponds to an application of the axiom ax + ay = ax + ay + a(x + y), and as h\underline{↔} U(h) Corollary 17.2 gives T_{B} ⊢ {// \atop \\}h{\\ \atop //} = {// \atop \\}U(h){\\ \atop //} for h ∈ IH. □

In Theorem 8 the fifth and seventh axioms of Table 2 may be replayed by

a ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i}) = a ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i}) + a ∑_{i=1}^{n} b_{i}y_{i} and a ∑_{i=1}^{n} b_{i}x_{i} + a ∑_{i=1}^{n} b_{i}y_{i} = a ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i}).

These laws derive the same closed substitution instances. Thus none of the axiomatizations require the operator I, or conditional equations. However, the laws above are axioms schemes which have instances for any choice of n ∈ IN. Even if Act is finite, the axiomatizations involving these laws are infinite.

Theorem 9 Suppose Act is infinite. For each of the semantics O ∈ {T, S, CT, F, R, F T, RT, RS, B, U} two BCCSP expressions with variables are O-equivalent iff they can be proved equal from the axioms marked with ‘+’ or ‘ω’ in the column for O in Table 2. It follows that the axioms marked with ‘v’ are derivable.

Proof: For O ∈ {T, CT, F, R, F T, RT, B} this has been established in Groote [23]. His proof for F, R, F T and RT can be applied to S and RS as well. The proof for U is rather trivial, but omitted here. □

Groote also showed that if Act is finite, Theorem 9 does not hold for F, R, F T and RT. But for B and CT it suffices to assume that Act is nonempty, and for T it suffices to assume that Act has at least two elements. I do not know which cardinality restriction on Act is needed in the cases of S and RS. A complete axiomatization for open terms for completed simulation or possible worlds semantics has so far not been provided.

17.3 Axiomatizing the preorders

In Table 3, complete axiomatizations can be found for the eleven preorders corresponding to the equivalences axiomatized in Table 2 (there is no preorder for tree semantics (U)). This time provability is defined according to the standards of either first-order logic with inequality or conditional inequational logic, i.e. it may be used that ⊑ is reflexive and transitive and satisfies the precongruence properties of Theorem 7b. For any semantics O the O-preorder and O-equivalence are related by p =_{O} q ⇔ p ⊑_{O} q ∧ q ⊑_{O} p. Thus either p = q is taken to be an abbreviation of p ⊑ q ∧ q ⊑ p or the conditional axioms p = q ⇒ p ⊑ q and p ⊑ q ∧ q ⊑ p ⇒ p = q are considered part of the axiomatizations. In the latter case, the axioms of Table 3 also constitute complete axiomatizations of the equivalences.

The three axioms in Table 3 in which the inequality is written “⊑” represent strengthenings of the corresponding axioms in Table 2. The axioms in which the inequality is written “⊒” are merely slick reformulations of the corresponding axioms in Table 2, and could be replaced by them. Unlike in Table 2, the characteristic axiom for the readiness preorder (the ninth) is now a substitution instance of the characteristic axiom for the failures preorder (the tenth).

Note that the characteristic axiom for the ready simulation preorder (the fifth) derives all closed instances of I(x) = I(y) ⇒ ax ⊑ a(x + y), which gives the fifth axiom of Table 2. Hence all closed instances of the characteristic axiom for the ready trace preorder (the seventh) are derivable from the fifth and eighth axioms. It follows that conditional (in)equations, involving the operator I, or unbounded sums, are no longer needed in the axiomatizations of ready simulation and failure trace semantics.

Theorem 10 For each of the semantics O ∈ {T, S, CT, CS, F, R, F T, RT, P W, RS, B} one has p ⊑_{O} q for p, q ∈ T(BCCSP) iff p ⊑ q can be proved from the axioms marked with “+” in the column for O in Table 3. The axioms marked with “v” are valid in O-semantics but not needed for the proof.

Proof: “If” (soundness): In the light of Theorem 7b it suffices to show that the closed instances of the indicated axioms are valid in the corresponding semantics. This is straightforward.

“Only if” (completeness): Let T_{O}^{∗} be the set of axioms marked with “+” in the column for O. Write T_{O}^{∗} ⊢ p ⊑ q if the inequation p ⊑ q is provable from T_{O}^{∗}. I have to show that

p ⊑_{O} q ⇒ T_{O}^{∗} ⊢ p ⊑ q  (5)

B RS PW RT FT R F CS CT S T
(x + y) + z = x + (y + z)  + + + + + + + + + + +
x + y = y + x  + + + + + + + + + + +
x + 0 = x  + + + + + + + + + + +
x + x = x  + + + + + + + + + + +
ax ⊑ ax + ay  + + + + + + v v v v
a(bx + by + z) = a(bx + z) + a(by + z)  + v v v v  v  v
I(x) = I(y) ⇒ ax + ay = a(x + y)  + v v v  v  v
ax + ay ⊒ a(x + y)  +  v  v  v
a(bx + u) + a(by + v) ⊒ a(bx + by + u)  + v  v  v
ax + a(y + z) ⊒ a(x + y)  +  v  v
ax ⊑ ax + y  + + v v
a(bx + u) + a(cy + v) = a(bx + cy + u + v) + v
x ⊑ x + y  + +
ax + ay = a(x + y)  +
I(0) = 0  + + + + + + + + + + +
I(ax) = a0  + + + + + + + + + + +
I(x + y) = I(x) + I(y)  + + + + + + + + + + +

Table 3: Complete axiomatizations for the preorders

for any p, q ∈ T(BCCSP). The case O = B follows from Proposition 12.1 and Theorem 8. For the cases O ∈ {S, CS, RS} (5) will be established with structural induction on p and q. So assume p ⊑_{O} q and (5) has been proven for all pairs of smaller expressions p′, q′ ∈ T(BCCSP).

Take O = S, so p ⊑_{S} q. Using the axiom x ⊑ x + y one finds that T_{S}^{∗} ⊢ p ⊑ q if for every summand ap′ of p there is a summand aq′ of q such that T_{S}^{∗} ⊢ ap′ ⊑ aq′. So let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ ⊑_{S} q′. Note that aq′ is a summand of q. By induction T_{S}^{∗} ⊢ p′ ⊑ q′, so T_{S}^{∗} ⊢ ap′ ⊑ aq′.

Take O = CS, so p ⊑_{CS} q. Using the axiom ax ⊑ ax + y one finds that T_{CS}^{∗} ⊢ p ⊑ q if I(p) ≠ ∅ and for every summand ap′ of p there is a summand aq′ of q such that T_{CS}^{∗} ⊢ ap′ ⊑ aq′. In case I(p) = ∅ it must be that I(q) = ∅ as well, and hence T_{CS}^{∗} ⊢ p = q = 0. Otherwise, let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ ⊑_{CS} q′. Note that aq′ is a summand of q. By induction T_{CS}^{∗} ⊢ p′ ⊑ q′, so T_{CS}^{∗} ⊢ ap′ ⊑ aq′.

Take O = RS, so p ⊑_{RS} q. Using the first five axioms of Table 3 one finds that T_{RS}^{∗} ⊢ p ⊑ q if I(p) = I(q) and for every summand ap′ of p there is a summand aq′ of q such that T_{RS}^{∗} ⊢ ap′ ⊑ aq′. As p ⊑_{RS} q one has I(p) = I(q). Let ap′ be a summand of p. Then p ⟶^{a} p′, so ∃q′ : q ⟶^{a} q′ and p′ ⊑_{RS} q′. Note that aq′ is a summand of q. By induction T_{RS}^{∗} ⊢ p′ ⊑ q′, so T_{RS}^{∗} ⊢ ap′ ⊑ aq′.

Take O = P W. Suppose p ⊑_{P W} q. The axiom a(bx + by + z) = a(bx + z) + a(by + z) allows to rewrite p and q to BCCSP expressions p′ = Σ_{i∈I}a_{i}p_{i} and q′ = Σ_{j∈J}a_{j}q_{j} with p_{i} and q_{j} deterministic. For expressions of this form it is easy to establish that p′ ⊑_{P W} q′ ⇔ p′ ⊑_{RS} q′. Using the soundness of the axiom employed, and the completeness of T_{RS} ⊆ T_{P W} for ⊑_{RS}, it follows that T_{P W} ⊢ p = p′ ⊑ q′ = q.

The remaining completeness proofs go by a variant of the method of graph transformations, where requirement 3 is replaced by

if g and h are normal forms, then g ⊑_{O} h ⇔ g ⊑_{N} h.

Here N should be a semantics finer than O, for which the completeness theorem has already been established, and for which T_{N}^{∗} ⊆ T_{O}^{∗}. The reasoning now goes exactly as in the proof of Theorem 8: Suppose p ⊑_{O} q. Rewrite U(G(p)) and U(G(q)) to normal forms g and h. Then

g =_{O} U(G(p))\underline{↔} G(p) ⊑_{O} G(q)\underline{↔} U(G(q)) =_{O} h.

Thus, with requirement 3, g ⊑_{N} h. Corollary 17.2 yields {// \atop \\}g{\\ \atop //} ⊑_{N} {// \atop \\}h{\\ \atop //}, and one obtains

T_{O}^{∗} ⊢ p = {// \atop \\}U(G(p)){\\ \atop //} = {// \atop \\}g{\\ \atop //} ⊑ {// \atop \\}h{\\ \atop //} = {// \atop \\}U(G(q)){\\ \atop //} = q.

For each of the six remaining completeness proofs, the class IH^{∗} and the graph transformations are the same as in the proof of Theorem 8. Thus requirements 1 and 2(a) are fulfilled. As (the closed instances of) the axioms for the respective equivalences from Table 2 are easily derivable from the ones for the corresponding preorders from Table 3, requirement 2(b) is fulfilled as well. Requirement 3, which used to follow from Theorem 6 and Propositions 16.3, 16.5, 16.7 and 16.8, now follows from Propositions 16.4, 16.6, 16.7 and 16.8. □

17.4 A language for finite, concrete, sequential processes with internal choice

Let BCSP be the language that extends BCCSP with a binary operator ⊕, modelling internal choice. Like p+q, the expression p⊕q represents a process, first being involved in a choice between its summands p and q, and then proceeding as the chosen process. However, whereas + represents a choice that can be influenced by the environment of the process (an external choice), ⊕ represents one that is due to internal nondeterminism of the specified system. BCSP can be regarded as a basic fragment of the language CSP of Hoare [31].

The set T(BCSP) of (closed) terms over BCSP, or (closed) BCSP-expressions, and its subset T_{1}(BCSP) of initially deterministic BCSP-expressions, are defined by:

• 0 ∈ T_{1}(BCSP) ⊆ T(BCSP),

• aP ∈ T_{1}(BCSP) for any a ∈ Act and P ∈ T(BCSP),

• p + q ∈ T_{1}(BCSP) for any p, q ∈ T_{1}(BCSP),

• P + Q ∈ T(BCSP) for any P, Q ∈ T(BCSP),

• P ⊕ Q ∈ T(BCSP) for any P, Q ∈ T(BCSP).

Again, subterms a0 may be abbreviated by a. Brackets are used for disambiguation only, assuming associativity of + and ⊕, and letting a bind stronger than + and ⊕. Semantically, BCSP-expressions represent nonempty, finite sets of initially deterministic BCSP expressions: for P, Q ∈ T(BCSP) let

[[0]] := {0} [[aP]] := {aP } [[P + Q]] := {p + q | p ∈ [[P]], q ∈ [[Q]]} [[P ⊕ Q]] := [[P]] ∪ [[Q]].

On T_{1}(BCSP) action relations ⟶^{a} for a ∈ Act are defined as the predicates on T_{1}(BCSP) generated by the action rules of Table 4. Here a ranges over Act, P over T(BCSP) and p and q over T_{1}(BCSP). This makes T_{1}(BCSP) into a labelled transition system. Hence, in the light of Section 1.5 all semantic equivalences of Sections 2–12 and 14 are well-defined on T(BCSP), and for each of the semantics it is determined when two BCSP-expressions denote the same process.

\frac{p ∈ [[P]]}{aP ⟶^{a} p}  \frac{p ⟶^{a} p′}{p + q ⟶^{a} p′}  \frac{q ⟶^{a} q′}{p + q ⟶^{a} q′}

Table 4: Action rules for BCSP

The following theorem says that all these semantic equivalences are congruences for BCSP. Even stronger, all the preorders of this paper are precongruences for BCCSP.

Theorem 11 Let P, Q, R, S ∈ T(BCSP) and let O be any of the semantics of Sections 2–12, 14. Then

\begin{matrix}P =_{O} Q ∧ R =_{O} S ⇒ aP =_{O} aQ ∧ P + R =_{O} Q + S ∧ P ⊕ R =_{O} Q ⊕ S, \\ P ⊑_{O} Q ∧ R ⊑_{O} S ⇒ aP ⊑_{O} aQ ∧ P + R ⊑_{O} Q + S ∧ P ⊕ R ⊑_{O} Q ⊕ S. \end{matrix}

Proof: Each of the preorders O has a modal characterization, given by P ⊑_{O} Q ⇔ O(P) ⊆ O(Q), where O(P) = ⋃_{p∈[[P]]} O(p) for P ∈ T(BCSP) and O(p) = {φ ∈ L_{O} | p ⊧ φ} for p ∈ T_{1}(BCSP). Now O(P ⊕ Q) = O(P) ∪ O(Q). This immediately yields the compositionality of O w.r.t. ⊕: P ⊑_{O} Q ∧ R ⊑_{O} S ⇒ P ⊕ R ⊑_{O} Q ⊕ S, and hence P =_{O} Q ∧ R =_{O} S ⇒ P ⊕ R =_{O} Q ⊕ S.

Note that every formula in the infinitary Hennessy-Milner logic is logically equivalent to a disjunction of formulas of the form ⋀_{i∈I} a_{i}φ_{i} ∧ ⋀_{j∈J} ¬a_{j}φ_{j}. Let O′(P) be the class of formulas in O(P) of that form. It follows that P ⊑_{O} Q ⇔ O′(P) ⊆ O′(Q) for P, Q ∈ T(BCSP).

For p, q ∈ T_{1}(BCSP) one has p + q ⊧ ⋀_{i∈I} a_{i}φ_{i} ∧ ⋀_{j∈J} ¬a_{j}φ_{j} iff I can be written as I_{1} ∪ I_{2} such that p ⊧ ⋀_{i∈I_{1}} a_{i}φ_{i} ∧ ⋀_{j∈J} ¬a_{j}φ_{j} and q ⊧ ⋀_{i∈I_{2}} a_{i}φ_{i} ∧ ⋀_{j∈J} ¬a_{j}φ_{j}. Moreover, for each semantics O of this paper, if ⋀_{i∈I} a_{i}φ_{i}∧⋀_{j∈J} ¬a_{j}φ_{j} ∈ L_{O} and I′ ⊂ I, then ⋀_{i∈I′} a_{i}φ_{i}∧⋀_{j∈J} ¬a_{j}φ_{j} ∈ L_{O}^{12}. Thus, for P, Q ∈ T(BCSP) and ⋀_{i∈I} a_{i}φ_{i} ∧⋀_{j∈J} ¬a_{j}φ_{j} ∈ L_{O}, one has ⋀_{i∈I} a_{i}φ_{i} ∧⋀_{j∈J} ¬a_{j}φ_{j} ∈ O′(P +Q) iff I = I_{1} ∪ I_{2} such that ⋀_{i∈I_{1}} a_{i}φ_{i} ∧ ⋀_{j∈J} ¬a_{j}φ_{j} ∈ O′(P) and ⋀_{i∈I_{2}} a_{i}φ_{i} ∧ ⋀_{j∈J} ¬a_{j}φ_{j} ∈ O′(Q). This immediately yields the compositionality of O w.r.t. +.

The compositionality of O w.r.t. a is straightforward. □

If P ∈ T(BCSP), then G([[P]]) is a finite process graph with multiple roots. Vice versa, any finite process graph with multiple roots g ∈ ^{|}G^{mr} can be represented by a BCSP-expression {// \atop \\}g{\\ \atop //} ∈ T(BCSP), such that G({// \atop \\}g{\\ \atop //})\underline{↔} g. Just extend Definition 17.1 by {// \atop \\}g{\\ \atop //} = ⨁_{r∈roots(g)} {// \atop \\}g_{r}{\\ \atop //}.

Axioms In Table 5, complete axiomatizations in terms of BCSP can be found for the same eleven semantics axiomatized in terms of BCCSP in Tables 2 and 3. The first two sections of the table apply to the equivalences and the first and last section to the preorders. These axioms are mild variations of the ones in Tables 2 and 3, and have been found by exploiting a close correspondence in semantic validity between BCSP and BCCSP expressions. First of all, using the definitions just given, the soundness of the axioms in the first section of Table 5 is easily established. Using these, any closed BCSP expression can be rewritten in the form ⨁_{i=1}^{n} p_{i} with p_{i} closed BCCSP expressions. Now the following lemma reduces the validity of (in)equations over BCSP to that of (in)equations over BCCSP.

Lemma 17.1 ⨁_{i=1}^{n} p_{i} ⊑_{O} ⨁_{j=1}^{m} q_{j} ⇔ ∑_{i=1}^{n} ap_{i} ⊑_{O} ∑_{j=1}^{m} aq_{j} for p_{i}, q_{j} ∈ T(BCCSP).

Proof: φ ∈ O(⨁_{i=1}^{n} p_{i}) ⇔ aφ ∈ O(∑_{i=1}^{n} ap_{i}). □

12At least when replacing the modality X of R, RT, P W and RS by ⋀_{a∈Y} ¬a⊤ ∧ ⋀_{a∈Z} a⊤.

B RS PW RT FT R F CS CT S T
(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)  + + + + + + + + + + +
x ⊕ y = y ⊕ x  + + + + + + + + + + +
x ⊕ x = x  + + + + + + + + + + +
(x + y) + z = x + (y + z)  + + + + + + + + + + +
x + y = y + x  + + + + + + + + + + +
x + 0 = x  + + + + + + + + + + +
(x ⊕ y) + z = (x + z) ⊕ (y + z)  + + + + + + + + + + +
a(x ⊕ y) = ax + ay  + + + + + + + + + + +
∑_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i}) = ∑_{i=1}^{n}(b_{i}x_{i}+b_{i}y_{i}) ⊕ ∑_{i=1}^{n}b_{i}y_{i}  + v v v v v v v v v
bx + by + z = (bx + z) ⊕ (by + z)  + v v v v  v  v
∑_{i=1}^{n} b_{i}x_{i} ⊕ ∑_{i=1}^{n} b_{i}y_{i} = ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i})  + + v v  v  v
x + x = x  +  v  v  v
(bx + u) ⊕ (by + v) = (bx + by + u) ⊕ (by + v)  + +  v  v
x ⊕ (y + z) = x ⊕ (x + y) ⊕ (y + z)  +  v  v
x + by + z = (x + by + z) ⊕ (by + z)  + v v v
(bx + u) ⊕ (cy + v) = bx + cy + u + v + v
x + y = (x + y) ⊕ y  + v
x ⊕ y = x + y  +
x ⊑ x ⊕ y  + + + + + + + + + +
bx + by + z = (bx + z) ⊕ (by + z)  + v v v v  v  v
∑_{i=1}^{n} b_{i}x_{i} ⊕ ∑_{i=1}^{n} b_{i}y_{i} = ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i})  + v v v  v  v
x + x = x  +  v  v  v
(bx + u) ⊕ (by + v) ⊒ bx + by + u  + v  v  v
x ⊕ (y + z) ⊒ x + y  +  v  v
ax ⊑ ax + y  + v v v
(bx + u) ⊕ (cy + v) = bx + cy + u + v + v
x ⊑ x + y  + v
x ⊕ y = x + y  +

Table 5: Complete axiomatizations in terms of BCSP

Most of the axioms in the last two sections of Table 5 can be recognized as restatements of the axioms of Tables 2 and 3, using the insight of Lemma 17.1. However, in BCSP it is not so clear how the set of initial actions of a process should be defined, and the obvious adaptations of the axioms involving the operator I would not be sound. Therefore the alternatives to those axioms discussed near the end of Section 17.2 are used. Moreover, in BCSP the axiom x + x = x is not sound for readiness semantics. Substituting a ⊕ b for x, one derives a ⊕ (a + b) ⊕ b = a ⊕ b, of which only the left-hand side has a ready pair ^{/} \ε, {a, b}^{\} /. However, in the setting of BCCSP all closed instances of x + x = x are derivable from the law ax + ax = ax, which corresponds with the BCSP axiom x ⊕ x = x. Following Lemma 17.1, the characteristic axiom for failure trace equivalence should be x⊕y = x⊕y ⊕(x+y). This axiom is derivable from x+x = x, and all closed instances of x+x = x are derivable from x ⊕ y = x ⊕ y ⊕ (x + y) and the axioms in the first section of Table 5.

Let U_{O} be the set of axioms marked with “+” in the column for O in the first two sections of Table 5, and U_{O}^{∗} be the set of axioms marked with “+” in the column for O in the first and last section of Table 5. Write S ⊢ Φ if the formula Φ is provable from the set of axioms S.

Theorem 12 For O ∈ {T, S, CT, CS, F, R, F T, RT, P W, RS, B} and P, Q ∈ T(BCSP) one has P =_{O} Q ⇔ U_{O} ⊢ P = Q and P ⊑_{O} Q ⇔ U_{O}^{∗} ⊢ P ⊑ Q.

Proof: “⇐” (soundness): In the light of Theorem 11 it suffices to show that the closed instances of the indicated axioms are valid in the corresponding semantics. In fact, one may restrict attention to the instances where expressions ⨁_{i=1}^{n} p_{i} with p_{i} closed BCCSP expressions are substituted for the variables. It is not difficult to check, for each of these axioms, that such instances of it are derivable from the instances of it where simple closed BCCSP expressions are substituted for the variables (but taking x ⊕ y = x ⊕ y ⊕ (x + y) instead of x + x = x to be the characteristic axiom for failure trace semantics). That the instances of the latter kind are valid in the corresponding semantics follows immediately from Lemma 17.1 and the soundness of the axioms for BCCSP.

“First ⇒” (completeness of the axioms for the equivalences): Let T′_{O} be the set of axioms marked with “+” in the column for O in Table 2, but using a ∑_{i=1}^{n} b_{i}x_{i} + a ∑_{i=1}^{n} b_{i}y_{i} = a ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i}) and a ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i}) = a ∑_{i=1}^{n}(b_{i}x_{i} + b_{i}y_{i}) + a ∑_{i=1}^{n} b_{i}y_{i} instead of the axioms involving the operator I. As Theorem 8 establishes completeness for closed terms only, it holds for T′_{O} as well.

Claim: If T′_{O} ⊢ p = ∑_{j=1}^{m} aq_{j} for p, q_{j} ∈ T(BCCSP), then, modulo applications of the first three axioms of Table 2, p has the form p = ∑_{i=1}^{n} ap_{i}.

Proof of the claim: As all axioms in T′_{O} are equations, I may use induction on the proof of p = ∑_{j=1}^{m} aq_{j} in equational logic. The case that p = ∑_{j=1}^{m} aq_{j} is a closed instance of an axiom of T′_{O} proceeds by inspection of those axioms. The cases of placing an equation in a context, as well as reflexivity, symmetry and transitivity, are trivial.

Claim: T′_{O} ⊢ ∑_{i=1}^{n} ap_{i} = ∑_{j=1}^{m} aq_{j} ⇒ U_{O} ⊢ ⨁_{i=1}^{n} p_{i} = ⨁_{j=1}^{m} q_{j} for any p_{i}, q_{j} ∈ T(BCCSP).

Proof of the claim: I use induction on the proof of ∑_{i=1}^{n} ap_{i} = ∑_{j=1}^{m} aq_{j} from T′_{O} in equational logic. The case that ∑_{i=1}^{n} ap_{i} = ∑_{j=1}^{m} aq_{j} is a closed instance of an axiom of T′_{O} proceeds by inspection of those axioms, taking into account the remark about x ⊕ y = x ⊕ y ⊕ (x + y) right before this theorem. The case of a closed instance of an axiom of T′_{O} in a context is straightforward, also using that all closed instances of axioms of T′_{O} are derivable from the ones of U_{O}, taking into account the remark about x + x = x right before this theorem. The cases of reflexivity and symmetry are trivial. Transitivity follows from the previous claim.

Completeness proof: Suppose P =_{O} Q for certain P, Q ∈ T(BCSP). Using the axioms in the first section of Table 5 one obtains U_{O} ⊢ P = ⨁_{i=1}^{n} p_{i} and U_{O} ⊢ Q = ⨁_{j=1}^{m} q_{j} with p_{i}, q_{j} ∈ T(BCCSP). By the soundness of these axioms one has ⨁_{i=1}^{n} p_{i} =_{O} ⨁_{j=1}^{m} q_{j}. Therefore ∑_{i=1}^{n} ap_{i} =_{O} a ⨁_{i=1}^{n} p_{i} =_{O} a ⨁_{j=1}^{m} q_{j} =_{O} ∑_{j=1}^{m} aq_{j} by the soundness of a(x ⊕ y) = ax + ay and Theorem 11, and hence T′_{O} ⊢ ∑_{i=1}^{n} ap_{i} = ∑_{j=1}^{m} aq_{j} by the completeness of T′_{O}. Now U_{O} ⊢ P = Q follows by the claim above.

The second “⇒” (completeness of the axioms for the preorders) goes likewise, except that in the proof of the second claim, in order to handle the axioms ax ⊑ ax + y and x ⊑ x + y, one uses the axiom x ⊑ x ⊕ y of U_{O}^{∗}. Furthermore, ax ⊑ ax + y is derivable from U_{CT}^{∗}, and x ⊑ x + y from U_{T}^{∗}. □

18 Criteria for selecting a semantics for particular applications

Must testing Assume the testing scenario of trace semantics: we are unable to influence the behaviour of an investigated system in any way and can observe the performed actions only. Not even deadlock is observable. In this case there appears to be no reason to distinguish the two processes of Counterexample 3, ab + a(b + c) and a(b + c). They have the same traces, and consequently allow the same observations. Likewise, one might see no reason to distinguish between the two processes of Counterexample 2, ab + a and ab; also these have the same traces. However, when buying process ab, it may come with the guarantee that, in every run of the system, sooner or later it will perform the action b, at least if the action a is known to terminate. Such a guarantee cannot be given for ab + a. The distinction between ab and ab + a alluded to here can be formalized with the concept of must testing, originally due to De Nicola & Hennessy [17]: ab must do a b, whereas ab + a must not.

For finite processes, must testing could be formalized as follows. For t ⊆ Act^{∗} we say that a finite process p ∈ IP must pass the test t if CT (p) ⊆ t. To test whether a process will sooner or later perform a b-action take t to be all sequences of actions containing a b. To test whether a process will always perform a b immediately after it does an a, take t to be all traces in which any a is immediately followed by a b. Now write p ⊑_{T}^{must} q if for all tests t ⊆ Act^{∗} such that p must pass t, q must pass t as well. It is easy to see that, for finite processes p and q, p ⊑_{T}^{must} q iff q ⊑_{CT} p.

All testing scenarios O sketched earlier in this paper can be regarded as forms of may testing: it is recorded whether an observation φ ∈ L_{O} may be made for a process p, and one writes p ⊑_{O} q if any observation that may be made for p, may also be made for q.

In the context of a testing scenario O with O ⪰ CT, a plausible form of must testing can be defined as well, and for finite processes plausible formalizations yield that p ⊑_{O}^{must} q iff q ⊑_{O} p.

For infinite processes there are several ways to formalize must testing, and analyzing the resulting preorders falls outside of the scope if this paper.

Deadlock behaviour A process is said to reach a state of deadlock if it can do no further actions.^{13} The process ab + a for instance may deadlock right after performing an a-action, whereas the process ab may not. One could say that a semantics O respects deadlock behaviour iff O ⪰ CT. Counterexample 4 then shows that none of the semantics on the left in Figure 9 respects deadlock behaviour; only the left-hand process of Counterexample 4 can deadlock after an a-move. Respecting deadlock behaviour may be a requirement on semantics in applications where either deadlock is important in its own right, or where (implicitly) a form of must-testing is considered.

Full abstraction Many testing scenarios mentioned in this paper employ the notion that an action can happen only if it is not blocked by the environment, that is, only if both the investigated process and the environment are ready to participate in it. Modelling both the investigated process and the responsible part of the environment as process graphs gives rise to the following binary intersection operator that allows an action to happen only if it can happen in both of its arguments.

Definition 18.1 Let ∩ be the binary operator on process graphs defined by

• nodes(g ∩ h) = nodes(g) × nodes(h), • roots(g ∩ h) = roots(g) × roots(h),

13In settings were successful termination is modelled (cf. Section 19) a state of deadlock is only reached if moreover the process cannot terminate successfully.

• ((s, t), a, (s′, t′)) ∈ edges(g) iff (s, a, s′) ∈ edges(g) ∧ (t, a, t′) ∈ edges(h).

In order to obtain a connected process graph, unreachable parts need to be removed.

This operator is also called synchronous parallel composition and is denoted ∥ in Hoare [31]. It

can be added to BCCSP or BCSP by employing the action rule \frac{p ⟶^{a} p′, q ⟶^{a} q′}{p ∩ q ⟶^{a} p′ ∩ q′} .

Trace semantics turns out to compositional for the intersection operator, i.e. if g =_{T} g′ and h =_{T} h′ then g ∩ h =_{T} g′ ∩ h′. For T (g ∩ h) = T (g) ∩ T (h). So are failures and readiness semantics:

/ \σ, X^{\} / ∈ F (g ∩ h) ⇔ ∃^{/} \σ, Y ^{\} / ∈ F (g), ^{/} \σ, Z^{\} / ∈ F (h) : X = Y ∪ Z
/ \σ, X^{\} / ∈ R(g ∩ h) ⇔ ∃^{/} \σ, Y ^{\} / ∈ R(g), ^{/} \σ, Z^{\} / ∈ R(h) : X = Y ∩ Z.

In fact, it is not hard to see that all semantics of this paper are compositional for ∩, except for CT and CS, and their (in)finitary versions. The two processes of Counterexample 3, ab + a(b + c) and a(b+c), are completed trace equivalent, even completed simulation equivalent, yet after intersecting them with ac only the first one has a completed trace a.

In applications where the intersection operator is used, one may require a suitable semantics to be compositional for it. This rules out CT and CS. If also deadlock behaviour is of importance, F appears to be the coarsest semantics to be considered, as least among the ones reviewed in this paper. As a matter of fact, it is the coarsest semantics even among the ones not reviewed here.

Definition 18.2 An equivalence relation is called fully abstract w.r.t. a property if it is the coarsest equivalence with that property, i.e. if it has the property, and any other equivalence having that property is finer.

An equivalence is said to fully abstract w.r.t. another equivalence ∼ and some operators, if it is the coarsest equivalence finer than ∼ that is compositional w.r.t. those operators.

An equivalence ≈ on ^{|}G is fully abstract w.r.t. an equivalence ∼ and a set L of operators on ^{|}G iff (1) it is compositional w.r.t. the operators in L, and

(2) for any two process graphs g, h ∈ ^{|}G with g ≉ h there exists a context C[·] of operators from L such that C[g] ≁ C[h].

In fact, for every equivalence relation ∼ on ^{|}G and every set L of operators on ^{|}G there exists a unique equivalence relation ≈ that is fully abstract w.r.t. ∼ and the operators in L, namely the one defined by g ≈ h iff C[g] ∼ C[h] for every context C[·] of operators from L.

Theorem 13 Failures equivalence is fully abstract w.r.t. =_{CT} and ∩, i.e. w.r.t. deadlock behaviour and intersection.

Proof: (1) has already been established. For (2), let g ≠_{F} h. W.l.o.g. let ^{/} \σ, X^{\} / ∈ F (g) − F (h). Let k be the process graph that is shaped like the failure pair ^{/} \σ, X^{\} /, i.e. the process that performs the actions of σ in succession, after which it offers a choice between the actions of X, and nothing else. Then σ ∈ CT (g ∩ k) − CT (h ∩ k). □

Variants of Theorem 13 are abundant in the literature. See e.g. [11].

Renaming For every function f : Act → Act one can define a unary renaming operator on ^{|}G that renames the labels of all transitions in its argument according to f. In case f is injective, all semantics of this paper are compositional for the associated renaming operator, as is trivial to check. Non-injective renaming operators are useful to express a degree of abstraction. Imagine a process that can do, among others, actions a_{1} and a_{2}. At some level of abstraction, the difference between a_{1} and a_{2} may be considered irrelevant. This can be expressed by applying a renaming that relabels both a_{1} and a_{2} into the same action a. Naturally, if two processes are equivalent before applying such a renaming operator, one would expect them to still be equivalent afterwards, i.e. after abstracting from the difference between a_{1} and a_{2}. It is for this reason that one might require semantics to be compositional for (non-injective) renaming. As it happens, all semantics between F^{1} and B^{−} fail this requirement. For the two processes of Counterexample 4 are HML-equivalent (=_{B}^{−}), but after renaming all actions b_{i} into b (for i = 1, 2, …) the resulting processes are not even singleton-failures equivalent (=_{F}^{1} ). For only the first one has a singleton-failure pair ^{/} \a, b^{\} /. This can be considered an argument against the semantics on the left of Figure 9.

Counterexample 20 shows that also F2S^{∗}, R2S^{∗}, FB^{∗} and RB^{∗} are not compositional for renaming. In this counterexample b is a shorthand for Σ_{i=1}^{∞}b_{i}, in the sense that whenever a transition p ⟶^{b} q is displayed, all the transitions p ⟶^{b_{i}} q for i ≥ 1 are meant to be present. With some effort

b  _{b} _{b_{1}}_{c} _{b} _{b_{2}}_{c} _{b} _{b_{3}}_{c}_{a}  _{a}_{a}  _{a}  …  _{b} _{b_{1}}_{c} _{b} _{b_{2}}_{c} _{b} _{b_{3}}_{c}_{a}_{a} _{a}  …_{=_{RB}^{∗}}_{≠_{2S}^{ω}}_{=_{RS}}

Counterexample 20: F2S^{∗}, R2S^{∗}, FB^{∗} and RB^{∗} are not compositional for renaming

one checks that both processes satisfy the same formulas in L_{RB}^{∗}. However, after renaming all actions b_{i} into b they are no longer 2S^{−}-equivalent: only the first process satisfies a¬(bc⊤). For all other semantics of Figure 9 it is rather easy to establish that they are compositional for renaming.

Other compositionality requirements Many formal languages for the description of concurrent systems, including CCS [37], SCCS [39], CSP [31] and ACP [7], are De Simone languages (cf. [3]). This means that their operators (the De Simone operators) can be defined with action rules of a particular form (the De Simone format). Because De Simone languages are used heavily in algebraic system verification, semantic equivalences that are compositional for such languages are often desirable.

Theorem 14 The semantics T , T^{∞}, F , F^{∞}, R, R^{∞}, FT , FT^{∞}, RT , RT^{∞}, PF , PF^{∞}, S^{∗}, S^{ω}, S, FS^{∗}, RS^{∗}, RS^{ω}, RS, 2S^{ω}, 2S, B^{ω} and B are compositional w.r.t. all De Simone languages. Proof: Omitted. □

For all the other semantics of Figure 9, which are displayed there in red (or shaded), there are counterexamples against such a result. Tree semantics fails to be compositional w.r.t. the + of BCCSP, unless the action relations are upgraded with multiplicities, but that takes us outside of De Simone format. The semantics F^{1} , F^{−}, R^{−}, FT^{−}, RT^{−}, RS^{−}, 2S^{−}, B^{−}, F2S^{∗}, R2S^{∗}, FB^{∗} and RB^{∗} fail to be compositional w.r.t. renaming, and CT , CT^{∞}, CS, CS^{ω}, CS fail to be compositional w.r.t. intersection. These are all De Simone operators. Finally, Counterexample 21 shows that P W is not compositional for the synchronization operator × of SCCS [39]—also a De Simone operator. This operator can be used to create a context, in which the two possible worlds equivalent processes of Counterexample 8 are converted into the two processes below. These are no longer possible

a_{3}  a_{3} b_{1} b_{2} b_{1} b_{2} c_{4}  d_{4} (abc + abd) × 3(1.4 + 2.4)  ≠_{PW}  a_{3} b_{1} b_{2} b_{1} b_{2} c_{4}  d_{4} a(bc + bd) × 3(1.4 + 2.4)

Counterexample 21: Possible worlds semantics is not compositional for synchronization

worlds equivalent, for only the one on the right has a possible world a_{3}(b_{1}c_{4} + b_{2}d_{4}). The same counterexample can also be created with the inverse image operator of CSP [31].

In Baeten, Bergstra & Klop [6] a unary priority operator was defined on process graphs. This operator, which is not a De Simone operator, assumes a partial ordering < on Act, i.e. there is one priority operator for each such ordering. The operator acts on graphs by removing all transitions (s, a, t) for which there is a transition (s, b, u) with b > a (and unreachable parts are removed as well). Thus, in a choice between several actions, only the actions with maximal priority may be executed. It is known that RT, RS, B and U are compositional for the priority operators. I think that RT^{∞}, P W, RS^{∗}, RS^{ω}, RB^{∗} and B^{ω} are too. However, none of the other semantics of Figure 9 is. Thus, in applications where priority operators are used and algebraic reasoning makes compositionality essential, only semantics like RT, RS and B are recommendable.

Depending on the application, compositionality for other operators may be required as well, leading to various restrictions on the array of suitable semantics. More on which semantics are compositional for which operators can be found in Aceto, Fokkink & Verhoef [3] and the references therein.

The Recursive Specification Principle A recursive specification is an equation of the form X = t with X a variable and t a term (in a language such as BCCSP) containing no other variables than X. (In the literature often recursive specifications are allowed to involve more variables and more such equations, but I do not need those here.) A recursive specification X = t over BCCSP is guarded if every occurrence of X in t occurs in a subterm at′ of t with a ∈ Act. Recursive specifications are meant to specify processes. A process p is said to be a solution of the recursive specification X = t, using the semantics O, if the equation evaluates to a true statement when substituting p for X and interpreting = as =_{O}. The recursive specification principle (RSP) says that guarded recursive specifications have unique solutions. It has been established for bisimulation semantics by Milner [39] (using the language SCCS), and holds in fact for most semantics encountered in this paper. In process algebra, two processes are often proven semantically equivalent by showing that they are solutions of the same recursive specification (cf. [5]). For this purpose it is important to work with a semantics in which RSP holds. In the infinitary semantics between T^{∞} and P W this is in fact not the case. For in those semantics the two different processes of Counterexample 1 are both solutions of the guarded recursive specification X = aX + a. For the finitary semantics this counterexample does not apply, because the two processes are identified, whereas in simulation semantics (of finer) these two processes fail to be solutions of the same recursive specification.

Other considerations In general it depends on the kind of interactions that are permitted between a process and its environment (i.e. the testing scenario) which semantics is sufficiently discriminating for a particular application. When a range of appropriate semantics is found, also considering the criteria discussed earlier in the section, the question rises which of these semantics to actually use (e.g. in making a formal verification). A natural choice is the coarsest of the appropriate semantics, i.e. the one which is fully abstract w.r.t. the requirements it has to meet in order to be adequate in the context in which the investigated processes will be operating. In this semantics more equations are valid than in any other. If the goal is to prove that two processes are equivalent, this may succeed when using the fully abstract semantics, whereas it may not even be true in a finer one. Sometimes it is argued that the complexity of deciding equivalence between processes is too high for certain semantics; using them would give rise to too hard verifications. However, this can not be an argument for rejecting a semantics in favour of a finer one. For doing the verification in the finer semantics is actually a method of establishing equivalence in the coarser semantics. In other words, when O ≺ N, establishing p =_{O} q cannot be harder than establishing p =_{N} q, as establishing p =_{N} q is one of the ways of establishing p =_{O} q. If deciding O-equivalence has a higher complexity than deciding N -equivalence, the hard cases to decide must be the equations p =_{O} q for which p =_{N} q is not even true. It is especially for those applications that O-semantics has a distinct advantage over N -semantics. This argument has been made forcefully in Valmari [48].

In practice, it may not always be certain in what ways the environment can interact with investigated processes, and hence what constitutes their observable behaviour. Moreover, the processes under investigation may be transferred to more powerful environments long after their initial use. One of the ways this could happen is through the introduction of more operators for which the underlying semantics has to be compositional. A big disadvantage of semantics that are fully abstract with respect to non-stable notions of observability (or non-stable sets of operators) is that whenever a verification is carried out in a such a semantics, and one decides that the context in which the verified system will be working is such that actually a little bit more can be observed that what was originally accounted for, the verification has to be completely redone. Moreover, the correctness of the investigated systems keeps depending on the completeness of the underlying testing scenario. In such cases it is preferable to carry out verifications in the finest semantics for which this is convenient. This gives stronger equivalence results, which have a greater change of surviving in conditions where the environment gets more powerful than originally anticipated. Especially using bisimulation is safe bet, as it respects the internal structure of processes to such a degree that it is hard to imagine ever running into an environment that distinguishes bisimilar processes. In Bloom, Istrail & Meyer [12] it is argued that ready simulation semantics already respects the limits of observable behaviour, so this may be a good alternative. It should be pointed out, however, that most applications involve abstraction from internal actions (not treated in this paper), and hence require variants of the semantics treated here that accommodate such abstractions. In this setting, the question of which semantics represents the limit of observable behaviour is much harder.

19 Distinguishing deadlock and successful termination

Often researchers feel the need to distinguish two ways in which a process can end: successfully (by completing its mission) or unsuccessfully (for instance because its waits for an input from the environment that will never arrive). This distinction can be formally modelled in the context of labelled transition systems by considering triples (IP, →, √) in which (IP, →) is a labelled transition system as in Definition 1.1 and √ ⊆ IP is a predicate on processes expressing which ones can terminate successfully in their current state. It may or may not be required that the processes p ∈ IP with √(p) have no outgoing transitions. Likewise, in the setting of process graphs, one studies tuples (nodes(g), root(g), edges(g), √(g)) with √(g) ⊆ nodes(g). Now any labelled transition system over an alphabet Act equipped with such a successful termination predicate, can be encoded as an ordinary labelled transition system over an alphabet Act ∪ {√} with √ ∉ Act. Namely, instead of labelling the processes/states where successful termination occurs with √, one can view successful termination as a kind of action, and add √-labelled transitions from those processes/states to fresh endstates. Now any semantic equivalence defined on ordinary labelled transition systems extends to labelled transition systems with a successful termination predicate by declaring two processes equivalent iff they are equivalent in the encoded transition system. In fact, in the same way all equivalences and preorders of this paper extend to labelled transition systems equipped with arbitrary predicates P ⊆ IP. Below, three of the thusly defined equivalences are characterized explicitly in terms of √.

Definition 19.1 Let (IP, →, √) be a labelled transition system with successful termination. σ ∈ Act^{∗} is a terminating trace of a process p if there is a process q such that p ⟶^{σ} q and √(q). Let L(p) denote the set of terminating traces of p (and let T (p) and CT (p) be defined as before).

Now two processes p and q are trace equivalent iff T (p) = T (q) and L(p) = L(q). They are completed trace equivalent iff T (p) = T (q), CT (p) = CT (q) and L(p) = L(q). They are bisimulation equivalent iff there exists a binary relation R on IP with pRq, satisfying, for a ∈ Act:

• if pRq and p ⟶^{a} p′, then ∃q′ : q ⟶^{a} q′ and p′Rq′;

• if pRq and q ⟶^{a} q′, then ∃p′ : p ⟶^{a} p′ and p′Rq′;

• if pRq, then √(p) ⇔ √(q).

Language semantics The nondeterministic automata studied in automata theory (cf. Hopcroft & Ullman [33]) can be regarded as process graphs with a termination predicate (except that in automata theory the focus is on finite automata). The states s ∈ nodes(g) with √(s) are called accepting or final states, and a string σ ∈ Act^{∗} is said to be accepted by the automaton g iff σ ∈ L(g). The set L(g) of all strings accepted by g is called the language accepted by g. In automata theory two automata are considered equivalent iff they accept the same language. Therefore language equivalence can be defined as follows.

Definition 19.2 Two processes p and q in a labelled transition system with successful termination are language equivalent, notation p =_{L} q, if L(p) = L(q). Write p ⊆_{L} q iff L(p) ⊆ L(q).

Clearly, language semantics makes more identifications than trace semantics (i.e. L ≺ T). It could be appended to the bottoms of Figures 1 and 9. The reason for not treating it earlier in this paper is that it cannot be defined uniformly in terms of action relations. For either the definition depends on the predicate √, which is not a part of ordinary labelled transition systems, or, when encoding the √-predicate by a transition label √, the definition treats ⟶^{√} different from the other action relations.

Complete axiomatizations A variant of the language BCCSP of Section 17 that distinguishes between deadlock and successful termination is the language BCCSP_{δε}, obtained from BCCSP by replacing the constant 0 by two constants δ and ε, representing deadlock and successful termination, respectively. On T(BCCSP_{δε}) action relations ⟶^{a} for a ∈ Act are again defined as the predicates on T(BCCSP_{δε}) generated by the action rules of Table 1. Furthermore, the predicate √ ⊆ T(BCCSP_{δε}) is generated by the rules of Table 6. Now the complete axiomatizations of Table 2 apply to BCCSP_{δε}

√(ε)  \frac{√(p)}{√(p + q)}  \frac{√(q)}{√(p + q)}

Table 6: Rules for the termination predicate

as well, provided that the occurrences of 0 are changed into δ, an axiom I(ε) = ε is added, and the characteristic axioms for CS and CT also get variants in which by + z resp. cy + v is replaced by ε. Language equivalence can be axiomatized by adding the axiom aδ = δ to the axioms for trace equivalence. This axiom corresponds with a transformation on finite process trees that removes states from which it is impossible to reach a state of successful termination. On the normal forms w.r.t. this transformation, language equivalence and trace equivalence coincide.

Successful termination as default Naturally, ordinary transition systems can be regarded as transition systems with successful termination by taking the termination predicate to be empty. On such transition systems, language equivalence turns out to be the universal relation, axiomatized by the equation x = y. Alternatively, ordinary transition systems can be regarded as transition systems with successful termination by letting √ be the set of processes without outgoing transitions, i.e. by regarding all termination to be successful. In this context, on a transition system (IP, →) on can define any of the semantics O of this paper as in Section 15, or by taking successful termination into account as in the present section. Denote the latter version of O by O^{√}. Then two processes are O^{√}- equivalent iff they are O-equivalent after appending a √-transition to every endstate. Comparing semantics that take termination into account as well as semantics that abstract from it yields in first approximation a “double” version of Figure 9, of which a tiny fragment is displayed in Figure 12(a). However, for processes p for which all termination is successful one has CT (p) = L(p). Hence the semantics T^{√}, CT^{√} and CT coincide. One also verifies easily that R coincides with R^{√}, F T with F T^{√}, RT with RT^{√}, RS with RS^{√}, B with B^{√}, etc. However, F and F^{√} differ, as demonstrated by Counterexample 22. There F (left) = F (right) but ^{/} \a, {c, √}^{\} / ∈ F^{√}(left) − F^{√}(right). Also PF differs from PF^{0} and 2S from 2S^{0} , for in Counterexample 14 one has left =_{2S} right but, after appending a √-transition to every endnode, a¬b√0 ∈ L_{2S}^{√} (left) − L_{2S}^{√} (right). Thus Figure 12(a) collapses to Figure 12(b). In Groote & Huttel [24] normed processes are studied: processes that never loose the possibility to terminate eventually. A process p is normed iff for each process q reachable from p, there is a process r reachable from q that terminates (i.e. has

L^{√} T^{√} CT^{√} F^{√} R^{√}  T CT F R (a) first approximation  (b) general case  (c) normed processes L^{√}  T CT F F^{√} R  T L^{√} F F^{√} R

Figure 12: The linear time – branching time spectrum for successfully terminating processes

no outgoing transitions) (and all termination is considered successful). For normed processes p, T (p) is completely determined by L(p). Hence Figure 12(b) collapses further to Figure 12(c). This explains why in [24] L^{√} coincides with CT and is finer than T.

Sequencing and sequential composition The sequential composition of processes p and q (cf. [31, 7]), denoted p · q, is the process that first executes p, and upon successful termination of p executes q. This operator is defined only on domains of processes on which successful termination is somehow represented. Sequencing on the other hand is defined on domains of processes that do not distinguish between deadlock and successful termination: let p;q denote the process that first executes p until it can do no further actions, and then q [12]. On process graphs, g;h can be constructed by appending (at its root) a disjoint copy of h to every endnode of g. On process graphs with successful termination, g · h on the other hand can be constructed by appending a disjoint copy of h to every node s of g with √(s). In case √(s) is possible even if s is not an endnode, the graph h needs to be transformed first in such a way that its root has no incoming edges [7].

a a a b b c a + ab + a(b + c)  =_{F} ≠_{F}^{√} =_{F}^{1√}  a a  b c a + a(b + c)

Counterexample 22: Failures semantics is not compositional for sequencing

Counterexample 22 shows that failures semantics is not compositional for sequencing. There left =_{F} right, but left;c ≠_{F} right;c. The same counterexample, with all endnodes successfully terminating, shows that singleton-failures semantics is not compositional for either sequencing or sequential composition. Likewise, Counterexample 14 shows that PF and 2S are not compositional for sequencing, and Counterexample 4 shows that none of the semantics between T and B^{−} are. All of the semantics studied in this paper, except for F^{1}, are compositional for sequential composition. As sequencing is the same as sequential composition on processes where all endstates, and only those, are considered to be successfully terminating, this implies that all the semantics O^{√}, except for F^{1√}, are compositional for sequencing. If c is an action that does not occur in p or q, then p;c =_{O} q;c ⇔ p =_{O}^{√} q. (Think of c as √.) From this it follows that for all semantics O, except F^{1}, O^{√} is fully abstract w.r.t. O and sequencing, at least for processes that can not execute every action in Act.

Concluding remarks

In this paper various semantic equivalences for concrete sequential processes are defined, motivated, compared and axiomatized. Of course many more equivalences can be given than the ones presented here. The reason for selecting just these, is that they can be motivated rather nicely and/or play a rôle in the literature on semantic equivalences. In Abramsky & Vickers [2] the observations which underly many of the semantics in this paper are placed in a uniform algebraic framework, and some general completeness criteria are stated and proved. They also introduce acceptance semantics, which can be obtained from acceptance-refusal semantics (Section 7) by dropping the refusals, and analogously acceptance trace semantics. I am not aware of any reasonable testing scenario for these notions.

In Section 9 I remarked that a testing scenario for simulation and ready simulation semantics can be obtained by adding an undo-button to the scenario’s for trace and ready trace semantics. Likewise, Schnoebelen [47] investigates the addition of an undo-button to the testing scenarios for completed trace, readiness, failures and failure trace semantics, thereby obtaining 3 new equivalences CT_{#}, R_{#} and F_{#}. Undo-failure trace equivalence coincides with finitary failure simulation equivalence, just like undo-trace and undo-ready trace equivalence coincide with finitary simulation and finitary ready simulation equivalence. For image finite processes R_{#} coincides with F_{#}. Furthermore R ⪯ R_{#} ⪯ RS^{∗}, F ⪯ F_{#} ⪯ FS^{∗}, CT ⪯ CT_{#} ⪯ CS^{∗} and S^{∗} ⪯ CT_{#} ⪯ F_{#} ⪯ R_{#}.

An interesting topic is the generalization of this work to a setting with silent moves and/or with parallelism. In both cases there turn out to be many interesting variations. The generalization to a setting with invisible actions will be tackled in [21]. Some work towards generalizing the spectrum to a setting with parallelism can be found for instance in [44] and [19].

References

[1] S. Abramsky (1987): Observation equivalence as a testing equivalence. Theoretical Computer Science 53, pp. 225–241.

[2] S. Abramsky & S. Vickers (1993): Quantales, observational logic and process semantics. Mathematical Structures in Computer Science 3, pp. 161–227.

[3] L. Aceto, W.J. Fokkink & C. Verhoef (2000): Structural operational semantics. In J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra, chapter 3. Elsevier.

[4] P. Aczel (1988): Non-well-founded Sets, CSLI Lecture Notes 14. Stanford University.

[5] J.C.M. Baeten, editor (1990): Applications of Process Algebra. Cambridge Tracts in Theoretical Computer Science 17. Cambridge University Press.

[6] J.C.M. Baeten, J.A. Bergstra & J.W. Klop (1987): Ready-trace semantics for concrete process algebra with the priority operator. Computer Journal 30(6), pp. 498–506.

[7] J.C.M. Baeten & W.P. Weijland (1990): Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press.

[8] J.W. de Bakker, J.N. Kok, J.-J.Ch. Meyer, E.-R. Olderog & J.I. Zucker (1986): Contrasting themes in the semantics of imperative concurrency. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: Current Trends in Concurrency, LNCS 224, Springer, pp. 51–121.

[9] J.W. de Bakker & J.I. Zucker (1982): Processes and the denotational semantics of concurrency. Information and Control 54(1/2), pp. 70–120.

[10] J.A. Bergstra, J.W. Klop & E.-R. Olderog (1986): Failure semantics with fair abstraction. Report CS-R8609, CWI, Amsterdam.

[11] J.A. Bergstra, J.W. Klop & E.-R. Olderog (1988): Readies and failures in the algebra of communicating processes. SIAM Journal on Computing 17(6), pp. 1134–1177.

[12] B. Bloom, S. Istrail & A.R. Meyer (1995): Bisimulation can’t be traced. Journal of the ACM 42(1), pp. 232–268.

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

[14] S.D. Brookes & A.W. Roscoe (1985): An improved failures model for communicating processes. In S.D. Brookes, A.W. Roscoe & G. Winskel, editors: Seminar on Concurrency, LNCS 197, Springer, pp. 281–305.

[15] P. Darondeau (1982): An enlarged definition and complete axiomatisation of observational congruence of finite processes. In M. Dezani-Ciancaglini & U. Montanari, editors: Proceedings international symposium on programming: 5^{th} colloquium, Aarhus, LNCS 137, Springer, pp. 47–62.

[16] R. De Nicola (1987): Extensional equivalences for transition systems. Acta Informatica 24, pp. 211–237.

[17] R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34, pp. 83–133.

[18] J. Engelfriet (1985): Determinacy → (observation equivalence = trace equivalence). Theoretical Computer Science 36(1), pp. 21–25.

[19] R.J. van Glabbeek (1990): The refinement theorem for ST-bisimulation semantics. In M. Broy & C.B. Jones, editors: Proceedings IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, North-Holland, pp. 27–52.

[20] R.J. van Glabbeek (1990): The linear time – branching time spectrum. Report CS-R9029, CWI, Amsterdam. Extended abstract in J.C.M. Baeten & J.W. Klop, editors: Proceedings CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, August 1990, LNCS 458, Springer-Verlag, 1990, pp. 278–297.

[21] R.J. van Glabbeek (1993): The linear time – branching time spectrum II; the semantics of sequential systems with silent moves. Manuscript. Preliminary version available by ftp

at ftp://boole.stanford.edu/pub/spectrum.ps.gz. Extended abstract in E. Best, editor:

Proceedings CONCUR’93, 4^{th} International Conference on Concurrency Theory, Hildesheim, Germany, August 1993, LNCS 715, Springer, pp. 66–81.

[22] R.J. van Glabbeek & J.J.M.M. Rutten (1989): The processes of De Bakker and Zucker represent bisimulation equivalence classes. In J.W. de Bakker, 25 jaar semantiek, liber amicorum, CWI, Amsterdam, pp. 243–246.

[23] J.F. Groote (1990): A new strategy for proving ω–completeness with applications in process algebra. In J.C.M. Baeten & J.W. Klop, editors: Proceedings CONCUR 90, Amsterdam, LNCS 458, Springer, pp. 314–331.

[24] J.F. Groote & H. Hüttel (1994): Undecidable equivalences for basic process algebra. Information and Control 115(2), pp. 354–371.

[25] J.F. Groote & F.W. Vaandrager (1992): Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), pp. 202–260.

[26] M. Hennessy (1985): Acceptance trees. Journal of the ACM 32(4), pp. 896–928.

[27] M. Hennessy & R. Milner (1980): On observing nondeterminism and concurrency. In J.W. de Bakker & J. van Leeuwen, editors: Proceedings 7^{th} ICALP, Noorwijkerhout, LNCS 85, Springer, pp. 299–309. This is a preliminary version of:

[28] M. Hennessy & R. Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), pp. 137–161.

[29] C.A.R. Hoare (1978): Communicating sequential processes. Communications of the ACM 21(8), pp. 666–677.

[30] C.A.R. Hoare (1980): Communicating sequential processes. In R.M. McKeag & A.M. Macnaghten, editors: On the construction of programs – an advanced course, Cambridge University Press, pp. 229–254.

[31] C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice Hall, Englewood Cliffs.

[32] M.J. Hollenberg (1995): Hennessy-Milner classes and process algebra. In A. Ponse, M. de Rijke & Y. Venema, editors: Modal Logic and Process Algebra: a Bisimulation Perspective, CSLI Lecture Notes 53, CSLI Publications, Stanford, California, pp. 187–216.

[33] J.E. Hopcroft & J.D. Ullman (1979): Introduction to Automata Theory, Languages and Computation. Addison-Wesley.

[34] J.K. Kennaway (1981): Formal semantics of nondetermism and parallelism. PhD thesis, University of Oxford.

[35] K.G. Larsen & A. Skou (1991): Bisimulation through probabilistic testing. Information and Computation, 94.

[36] A.R. Meyer (1985): Report on the 5^{th} international workshop on the semantics of programming languages in Bad Honnef. Bulletin of the European Association for Theoretical Computer Science 27, pp. 83–84.

[37] R. Milner (1980): A Calculus of Communicating Systems, LNCS 92. Springer.

[38] R. Milner (1981): Modal characterisation of observable machine behaviour. In G. Astesiano & C. Bohm, editors: Proceedings CAAP 81, LNCS 112, Springer, pp. 25–34.

[39] R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer Science 25, pp. 267–310.

[40] E.-R. Olderog & C.A.R. Hoare (1986): Specification-oriented semantics for communicating processes. Acta Informatica 23, pp. 9–66.

[41] D.M.R. Park (1981): Concurrency and automata on infinite sequences. In P. Deussen, editor: 5^{th} GI Conference, LNCS 104, Springer, pp. 167–183.

[42] I.C.C. Phillips (1987): Refusal testing. Theoretical Computer Science 50, pp. 241–284.

[43] A. Pnueli (1985): Linear and branching structures in the semantics and logics of reactive systems. In W. Brauer, editor: Proceedings 12^{th} ICALP, Nafplion, LNCS 194, Springer, pp. 15–32.

[44] L. Pomello (1986): Some equivalence notions for concurrent systems – An overview. In G. Rozenberg, editor: Advances in Petri Nets 1985, LNCS 222, Springer, pp. 381–400.

[45] A.W. Roscoe (1993): Unbounded non-determinism in CSP. Journal of Logic and Computation 3(2), pp. 131–172.

[46] W.C. Rounds & S.D. Brookes (1981): Possible futures, acceptances, refusals and communicating processes. In 22^{th} Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, IEEE, New York, pp. 140–149.

[47] Ph. Schnoebelen (1991): Experiments on processes with backtracking. In J.C.M. Baeten & J.F. Groote, editors: Proceedings CONCUR 91, Amsterdam, LNCS 527, Springer, pp. 80–94.

[48] A. Valmari (1995): Failure-based equivalences are faster than many believe. In J. Desel, editor: Proceedings of the International Workshop on Structures in Concurrency Theory, Berlin, May 1995, Workshops in Computing, Springer, pp. 326–340.

[49] S. Veglioni & R. De Nicola (1998): Possible worlds for process algebras. In D. Sangiorgi & R. de Simone, editors: Proceedings CONCUR 98, Nice, France, LNCS 1466, Springer, pp. 179–193.

[50] G. Winskel (1984): Synchronization trees. Theoretical Computer Science 34(1/2), pp. 33–82.

Index

\frac{2}{3}-bisimulation equivalence, 5, 34 2-nested simulation, 38 2-nested simulation equivalence, 38 2-nested simulation formulas, 38, 51 2-nested simulation machine, 39 2-nested simulation semantics, 5, 38

acceptance semantics, 80 acceptance trace semantics, 80 acceptance tree, 17 acceptance-refusal equivalent, 27 acceptance-refusal semantics, 26 acceptance-refusal triple, 27 accepted (by an automaton), 77 action, 6 action relations, 3, 6 action rules, 59 algebra, 3 anti-foundation axiom, 43 automata, 77 automata theory, 77

barbed semantics, 5 BCCSP, 59 BCSP, 68 bisimilar, 39 bisimulation, 39, 41 bisimulation equivalence, 39 bisimulation formulas, 51 bisimulation semantics, 4, 39 blocked, 14 branching, 6 branching equivalent, 43 button pushing experiments, 5

canonical graph, 8, 10, 13, 16, 24, 26 comparative concurrency semantics, 2 complete simulation, 33 complete trace, 11 completed simulation equivalent, 33 completed simulation formulas, 51 completed trace deterministic, 56 completed trace domain, 13 completed trace equivalent, 11 completed trace formulas, 12, 50 completed trace machine, 12 completed trace semantics, 4, 11 completeness, 62, 66 compositional, 59 concrete, 3 concurrency, 2 congruences, 59 connected, 7 continuations, 15 cross saturated, 57

De Simone languages, 74

deadlock, 72

deadlock behaviour, 72

decorated trace semantics, 52 denial formulas, 38 determinate, 55 deterministic, 7, 54 deterministic up to ≡, 55 domain, 3 domain theory, 3

edges, 7 embedding, 8 event structure, 3 exhibited behaviour semantics, 5 explicit domains, 3 explicit models, 10 external choice, 68

failure formulas, 15, 50

failure pair, 14 failure set, 14, 15 failure simulation equivalent, 33 failure simulation formulas, 53 failure trace, 19 failure trace augmentation, 20 failure trace equivalent, 19 failure trace formulas, 19, 50 failure trace machine, 18 failure trace relations, 19 failure trace semantics, 5, 19 failure trace set, 19, 20 failure trace simulation equivalent, 33 failures domain, 16 failures equivalent, 14 failures machine, 14 failures semantics, 4, 14 final states, 77 finitary simulation equivalent, 31 finitary simulation formulas, 31 finite, 7 finite ready trace formulas, 28 finite-failure trace equivalent, 21 finite-failures equivalent, 17 finite-failures semantics, 17 finite-ready trace equivalent, 28 finitely branching, 3, 7 free, 14 fully abstract, 73

generalized action relations, 6 generative processes, 36 global testing, 40 graph domains, 3 graph isomorphism, 7 graph transformations, 62 GSOS trace congruence, 5, 34, 38 guarded, 75

Hennessy-Milner formulas, 44 Hennessy-Milner logic (HML), 44 history, 63 history unambiguous, 63 HML-equivalent, 44

identifying, 63 image finite, 7 infinitary completed trace equivalent, 14 infinitary failure trace equivalent, 20 infinitary failures equivalent, 17 infinitary Hennessy-Milner formulas, 40 infinitary possible future, 28 infinitary possible-futures equivalent, 28 infinitary ready equivalent, 27 infinitary ready trace equivalent, 24 infinitary simulation equivalence, 31 infinitary trace equivalent, 11 infinitary trace semantics, 11 infinite failure trace, 20 infinite ready trace, 24 infinite trace, 11 initial actions, 7 initial nondeterminism, 9 initial state, 7 initially deterministic BCSP-expressions, 68 internal choice, 68 intersection operator, 72 isometry, 43 isomorphic, 7

labelled transition system, 3, 6 language accepted by g, 77 language equivalent, 77 language semantics, 77 linear time – branching time spectrum, 3 lookahead, 39

may testing, 72 menu, 13, 22 modal characterization, 51 modelling, 2 must testing, 72

nodes, 7

nondeterminism, 9 normal form, 62 normal ready trace, 23 normed processes, 78

observational equivalence, 4, 44

parallel, 2

partial traces, 4

path, 7 Petri net, 3 possible future, 26 possible world, 48, 49 possible worlds equivalent, 48, 49 possible worlds formulas, 51 possible worlds semantics, 5, 49 possible-futures equivalent, 26 possible-futures formulas, 51 possible-futures semantics, 5, 26 precongruences, 60 process, 2 process domain, 3 process expressions, 59 process graph, 7 process graphs with multiple roots, 9 process theory, 2

reachable, 6 reactive machines, 36 readiness domain, 26 readiness formulas, 25, 50 readiness machine, 25 readiness semantics, 5, 25 ready equivalent, 25 ready pair, 25 ready set, 25 ready simulation, 33 ready simulation equivalent, 33 ready simulation formulas, 51 ready simulation machine, 36 ready simulation semantics, 5, 33 ready trace, 22, 23 ready trace deterministic, 56 ready trace domain, 24 ready trace equivalent, 22 ready trace formulas, 23, 51 ready trace machine, 22 ready trace relations, 22 ready trace semantics, 5, 22 ready trace set, 22 ready trace simulation equivalent, 33 recursive specification, 75 recursive specification principle (RSP), 75 refusal equivalence, 19 refusal relations, 19 refusal semantics, 5 refusal set, 14, 19 refusal testing, 19 replicator, 33 root, 7 RT-saturated, 58

satisfaction relation, 10, 12, 15, 19, 23, 25, 28,

29, 31, 38, 40, 44 saturated, 58 semantic equivalence, 3 semantics, 2, 8 sequencing, 79 sequential, 2, 3, 6 sequential composition, 79 similar, 29 simulation, 5, 29, 30 simulation equivalence, 29 simulation formulas, 29, 51 simulation semantics, 5, 29 singleton-failure formulas, 50 singleton-failure pair, 37 singleton-failures equivalent, 37 singleton-failures semantics, 37 solution, 75 soundness, 61, 66 state transition diagram, 3 states, 7 successful termination, 77 summand, 59 synchronous parallel composition, 73

term domains, 3 terminating, 62 terminating trace, 77 termination, 77 terms, 59 testing equivalences, 5 trace, 9, 10, 63 trace domain, 10 trace equivalent, 9 trace formulas, 10, 50 trace machine, 12 trace semantics, 4, 9 trace set, 10 transitions, 7 tree, 7 tree equivalent, 47 tree semantics, 5, 47

unfolding, 47

uniform concurrency, 3

uniformly, 3

universal algebra, 3

verification, 2

weather, 40 well-founded, 7