To appear in EPTCS.

\begin{matrix}c \\ ◯ \end{matrix} R.J. van Glabbeek

This work is licensed under the

Creative Commons Attribution License.

On the Meaning of Transition System Specifications

Rob van Glabbeek

Data61, CSIRO, Sydney, Australia School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

                                       rvg@cs.stanford.edu

Transition System Specifications provide programming and specification languages with a semantics. They provide the meaning of a closed term as a process graph: a state in a labelled transition system. At the same time they provide the meaning of an n-ary operator, or more generally an open term with n free variables, as an n-ary operation on process graphs. The classical way of doing this, the closedterm semantics, reduces the meaning of an open term to the meaning of its closed instantiations. It makes the meaning of an operator dependent on the context in which it is employed. Here I propose an alternative process graph semantics of TSSs that does not suffer from this drawback.

Semantic equivalences on process graphs can be lifted to open terms conform either the closedterm or the process graph semantics. For pure TSSs the latter is more discriminating.

I consider five sanity requirements on the semantics of programming and specification languages equipped with a recursion construct: compositionality, applied to n-ary operators, recursion and variables, invariance under α-conversion, and the recursive definition principle, saying that the meaning of a recursive call should be a solution of the corresponding recursion equations. I establish that the satisfaction of four of these requirements under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics.

1 Introduction

Transition System Specifications (TSSs) [16] are a formalisation of Structural Operational Semantics [22] providing programming and specification languages with an interpretation. They provide the meaning of a closed term as a process graph: a state in a labelled transition system. At the same time they provide the meaning of an n-ary operator of the language, or more generally an open term with n free variables, as an n-ary operation on process graphs. The classical way of doing this proceeds by reducing the meaning of an open term to the meaning of its closed instantiations. I call this the closed-term semantics of TSSs. A serious shortcoming of this approach is that it makes the meaning of an operator dependent on the context in which it is employed.

Example 1 Consider a TSS featuring unary operators f, id and a. for each action a drawn from an alphabet A, and a constant 0. The set of admitted transition labels is Act := A ⊎ {τ}. The transition rules are

a.x −→^{a} x (for all a ∈ A)  \frac{x −→^{a} x′}{f(x) −→^{a} f(x′)} (for all a ∈ A)  \frac{x −→^{α} x′}{id(x) −→^{α} id(x′)} (for all α ∈ Act)

When considered in their own right, the operators f and id are rather different: the latter can mimic τ-transitions of its argument, and the former can not. Yet, in the context of the given TSS, one has f(p) \underline{↔} id(p), no matter which term p is substituted for the argument of these operators. Here \underline{↔} denotes strong bisimulation equivalence, as defined in [21, 12]. This is because no process in the given TSS ever generates a transition with the label τ. The identification of f and id up to \underline{↔} can be considered unfortunate, one reason being that is ceases to hold as soon as the language is enriched with a fresh operator τ. with the transition rule τ.x −→^{τ} x. As I will show later, this invalidates an intuitively plausible theorem on the relative expressiveness of specification languages. Here I propose an alternative process graph semantics of TSSs that does not suffer from this drawback.

In [10] I proposed five requirements on the semantics of programming and specification languages equipped with a recursion construct: compositionality, applied to n-ary operators, recursion and variables, invariance under α-conversion, and the recursive definition principle, saying that the meaning of a recursive call should be a solution of the corresponding recursion equations.

In many prior works on structural operational semantics, (some of) these requirements have been shown to hold for various TSSs when employing the closed-term semantics. It would be time consuming to redo all that work for the process graph semantics proposed here. To prevent this I show that the satisfaction of four of these requirements under the closed-term semantics of a TSS implies their satisfaction under the process graph semantics. The remaining requirement holds almost always.

Overview of the paper Section 2 presents the syntax of the programming and specification languages I consider here. For simplicity I restrict myself to languages with single-sorted signature, optionally featuring a recursion construct. This is a rich enough setting to include process algebras like CCS [21], CSP [5], ACP [3], Meije [1, 24] and SCCS [20].

The traditional “closed-term” interpretation of the process calculi CCS, Meije and SCCS effectively collapses syntax and semantics by interpreting the entire language as one big labelled transition system (LTS) in which the closed terms of the language constitute the set of states. This LTS is generated by a TSS, as formally defined in Section 5. Semantic equivalences on LTSs thereby directly relate closed terms. Two open terms are judged equivalent iff each of their closed substitutions are.

In Section 3 I present an interpretation of programming and specification languages that is more common in universal algebra and mathematical logic [19], and is also used in the traditional semantics of ACP and CSP. It separates syntax and semantics through a semantic mapping that associates with each closed term a value, and with each open term an operation on values. This matches with what often is called denotational semantics, except that I do not require the meaning of recursion constructs to be provided by means of fixed point techniques. In Section 7 I specialise this general approach to an operational one by taking the values to be process graphs: states in labelled transition systems. Likewise, Section 6 casts the closed-term interpretation as a special case of the approach from Section 3, by taking the values to be the closed terms.

Section 3 also formulates the five sanity requirements mentioned above, most in a couple of equivalent forms. Section 6 shows how these requirements simplify to better recognisable forms under the closed-term interpretation of programming and specification languages. These requirements are parametrised by the choice of a semantic equivalence ∼ on values, relating values that one does not need to distinguish. The traditional treatments of universal algebra and mathematical logic, and the process algebra CSP, do not involve such a semantic equivalence; this corresponds to letting ∼ be the identity relation. In Section 4 I observe that any choice of ∼ can be reduced to the identity relation, namely by taking as values ∼-equivalence classes of values. This reduction preserves the five sanity requirements.

After these preparations, Section 8 defines the promised process graph interpretation of TSSs. Some TSSs do not have a process graph interpretation, but I show that the large class of pure TSSs do.

Semantic equivalences on process graphs can be lifted to open terms conform either the closed-term or the process graph interpretation. Section 9 shows, under some mild conditions, that for pure TSSs the latter is more discriminating. Section 10 illustrates on a practical process algebra that whether a semantic equivalence is a congruence may depend on which of the two interpretations is chosen.

Section 11 proves the promised result that when four of the five sanity requirements have been established for the closed-term interpretation of a TSS, they also hold for its process graph interpretation. It also shows that the remaining requirement almost always holds

Section 12 argues that something is gained by moving from the closed-term interpretation of TSSs to the process-graph interpretation. Based on Example 1 it formulates an intuitively plausible theorem relating relative expressiveness of specification languages and conservative extensions, and shows how this theorem fails under the closed-term interpretation, but holds under the process graph interpretation.

Section 13 addresses related work, and Section 14 evaluates the five sanity requirements for languages specified by TSSs of a specific form.

2 Syntax

In this paper Var is an infinite set of variables, ranged over by X,Y,x,y,x_{i} etc.

Definition 1 (Terms). A function declaration is a pair (f,n) of a function symbol f ∉ Var and an arity n ∈ ℕ.^{1} A function declaration (c,0) is also called a constant declaration. A signature is a set of function declarations. The set 𝕋^{r}(Σ) of terms with recursion over a signature Σ is defined inductively by:

• Var ⊆ 𝕋^{r}(Σ),

• if (f,n) ∈ Σ and t_{1},...,t_{n} ∈ 𝕋^{r}(Σ) then f(t_{1},...,t_{n}) ∈ 𝕋^{r}(Σ),

• If V_{S} ⊆ Var, S: V_{S} → 𝕋^{r}(Σ) and X ∈ V_{S}, then ^{/} \X|S^{\} /∈ 𝕋^{r}(Σ). A term c() is abbreviated as c. A function S as appears in the last clause is called a recursive specification. It is often displayed as {X = S_{X} | X ∈ V_{S}}. Each term S_{Y} for Y ∈ V_{S} counts as a subterm of ^{/} \X|S^{\} /. An occurrence of a variable y in a term t is free if it does not occur in a subterm of the form ^{/} \X|S^{\} /with y ∈ V_{S}. For t ∈ 𝕋^{r}(Σ) a term, var(t) denotes the set of variables occurring free in t. A term is closed if it contains no free occurrences of variables. For W ⊆ Var, let 𝕋^{r}(Σ,W) denote the set of terms t with var(t) ⊆ W, and let T^{r}(Σ) = 𝕋^{r}(Σ,∅) be the set of closed terms over Σ. The sets 𝕋(Σ), 𝕋(Σ,W) and T(Σ) of open and closed terms over Σ without recursion are defined likewise, but without the last clause.

Definition 2 (Substitution). A Σ-substitution σ is a partial function from Var to 𝕋^{r}(Σ). It is closed if it is a total function from Var to T^{r}(Σ). If σ is a substitution and t a term, then t[σ] denotes the term obtained from t by replacing, for x in the domain of σ, every free occurrence of x in t by σ(x), while renaming bound variables if necessary to prevent name-clashes. In that case t[σ] is called a substitution instance of t. A substitution instance t[σ] where σ is given by σ(x_{i}) = u_{i} for i ∈ I is denoted as t[u_{i}/x_{i}]_{i∈I}, and for S a recursive specification ^{/} \t|S^{\} /abbreviates t[^{/} \Y |S^{\} //Y]_{Y ∈V_{S}}.

Sometimes the syntax of a language is given as a signature together with an annotation that places some restrictions on the use of recursion [10]. This annotation may for instance require the sets V_{S} to be finite, the functions S computable, or the sets of equations S to be guarded: a syntactic criterion that ensures that they have unique solutions under a given interpretation. It may also rule out recursion altogether.

3 Semantics

A language can be given by an annotated signature, specifying its syntax, and an interpretation, assigning to every term t its meaning [[t]]. The meaning of a closed term is a value chosen from a class of values 𝔻, which is called a domain. The meaning of an open term is a Var-ary operation on 𝔻: a function of type 𝔻^{Var}→ 𝔻, where 𝔻^{Var} is the class of functions from Var to 𝔻. It associates a value [[t]](ρ) ∈ 𝔻 to t that depends on the choice of a valuation ρ: Var → 𝔻. The valuation assigns a value from 𝔻 to each variable.

1This work generalises seamlessly to operators with infinitely many arguments. Such operators occur, for instance, in [4, Appendix A.2]. Hence one may take n to be any ordinal. It also generalises to operators, like the summation or choice of CCS [21], that take any set of arguments.

A partial valuation is a function ξ : W → 𝔻 for W ⊆ Var that assigns a value only to certain variables. A W-ary operation, for W ⊆ Var, is a function F : 𝔻^{W} → 𝔻. It associates a value to every W -tuple of values, i.e. to every partial valuation of the variables with domain W. If F : 𝔻^{Var} → 𝔻 and ζ ∈ 𝔻^{Var\W} then F (ζ) : 𝔻^{W}→ 𝔻 is given by F (ζ)(ξ) = F (ξ ∪ζ) for any ξ ∈ 𝔻^{W}. For ρ a valuation and W a set of variables, ρ\W is the partial valuation with domain Var\W such that (ρ\W)(x) = ρ(x) for x ∈ Var\W.

3.1 Sanity requirements on interpretations

Usually interpretations are required to satisfy some sanity requirements. The work [10] proposed five such requirements: compositionality, applied to variables, n-ary operators and recursion, invariance under α-conversion, and the recursive definition principle (RDP).

In this paper I work with domains of interpretation 𝔻 that are equipped with a semantic equivalence relation ∼ ⊆ 𝔻×𝔻. It indicates that values v,w ∈ 𝔻 with v ∼ w need not be distinguished on our chosen level of abstraction. The equivalence ∼ extends to functions F,G:𝔻^{W}→ 𝔻 by F ∼G iff F (ξ)∼G(ξ) for all ξ ∈𝔻^{W}. It extends to partial valuations ρ,ν : W → 𝔻 or functions ρ,ν of type (𝔻^{W}→ 𝔻)^{W}by ρ ∼ ν iff ρ(X) ∼ ν(X) for all X ∈ W. Such an equivalence relation relaxes the requirements invariance under α-conversion and RDP, and modifies compositionality; I speak of compositionality up to ∼. The default case in which no semantic equivalence is in force corresponds to taking ∼ to be the identity relation.

Compositionality up to ∼ demands that the meaning of a variable is given by the chosen valuation,

i.e., [[x]](ρ) ∼ ρ(x)  (1)

for each x ∈ Var and valuation ρ : Var → 𝔻, and that the meaning of a term is completely determined by the meaning of its direct subterms. This means that for operators (f,n) ∈ Σ and valuations ρ,ν : Var → 𝔻

[[t_{i}]](ρ) ∼ [[u_{i}]](ν) (for all i = 1,...,n) ⇒ [[f(t_{1},...,t_{n})]](ρ) ∼ [[f(u_{1},...,u_{n})]](ν)  (2)

and for recursive specifications S and S′with X ∈ V_{S} = V_{S′}and valuations ρ,ν : Var → 𝔻

[[S_{Y}]](ρ\V_{S}) ∼ [[S′_{Y}]](ν\V_{S}) (for all Y ∈ V_{S}) ⇒ [[^{/} \X|S^{\} /]](ρ) ∼ [[^{/} \X|S′^{\} /]](ν).  (3)

Note that the precondition of (3) evaluates the variables in S_{Y} and S′_{Y} that are free in ^{/} \X|S^{\} /and ^{/} \X|S′^{\} / according to ρ and ν, respectively, and the variables from V_{S} = V_{S′}under any common valuation ζ.

Invariance under α-conversion demands that the meaning of a term is independent of the names of its bound variables, i.e. for any injective substitution γ : V_{S} → Var such that the range of γ contains no variables occurring free in ^{/} \S_{Y}|S^{\} /for some Y ∈ V_{S}

[[^{/} \γ(X)|S[γ]^{\} / ]]∼ [[^{/} \X|S^{\} /]].  (4)

Finally, the meaning of a term ^{/} \X|S^{\} /should be the X-component of a solution of S. To be precise,

[[^{/} \X|S^{\} /]]∼ [[^{/} \S_{X}|S^{\} /]].  (5)

This property is called the recursive definition principle [6].

A straightforward structural induction on t using (1), (2) and (3) shows that [[t]](ρ) depends only on the restriction of ρ to those variables that occur free in t. If there are no such variables, [[t]](ρ) does not depends on ρ at all, and consequently can be abbreviated to [[t]].

3.2 Alternative forms of the sanity requirements

Note that (2) holds iff for every (f,n) ∈ Σ there is a function f^{𝔻} : 𝔻^{n} → 𝔻 such that

∀ρ ∈ 𝔻^{Var} : [[f(t_{1},...,t_{n})]](ρ) ∼ f^{𝔻}([[t_{1}]](ρ),...,[[t_{n}]](ρ)).

Requirement (3) can be characterised in the same vein: Proposition 1 Property (3) holds iff for every set W ⊆ Var there is a function μ_{W}^{𝔻}: (𝔻^{W}→ 𝔻)^{W}→ 𝔻^{W} such that for every recursive specification S: W → 𝕋^{r}(Σ) with X ∈ W, and every ρ : Var → 𝔻,

[[^{/} \X|S^{\} /]](ρ) ∼ μ_{W}^{𝔻}([[S]](ρ\W))(X).

Proof: Since the meaning of term S_{Y} ∈ 𝕋^{r}(Σ) is of type 𝔻^{Var} → 𝔻, the meaning of a recursive specification S : W → 𝕋^{r}(Σ) is of type [[S]]: W → (𝔻^{Var} → 𝔻). Applying to that a partial valuation ρ\W : Var\W → 𝔻 yields a function [[S]](ρ\W) of type (𝔻^{W}→ 𝔻)^{W}. Now for each χ ∈ (𝔻^{W}→ 𝔻)^{W} choose, if possible, a pair S^{χ} : W → 𝕋^{r}(Σ) and ρ^{χ} : Var → 𝔻 such that [[S^{χ} ]](ρ^{χ}\W) ∼ χ, and define μ_{W}^{𝔻}(χ)(X), for X ∈ W, to be [[^{/} \X|S^{χ} ^{\} /]](ρ^{χ}). For a χ for which no such pair can be found the definition of μ_{W}^{𝔻}(χ)(X) is arbitrary. Now pick S : W → 𝕋^{r}(Σ) and ρ : Var → 𝔻. Let χ := [[S]](ρ\W). Then [[S]](ρ\W) = χ ∼ [[S^{χ} ]](ρ^{χ}\W), so by (3) one has

[[^{/} \X|S^{\} /]](ρ) ∼ [[^{/} \X|S^{χ} ^{\} /]](ρ^{χ}) = μ_{W}^{𝔻}(χ)(X) = μ_{W}^{𝔻}([[S]](ρ\W))(X).

The other direction, that the existence of such a μ_{W}^{𝔻} implies (3), is trivial. □ Write t =^{α} uif the terms t,u ∈ 𝕋^{r}(Σ) differ only in the names of their bound variables. Then (4) can be rewritten as

t =^{α} u ⇒ [[t]]∼ [[u]].  (6)

Proposition 2 In the presence of (2) and (3), (4) is equivalent to (6). Proof: Clearly, (4) is a special case of (6). The other direction proceeds by structural induction on t.

In case t = X ∈ Var then u = X and thus [[t]]∼ [[u]].

Let t = f(t_{1},...,t_{n}). Then u = f(u_{1},...,u_{n}) and t_{i} =^{α} u_{i} for each i = 1,...,n. By induction [[t_{i}]]∼ [[u_{i}]] for each i. This means that [[t_{i}]](ρ) ∼ [[u_{i}]](ρ) for each ρ : Var → 𝔻. Hence, by (2), [[t]]∼ [[u]].

Let t = ^{/} \X|S^{\} /. Then u = ^{/} \γ(X)|S′[γ]^{\} /for a recursive specification S′: V_{S} → 𝕋^{r}(Σ) with S_{Y} =^{α} S′_{Y} for all Y ∈ V_{S}, and an injective substitution γ : V_{S} → Var such that the range of γ contains no variables occurring free in ^{/} \S′_{Y}|S^{\} / for some Y ∈ V_{S}. By induction [[S_{Y}]]∼ [[S′_{Y}]]for each Y. This means that [[S_{Y}]](ρ) ∼ [[S′_{Y}]](ρ) for each ρ : Var → 𝔻, so in particular [[S_{Y}]](ρ\V_{S}) ∼ [[S′_{Y}]](ρ\V_{S}) for each such ρ. Hence, by (3), [[^{/} \X|S^{\} /]]∼ [[^{/} \X|S′^{\} /]]. Thus, by (4), [[t]]∼ [[^{/} \X|S′^{\} /]]∼ [[^{/} \γ(X)|S′[γ]^{\} / ]]= [[u]]. □

3.3 Applying semantic interpretations to substitutions

The semantic mapping [[ ]]: 𝕋^{r}(Σ) → ((Var → 𝔻) → 𝔻) extends to substitutions σ : Var ⇀ 𝕋^{r}(Σ) by [[σ]](ρ)(X) := [[σ(X)]](ρ) for all X ∈ Var and ρ : Var → 𝔻—here σ is extended to a total function by σ(Y) := Y for all Y ∉ dom(σ). Thus [[σ]]is of type (Var → 𝔻) → (Var → 𝔻), i.e. a map from valuations to valuations. The following results applies to languages satisfying sanity requirements (1)–(4). Proposition 3 Let t ∈ 𝕋^{r}(Σ) be a term, σ : Var ⇀ 𝕋^{r}(Σ) a substitution, and ρ : Var → 𝔻 a valuation.

Then [[t[σ]]](ρ) ∼ [[t]]([[σ]](ρ)).  (7)

Proof: By the definition of substitution, there is an u ∈ 𝕋^{r}(Σ) with t =^{α} u, such that t[σ] = u[σ], and when performing the substitution σ on u there is no need to rename any bound variables occurring in u. It now suffices to obtain [[u[σ]]](ρ) ∼ [[u]]([[σ]](ρ)), because then [[t[σ]]](ρ) = [[u[σ]]](ρ) ∼ [[u]]([[σ]](ρ)) ∼^{(6)} [[t]]([[σ]](ρ)). For this reason it suffices to establish (7) for terms t and substitutions σ with the property (*) that whenever a variable Z occurs free within a subterm ^{/} \X|S^{\} /of t with Y ∈ V_{S} then Y does not occur free in σ(Z). I proceed with structural induction on t, while quantifying over all ρ.

Let t = X ∈ Var. Then [[X]]([[σ]](ρ)) ∼^{(1)} ([[σ]](ρ))(X) =^{def}[[σ(X)]](ρ) = [[X[σ]]](ρ).

Let t = f(t_{1},...,t_{n}). By induction I may assume that [[t_{i}[σ]]](ρ) ∼ [[t_{i}]]([[σ]](ρ)) for i = 1,...,n. Hence

[[f(t_{1},...,t_{n})[σ]]](ρ) = [[f(t_{1}[σ],...,t_{n}[σ])]](ρ) ∼^{(2)} [[f(t_{1},...,t_{n})]]([[σ]](ρ)).

Let t = ^{/} \X|S^{\} /. Then t[σ] = ^{/} \X|S[σ\V_{S}]^{\} / . Given that the pair t,σ satisfies property (*), so do the pairs S_{Y},σ\V_{S} for all Y ∈ V_{S}. Moreover, no Y ∈ V_{S} occurs free in σ(Z) for Z ∉ V_{S} occurring free in S. (#) By induction I assume [[S_{Y}[σ\V_{S}]]](ρ) ∼ [[S_{Y}]]([[σ\V_{S}]](ρ)) for all Y ∈ V_{S} and all ρ : Var → 𝔻. Any such ρ can be written as (ρ\V_{S}) ∪ ξ for some ξ : V_{S} → 𝔻. Now (#) yields that for all Z ∈ Var occurring free in S

([[σ\V_{S}]]((ρ\V_{S}) ∪ ξ))(Z) = ((([[σ]](ρ))\V_{S}) ∪ ξ)(Z).

Hence [[S_{Y}[σ\V_{S}]]](ρ\V_{S})(ξ) ∼ [[S_{Y}]]([[σ\V_{S}]]((ρ\V_{S}) ∪ ξ)) = [[S_{Y}]](([[σ]](ρ))\V_{S})(ξ) for all Y ∈ V_{S}, ρ: Var→ 𝔻 and ξ: V_{S}→ 𝔻. So [[S_{Y}[σ\V_{S}]]](ρ\V_{S}) ∼ [[S_{Y}]](([[σ]](ρ))\V_{S}) for all Y ∈V_{S} and ρ: Var→ 𝔻.

One obtains  [[^{/} \X|S^{\} /[σ]]](ρ) = [[^{/} \X|S[σ\V_{S}]^{\} /]](ρ) ∼^{(3)} [[^{/} \X|S^{\} /]]([[σ]](ρ)).  □

4 Quotient Domains

An equivalence relation ∼ on 𝔻 is a congruence^{2} for L if

ρ ∼ ν ⇒ [[t]](ρ) ∼ [[t]](ν)  (8)

for any term t and any valuations ρ,ν : Var → 𝔻.

Proposition 4 If a language L is compositional up to an equivalence ∼ then ∼ is a congruence for L.

Proof: A straightforward structural induction on t. □

Given a domain 𝔻 for interpreting languages and an equivalence relation ∼, the quotient domain 𝔻/_{∼} consists of the ∼-equivalence classes of elements of 𝔻. For v ∈ 𝔻 let [v]_{∼} ∈ 𝔻/_{∼} denote the equivalence class containing v ∈ 𝔻. Likewise, for a valuation ρ : Var → 𝔻 in 𝔻, the valuation [ρ]_{∼} : Var → 𝔻/_{∼} in 𝔻/_{∼} is given by [ρ]_{∼} (x) := [ρ(x)]_{∼}; it also represents the ∼-equivalence class of valuations in 𝔻 of which ρ is a member. Each valuation in 𝔻/_{∼} is of the form [ρ]_{∼}.

An interpretation [[ ]]: 𝕋^{r}(Σ) → (𝔻^{Var} → 𝔻) that satisfies (8) is turned into the quotient interpretation [[ ]]_{∼} : 𝕋^{r}(Σ) → ((𝔻/_{∼})^{Var} → 𝔻/_{∼}) by defining [[t]]_{∼} ([ρ]_{∼}) := [[[t]](ρ)]_{∼}. By (8), this is independent of the choice of a representative valuation ρ within the equivalence class [ρ]_{∼}.

Let [[ ]]be an interpretation and ∼ an equivalence such that (8) holds. Then [[ ]]satisfies the sanity requirements (1)–(5) of Section 3 up to ∼ iff [[ ]]_{∼} satisfies these requirements up to =.

2This property is called lean congruence in [13]. There ∼ is called a full congruence for L iff L is compositional up to ∼.

In the absence of recursion this is equivalent to (8), but in general it is a stronger requirement—i.e., the reverse of Proposition 4 does not hold [13].

5 Transition System Specifications

Definition 3 (Transition system specification; Groote & Vaandrager [16]). Let Σ be an annotated signature and A a set (of actions). A (positive) (Σ,A)-literal is an expression t −→^{a} t′with t,t′∈ 𝕋^{r}(Σ) and a ∈ A. A transition rule over (Σ,A) is an expression of the form \frac{H}{λ} with H a set of (Σ,A)-literals (the premises of the rule) and λ a (Σ,A)-literal (the conclusion). A rule \frac{H}{λ} with H = ∅ is also written λ. A transition system specification (TSS) is a triple (Σ,A,R) with R a set of transition rules over (Σ,A).

The following definition (from [9]) tells when a literal is provable from a TSS. It generalises the standard definition (see e.g. [16]) by (also) allowing the derivation of transition rules. The derivation of a literal t −→^{a} t′corresponds to the derivation of the rule _{\frac{H}{t−→^{a} t′}}with H = ∅. The case H ≠ ∅ corresponds to the derivation of t −→^{a} t′under the assumptions H.

Definition 4 (Proof ). Let P = (Σ,A,R) be a TSS. A proof of a transition rule \frac{H}{λ} from P is a well-founded, upwardly branching tree of which the nodes are labelled by (Σ,A)-literals, such that:

• the root is labelled by λ, and

• if κ is the label of a node q and K is the set of labels of the nodes directly above q, then – either K = ∅ and κ ∈ H,

– or \frac{K}{κ} is a substitution instance of a rule from R. If a proof of \frac{H}{λ} from P exists, then \frac{H}{λ} is provable from P, denoted P ⊢ \frac{H}{λ}.

A labelled transition system (LTS) is a triple (S,A,→) with S a set of states or processes, A a set of actions, and → ⊆ S×A×S the transition relation, or set of transitions. A TSS P = (Σ,A,R) specifies the LTS (T^{r}(Σ),A,→) whose states are the closed terms over Σ and whose transitions are the closed literals provable from P.

For the sake of simplicity, the above treatment of TSSs deals with positive premises only. However, all results of this paper apply equally well, and with unaltered proofs, to TSS with negative premises t −↛^{a} , following the treatment below. The rest of the section may be skipped in first reading.

5.1 TSSs with negative premises

A negative (Σ,A)-literal is an expression t −↛^{a} . A transition rule may have positive and negative literals as premises, but must have a positive conclusion. Literals t −→^{a} uand t −↛^{a} are said to deny each other.

Definition 5 [11] Let P = (Σ,A,R) be a TSS. A well-supported proof from P of a closed literal λ is a well-founded tree with the nodes labelled by closed literals, such that the root is labelled by λ, and if κ is the label of a node and K is the set of labels of the children of this node, then:

1. either κ is positive and \frac{K}{κ} is a closed substitution instance of a rule in R;

2. or κ is negative and for each set N of closed negative literals with \frac{N}{ν} provable from P and ν a

closed positive literal denying κ, a literal in K denies one in N. P ⊢_{ws} λ denotes that a well-supported proof from P of λ exists. A standard TSS P is complete if for each p and a, either P ⊢_{ws} p −↛^{a} or there exists a closed term q such that P ⊢_{ws} p −→^{a} q.

In [11] it is shown that no TSS admit well-supported proofs of literals that deny each other. Only a complete TSSs specifies an LTS; its transitions are the closed positive literals with a well-supported proof.

6 The Closed-term Semantics of Transition System Specifications

The default semantics of a language given as a TSS (Σ,A,R) is to take the domain 𝔻 in which the expressions are interpreted to be T^{r}(Σ), the set of closed terms over Σ. The meaning of a closed expression p ∈ T^{r}(Σ) is simply itself: [[p]]:= p. The meaning [[t]]∈ 𝔻^{Var} → 𝔻 of an open expression t ∈ 𝕋^{r}(Σ) is given by [[t]](ρ) := t[ρ]. Here one uses the fact that a valuation ρ : Var → 𝔻 is also a closed substitution ρ : Var → T^{r}(Σ). Given a semantic equivalence relation ∼ ⊆ T^{r}(Σ) × T^{r}(Σ), the closed-term semantics of a TSS always satisfies Requirement (1), whereas (2)–(5) simplify to

p_{i} ∼ q_{i} (for all i = 1,...,n) ⇒ f(p_{1},...,p_{n}) ∼ f(q_{1},...,q_{n}) and  (2′)
S_{Y}[σ] ∼ S′_{Y}[σ] (for all Y ∈ W and σ : W → T^{r}(Σ)) ⇒ ^{/} \X|S^{\} /∼ ^{/} \X|S′^{\} /  (3′)
/ \γ(X)|S[γ]^{\} /∼ ^{/} \X|S^{\} /  (4′)
/ \X|S^{\} /∼ ^{/} \S_{X}|S^{\} /  (5′)

for all functions (f,n) ∈ Σ, closed terms p_{i},q_{i} ∈ T^{r}(Σ), recursive specifications S,S′: W → 𝕋^{r}(Σ,W) with X ∈ W ⊆ Var, and γ : W → Var injective.

7 Process Graphs

When the expressions in a language are meant to represent processes, they are called process expressions, and the language a process description language. Suitable domains for interpreting process description languages are the class of process graphs [3] and its quotients. In such graph domains a process is represented by either a process graph, or an equivalence class of process graphs. Process graphs are also known as state-transition diagrams or automata. They are LTSs equipped with an initial state. A process graph can also be seen as a state in an LTS.

Definition 6 A process graph, labelled over a set A of actions, is a triple G = (S,A,→,I) with – S a set of nodes or states,

– → ⊆ S × A × S a set of edges or transitions,

– and I ∈ S the root or initial state. Let 𝔾(A) be the domain of process graphs labelled over A.

One writes r −→^{a} s for (r,a,s) ∈ → . Virtually all so-called interleaving models for the representation of processes are isomorphic to graph models. For instance, the failure sets that represent expressions in the process description language CSP [5] can easily be encoded as equivalence classes of graphs, under a suitable equivalence. In [3] the language ACP is equipped with a process graph semantics, and the semantics of CCS, SCCS and Meije given in [21, 20, 1, 24] are operational ones, which, as I will show below, induce process graph semantics. In the languages L studied in this paper, the domain 𝔻 in which L -expressions are interpreted will be 𝔾(A) for some set of actions A, or a subclass of 𝔾(A).

Usually the parts of a graph that cannot be reached from the initial state by following a finite path of transitions are considered meaningless for the description of processes. This means that one is only interested in process graphs as a model of system behaviour up to some equivalence, and this equivalence identifies at least graphs with the same reachable parts.

Definition 7 The reachable part of a process graph (S,A,→,I) is the process graph (S′,A,→′,I) where • S′⊆ S is the smallest set such that (1) I ∈ S′and (2) if r ∈ S′and r −→^{a} s then s ∈ S′,

• and →′is the restriction of → to S′× A × S′.

8 A Process Graph Semantics of Transition System Specifications

This section proposes a process graph semantics of TSSs. For each TSS P = (Σ,A,R) it defines an interpretation [[ ]]_{P}: 𝕋^{r}(Σ) → (𝔾(A)^{Var} → 𝔾(A)), thus taking 𝔻 to be 𝔾(A).

Definition 8 (Interpreting the closed expressions in a TSS as process graphs). Let P = (Σ,A,R) be a TSS and p ∈ T^{r}(Σ). Then [[p]]_{P}^{∅} ∈ 𝔾(A) is the reachable part of the process graph (T^{r}(Σ),A,→,p) with → the set of transitions provable from P.

To define an interpretation [[ ]]_{P}: 𝕋^{r}(Σ) → (𝔾(A)^{Var} → 𝔾(A)) of the open Σ-terms in 𝔾(A) I would like to simply add to the signature Σ a constant G for each process graph G ∈ 𝔾(A). However, 𝔾(A) is a proper class, whereas a signature needs to be a set. For this reason I work with appropriate subsets 𝔾^{∗} of 𝔾(A) instead of with 𝔾(A) itself. I will discuss the selection of 𝔾^{∗} later, but one requirement will be

if (S,A,→,r) ∈ 𝔾^{∗} and r −→^{a} s then also (S,A,→,s) ∈ 𝔾^{∗} (transition closure).

Define the transition relation →_{𝔾}^{∗} ⊆ 𝔾^{∗}× A × 𝔾^{∗} by G −→^{a} _{𝔾}^{∗} G′iff (i) G = (S,A,→,r), (ii) there is a transition (r,a,s) ∈ → , and (iii) G′= (S,A,→,s) is the same graph but with s as initial state.

Now consider a term t ∈ 𝕋^{r}(Σ) and a valuation ρ : Var → 𝔾(A). In order to define [[t]]_{P}(ρ), make sure that 𝔾^{∗} supports (t,ρ), meaning that it contains ρ(x) for any variable x ∈ Var occurring free in t. Let P + 𝔾^{∗} be the TSS P to which all graphs G ∈ 𝔾^{∗} have been added as constants, and all transitions in →_{𝔾}^{∗} as transition rules without premises. As the valuation ρ now also is a substitution, t[ρ] is a closed term in the TSS P + 𝔾^{∗}. Define [[t]]_{P}^{𝔾^{∗}}(ρ) to be [[t[ρ]]]_{P+𝔾^{∗}}^{∅} ∈ 𝔾(A): the interpretation according to Definition 8 of the closed term t[ρ] from the TSS P + 𝔾^{∗}.

Definition 9 (The simple process graph semantics of TSSs). A TSS P manifestly induces a process graph semantics iff, for any term t and valuation ρ, the interpretation [[t]]_{P}^{𝔾^{∗}}(ρ)is independent of the choice of 𝔾^{∗}, as long as 𝔾^{∗} is transition-closed and supports (t,ρ). In that case [[t]]_{P}(ρ) is defined to be [[t]]_{P}^{𝔾^{∗}}(ρ).

It is possible to enlarge the class of TSSs that induce a process graph semantics a little bit:

Definition 10 (The process graph semantics of TSSs). Call a choice of 𝔾^{∗} adequate for (the interpretation of) [[t]]_{P}(ρ) if 𝔾^{∗} is transition-closed and supports (t,ρ), and [[t]]_{P}^{𝔾′}(ρ) = [[t]]_{P}^{𝔾^{∗}}(ρ) for any transition-closed superset 𝔾′of 𝔾^{∗}. Now P induces a process graph semantics iff, for any term t and valuation ρ, an adequate choice 𝔾^{∗} for [[t]]_{P}(ρ) exists. In that case [[t]]_{P}(ρ) is defined to be [[t]]_{P}^{𝔾^{∗}}(ρ) for any adequate choice of 𝔾^{∗}.

Example 1 (continued) Reconsider the operators f and id from Example 1. To judge whether they are essentially different one compares the open terms f(x) and id(x). Their meanings are values that depend on the choice of a valuation ρ, mapping variables to values. In fact they depend on the value ρ(x) only.

Under the closed term interpretation of the TSS P of Example 1, ρ(x) is a closed term in the language; it cannot have an outgoing τ-transition. Thus [[f(x)]]_{P}(ρ) \underline{↔} [[x]]_{P}(ρ) \underline{↔} [[id(x)]]_{P}(ρ) for any such ρ, so [[f(x)]]_{P} \underline{↔} [[x]]_{P} \underline{↔} [[id(x)]]_{P}, i.e., f and id are strongly bisimilar.

However, under the process graph interpretation, ρ(x) is a process graph, and one may take ρ(x) to be τ c , where the short arrow indicates the initial state. With this valuation, the process graph

[[id(x)]]_{P}(ρ) is isomorphic to ρ(x), whereas [[f(x)]]_{P} has no outgoing transitions. So [[f(x)]]_{P}(ρ) \underline{↮} [[x]]_{P}(ρ) \underline{↔} [[id(x)]]_{P}(ρ) and consequently [[f(x)]]_{P} \underline{↮} [[x]]_{P} \underline{↔} [[id(x)]]_{P}, i.e., f and id are not bisimilar.

The smallest set of process graphs 𝔾^{∗} that is adequate for the interpretation of [[f(x)]]_{P}(ρ) and

[[id(x)]]_{P}(ρ) is { τ  c , τ  c , τ  c }.

Example 2 A TSS with a rule c −→^{a} x (without premises) does not induce a process graph semantics. Namely, no matter which set 𝔾^{∗} one takes, there is always a larger set 𝔾′and a process graph G∈𝔾′\𝔾^{∗}. Thus, the process graph [[c]]_{P}^{𝔾′} has the transition c −→^{a} G but [[c]]_{P}^{𝔾^{∗}} does not. Hence 𝔾^{∗} is not adequate. Consequently, the TSS does not induce a process graph semantics.

Example 3 Let P be the TSS with constants c and 0 and as only rule

\frac{x −→^{a} y z −→^{b} y}{c −→^{a} 0}.

Then [[c]]_{P}^{𝔾^{∗}}(ρ) is independent of ρ, since c is a closed term. In any adequate choice of 𝔾^{∗} there is a graph in which an a-transition and a b-transition end in a common state, and using such a choice one finds that [[c]]_{P}^{𝔾^{∗}} has the transition c −→^{a} 0. However, when taking 𝔾^{∗} to be a set of trees, [[c]]_{P}^{𝔾^{∗}} has no transitions.

P induces a process graph semantics according to Definition 10, but not according to Definition 9.

If we stick with Definition 9, [[t]]_{P} = [[t]]_{P}^{∅} for closed terms t.

Definition 11 The rule-bound variables of a transition rule _{\frac{H}{t−→^{a} t′}}form the smallest set B such that • var(t) ⊆ B, and

• if u −→^{b} u′is a premise in H and var(u) ⊆ B then var(u′) ⊆ B. A TSS is called pure if all variables occurring free in one of its rules are rule-bound in that rule.

This concept of a pure TSS generalises the one from [16], and coincides with it for TSSs in the tyft/tyxt format studied in [16]. The TSSs of all common process algebras are pure. So is the TSS of Example 1, but the ones of Examples 2 and 3 are not.

Proposition 5 Any pure TSS manifestly induces a process graph semantics.

Proof: For a given term t ∈ 𝕋^{r}(Σ) and valuation ρ : Var → 𝔾(A), let 𝔾_{0}^{∗} be the smallest set of process graphs that is transition-closed and supports (t,ρ). Then for any 𝔾^{∗} ⊇ 𝔾_{0}^{∗} and any transition t[ρ] −→^{a} u provable from P + 𝔾^{∗}, any term v occurring in a proof of this transition, including the target u, has the form t′[ρ] with t′∈ 𝕋^{r}(Σ), such that ρ(x) ∈ 𝔾_{0}^{∗} for any x ∈ var(t). This follows by a fairly straightforward induction on the size of proofs, with a nested induction on the derivation of rule-boundedness. As a consequence, the process graph [[t[ρ]]]_{P+𝔾^{∗}}^{∅} does not depend in any way on 𝔾^{∗}\ 𝔾_{0}^{∗}. □

Remark One may wonder whether the above treatment can be simplified by skipping, in Definition 8, “the reachable part of”. The answer is negative, for in that case [[t]]_{P}^{𝔾^{∗}}(ρ)would never be independent of the choice of 𝔾^{∗}, because all G ∈ 𝔾^{∗} would occur as (unreachable) states in the process graph [[t]]_{P}^{𝔾^{∗}}(ρ).

Summary In this section, terms in a TSS are interpreted in the domain of process graphs as follows. Let P = (Σ,A,R) be a TSS and t ∈ 𝕋^{r}(Σ) a term. The meaning [[t]]_{P}: 𝔾(A)^{Var}→ 𝔾(A) of t is given by [[t]]_{P}(ρ) := [[t[ρ]]]_{P+𝔾^{∗}}^{∅}, with 𝔾^{∗} adequate for [[t]]_{P}(ρ). Here 𝔾^{∗} is transition-closed and supports (t,ρ); it is adequate if further increasing this set does not alter the definition of [[t]]_{P}(ρ). If no adequate 𝔾^{∗} exists, [[t]]_{P}(ρ) remains undefined, and P does not induce a process graph semantics. If P is pure, any transition-closed set 𝔾^{∗} ⊆ 𝔾(A) supporting (t,ρ) is adequate.

9 Lifting Semantic Equivalences to Open Terms

The following definition shows how any equivalence relation ∼ defined on a domain 𝔻 in which a language L is interpreted, lifts to the open terms of L.

Definition 12 (Lifting equivalences to open terms). For a language L, given as an annotated signature Σ and an interpretation [[ ]]: 𝕋^{r}(Σ) → (𝔻^{Var} → 𝔻), and an equivalence relation ∼ on 𝔻, write t ∼_{L} u for t,u ∈ 𝕋^{r}(Σ) iff [[t]](ρ) ∼ [[u]](ρ) for all valuations ρ : Var → 𝔻.

This definition can be applied to any language L given by a TSS P = (Σ,A,R). In this case ∼ must be defined on 𝔾(A). Write ∼_{P}^{pg} for ∼_{L} as defined above when taking as interpretation the process graph semantics [[ ]]: 𝕋^{r}(Σ) → (𝔾(A)^{Var} → 𝔾(A)) of L.

An equivalence ∼ on 𝔾(A) also lifts to the closed terms T^{r}(Σ) of L. Namely, let (T^{r}(Σ),A,→) be the LTS specified by P as defined in Section 5. Then (T^{r}(Σ),A,→,p) ∈ 𝔾(A) is a process graph for any p ∈ T^{r}(Σ). Now write p ∼ q, for p,q ∈ T^{r}(Σ), whenever (T^{r}(Σ),A,→,p) ∼ (T^{r}(Σ),A,→,p).

Using this, Definition 12can also be instantiated by taking as interpretation the closed-term semantics [[ ]]: 𝕋^{r}(Σ) → (T^{r}(Σ)^{Var} → T^{r}(Σ)) of L, as defined in Section 6. Write ∼_{P}^{ci} for ∼_{L} defined thusly. So

t ∼_{P}^{ci} u iff t[σ] ∼ u[σ] for any closed substitution σ,

i.e., two open terms are related by ∼_{P}^{ci} if all of their closed instantiations are related by ∼.

Having lifted semantic equivalences ∼ from process graphs to open terms in two ways, one wonders how the resulting equivalences compare. Instantiating ∼ with strong bisimilarity, \underline{↔} , Example 1 shows that f(x) \underline{↔} _{P}^{ci} id(x) yet f(x) \underline{↮} _{P}^{pg} id(x). For the other direction consider the TSS with constants 0, c and d, alphabet {a,b}, and the rules

d −→^{a} 0 \frac{x −→^{b} y}{c −→^{a} 0}.

Under the closed-term interpretation, no b-transition from any term can be derived, so 0 \underline{↔} ^{ci} c \underline{↮} ^{ci} d. Yet under the process graph interpretation, since there exists some graph that can do a b-transition, one has c −→^{a} 0, and obtains 0 \underline{↮} ^{pg} c \underline{↔} ^{pg} d. So in general \underline{↔} ^{ci} and \underline{↔} ^{pg} are incomparable.

The above TSS is not pure; the variable x is not rule-bound. For pure TSSs no such example exists.

Theorem 1 Let P = (Σ,A,R) be a pure TSS and ≈ an equivalence on 𝔾(A) that relates each process graph with its reachable part. Moreover, let ∼ ⊆ ≈ be a possibly finer, or more discriminating, equivalence that satisfies requirements (1)–(4) of Section 3.1. Then t ≈_{P}^{pg} u implies t ≈_{P}^{ci} u.

Proof: Suppose t ≈_{P}^{pg} u, and let σ : Var → T^{r}(Σ) be a closed substitution. It suffices to establish that t[σ] ≈ u[σ]. Let [[σ]]_{P} : Var → 𝔾(A) be the valuation defined by [[σ]]_{P}(X) := [[σ(X)]]_{P}. This is the definition of [[σ]]_{P} from Section 3.3, specialised to closed substitutions. Here [[q]]_{P}, for q ∈ T^{r}(Σ), is the process graph semantics of q as defined in Section 8, so [[q]]_{P} = [[q]]_{P+𝔾^{∗}}^{∅} for an adequate choice of 𝔾^{∗}. Since P is pure and q closed, the empty set of process graphs is adequate by Proposition 5. By Definition 8, [[q]]_{P}^{∅}is the reachable part of the process graph (T^{r}(Σ),A,→,p), so [[q]]_{P}^{∅}≈ (T^{r}(Σ),A,→,p). Since t ≈_{P}^{pg} u, one has [[t]]_{p}([[σ]]_{P}) ≈ [[u]]_{p}([[σ]]_{P}) by Definition 12. Moreover, [[t]]_{p}([[σ]]_{P}) ∼ [[t[σ]]]_{P} by Proposition 3. Hence

[[t[σ]]]_{P}^{∅} = [[t[σ]]]_{P} ≈ [[t]]_{p}([[σ]]_{P}) ≈ [[u]]_{p}([[σ]]_{P}) ≈ [[u[σ]]]_{P} = [[u[σ]]]_{P}^{∅}

and thus (T^{r}(Σ),A,→,t[σ]) ≈ [[t[σ]]]_{P+𝔾^{∗}}^{∅} ≈ [[u[σ]]]_{P}^{∅} ≈ (T^{r}(Σ),A,→,u[σ]), i.e., t[σ] ≈ u[σ]. □

So, under the conditions of Theorem 1, ≈_{P}^{pg} is a finer, or more discriminating, equivalence than ≈_{P}^{ci}.

10 Congruence Properties

Whether a semantic equivalence ∼ is a congruence (cf. (8) in Section 4) may depend on whether the closed-term or the process graph semantics is chosen. The following example illustrates this for a practical process algebra.

Example 4 Consider the TSS with constants 1 and α for α ∈ Act = A⊎{τ} and binary operators + and ;, denoting choice and sequencing in a process algebra, with the following transition rules:

α −→^{α} 1  \frac{x −→^{α} x′}{x + y −→^{α} x′}  \frac{y −→^{α} y′}{x + y −→^{α} y′}  \frac{x −→^{α} x′}{x;y −→^{α} x′;y} \frac{x −↛^{α} for all α ∈ Act y −→^{β} y′}{x;y −→^{β} y′}

The process 1, like 0 in CCS, has no outgoing transitions, meaning that it performs no actions. The sequencing operator performs all actions its first argument can do, until its first argument can perform no further actions; then it continues with its second argument. I employ no recursion here.

As equivalence relation ∼ I take weak bisimulation equivalence, \underline{↔} _{w}, as defined in [21, 12]. For the term t from (8) take x;b. Let ρ and ν be valuations with

ρ(x) =  a  and  ν(x) =  ^{a  τ}  .

Then ρ(x) \underline{↔} _{w} ν(x), so that I may assume ρ \underline{↔} _{w} ν. Now the term t performs the sequential composition of the process filled in for x with the process doing a single b action. One has [[x;b]](ρ) \underline{↮} _{w} [[x;b]](ν) because only the first of these processes can ever perform the b. Thus, when using the process graph semantics of this TSS, \underline{↔} _{w} fails to be a congruence for the language specified.

However, when taking the closed-term semantics, all processes that my be filled in for x are terms in the given language and thus must terminate after performing finitely many transitions. In this setting \underline{↔} _{w} is actually a congruence. However, it stops being a congruence when recursion is added to the language.

11 Relating Sanity Requirements for the Two Semantics of TSSs

Given an equivalence relation ∼ on 𝔾(A), let ∼_{P}^{cl} be the equivalence relation on the set T^{r}(Σ) of closed terms of a TSS P = (Σ,A,R) defined by p ∼_{P}^{cl} q iff [[p]]_{P}^{∅}∼ [[q]]_{P}^{∅} (cf. Definition 8). In case ∼ relates each process graph with its reachable part, the equivalence ∼_{P}^{cl} coincides with ∼_{P}^{ci}, as defined in Section 9.

Observation 1 If P is pure and p,q ∈ T^{r}(σ), then p ∼_{P}^{cl} q iff p ∼_{P}^{pg} q.

Theorem 2 Let P be a TSS that induces a process graph semantics [[ ]]_{P} and let ∼ be an equivalence relation on 𝔾(A). Then [[ ]]_{P} satisfies the sanity requirements (2)–(5) of Section 3 up to ∼ if the closedterm semantics of P + 𝔾^{∗} satisfies these requirements up to ∼_{P+𝔾^{∗}}^{cl} for any choice of 𝔾^{∗}.

Proof: Let ρ,ν : Var→ 𝔾(A), (f,n) ∈ Σ and t_{i},u_{i} ∈ 𝕋^{r}(Σ), such that [[t_{i}]]_{P}(ρ) ∼ [[u_{i}]]_{P}(ν) for i = 1,...,n. Let the set 𝔾^{∗} ⊆ 𝔾(A) be adequate for the definition of [[t_{i}]]_{P}(ρ) and [[u_{i}]]_{P}(ν) for i = 1,...,n as well as for [[f(t_{1},...,t_{n})]]_{P}(ρ) and [[f(u_{1},...,u_{n})]]_{P}(ν). Then [[t_{i}[ρ]]]_{P+𝔾^{∗}}^{∅} ∼ [[u_{i}[ν]]]_{P+𝔾^{∗}}^{∅}, i.e., t_{i}[ρ] ∼_{P+𝔾^{∗}}^{cl} u_{i}[ν], for i = 1,...,n. So f(t_{1}[ρ],...,t_{n}[ρ]) ∼_{P+𝔾^{∗}}^{cl} f(u_{1}[ν],...,u_{n}[ν])by Requirement (2′) for the closed-term semantics of P +𝔾^{∗}; that is, [[f(t_{1}[ρ],...,t_{n}[ρ])]]_{P+𝔾^{∗}}^{∅} ∼ [[f(u_{1}[ν],...,u_{n}[ν])]]_{P+𝔾^{∗}}^{∅}, or [[f(t_{1},...,t_{n})]]_{P}(ρ) ∼ [[f(u_{1},...,u_{n})]]_{P}(ν).

Let ρ,ν: Var→𝔾(A) and S,S′: W →𝕋^{r}(Σ) with X ∈W ⊆Var, such that [[S_{Y}]]_{P}(ρ\W) ∼ [[S′_{Y}]]_{P}(ν\W) for Y ∈ W. The latter means that [[S_{Y}]]_{P}(ρ\W)(ξ) ∼ [[S′_{Y}]]_{P}(ν\W)(ξ) for all Y ∈ W and ξ : W → 𝔾(A). Let 𝔾^{∗} ⊆ 𝔾(A) be adequate for [[S_{Y}]]_{P}(ξ ∪ρ\W) and [[S′_{Y}]]_{P}(ξ ∪ν\W) for all Y ∈ W and ξ : W → 𝔾(A), as well as for [[^{/} \X|S^{\} /]]_{P}(ρ) and [[^{/} \X|S′^{\} /]]_{P}(ν). Then S_{Y}[ρ\W][ξ] ∼_{P+𝔾^{∗}}^{cl} S′_{Y}[ν\W][ξ] for all Y ∈ W and ξ : W →𝔾(A). So ^{/} \X|S[ρ\W]^{\} /∼_{P+𝔾^{∗}}^{cl} ^{/} \X|S′[ν\W]^{\} /by Requirement (3′) for the closed-term semantics of P+ 𝔾^{∗}, and [[^{/} \X|S^{\} /]]_{P}(ρ) = [[^{/} \X|S^{\} /[ρ]]]_{P+𝔾^{∗}}^{∅} = [[^{/} \X|S[ρ\W]^{\} / ]]_{P+𝔾^{∗}}^{∅} ∼ [[^{/} \X|S′[ν\W]^{\} / ]]_{P+𝔾^{∗}}^{∅} = [[^{/} \X|S′^{\} /]]_{P}(ν).

Let S: V_{S} → 𝕋^{r}(Σ) with X ∈ V_{S} ⊆ Var, and let γ : V_{S} → Var be an injective substitution such that the range of γ contains no variables occurring free in ^{/} \S_{Y}|S^{\} /for some Y ∈ V_{S}. Take ρ : Var → 𝔾(A). Let 𝔾^{∗} be adequate for [[^{/} \X|S^{\} /]]_{P}(ρ) and [[^{/} \γ(X)|S[γ]^{\} / ]]_{P}(ρ). By Requirement (4′) for the closed-term semantics of P +𝔾^{∗} one has ^{/} \γ(X)|S[γ]^{\} / [ρ] ∼_{P+𝔾^{∗}}^{cl} ^{/} \X|S^{\} /[ρ], using that ^{/} \X|S^{\} /[ρ] = ^{/} \X|S[ρ\V_{S}]^{\} /and ^{/} \γ(X)|S[γ]^{\} / [ρ] = / \γ(X)|S[γ][ρ\γ(V_{S})]^{\} / = ^{/} \γ(X)|S[ρ\V_{S}][γ]^{\} / . So [[^{/} \γ(X)|S[γ]^{\} / ]]_{P}(ρ) ∼ [[^{/} \X|S^{\} /]]_{P}(ρ).

Let S: V_{S} → 𝕋^{r}(Σ) with X ∈ V_{S} ⊆ Var. Take ρ : Var → 𝔾(A). Let 𝔾^{∗} be adequate for [[^{/} \X|S^{\} /]]_{P}(ρ) and [[S_{X}|S]]_{P}(ρ). Then ^{/} \X|S[ρ\V_{S}]^{\} /∼_{P+𝔾^{∗}}^{cl} ^{/} \S_{X}[ρ\V_{S}]|S[ρ\V_{S}]^{\} / by Requirement (5′) for the closed-term

semantics of P +𝔾^{∗}. Hence [[^{/} \X|S^{\} /]]_{P}(ρ)=[[^{/} \X|S^{\} /[ρ]]]∅_{P+𝔾^{∗}} =[[^{/} \X|S[ρ\V_{S}]^{\} / ]]∅_{P+𝔾^{∗}} ∼[[^{/} \S_{X}[ρ\V_{S}]|S[ρ\V_{S}]^{\} / ]]∅_{P+𝔾^{∗}}

= [[^{/} \S_{X}|S^{\} /[ρ]]]∅_{P+𝔾^{∗}} = [[S_{X}|S]]_{P}(ρ). □

Theorem 2 does not extend to sanity requirement (1). In fact, this requirement always holds for the closed-term interpretation of a TSS, yet it does not always hold for the process graph interpretation:

Example 5 Let P be a TSS with the single rule \frac{x−→^{τ} y, y−→^{τ} z}{x−→^{τ} z}. Then the process graph semantics of P

fails to satisfy sanity requirement (1) up to \underline{↔} . Namely, if ρ(x) is a graph  ^{τ  τ} , then

[[x]]_{P}(ρ) is the graph τ τ τ , and the two graphs are not (strongly) bisimulation equivalent.

Nevertheless, requirement (1) holds for almost all process algebras found in the literature:

Proposition 6 Let P be a TSS that has no rule with a variable as the left-hand side of the conclusion. The process-graph interpretation of P always satisfies requirement (1) of Section 3 up to \underline{↔} .

Proof: For x ∈ Var and ρ : Var → 𝔾(A) let 𝔾^{∗} ⊆ 𝔾(A) be adequate for [[x]]_{P}(ρ) and let ρ(x) ∈ 𝔾^{∗} be the graph g = (S,→,I). For each state s ∈ S there is a graph g_{s} := (S,→,s) in 𝔾^{∗}. Now [[x]]_{P}(ρ) is the reachable part of the graph (G,→_{G},g), where G = {g_{s} | s ∈ S} and →_{G} = {(g_{s},a,g_{t}) | (s,a,t) ∈ → }. The relation R given by g_{s} R s for all states s ∈ S reachable from I clearly is a bisimulation. Therefore [[x]]_{P}(ρ) \underline{↔} ρ(x). □

12 Preservation of Relative Expressiveness under Conservative Extensions

Definition 13 If P = (Σ_{P},A,R_{P}) and Q = (Σ_{Q},A,R_{Q}) are TSSs with Σ_{P} and Σ_{Q} disjoint then P + Q denotes the TSS (Σ_{P}∪ Σ_{Q},A,R_{P}∪ R_{Q}).

Let P_{0} be the TSS of Example 1, but without the operator f. Let P_{f} be the part of the TSS of Example 1 that only contains the operator f, so that the entire TSS of Example 1 is P_{0} + P_{f}. This TSS does not feature recursion.

A translation between two languages with signatures Σ and Σ′is a mapping T : 𝕋^{r}(Σ) → 𝕋^{r}(Σ′). Consider the translation T_{id} from the language specified by P_{0} to the language specified by P_{0} + P_{f}, given by T_{id}(t) = t for all t ∈ Σ_{P_{0}}. Also consider the translation T_{op} in the opposite direction, given by T_{op}(a.t) := a.T_{op}(t), T_{op}(id(t)) := id(T_{op}(t)) and T_{op}(f(t)) := id(T_{op}(t)) for all t ∈ 𝕋(Σ_{P_{o}+P_{f}}).

In e.g. [14] a concept of expressiveness of specification languages is studied such that language L′is at least as expressive as language L up to a semantic equivalence relation ∼ iff there exist a translation from L into L′that is valid up to ∼. It is not important here to state the precise definition of validity; it suffices to point out that T_{op} is valid up to \underline{↔} iff one has f(x) \underline{↔} id(x). Thus, applying Definition 12, it is valid when employing the closed-term semantics, but not when employing the process graph semantics.

The transition T_{id} on the other hand is valid up to \underline{↔} regardless which of the two interpretations one picks. So under the closed-term interpretation the two languages are equally expressive, whereas under the process graph semantics the language given by P_{0}+ P_{f} is more expressive than the one given by P_{0}.

For TSSs P and Q, write P ⪯ Q if the language specified by Q is at least as expressive as the one specified by P. An intuitively plausible theorem is that

P_{1} ⪯ P_{2} implies P_{1}+ Q ⪯ P_{2}+ Q,  (9)

at least under some mild conditions on the TSSs P_{1}, P_{2} and Q, for instance that they are pure and fit the tyft format defined in [16].^{3} This theorem fails when employing the closed-term semantics of TSSs: take P_{1} to be P_{0}+ P_{f}, P_{2} to be P_{0}, with T_{op} being the witness for P_{1} ⪯ P_{2}, and Q to be the TSS with as single operator τ. and as only transition rule τ.x −→^{τ} x. For the operator f in the TSS P_{0}+ P_{f} + Q drops τ-transitions, and has no counterpart in the TSS P_{0}+ Q.

This problem is fixed when employing the process graph semantics. Once the omitted definition of validity is supplied [14], the proof of (9) is entirely straightforward.

13 Related Work

Dissatisfaction with the traditional closed-term interpretation of TSSs occurred earlier in [17, 18, 8, 23] and [2]. However, rather than adapting the interpretation of TSSs, as in the present paper, these papers abandon the notion of a TSS in favour of different frameworks of system specification that are arguably more suitable for giving meaning to open terms. Larsen and Liu [17] use context systems. The CCS transition rule

x −→^{a} x′ y −→^{ā} y′

x|y −→^{τ} x′|y′

for instance takes in a context system the shape x|y −→_{a,ā}^{τ} x′|y′, or rather, suppressing the redundant variable names, | −→_{a,ā}^{τ} |. It says that the operator | can perform a τ-transition, provided its first argument does an a-transition, and its second argument an ā. The context systems of [17] form the counterpart of TSSs in the De Simone format [24]. The model is generalised by Lynch & Vaandrager [18] to action transducers, by Gadducci & U. Montanari [8] to the tile model, and by Rensink [23] to conditional transition systems. The latter two proposals are further generalised to symbolic transition systems by Baldan, Bracciali & Bruni [2].

One method to relate these models with TSSs under the closed-term and process graph interpretations is through notions of strong bisimilarity on open terms. This is a central theme in [23]. The most natural notion of bisimulation on the above models is bisimulation under formal hypothesis, \underline{↔} ^{fh}. That name stems from De Simone [24], who defined the same concept in terms of TSSs. On the context systems sketched above it requires the usual transfer property for bisimulations for doubly labelled transitions such as −→_{a,ā}^{τ} . On TSSs, a bisimulation under formal hypothesis essentially is a symmetric relation R on open terms such that

if t R u and P ⊢ \frac{\{x_{i} −→^{a_{i}} y_{i} | i ∈ I\}}{t −→^{a} t′} then P ⊢ \frac{\{x_{i} −→^{a_{i}} y_{i} | i ∈ I\}}{u −→^{a} u′} for an u′∈ 𝕋^{r}(Σ_{Q}) with t′R u′.

Rensink [23] shows that \underline{↔} ^{fh} is strictly finer than \underline{↔} ^{ci}. Example 6 Let P be the TSS with inaction 0, action prefix, choice and intersection, specified by the following rules:

a.x −→^{a} x  \frac{x −→^{a} x′}{x + y −→^{a} x′}  \frac{y −→^{a} y′}{x + y −→^{a} y′}  \frac{x −→^{a} x′ y −→^{a} y′}{x ∩ y −→^{a} x′∩ y′}

3These mild conditions should ensure that P_{i}+ Q is a conservative extension of P_{i}, for i = 1,2, as defined in [16].

where a ranges over a set of actions A. Then b.0+b.a.0+b.(x ∩a.0) \underline{↔} ^{ci} b.0+b.a.0, for no matter what one fills in for x, the process x∩a.0 either cannot perform any transitions, or it can only do a single a. So the term b.(x ∩a.0) behaves either like b.0 or like b.a.0. On the other hand, b.0+b.a.0+b.(x ∩a.0) \underline{↮} ^{fh} b.0 + b.a.0. Namely any bisimulation under formal hypothesis R relating b.0 + b.a.0 + b.(x ∩ a.0) with b.0 + b.a.0 would also have to relate x ∩ a.0 with either 0 or a.0. However, once this choice is made, substituting the wrong value for x shows that R relates two terms that are not equivalent. Rensink also defines a hypotheses-preserving bisimulation equivalence \underline{↔} ^{hp} on open terms, which is situated strictly between \underline{↔} ^{fh} and \underline{↔} ^{ci}. One has b.0 + b.a.0 + b.(x ∩ a.0) \underline{↮} ^{hp} b.0 + b.a.0. His analysis can be reused to show that \underline{↔} ^{hp} is finer than \underline{↔} ^{pg}. Note that b.0 + b.a.0 + b.(x ∩ a.0) \underline{↔} ^{pg} b.0 + b.a.0, for the same reasons as in Example 6. Thus, under the conditions of Theorem 1, we arrive at a hierarchy

\underline{↔} ^{fh} ⊆ ^{\underline{↔} ^{hp}} ⊆ ^{\underline{↔} ^{pg}} ⊆ ^{\underline{↔} ^{ci}} .

14 Concluding Remarks

This paper proposed a process graph semantics of TSSs as an alternative to the traditional closed-term semantics. It interprets an operator from the language as an operation on process graphs. Unlike the closed-term semantics, this interpretation is independent of the selection of processes that are expressible in the TSS as a whole. The intuitively plausible statement that an expressiveness inclusion between languages is preserved under a conservative extension of source and target language alike, fails for the closed-term semantics but holds for the proposed process graph semantics.

I reviewed five sanity requirements on languages equipped with a semantic equivalence relation ∼, and showed that four of them hold under the process semantics of a language if they hold under the closed-term semantics. Here I end with a few observations on when these requirements hold at all.

In [13], the ntyft/ntyxt format with recursion is introduced. It defines a wide class of TSSs, containing many known process algebras, including CCS, CSP, ACP, Meije and SCCS. It generalises the ntyft/ntyxt format of [15] by the addition of recursion as a separate language construct. The tyft/tyxt format with recursion is the same, but not allowing negative premises. [13] shows that all languages specified by a TSS in the ntyft/ntyxt format with recursion satisfy property (8) up to \underline{↔} , saying that strong bisimilarity is a congruence. This is a stronger property than (2) up to \underline{↔} , which thus also holds for the ntyft/ntyxt format. This was shown for the closed-term interpretation of TSSs. By Theorem 2 we now also have (2) up to \underline{↔} for the process graph semantics of pure TSSs in the ntyft/ntyxt format with recursion.

The same paper establishes that (3) holds up to \underline{↔} for the closed-term semantics of all TSSs in the tyft/tyxt format with recursion, thereby generalising a result from [23]. It thus also holds for the process graph semantics of all pure TSSs in the tyft/tyxt format with recursion.

It is not hard to show that also requirements (4) and (5) hold up to \underline{↔} for the closed-term interpretation of TSSs in the ntyft/ntyxt format with recursion, and thus for the process graph semantics of pure TSSs in the ntyft/ntyxt format with recursion.

Thanks to the equational nature of requirements (1), (4) and (5), once they hold up to \underline{↔} , they surely hold up to any coarser equivalence. This covers most semantic equivalences found in the literature. The same cannot be said for requirements (2) and (3). These need to be reestablished for each semantic equivalence. There is a lot of work on congruence formats, ensuring (2) for a variety of semantic equivalence. See for instance [7], and references therein. Yet, besides [23] and [13] I know of no congruence formats targeting requirement (3).

Acknowledgement My thanks to the referees for their thorough proofreading and helpful suggestions.

16 On the Meaning of Transition System Specifications

References

[1] D. Austry & G. Boudol (1984): Algèbre de processus et synchronisations. Theoretical Computer Science

30(1), pp. 91–131, doi:10.1016/0304-3975(84)90067-7.

[2] P. Baldan, A. Bracciali & R. Bruni (2007): A semantic framework for open processes. Theoretical Computer Science 389(3), pp. 446–483, doi:10.1016/j.tcs.2007.09.004.

[3] J.A. Bergstra & J.W. Klop (1984): The algebra of recursively defined processes and the algebra of regular processes. In J. Paredaens, editor: Proceedings 11^{th} ICALP, Antwerpen, LNCS 172, Springer, pp. 82–94,

doi:10.1007/3-540-13345-3_7.

[4] E. Bres, R.J. van Glabbeek & P. Höfner (2016): A Timed Process Algebra for Wireless Networks with an Application in Routing. Technical Report 9145, NICTA. Available at http://arxiv.org/abs/1606. 03663. Extended abstract in P. Thiemann, editor: Programming Languages and Systems: Proceedings 25th European Symposium on Programming, ESOP’16; held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’16, LNCS 9632, Springer, 2016, pp. 95-122.

[5] 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, doi:10.1145/828.833.

[6] W.J. Fokkink (2000): Introduction to Process Algebra. Texts in Theoretical Computer Science, An EATCS

Series, Springer, doi:10.1007/978-3-662-04293-9.

[7] W.J. Fokkink, R.J. van Glabbeek & B. Luttik (2017): Divide and Congruence III: Stability & Divergence. In R. Meyer & U. Nestmann, editors: Proceedings 28th International Conference on Concurrency Theory, CON-CUR’17, Leibniz International Proceedings in Informatics (LIPIcs) 85, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 15:1–15:16, doi:10.4230/LIPIcs.CONCUR.2017.15. Available at

http://theory.stanford.edu/~rvg/abstracts.html#124.

[8] F. Gadducci & U. Montanari (2000): The tile model. In G.D. Plotkin, C. Stirling & M. Tofte, editors: Proof, Language, and Interaction, Essays in Honour of Robin Milner, The MIT Press, pp. 133–166.

[9] R.J. van Glabbeek (1993): Full abstraction in structural operational semantics (extended abstract). In M. Nivat, C. Rattray, T. Rus & G. Scollo, editors: Proceedings 3^{rd} International Conference on Algebraic Methodology and Software Technology, AMAST’93, Twente, The Netherlands, June l993, Workshops in Computing,

Springer, pp. 77–84. Available at http://theory.stanford.edu/~rvg/abstracts.html#28.

[10] R.J. van Glabbeek (1994): On the expressiveness of ACP (extended abstract). In A. Ponse, C. Verhoef & S.F.M. van Vlijmen, editors: Proceedings First Workshop on the Algebra of Communicating Processes, ACP94, Workshops in Computing, Springer, pp. 188–217, doi:10.1007/978-1-4471-2120-6_8. Avail-

able at http://theory.stanford.edu/~rvg/abstracts.html#31.

[11] R.J. van Glabbeek (2004): The Meaning of Negative Premises in Transition System Specifications II. Journal of Logic and Algebraic Programming 60–61, pp. 229–258, doi:10.1016/j.jlap.2004.03.007. Available

at http://theory.stanford.edu/~rvg/abstracts.html#53.

[12] R.J. van Glabbeek (2011): Bisimulation. In D. Padua, editor: Encyclopedia of Parallel Computing, Springer,

pp. 136–139, doi:10.1007/978-0-387-09766-4_149. Available at http://theory.stanford.edu/
~rvg/abstracts.html#45.

[13] R.J. van Glabbeek (2017): Lean and Full Congruence Formats for Recursion. In: Proceedings 32^{nd} Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’17, Reykjavik, Iceland, 2017, IEEE Computer

Society Press, doi:10.1109/LICS.2017.8005142. Available at https://arxiv.org/abs/1704.03160.

[14] R.J. van Glabbeek (2018): A Theory of Encodings and Expressiveness. In C. Baier & U. Dal Lago, editors: Proceeding 21st International Conference on Foundations of Software Science and Computational Structures, FoSSaCS’18; held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’18, LNCS 10803, Springer, pp. 183–202, doi:10.1007/978-3-319-89366-2_10.

[15] J.F. Groote (1993): Transition System Specifications with Negative Premises. Theoretical Computer Science

118, pp. 263–299, doi:10.1016/0304-3975(93)90111-6.

R.J. van Glabbeek 17

[16] J.F. Groote & F.W. Vaandrager (1992): Structured Operational Semantics and Bisimulation as a Congruence. Information and Computation 100(2), pp. 202–260, doi:10.1016/0890-5401(92)90013-6.

[17] K.G. Larsen & X. Liu (1991): Compositionality through an Operational Semantics of Contexts. Journal of Logic and Computation 1(6), pp. 761–795, doi:10.1093/logcom/1.6.761.

[18] N.A. Lynch & F.W. Vaandrager (1996): Action Transducers and Timed Automata. Formal Aspects of Computing 8(5), pp. 499–538, doi:10.1007/BF01211907.

[19] Y.I. Manin (1977): A Course in Mathematical Logic. Graduate Texts in Mathematics 53, Springer, doi:10.

1007/978-1-4757-4385-2.

[20] R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer Science 25(3), pp. 267–310,

doi:10.1016/0304-3975(83)90114-7.

[21] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer, 1980.

[22] G.D. Plotkin (2004): A Structural Approach to Operational Semantics. Journal of Logic and Algebraic Programming 60–61, pp. 17–139, doi:10.1016/j.jlap.2004.05.001. Originally appeared in 1981.

[23] A. Rensink (2000): Bisimilarity of Open Terms. Information and Computation 156(1-2), pp. 345–385,

doi:10.1006/inco.1999.2818.

[24] R. de Simone (1985): Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science

37, pp. 245–267, doi:10.1016/0304-3975(85)90093-3.