BRICS RS-03-18 Klin & Sobociński: Syntactic Formats for Free: An Abstract Approach to Process Equivalence BRICS

Basic Research in Computer Science

Syntactic Formats for Free: An Abstract Approach to Process Equivalence

Bartek Klin Pawe� Sobociński

BRICS Report Series RS-03-18 ISSN 0909-0878 April 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Bartek Klin & Pawe� Sobociński.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/03/18/

Syntactic Formats for Free: An Abstract Approach to Process

Equivalence

Bartek Klin Paweł Sobociński BRICS^{∗} University of Aarhus, Denmark

April, 2003

Abstract

A framework of Plotkin and Turi’s, originally aimed at providing an abstract notion of bisimulation, is modified to cover other operational equivalences and preorders. Combined with bialgebraic methods, it yields a technique for the derivation of syntactic formats for transition system specifications which guarantee that various operational preorders are precongruences. The technique is applied to the trace preorder, the completed trace preorder and the failures preorder. In the latter two cases, new syntactic formats guaranteeing precongruence properties are introduced.

1 Introduction

Structural operational semantics [21, 2] is one of the most fundamental frameworks for providing a precise interpretation of programming and specification languages. Due to its flexibility and generality, it has gained much popularity in the theory of concurrent processes. It is usually presented as a labelled transition system (LTS), in which states (sometimes called processes) are closed terms over some syntactic signature, and transitions are labelled with elements of some fixed set of actions. The transition relation is in turn defined by a transition system specification, i.e., a set of derivation rules.

∗ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

Many operational equivalences and preorders have been defined on processes. Among these are: bisimulation equivalence [19], simulation preorder, trace preorder, completed trace preorder, failures preorder [13, 23] and many others (for a comprehensive list see [10]). In the case of processes without internal actions, all of the above have been given modal characterisations [10], obtained by considering appropriate subsets of the Hennessy-Milner logic [12].

Reasoning about operational equivalences and preorders is significantly easier when they are congruences (resp. precongruences). This facilitates compositional reasoning and full substitutivity. In general, operational equivalences are not necessarily congruences on processes defined by operational rules. Similarly, operational preorders are not necessarily precongruences. Proofs of such congruence results for given transition system specifications can be quite demanding. This has been an acute problem in the process calculus community and has led to new reasoning approaches, for instance, the notion of barbed congruence [18].

One way to ensure congruential properties is to impose syntactic restrictions (called syntactic formats) on operational rules. Many such formats have been developed. For bisimulation equivalence, the examples are: de Simone format [27], GSOS [8], and ntyft/ntyxt [11], each of these generalising the previous one. For trace equivalence, examples include [31, 5], while several versions of decorated trace preorders have been provided with formats in [6]. For an overview of the subject see [2]. Another approach which generates LTS on which bisimulation is a congruence is the smallest-contexts-as-labels approach [26, 17, 25].

The search for an abstract theory of processes, bisimulation and ’wellbehaved’ operational semantics has led to development of final coalgebra semantics [24], and — later — of bialgebraic semantics [29, 30] of processes. In these frameworks, the notion of a transition system is parametrised by a notion of behaviour. Bisimulation is modelled abstractly as a span of coalgebra morphisms. The abstract notion specialises to the classical one, indeed, the class of finitely branching labelled transition systems is in 1-1 correspondence with the coalgebras of the functor P_{f}(A × −), and to give a (classical) bisimulation relation is to give a span of coalgebra morphisms for this functor [3, 24]. Another abstract approach to bisimulation is via open maps [15].

In [29, 30] it was shown how to define operational rules on an abstract level. For abstract transition system specifications defined in this way, bisimulation equivalence (defined abstractly, using spans of coalgebra morphisms) is guaranteed to be a congruence.

At the core of this so-called abstract GSOS is the modelling of a transition system specification as a natural transformation

λ : Σ(id ×B) → BT

where Σ is the syntactic endofunctor, T is the monad freely generated from Σ, and B is some behaviour endofunctor. In the special case of the behaviour endofunctor P_{f}(A×−), the abstract operational rules specialise to GSOS rules.

The abstract framework which defines bisimulation as a span of coalgebra morphisms is not sufficient for certain purposes [22] and in particular one runs into problems when working with complete partial orders. Recently, another abstract notion of bisimulation, based on topologies (or complete boolean algebras) of tests, has been proposed [20, 28]. Again, for the familiar process behaviour the novel abstract notion is equivalent to the classical one.

In this paper we show that the latter abstract definition of bisimulation can in fact be modified in a structured manner, to yield other known operational equivalences and preorders. We illustrate this approach on trace preorder, completed trace preorder and failures preorder (and respective equivalences). This constitutes another systematic approach to various operational preorders and equivalences, such as those based on testing scenarios and modal logics [10], as well as quantales [1].

Although the framework is general, in this paper we shall concentrate on the category of sets and functions, Set. We define the test-suite fibration with total category Set^{∗} having as objects pairs consisting of a set X and a test suite (a subset of PX) over X. We define a way of lifting the abstract-GSOS framework to Set^{∗} by describing how to lift the syntax functor Σ and the behaviour functor B. By changing how B lifts to Set^{∗} we alter the specialisation preorder of certain test suites in Set^{∗}. In particular, taking particular liftings which strongly resemble fragments of the Hennessy-Milner logic [12] causes the specialisation preorder to vary between known operational preorders. The abstract framework guarantees precongruence properties. The only hurdle is proving that a particular transition system specification (natural transformation) λ lifts to a natural transformation in Set^{∗}:

λ : Σ^{∗}(id ×B^{∗}) → B^{∗}T^{∗}.

The consideration of which properties λ must satisfy in order to lift provides us with syntactic sub-formats of GSOS which guarantee precongruence properties for various operational preorders.

In this paper, we illustrate this approach by presenting precongruence formats for the trace preorder, the completed trace preorder and the failures preorder. The format derived for the trace preorder coincides with the well known de Simone format [31] and we include it here as an illustration of the technique on a relatively simple example. The format derived for the completed trace preorder is, to the best of our knowledge, the first such format published. The format derived for the failures preorder is incomparable with the analogous format given in [6].

The structure of the paper is as follows. After §2 of preliminaries, we present the three obtained syntactic formats in §3, together with some examples and counterexamples from literature. The remaining sections are devoted to proving that the presented formats are indeed precongruence formats w.r.t. their respective preorders, and at the same time to illustrating the method of deriving such formats from a given operational preorder. In §4, we recall the basics of bialgebraic semantics. In §5, we present an abstract approach to operational preorders based on the notion of a test suite. In §6, this approach is merged with the bialgebraic framework to yield a general way of checking whether a given operational preorder is a congruence for a given transition system specification. Finally, in §7, we prove that the formats presented in §3 ensure the respective precongruence results. We conclude in §8 by showing possible directions of future work.

Acknowledgements. Most of the contents of §5 and §6 is a modified version of the framework developed (and, unfortunately, not yet published) by Gordon Plotkin [20] and Daniele Turi [28]. We are indebted to Mikkel Nygaard for reading the extended abstract of this report and providing us with many helpful comments. The first author is also grateful to Daniele Turi for introducing him to the subject and for inspiration, and to Gordon Plotkin for discussions and encouragement.

2 Preliminaries

A labelled transition system (LTS) is a set P of processes, a set A of actions, and a transition relation ▶ ⊆ P × A × P. As usual, we write p ^{a} ▶ p′ instead of ⟨p, a, p′⟩ ∈ ▶. An LTS is finitely branching, if for every process p there are only finitely many transitions p ^{a} ▶ p′.

Given a set of actions A, three sets of modal formulae F_{Tr}, F_{CTr}, and F_{Fl} are given by the following BNF grammars:

\begin{matrix}F_{Tr} & ϕ ::= ⊤ | ⟨a⟩ ϕ \\ F_{CTr} & ϕ ::= ⊤ | ⟨a⟩ ϕ | Ã \\ F_{Fl} & ϕ ::= ⊤ | ⟨a⟩ ϕ | Q̃ \end{matrix}

where a ranges over A, and Q ranges over subsets of A. Formulae in F_{Tr} are called traces over A. Formulae in F_{CTr} ended with Ã are called completed traces, and formulae in F_{Fl} — failures.

Given an LTS, the satisfaction relation ⊧ between processes and modal formulae is defined inductively as follows:

p ⊧ ⊤
p ⊧ ⟨a⟩ ϕ ⟺ p′ ⊧ ϕ for some p′ such that p ^{a} ▶ p′
p ⊧ Q̃  ⟺ there is no a ∈ Q, p′ ∈ P such that p ^{a} ▶ p′

If p ⊧ ϕ, we will say that ϕ is a trace (completed trace, failure) of p.

Then three operational preorders on the set of processes are defined: the trace preorder ⊑_{Tr}, the completed trace preorder ⊑_{CTr}, and the failures preorder ⊑_{Fl}:

p ⊑_{W} p′ ⟺ (∀ϕ ∈ F_{W} .p ⊧ ϕ ⟹ p′ ⊧ ϕ)

where W ∈ {Tr, CTr, Fl}.

In the context of structural operational semantics, processes are usually closed terms over some signature. A signature Σ is a set (also denoted Σ) of language constructs, together with an arity function ar : Σ → ℕ. For a given set X of variables, ΣX is the set of expressions of the form f(x_{1}, …, x_{ar(f)}), where f ∈ Σ and x_{i} ∈ X. In other words,

ΣX ≅ ∐_{f∈Σ} X^{ar(f)}

where ∐ denotes disjoint union. Given a signature Σ and a set X, the set T_{Σ}X of terms over Σ with variables X is (isomorphic to) the least fixpoint of the operator

ΦY = X + ΣY

where + denotes disjoint union of sets. When describing terms from T_{Σ}X the injections ι_{1} : X → T_{Σ}X and ι_{2} : ΣT_{Σ}X → T_{Σ}X will often be omitted, i.e., we will write f(x, y) rather than ι_{2}(f(ι_{1}(x), ι_{1}(y))). Also the subscript in T_{Σ}X will be omitted if Σ is irrelevant or clear from the context. Elements of T ∅ are called closed terms over Σ.

For a term t ∈ T X and a function σ : X → Y, t[σ] will denote the term in T Y resulting from t by simultaneously replacing every x ∈ X with σ(x).

In the following, we assume a fixed, infinite set of variables Ξ, ranged over by x_{1}, x_{2}, …, y_{1}, y_{2}, . . .. Terms with variables from Ξ will be typeset t, t′, etc.

Let us fix an arbitrary set of labels A. For a signature Σ, a positive Σliteral is an expression t ^{a} ▶ t′, and a negative Σ-literal is an expression t ^{a} ▶̸, where t, t′ ∈ T Ξ and a ∈ A. A transition rule ρ over Σ is an expression \frac{H}{α}, where H is a set of Σ-literals and α is a positive Σ-literal. Elements of H are then called premises of ρ, and α — the conclusion of ρ. The left-hand side and the right-hand side of the conclusion of ρ are called the source and the target of ρ, respectively.

Similarly, a Σ-semiliteral is either a negative Σ-literal, or an expression t ^{a} ▶, where t ∈ T Ξ and a ∈ A. A positive literal t ^{a} ▶ t′ completes the semiliteral t ^{a} ▶, and we say that a negative literal completes itself.

A transition system specification over Σ is a set of transition rules over Σ.

In the following definition assume a fixed signature Σ, and a finite set A.

Format 1 (GSOS). A transition system specification R is in GSOS [8] format if every rule ρ ∈ R is of the form

\frac{\{ x_{i} ^{a_{ij}} ▶ y_{ij} : i ≤ n, j ≤ m_{i} \} ∪ \{ x_{i}^{b_{ik}} ▶̸ : i ≤ n, k ≤ n_{i} \}}{f(x_{1}, …, x_{n}) ^{c} ▶ t}

with f ∈ Σ and n = ar(f), such that x_{i} ∈ Ξ and y_{ij} ∈ Ξ are all distinct and are the only variables that occur in ρ. In the following, we will consider only image finite GSOS specifications, i.e. those with finitely many rules for each construct f ∈ Σ and action c ∈ A.

Given a transition system specification R in GSOS format, one defines a notion of a provable positive literal in a straightforward way. The set of all provable literals forms a finitely branching LTS with closed terms over Σ as processes, and with positive closed literals as transitions (for details, see [2]).

An operational preorder ⊑ is a precongruence with respect to a transition system specification R, if in the LTS induced by R, for each f ∈ Σ with arity n, if t_{1} ⊑ t′_{1}, …, t_{n} ⊑ t′_{n}, then f(t_{1}, …, t_{n}) ⊑ f(t′_{1}, …, t′_{n}).

The examples in §3 are based on basic process algebra BPA. Assuming a finite set A of actions, its syntax Σ is defined by the BNF grammar

t ::= 0 | αt | t+t

and the transition system specification BPA over Σ is a collection of rules

\overline{αx  ^{α} ▶ x}    \frac{x  ^{α} ▶ x′}{x + y  ^{α} ▶ x′}  \frac{y  ^{α} ▶ y′}{x + y  ^{α} ▶ y′}

where α ranges over A. When presenting terms over the above syntax, the trailing 0’s will be omitted. It is easy to see that BPA is in the GSOS format.

3 Precongruence Formats

In this section we introduce the syntactic formats derived using the framework described in the latter parts of the paper. The precongruence properties of these formats are formally stated in §7.

Format 2 (Tr-format). A set of GSOS rules R is in Tr-format, if for each ρ ∈ R:

• all premises of ρ are positive,

• no variable occurs more than once in the left-hand sides of premises and in the target.

It is easy to see that this format coincides with the well-known de Simone format [27]. The fact that this syntactic format ensures the trace preorder to be a precongruence was first proved in [31].

We proceed to define an analogous syntactic format for the completed trace preorder.

Definition 1 (CTr-testing set). A CTr-testing set over a set of variables {x_{1}, …, x_{n}} is a set of semiliterals P of the form

P = { x_{i} ^{a_{i}} ▶̸ : i ∈ I } ∪ { x_{i} ^{a} ▶ : i ∈ J, a ∈ A }

where I, J ⊆ {1, …, n}.

Format 3 (CTr-format). A set of GSOS rules R is in CTr-format, if

1. For each rule ρ ∈ R:

• if ρ has a negative premise x ^{a} ▶̸, than for every label b ∈ A, ρ has also the negative premise x ^{b} ▶̸,

• no variable occurs more than once in the target of ρ,

• no variable occurs simultaneously in the left-hand side of a premise and in the target of ρ,

• no variable occurs simultaneously in the left-hand side of a positive premise and in the left-hand side of any other premise of ρ.

2. For each construct f(x_{1}, …, x_{n}) of the language, there exists a sequence P_{1}, …, P_{k} of CTr-testing sets over {x_{1}, …, x_{n}}, such that

• For every (possibly renamed) rule ρ ∈ R with source f(x_{1}, …, x_{n}) there exists a sequence p_{1}, … p_{k} of semiliterals from P_{1}, …, P_{k} respectively, such that for every i ∈ {1, …, k} there exists a premise r of ρ such that r completes p_{i}.

• For every sequence p_{1}, …, p_{k} of semiliterals from P_{1}, …, P_{k} respectively, there exists a (possibly renamed) rule ρ ∈ R with source f(x_{1}, …, x_{n}) such that for each premise r of ρ there exists an i ∈ {1, …, k} such that r completes p_{i}.

Note, in particular, that if k = 0 then the first part of condition 2 above is always true. Also, if k = 1 and P_{1} = ∅, then the second part of condition 2 is always true.

Proposition 2. BPA is in CTr-format.

Proof. It is clear that all rules of BPA satisfy condition 1 of CTr-format. For condition 2, consider a language construct a− corresponding to a ∈ A. Take k = 0 and check that condition 2 holds. For the binary construct +, take k = 1 and P_{1} = { x ^{a} ▶ : a ∈ A } ∪ { y ^{a} ▶ : a ∈ A }.

The following example is taken from [2]. Assume A = {a, b}, and extend BPA with an operational rule for the so-called encapsulation operator ∂_{{b}}:

\frac{x ^{a} ▶ y}{∂_{\{b\}}(x) ^{a} ▶ ∂_{\{b\}}(y)}

Then it is easy to check that aa + ab ∼_{CTr} a(a + b) but that ∂_{{b}}(aa + ab) ⋢_{CTr} ∂_{{b}}(a(a + b)).

Another example of an operational construct that is not well behaved with respect to completed traces is the synchronous composition, as shown in [31]. Here, we add the rules

\frac{x ^{α} ▶ x′ y ^{α} ▶ y′}{x × y ^{α} ▶ x′ × y′}

where α ranges over A = {a, b}. Here it is easy to see that aa × (aa + ab) ⋢_{CTr} aa × a(a + b).

These two examples have led the authors of [2] to speculate that one cannot hope for a general syntactic congruence format for completed trace equivalence.

Proposition 3. The semantics for the encapsulation operator ∂ and the synchronous composition × are not in CTr-format.

Proof. Both semantics fail to satisfy condition 2 of CTr-format.

For the encapsulation operator, assume a sequence P_{1}, …, P_{k} of CTrtesting sets over {x}. From the first part of condition 2, we have x ^{a} ▶ ∈ P_{i} for 1 ≤ i ≤ k. This, by definition of CTr-testing set, means that also x ^{b} ▶ ∈ P_{i} for 1 ≤ i ≤ k. Now take p_{i} = x ^{b} ▶ for 1 ≤ i ≤ k and see that no rule satisfies the second part of condition 2.

For the synchronous composition operator, assume a sequence P_{1}, …, P_{k} of CTr-testing sets over {x, y}. From the first part of condition 2, we have that for each 1 ≤ i ≤ k, x ^{a} ▶ ∈ P_{i} or y ^{a} ▶ ∈ P_{i}. By definition of a CTr-testing set, this means that for each 1 ≤ i ≤ k, x ^{a} ▶ ∈ P_{i} or y ^{b} ▶ ∈ P_{i}. Now for each 1 ≤ i ≤ k, take p_{i} to be x ^{a} ▶ if x ^{a} ▶ ∈ P_{i}, and y ^{b} ▶ otherwise. It is easy to see that no rule satisfies the second part of condition 2 for this sequence of p_{i}.

For a non-trivial example of a transition system specification in CTrformat, extend BPA with sequential composition, defined by rules

\frac{x  ^{α} ▶ x′}{x; y  ^{α} ▶ x′; y}    \frac{x ^{a} ▶̸ for all a ∈ A y  ^{α} ▶ y′}{x; y  ^{α} ▶ y′}

where α ranges over A.

Proposition 4. BPA extended with sequential composition is in CTrformat.

Proof. Condition 1 of CTr-format is checked easily. For condition 2, it is enough to check it for the sequential composition operator. Take k = |A| + 1, and

\begin{matrix}P_{i} = \{ x ^{a} ▶ : a ∈ A \} ∪ \{x^{a_{i}} ▶̸\} & for 1 ≤ i < k \\ P_{k} = \{ x ^{a} ▶ : a ∈ A \} ∪ \{ y ^{a} ▶ : a ∈ A \} \end{matrix}

It is straightforward to check that both parts of condition 2 hold for this choice of P_{i}.

We proceed to define a precongruence syntactic format for the failures preorder.

Definition 5 (Fl-testing set). An Fl-testing set over a set of variables {x_{1}, …, x_{n}} is a set of semiliterals P of the form

P = { x_{i} ^{a_{i}} ▶̸ : i ∈ I } ∪ { x_{i} ^{b_{ij}} ▶ : 1 ≤ i ≤ n, 1 ≤ j ≤ m_{i} }

(where I ⊆ {1, …, n}, m_{i} ∈ ℕ), such that for any labels a, b ∈ A, if x_{i} ^{a} ▶ ∈ P and x_{i} ^{b} ▶̸ ∈ P then x_{i} ^{b} ▶ ∈ P.

Format 4 (Failures Format). A set of GSOS rules R is in Fl-format, if

1. For each rule ρ ∈ R:

• no variable occurs more than once in the target of ρ,

• no variable occurs simultaneously in the left-hand side of a premise and in the target of ρ,

• no variable occurs simultaneously in the left-hand side of a positive premise and in the left-hand side of any other premise of ρ.

2. For each construct f(x_{1}, …, x_{n}) of the language, and for each set of labels Q ⊆ A, there exists a sequence P_{1}, …, P_{k} of Fl-testing sets over {x_{1}, …, x_{n}}, such that

• For every (possibly renamed) rule ρ ∈ R with the conclusion f(x_{1}, …, x_{n}) ^{a} ▶ t with a ∈ Q and an arbitrary t, there exists a sequence p_{1}, …, p_{k} of semiliterals from P_{1}, …, P_{k} respectively, such that for every i ∈ {1, …, k} there exists a premise r of ρ such that r completes p_{i}.

• For every sequence p_{1}, …, p_{k} of semiliterals from P_{1}, …, P_{k} respectively, there exist a label a ∈ Q, a term t, and a (possibly renamed) rule ρ ∈ R with the conclusion f(x_{1}, …, x_{n}) ^{a} ▶ t such that for each premise r of ρ there exists an i ∈ {1, …, k} such that r completes p_{i}.

Proposition 6. BPA is in Fl-format.

Proof. Again, clearly all rules of BPA satisfy condition 1 of Fl-format. For condition 2, consider a language construct a− corresponding to a ∈ A. For any Q ⊆ A, if a ∈ Q then take k = 0 and check that condition 2 holds. Similarly, if a ∉ Q, take k = 1 and P_{1} = ∅. For the binary construct +, given Q ⊆ A, take k = 1 and

P_{1} = { x ^{a} ▶ : a ∈ Q } ∪ { y ^{a} ▶ : a ∈ Q }

and check that condition 2 holds.

In [7] it was shown that the failures preorder is not a precongruence for BPA extended with sequential composition.

Proposition 7. If A contains at least two different labels a, b, then BPA extended with sequential composition is not in Fl-format.

Proof. Condition 2 of Fl-format fails for the sequential composition operator. Indeed, take Q = {a} and assume a sequence P_{1}, P_{2}, …, P_{k} of Fl-testing sets over {x, y}. Consider the first part of condition 2 applied to the first rule for the sequential operator instantiated with α = a. It is easy to see that x ^{a} ▶ ∈ P_{i} for all 1 ≤ i ≤ k. Similarly, applying the same condition to the second rule (instantiated with α = a), one sees that for all 1 ≤ i ≤ k, either y ^{a} ▶ ∈ P_{i} or x ^{b} ▶̸ ∈ P_{i} for some b ∈ A. This means that there exists a sequence p_{1}, …, p_{k} such that p_{i} ∈ P_{i} and p_{i} ≠ x ^{a} ▶ for all 1 ≤ i ≤ k.

Now from the second part of condition 2 applied to this sequence it follows that for some 1 ≤ i ≤ k, p_{i} = x ^{b} ▶̸ for some b ≠ a. This means that x ^{b} ▶̸ ∈ P_{i}, and since x ^{a} ▶ ∈ P_{i}, by definition of Fl-testing set also x ^{b} ▶ ∈ P_{i}.

Now take

p′_{i} = \{ \begin{matrix}x ^{b} ▶ & if p_{i} = x ^{b} ▶̸ \\ p_{i} & otherwise \end{matrix}

The second part of condition 2 fails for this sequence. In the first rule (necessarily instantiated with α = a), the premise x ^{a} ▶ x′ does not complete any p′_{i}. In the second rule (also necessarily instantiated with α = a), the premise x ^{b} ▶̸ does not complete any p′_{i}.

The Fl-format excludes many examples of transition system specifications that behave well with respect to the failures preorder. Many of these examples are covered by the ‘failure trace format’ introduced in [6]. However, the latter format excludes also some examples covered by Fl-format. Indeed, assume a, b ∈ A and extend BPA with two unary constructs g, h and operational rules

\frac{x  ^{α} ▶ x′}{g(x) ^{α} ▶ h(x′)}  \frac{x ^{a} ▶̸}{h(x) ^{b} ▶ 0}

where α ranges over A.

Proposition 8. BPA extended with g and h as above, is in Fl-format.

Proof. Condition 1 of Fl-format is obviously satisfied, and it is enough to check condition 2 for constructs g and h only.

For g, for any Q ⊆ A take k = 1 and P_{1} = { x ^{a} ▶ : a ∈ Q }. It is easy to see that condition 2 holds. For h, for any Q ⊆ A, if b ∈ Q then take k = 1 and P_{1} = {x ^{a} ▶̸}. If b ∉ Q, take k = 1 and P_{1} = ∅. Condition 2 is also satisfied.

However, the rules above are not in the ‘failure trace format’ proposed in [6]. This means that Fl-format is incomparable with that format.

4 An Abstract Approach

In this section we shall recall the foundations needed for the framework described in §5 and §6. First, we briefly recall how LTS can be described as coalgebras for a specific behaviour endofunctor and briefly recall final coalgebra semantics. We then proceed to recall several notions from the abstract approach to operational semantics of Plotkin and Turi [30].

In the following, P : Set → Set will denote the (covariant) powerset functor. The (covariant) finite powerset functor P_{f} : Set → Set takes a set to the set of its finite subsets.

The reader is referred to [16] for any unexplained categorical notation used henceforward.

4.1 Coalgebras

There is a bijection between the set of finitely branching LTS over a fixed set of actions A and the coalgebras of the functor P_{f}(A × −). Indeed, given an LTS ⟨P, A, ▶⟩ let

h : P → P_{f}(A × P)

be defined by h(p) = { ⟨a, p′⟩ : p ^{a} ▶ p′ }.

The functor P_{f}(A×−) has a final coalgebra φ : S → P_{f}(A×S), that is, a terminal object in the category of P_{f}(A × −)-coalgebras and P_{f}(A × −)- coalgebra morphisms. The carrier S of this coalgebra may be described as the set of synchronisation trees with edges having labels from A, quotiented by bisimulation [4, 29].

4.2 GSOS is natural

In the following we specialise the framework of [30] to the category Set and behaviour functor P_{f}(A × −). Any syntactic signature Σ determines a so-called syntactic endofunctor Σ : Set → Set which acts on sets by sending

Σ : X ↦ ∐_{f∈Σ} X^{ar(f)}

and the action on functions is the obvious one. The functor Σ freely generates a monad ⟨T, μ, η⟩ : Set → Set. It turns out that T X is (isomorphic to) the set of all terms over Σ with variables from X.

The following theorem is from [30].

Theorem 9. There is a correspondence between sets of rules in the GSOS format (Format 1) and natural transformations

λ : Σ(id ×P_{f}(A × −)) → P_{f}(A × T −)

Moreover, the correspondence is 1-1 up to equivalence of sets of rules.

Proof. Here we only show how to construct a natural transformation λ from a set of rules R. Given a function symbol f ∈ Σ with arity n and a set X, a rule ρ in the GSOS format (Format 1)

\frac{\{ x_{i} ^{a_{ij}} ▶ y_{ij} : i ≤ n, j ≤ m_{i} \} ∪ \{ x_{i}^{b_{ik}} ▶̸ : i ≤ n, k ≤ n_{i} \}}{f(x_{1}, …, x_{n}) ^{c} ▶ t}

defines a map ρ_{X} : (X × P(A × X))^{n} → P_{f}(A × T X) as follows: ⟨c, t⟩ ∈ ρ_{X} ⟨x_{i}, β_{i}⟩_{i≤n} iff there exists σ : Ξ → X satisfying

1. σ(x_{i}) = x_{i}

2. ∀i ≤ n ∀j ≤ m_{i} ⟨a_{ij}, σ(y_{ij})⟩ ∈ β_{i}

3. ∀i ≤ n ∀k ≤ n_{i} ∀x ∈ X ⟨b_{ij}, x⟩ ∉ β_{i}

4. t[σ] = t

Then given a set R of rules in the GSOS format we can define a function λ_{X} : Σ(X × P_{f}(A × X)) → P_{f}(A × T X) by defining for each f ∈ Σ a function f_{X} : (X × P_{f}(A × X))^{n} → P_{f}(A × T X) as follows:

f_{X} : ⟨x_{i}, U_{i}⟩_{i≤n} ↦ ⋃_{ρ∈R ρ a rule for f} ρ_{X}⟨x_{i}, β_{i}⟩_{i≤n}

Finally, λ_{X} is determined uniquely by the f_{X}s since it is a function from a coproduct.

4.3 λ-models

We shall now recall some central results of [30].

Assume a natural transformation λ : Σ(id ×B) → BT. A λ-model is a pair

ΣX ⟶^{h} X ⟶^{g} BX

which satisfies g ∘ h = Bh^{♯} ∘ λ_{X} ∘ Σ ⟨id, g⟩, where h^{♯} : T X → X is the inductive extension of h. A λ-model morphism between ΣX ⟶^{h} X ⟶^{g} BX and ΣX′ ⟶^{h′} X′ ⟶^{g′} BX′ is a morphism f : X ⟶ X′ which is simultaneously a Σ-algebra morphism and a B-coalgebra morphism, ie. h′ ∘ Σf = g ∘ h and g′ ∘ f = Bf ∘ g. Let λ-Mod denote the category of λ-models and λ-model morphisms.

Theorem 10. Suppose that C is a category, Σ is an endofunctor which freely generates a monad T and B is an endofunctor which cofreely generates a comonad D. Then the following hold:

1. λ-Mod has an initial and final object,

2. the carrier and algebra part of the initial λ-model is the initial Σ-algebra,

3. the carrier and coalgebra part of the final λ-model is the final Bcoalgebra and

4. the coalgebra part of the initial λ-model is the so-called intended operational model of λ.

Proof. See [30]. In particular, if C = Set and B = P_{f}(A × −), then the intended operational model of λ is the LTS generated by the GSOS rules associated to λ.

If the conditions of Theorem 10 hold and ψ : ΣN → N is the initial Σ-algebra and φ : S → BS is the final B-coalgebra then there exists a Σ-algebra δ : ΣS → S and a B-coalgebra ϵ : N → BN so that ⟨ψ, ϵ⟩ is the initial object of λ-Mod and ⟨δ, φ⟩ is the final object of λ-Mod. Then, by initiality (or finality) there exists a unique λ-model morphism k : N → S as illustrated below:

\xymatrix{ΣN \ar[d]_{ψ} \ar[r]^{T k} & ΣS \ar[d]^{δ} \\ N \ar[d]_{ϵ} \ar[r]^{k} & S \ar[d]^{φ} \\ BN \ar[r]_{Bk} & BS.}

In the following, we shall use the fact that theorem 10 applies to Set, Σ and P_{f}(A × −).

5 Process Equivalences from Fibred Functors

In this section, we introduce the central concept of a test suite fibration. This is a modification of the yet unpublished framework [20, 28] due to Plotkin and Turi. In that approach, the test suites (Definition 11) are necessarily topologies, that is, they satisfy certain closure properties. We relax this definition and require only that a test suite contains the largest test. This modification allows us to consider operational preorders and equivalences different from bisimulation. Also, the original framework was developed largely for Cppo-enriched categories, here we deal primarily with Set.

We define 2 = {tt, ff}. Given a function f : X → Y and subsets V ⊆ X, V′ ⊆ Y, we shall use f(V) to denote the set { y ∈ Y : ∃x ∈ X. fx = y } and similarly f^{−1}(V′) to denote { x ∈ X : fx ∈ V′ }. Given a set τ ⊆ PX, the specialisation preorder of τ is defined by

x ≤_{τ} x′ iff ∀V ∈ τ. x ∈ V ⇒ x′ ∈ V

We will sometimes omit the subscript in ≤_{τ}, where τ will be clear from the context.

For an introduction to fibrations and related terminology, the reader is referred to the first chapter of [14].

Definition 11 (Test suite). A test on a set X is a function V : X → 2. We say that an element x passes a test V iff V x = tt. A test suite on X is a collection of tests on X which includes the maximal test, that is, the function constant at tt. Let X^{∗} denote the poset of test suites on X ordered by inclusion.

We can define a functor (−)^{∗} : Set^{op} → Pos which sends a set to the poset of test suites X^{∗} and sends a function f : X → Y to f^{∗} : Y^{∗} → X^{∗} defined by

f^{∗}τ′ = { V′ ∘ f : V′ ∈ τ′ } .

Intuitively, we usually think of tests on X as subsets of X. Then f^{∗} is the pre-image operation, taking each test on Y to the test on X which maps to Y via f. This intuition poses no problem since there is a canonical isomorphism between the sets of subsets V ⊆ X and functions V : X → 2. Thus we shall sometimes use set-theoretical notation when talking about tests, that is, we shall make use of notions such as membership, union and cartesian product. Similarly, we shall usually denote the maximal test on X as simply X. We shall, however, be careful to indicate when we are using set-theoretical notation as opposed to similar operations on functions.

Definition 12 (Test suite fibration). A fibration of test suites for (−)^{∗} is the fibration obtained using the Grothendieck construction, ie. the total category Set^{∗} has

• objects: pairs ⟨X, τ⟩ where X ∈ Set and τ ∈ X^{∗}, τ is a test suite.

• arrows: ⟨X, τ⟩ ⟶^{f} ⟨X′, τ′⟩ iff f : X → X′ and f^{∗}τ′ ⊆ τ.

It is then a standard result that the obvious forgetful functor U : Set^{∗} → Set taking ⟨X, τ⟩ to X is a fibration.

It will be useful to define various operations on test suites τ. Letting ∇ : 2 + 2 → 2 be the codiagonal and ∧ : 2 × 2 → 2 be logical-and, we let

τ ⊕ τ′ = { ∇ ∘ (V + V′) : V ∈ τ, V′ ∈ τ′ }
τ ⊗ τ′ = { ∧ ∘ (V × V′) : V ∈ τ, V′ ∈ τ′ }
τ ⋈ τ′ = { V ∘ π_{1} : V ∈ τ } ∪ { V′ ∘ π_{2} : V′ ∈ τ′ } .

It is easy to check that given two test suites, families τ ⊕ τ′, τ ⊗ τ′ and τ ⋈ τ′ are test suites. Intuitively, given test suites τ and τ′ on X and Y, τ ⊕ τ′ is the test suite on X + Y obtained by taking (disjoint) unions of tests from τ on X and τ′ on Y, τ ⊗ τ′ is the test suite on X × Y consisting of tests built by performing a test from τ on X and simultaneously performing a test from τ′ on Y and accepting when both tests accept; finally, τ ⋈ τ′ is the test on X × Y which consists of either a test from τ on X or a test from τ′ on Y.

Proposition 13. The category Set^{∗} has coproducts and products:

\begin{matrix}⟨X, τ⟩ + ⟨Y, τ′⟩ = ⟨X + Y, τ ⊕ τ′⟩ \\ ⟨X, τ⟩ × ⟨Y, τ′⟩ = ⟨X × Y, τ ⋈ τ′⟩ \end{matrix}

Proof. For the product, the projections are the projections in Set,

⟨X, τ⟩ ⟵^{π_{1}} ⟨X × Y, τ ⋈ τ′⟩ ⟶^{π_{2}} ⟨Y, τ′⟩

and clearly π_{1}^{∗}τ = { V ∘ π_{1} : V ∈ τ } ⊆ τ ⋈ τ′ and similarly π_{2}^{∗}τ′ ⊆ τ ⋈ τ′. The universal property follows from the universal property in Set, indeed, given ⟨Z, τ′′⟩ and morphisms f : ⟨Z, τ′′⟩ → ⟨X, τ⟩ and g : ⟨Z, τ′′⟩ → ⟨Y, τ⟩ the morphism induced by the universal property in Set, ⟨f, g⟩ : ⟨Z, τ′′⟩ → ⟨X × Y, τ ⋈ τ′⟩ is defined in Set^{∗}:

⟨f, g⟩^{∗} (τ ⋈ τ′) = ⟨f, g⟩^{∗} ({ V ∘ π_{1} : V ∈ τ } ∪ { V′ ∘ π_{2} : V′ ∈ τ′ })
= { V ∘ f : V ∈ τ } ∪ { V′ ∘ g : V′ ∈ τ }

⊆ τ′′ ∪ τ′′ = τ′′ (as f and g are morphisms in Set^{∗})

For the coproduct, the injections are similarly the underlying injections

⟨X, τ⟩ ⟶^{i_{1}} ⟨X + Y, τ ⊕ τ′⟩ ⟵^{i_{2}} ⟨Y, τ′⟩

indeed, i_{1}^{∗}(τ ⊕ τ′) = { ∇ ∘ (V + W) ∘ i_{1} : V ∈ τ, W ∈ τ′ } = τ and similarly i_{2}^{∗}(τ ⊕ τ′) = τ′. The universal property also follows easily from the one in Set.

In the following it will be also useful to use the following tensor product on Set^{∗}:

⟨X, τ⟩ ⊗ ⟨Y, τ′⟩ = ⟨X × Y, τ ⊗ τ′⟩

Let B : Set → Set be some behaviour endofunctor. A lifting of B to Set^{∗} is an endofunctor B^{∗} : Set^{∗} → Set^{∗} such that, for some B_{X} : X^{∗} → (BX)^{∗} we have B^{∗} ⟨X, τ⟩ = ⟨BX, B_{X}τ⟩ and B^{∗}f = Bf. It turns out that there are many possible choices for B_{X} giving different liftings of the behaviour endofunctor B to Set^{∗}. One systematic way to construct such liftings is via families of functions from B2 to 2. Intuitively, such functions correspond to modalities like those in the Hennessy-Milner logic. In the original framework due to Plotkin and Turi [20, 28] the canonical choice of all functions from B2 to 2 is taken.

For any X, let Cl_{X} : PPX → X^{∗} denote a closure operator. We shall only demand that for all f : X → Y and Z some set of subsets of Y we have Cl_{X} f^{∗}Z = f^{∗} Cl_{Y} Z (with the obvious extension of the domain of f^{∗} to all sets of subsets). Intuitively, a closure operator corresponds to a set of propositional connectives.

Given an arbitrary family W of functions B2 → 2, we define an operator B_{X}^{W} : X^{∗} → (BX)^{∗} as follows:

B_{X}^{W} (τ) = Cl_{BX} { w ∘ BV : w ∈ W and V ∈ τ } .

We are now in a position to construct a lifting of B to Set^{∗}. Indeed, we let B^{W} ⟨X, τ⟩ = ⟨BX, B_{X}^{W} τ⟩ and B^{W} f = Bf. One needs to check that for any f : ⟨X, τ⟩ → ⟨X′, τ′⟩, Bf : ⟨BX, B_{X}^{W} τ⟩ → ⟨BX′, B_{X′}^{W}τ′⟩ is a morphism in Set^{∗}. Indeed,

(Bf)^{∗}B_{X′}^{W}τ′ = (Bf)^{∗} Cl_{BX′} { w ∘ BV′ : w ∈ W, V′ ∈ τ′ }
= Cl_{BX}(Bf)^{∗} { w ∘ BV′ : w ∈ W, V′ ∈ τ′ }
= Cl_{BX} { w ∘ BV′ ∘ Bf : w ∈ W, V′ ∈ τ′ }
= Cl_{BX} { w ∘ B(V′ ∘ f) : w ∈ W, V′ ∈ τ′ }
⊆ Cl_{BX} { w ∘ BV : w ∈ W, V ∈ τ }  (f^{∗}τ′ ⊆ τ)
= B_{X}^{W} τ

Theorem 14. Suppose that B : Set → Set has a final coalgebra

φ : S → BS.

Then φ : ⟨S, M^{W} ⟩ → ⟨BS, B_{S}^{W} M^{W} ⟩ is a final B^{W} coalgebra where M^{W} is the least fixpoint of the operator Φ(τ) = φ^{∗}B_{S}^{W} τ on S^{∗}.

Proof. First, by definition φ^{∗}(B_{S}^{W} M) = M and therefore φ is a morphism in Set^{∗}.

Suppose that h : ⟨X, τ⟩ → ⟨BX, B_{X}^{W} τ⟩ is an arbitrary B^{W} -coalgebra. Then h : X → BX is a B-coalgebra and we have a unique k : X → S such that Bk ∘ h = φ ∘ k:

\xymatrix{X \ar[r]^{k} \ar[d]_{h} & S \ar[d]^{φ} \\ BX \ar[r]_{Bk} & BS.}

It remains to verify that k is a morphism in the total category. Thus we have to show that k^{∗}M ⊆ τ. We do this by proving that k^{∗}M is the least prefixpoint of the operator Φ′(τ) = h^{∗}B_{X}^{W} τ. First notice that

Φ′(k^{∗}τ) = h^{∗}B_{X}^{W} k^{∗}τ
= Cl_{BX} { w ∘ B(V ∘ k) ∘ h : w ∈ W and V ∈ τ }
= Cl_{BX} { w ∘ BV ∘ Bk ∘ h : w ∈ W and V ∈ τ }
= Cl_{BX} { w ∘ BV ∘ φ ∘ k : w ∈ W and V ∈ τ } (diagram)
= k^{∗}φ^{∗}B_{S}^{W} τ
= k^{∗}Φ(τ)

Then

⋃_{n∈ℕ}Φ′^{n}∅ = ⋃_{n∈ℕ}Φ′^{n}k^{∗}∅ = ⋃_{n∈ℕ}k^{∗}Φ^{n}∅ = k^{∗}( ⋃_{n∈ℕ}Φ^{n}∅) = k^{∗}M

We know that since h is a B^{W} coalgebra that h^{∗}B_{X}^{W} τ = Φ′(τ) ⊆ τ. Thus it follows immediately that k^{∗}M ⊆ τ.

Suppose that B : Set → Set lifts to a functor B^{W} : Set^{∗} → Set^{∗} with B^{W} defined as before.

Theorem 15. Take any coalgebra h : X → BX, and let k : X → S be the unique coalgebra morphism from h to the final B-coalgebra. Then k^{∗}M (where ⟨S, M⟩ is the carrier of the final B^{W} -coalgebra) is the least test suite τ on X such that h : ⟨X, τ⟩ → ⟨BX, B_{X}^{W} τ⟩ is a morphism in Set^{∗}.

Proof. Immediate from the proof of Theorem 14, where we showed that k^{∗}M was the least prefixpoint of Φ′(τ) = h^{∗}B_{X}^{W} τ.

From now on we shall assume a finite set of labels A and confine our attention to the endofunctor BX = P_{f}(A × X) on Set.

Assuming a ∈ A and Q ⊆ A, let w_{⟨a⟩}, w_{rQ} : B2 → 2 denote the functions

w_{⟨a⟩}X = \begin{cases}tt & if ⟨a, tt⟩ ∈ X \\ ff & otherwise, \end{cases}

w_{rQ}X = \begin{cases}tt & if ∀a ∈ Q ∀v ∈ 2 ⟨a, v⟩ ∉ X \\ ff & otherwise. \end{cases}

In particular, w_{rA}X = tt iff X = ∅.

We shall now define three subsets of maps B2 → 2:

• Tr = { w_{⟨a⟩} : a ∈ A }

• CTr = Tr ∪ {w_{rA}}

• Fl = Tr ∪ { w_{rQ} : Q ⊆ A }

The set Tr together with the closure operator Cl_{X}^{⊤}(τ) = τ ∪ {X}, determines B_{X}^{Tr} for any X and therefore determines a lifting of B to B^{Tr} : Set^{∗} → Set^{∗}.

Similarly, CTr with Cl^{⊤} and and Fl with Cl^{⊤} determine liftings B^{CTr} and B^{Fl} respectively.

The following Theorems 16, 17 and 18 show that the three liftings as defined above cause the specialisation preorders in the final B^{Tr}, B^{CTr} and B^{Fl}-coalgebras to coincide with the trace, the completed trace and the failures preorders. We use these facts to prove Theorem 19 which states that given any B-coalgebra (LTS) h : X → P_{f}(A × X), the specialisation preorder on k^{∗}M where k is the unique morphism to the final coalgebra given by finality, coincides with the operational preorder corresponding to the choice of the lifting of B.

Theorem 16. In the final B^{Tr}-coalgebra, the specialisation preorder coincides with the trace preorder.

Proof. Let φ : ⟨S, M^{Tr}⟩ → ⟨BS, B_{S}^{Tr}M^{Tr}⟩ be the final coalgebra of B^{Tr}, constructed as in Theorem 14.

Let α range over traces over the alphabet A. Let S_{α} denote the set of synchronisation trees in which α is a possible trace.

We know that M^{Tr} = ⋃_{n} Φ^{n}(∅) where Φ(τ) = φ^{∗}B_{S}^{⊤}τ. We shall show by induction that

Φ^{n}(∅) = { S_{α} : |α| < n } .

The proposition holds trivially for n = 1 as Φ(∅) = Cl^{Tr}(∅) = {S} = {S_{ϵ}} = { S_{α} : |α| < 1 }.

Now

Φ^{n+1}(∅) = φ^{∗}B_{S}^{Tr}Φ^{n}(∅)
= { w_{⟨a⟩} ∘ P_{f}(A × S_{α}) ∘ φ : a ∈ A, |α| < n } ∪ {S}

using the induction hypothesis. We need to understand the synchronisation trees which pass w_{⟨a⟩} ∘ P_{f}(A × S_{α}) ∘ φ. Unpacking the definition yields

(w_{⟨a⟩} ∘ P(A × S_{α}) ∘ φ)s = tt ⇔ ⟨a, tt⟩ ∈ (P(A × S_{α}) ∘ φ)s
⇔ ⟨a, s′⟩ ∈ φs, s′ ∈ S_{α}
⇔ s ^{a} ▶ s′, s′ ∈ S_{α}
⇔ s ∈ S_{aα}

Clearly we have { S_{α} : |α| < n + 1 } = { S_{aα} : a ∈ A and |α| < n }∪{S} and so we have established the property.

Now:

s ≤ s′ iff ∀V ∈ M (s ∈ V ⇒ s′ ∈ V)
iff ∀α (s ∈ S_{α} ⇒ s′ ∈ S_{α})
iff ∀α (s ⊧ α ⇒ s′ ⊧ α)
iff s ⊑_{Tr} s′.

Suppose that Q ⊆ A and let S_{αQ̃} denote the set of synchronisation trees which have αQ̃ as a failure.

Theorem 17. In the final B^{CTr}-coalgebra, the specialisation preorder coincides with the completed trace preorder.

Proof. We shall show by induction that for n ≥ 2

Φ^{n}(∅) = { S_{α} : |α| < n } ∪ { S_{αÃ} : |α| < n − 1 }

Indeed, we have

Φ^{2}(∅) = Φ({S})

= { w_{⟨a⟩} ∘ P_{f}(A × S) ∘ φ : a ∈ A } ∪ {S} ∪ {w_{rA} ∘ P_{f}(A × S) ∘ φ} = { S_{α} : |α| < 2 } ∪ S_{ϵÃ}

since w_{rA} ∘ P(A × S) ∘ φ = S_{ϵÃ} is the singleton set containing the (equivalence class of) synchronisation tree with one node and no transitions.

Now

Φ^{n+1}(∅) = Φ(Φ^{n}(∅))
= Φ({ S_{α} : |α| < n } ∪ { S_{αÃ} : |α| < n − 1 }) (ind. hyp.)
= { w_{⟨a⟩} ∘ P_{f}(A × S_{α}) ∘ φ : a ∈ A and |α| < n } ∪ S
∪ { w_{⟨a⟩} ∘ P_{f}(A × S_{αÃ}) ∘ φ : a ∈ A and |α| < n − 1 }
∪ { w_{rA} ∘ P_{f}(A × S_{α}) ∘ φ : |α| < n }
∪ { w_{rA} ∘ P_{f}(A × S_{αÃ}) ∘ φ : |α| < n − 1 }
= { S_{α} : |α| < n + 1 } ∪ { S_{aαÃ} : a ∈ A and |α| < n − 1 } ∪ S_{ϵÃ}
= { S_{α} : |α| < n + 1 } ∪ { S_{αÃ} : |α| < n }

It follows that:

s ≤ s′ iff ∀V ∈ M (s ∈ V ⇒ s′ ∈ V)
iff ∀α (s ∈ S_{α} ⇒ s′ ∈ S_{α}) ∧ ∀α (s ∈ S_{α,A} ⇒ s′ ∈ S_{α,A})
iff ∀α (s ⊧ α ⇒ s′ ⊧ α) ∧ ∀α (s ⊧ αÃ ⇒ s′ ⊧ αÃ)
iff s ⊑_{CTr} s′.

Theorem 18. In the final B^{Fl}-coalgebra, the specialisation preorder coincides with the failures preorder.

Proof. We shall show by induction for n ≥ 2 that

Φ^{n}(∅) = { S_{α} : |α| < n } ∪ { S_{αQ̃} : |α| < n − 1 and Q ⊆ A }

We have

Φ^{2}(∅) = Φ({S})
= { w_{⟨a⟩} ∘ P_{f}(A × S) ∘ φ : a ∈ A } ∪ {S}
∪ { w_{rQ} ∘ P_{f}(A × S) ∘ φ : a ∈ A and Q ⊆ A }
= { S_{α} : |α| < 2 } ∪ { S_{ϵQ̃} : Q ⊆ A }

Now,

Φ^{n+1}(∅) = Φ(Φ^{n}(∅))
= Φ({ S_{α} : |α| < n } ∪ { S_{αQ̃} : |α| < n − 1 and Q ⊆ A })
= { w_{⟨a⟩} ∘ P_{f}(A × S_{α}) ∘ φ : a ∈ A and |α| < n } ∪ S
∪ { w_{⟨a⟩} ∘ P_{f}(A × S_{αQ̃}) ∘ φ : a ∈ A, |α| < n − 1 and Q ⊆ A }
∪ { w_{rQ} ∘ P_{f}(A × S_{α}) ∘ φ : |α| < n and Q ⊆ A }
∪ { w_{rQ} ∘ P_{f}(A × S_{αQ̃′}) ∘ φ : |α| < n − 1 and Q, Q′ ⊆ A }
= { S_{α} : |α| < n + 1 }
∪ { S_{aαQ̃} : a ∈ A, |α| < n − 1 and Q ⊆ A } ∪ { S_{ϵQ̃} : Q ⊆ A }
= { S_{α} : |α| < n + 1 } ∪ { S_{αQ̃} : |α| < n and Q ⊆ A }

Noticing that S_{α} = S_{α˜∅} we can write

M^{Fl} = ⋃_{n} Φ^{n}(∅) = ⋃_{n} { S_{αQ̃} : |α| < n and Q ⊆ A. }

It is easy to see that:

s ≤ s′ iff ∀V ∈ M (s ∈ V ⇒ s′ ∈ V)
iff ∀α, Q ⊆ A (s ∈ S_{αQ̃} ⇒ s′ ∈ S_{αQ̃})
iff ∀α, Q ⊆ A (s ⊧ αQ̃ ⇒ s′ ⊧ αQ̃)
iff s ⊑_{Fl} s′.

Theorem 19. Suppose that h : X → P(A × X) is a coalgebra (LTS), φ : S → BS is the final B-coalgebra and that k : X → S is the unique morphism given by finality. Then x ≤ x′ according to the specialisation preorder of • k^{∗}(M^{Tr}) iff x ⊑_{Tr} x′

• k^{∗}(M^{CTr}) iff x ⊑_{CTr} x′

• k^{∗}(M^{Fl}) iff x ⊑_{Fl} x′.

Proof. We shall prove the first item, the other two are similar. We have

x ≤ x′ ⇔ ∀V ∈ M^{Tr} (x ∈ h^{∗}V ⇒ x′ ∈ h^{∗}V)
⇔ ∀V ∈ M^{Tr} (hx ∈ V ⇒ hx′ ∈ V)
⇔ kx ⊑_{Tr} kx′  (Theorem 16)
⇔ x ⊑_{Tr} x′

where the last step follows from the fact that k is a coalgebra morphism and therefore { ⟨x, kx⟩ : x ∈ X } is a bisimulation [24].

6 Application: Congruence Formats from Bialgebras

To lift the bialgebraic framework to the total category Set^{∗}, we need a way to lift the syntactic and the behaviour functors together with the natural transformation λ. Various ways to lift the behaviour B were shown in the previous section, now we proceed to show a lifting of the syntactic functor.

Given a syntactic endofunctor Σ on Set:

ΣX = ∐_{i=1}^{k} X^{n_{i}}

define an endofunctor Σ^{∗} on Set^{∗}: Σ^{∗} ⟨X, τ⟩ = ⟨ΣX, Σ_{X}τ⟩, where

Σ_{X}τ = Cl^{∪} ( ⨁_{i=1}^{k} τ^{⊗n_{i}})

where Cl^{∪} is the closure under arbitrary unions, and we write τ^{⊗n_{i}} for \underbrace{τ ⊗ τ ⊗ ⋯ ⊗ τ}_{n_{i} times}. On arrows, given f : ⟨X, τ⟩ → ⟨X′, τ′⟩, we define simply

Σ^{∗}f = Σf. Preservation of identities and composition follows from the fact that Σ is a functor. It suffices to show that Σf is a morphism in Set^{∗}, and indeed

(Σf)^{∗}Σ_{X′}τ′ = (Σf)^{∗} Cl^{∪} ( ⨁_{i=1}^{k} τ′^{⊗n_{i}})

= Cl^{∪}(Σf)^{∗}( ⨁_{i=1}^{k} τ′^{⊗n_{i}})

= Cl^{∪} ( ⨁_{i=1}^{k} (f^{∗}τ′)^{⊗n_{i}})

⊆ Cl^{∪} ( ⨁_{i=1}^{k} τ^{⊗n_{i}}) (since f^{∗}τ′ ⊆ τ)

= Σ_{X}τ

Theorem 20. Suppose that an endofunctor F lifts to a endofunctor F^{∗}, and has an initial algebra ψ : F N → N. Then ψ : ⟨F N, F_{N}P ⟩ → ⟨N, P ⟩ is the initial F^{∗} algebra where P is the greatest fixpoint of the operator Ψ(τ) = (ψ^{−1})^{∗}F_{N}τ.

Proof. First, by definition ψ^{∗}P = ψ^{∗}(ψ^{−1})^{∗}F_{N}P = F_{N}P and therefore ψ is a morphism in the total category.

Suppose that h : ⟨F X, F_{X}τ⟩ → ⟨X, τ⟩ is any F^{∗}-algebra. Then h^{∗}τ ⊆ F_{X}τ and h : F X → X is an F -algebra, and we have a unique k : N → X such that h ∘ F k = k ∘ ψ:

\xymatrix{F N \ar[r]^{F k} \ar[d]_{ψ} & F X \ar[d]^{h} \\ N \ar[r]_{k} & X}

It remains to verify that k is a morphism in the total category, i.e., that k^{∗}τ ⊆ P. This is done by proving that k^{∗}τ is a postfixpoint of Ψ:

Ψ(k^{∗}τ) = (ψ^{−1})^{∗}F_{N}(k^{∗}τ)
⊇ (ψ^{−1})^{∗}(F k)^{∗}(F_{X}(τ))  (functoriality of F)
⊇ (ψ^{−1})^{∗}(F k)^{∗}h^{∗}τ
= k^{∗}τ

P, as the greatest fixpoint of Ψ, is also the greatest postfixpoint of Ψ, hence k^{∗}τ ⊆ P.

Corollary 21. For any syntactic endofunctor Σ, the functor Σ^{∗} freely generates a monad T^{∗} that lifts the monad T freely generated by Σ.

Proof. By definition, T^{∗} ⟨X, τ⟩ is the carrier of the initial (⟨X, τ⟩+Σ^{∗}−)- algebra. Since Σ^{∗} lifts Σ, by Theorem 20 we know that this initial algebra exists, and it is of the form T^{∗} ⟨X, τ⟩ = ⟨T X, T_{X}τ⟩, where ψ : X + ΣT X → T X is the initial (X + Σ−)-algebra, and T_{X}τ is the greatest fix point of the operator

Ψτ′ = (ψ^{−1})^{∗}(τ ⊕ Σ_{T X}τ′)

A similar corollary about a behaviour B^{W} cofreely generating a comonad D^{W} can be drawn from Theorem 14. These two corollaries allow us to apply Theorem 10 for the category Set^{∗} and endofunctors Σ^{∗} and B^{W}.

The following theorem is a crucial property of the endofunctor Σ^{∗}. Indeed, varying the definition of Σ^{∗} in our framework would lead to definition of various precongruence formats, but only as long as the following property holds.

Theorem 22. For any Σ^{∗}-algebra h : ⟨ΣX, Σ_{X}τ⟩ → ⟨X, τ⟩, the specialisation preorder ≤_{τ} is a precongruence on h : ΣX → X.

Proof. Take f : X^{n} → ΣX to be one of the coproduct injections to ΣX, and consider elements x_{1}, y_{1}, …, x_{n}, y_{n} of X such that x_{i} ≤_{τ} y_{i} for i = 1..n. This means that

⟨x_{1}, …, x_{n}⟩ ≤_{τ^{⊗n}} ⟨y_{1}, …, y_{n}⟩

Observe that the closure operator Cl^{∪} does not change specialisation preorders: for any test suite τ, we have ≤_{Cl^{∪} τ}=≤_{τ}. Hence

f ⟨x_{1}, …, x_{n}⟩ ≤_{Σ_{X}τ} f ⟨y_{1}, …, y_{n}⟩

Now since h is a morphism in the total category, we know that h^{∗}τ ⊆ Σ_{X}τ, hence

f ⟨x_{1}, …, x_{n}⟩ ≤_{h^{∗}τ} f ⟨y_{1}, …, y_{n}⟩

and

h(f ⟨x_{1}, …, x_{n}⟩) ≤_{τ} h(f ⟨y_{1}, …, y_{n}⟩)

We now have the technology needed to prove the main result of this section.

Consider a natural transformation λ : Σ(id ×B) → BT. By Theorem 10, the coalgebraic part of the initial λ-model has N = T ∅ as its carrier, and it is the intended operational model of λ. If B = P_{f}(A × −), then the intended operational model is the LTS generated by GSOS rules associated to λ. Let k : N → S be the final coalgebra morphism from the intended operational model to the final B-coalgebra. Assume B lifts to some B^{∗} as before, and let ⟨S, M⟩ be the carrier of the initial B^{∗}- coalgebra.

Theorem 23. If λ lifts to a natural transformation in the total category:

λ : Σ^{∗}(id ×B^{∗}) → B^{∗}T^{∗}.

then the specialisation preorder on k^{∗}M is a precongruence on N.

Proof. By Theorem 10, there exists an initial λ-model (in Set^{∗})

Σ^{∗} ⟨N, P ⟩ ⟶^{ψ} ⟨N, P ⟩ ⟶^{ϵ} B^{∗} ⟨N, P ⟩

and a final λ-model (in Set^{∗})

Σ^{∗} ⟨S, M⟩ ⟶^{δ} ⟨S, M⟩ ⟶^{φ} B^{∗} ⟨S, M⟩

where ψ : Σ^{∗} ⟨N, P ⟩ → ⟨N, P ⟩ and φ : ⟨S, M⟩ → B^{∗} ⟨S, M⟩ are respectively the initial Σ^{∗}-algebra and the final B^{∗}-coalgebra. By initiality (or finality) there exists a unique morphism k : ⟨N, P ⟩ → ⟨S, M⟩ of λ-models so that (i) below is commutative.

\xymatrix{Σ^{∗} ⟨N, P ⟩ \ar[d]_{ψ} \ar[rr]^{Σ^{∗}k} &  & Σ^{∗} ⟨S, M⟩ \ar[d]^{δ} & Σ^{∗} ⟨N, k^{∗}M⟩ \ar[d]_{ψ} \ar[rr]^{Σ^{∗}k} &  & Σ^{∗} ⟨S, M⟩ \ar[d]^{δ} \\ _{⟨N, P ⟩} \ar[d]_{ϵ} \ar[rr]^{k} &  & _{⟨S, M⟩} \ar[d]^{φ} & _{⟨N, k^{∗}M⟩} \ar[d]_{ϵ} \ar[rr]^{k} &  & _{⟨S, M⟩} \ar[d]^{φ} \\ B^{∗} ⟨N, P ⟩ \ar[rr]_{B^{∗}k} &  & B^{∗} ⟨S, M⟩ & B^{∗} ⟨N, k^{∗}M⟩ \ar[rr]_{B^{∗}k} &  & B^{∗} ⟨S, M⟩ \\  & (i) &  &  & (ii)}

Our goal is to show that (ii) above a diagram in Set^{∗}. If all the morphisms are defined then its commutativity follows from the commutativity of (i). By Theorem 15, ϵ : ⟨N, k^{∗}M⟩ → B^{∗} ⟨N, k^{∗}M⟩ is a B^{∗}- coalgebra.

Now

ψ^{∗}k^{∗}M = (Σ^{∗}k)^{∗}δ^{∗}M
= (Σk)^{∗}δ^{∗}M
⊆ (Σk)^{∗}(Σ_{S}M) (since δ is in Set^{∗})
⊆ Σ_{X}(k^{∗}M) (since Σ^{∗} is a functor)

Thus ψ : ⟨N, k^{∗}M⟩ → B^{∗} ⟨N, k^{∗}M⟩ is a Σ^{∗}-algebra and by Theorem 22 the specialisation preorder of k^{∗}M is a precongruence.

7 Precongruence Formats for (almost) Free

In this section we consider a syntactic endofunctor Σ with a freely generated monad T, the behaviour functor BX = P_{f}(A × X), and a set R of GSOS rules with the corresponding natural transformation

λ : Σ(id ×B) → BT

The purpose is to describe syntactic conditions on R that would ensure that λ lifts to a natural transformation

λ : Σ^{∗}(id ×B^{W}) → B^{W} T^{∗}

where W ∈ {Tr, CTr, Fl}. As a consequence of Theorem 23, such syntactic conditions ensure that the respective operational preorders are precongruences.

Theorem 24. If R is in Tr-format (Format 2), then

λ : Σ^{∗}(Id × B^{Tr}) → B^{Tr}T^{∗}

is a natural transformation in Set^{∗}.

Proof. It is enough to ensure that given an object ⟨X, τ⟩ in Set^{∗},

λ : Σ^{∗}(⟨X, τ⟩ × B^{Tr} ⟨X, τ⟩) → B^{Tr}T^{∗} ⟨X, τ⟩

is a morphism in Set^{∗}; in other words, that for every test V ∈ B_{T X}^{Tr}T_{X}τ, λ^{−1}V is a test in Σ_{X×BX}(τ ⋈ B_{X}^{Tr}τ).

To do this, it will be useful to understand the nature of tests in Σ_{X}τ, T_{X}τ and B_{T X}^{Tr}T_{X}τ, for a given ⟨X, τ⟩.

Definition 25. For a syntactic Σ, a set X and a test suite τ on X, a basic flat τ-check on ΣX is a term

γ ∈ Στ

A term t ∈ ΣX passes a basic flat τ-check γ, if t can be obtained from γ by replacing every V ∈ τ by some x ∈ V.

The set of terms passing a given basic flat τ-check γ is denoted υ(γ). Sets of this kind will be called basic flat τ-tests on ΣX.

Lemma 26. For any Σ, ⟨X, τ⟩, tests from Σ_{X}τ are exactly all unions of basic flat τ-tests on ΣX.

Proof. Take any test

V ∈ ⨁_{i=1}^{k} τ^{⊗n_{i}}

By definition, V = V_{1} + ⋯ + V_{k}, where V_{i} ∈ τ^{⊗n_{i}}. Then for every 1 ≤ i ≤ k,

V_{i} = U_{1} × ⋯ × U_{n_{i}} where U_{j} ∈ τ

(in the above, + and × denote disjoint union and cartesian product on sets). Note that γ = ι_{i} ⟨U_{1}, …, U_{n_{i}}⟩ is a basic flat τ-check, and

ι_{i}(V_{i}) = υ(γ)

where ι_{i} : X^{n_{i}} → ΣX is the i-th coproduct injection into ΣX. Finally

V = V_{1} + V_{2} ⋯ + V_{k} = ι_{1}(V_{1}) ∪ ι_{2}(V_{2}) ∪ ⋯ ∪ ι_{k}(V_{k})

which completes the presentation of V as a union of basic flat τ-tests.

Definition 27. For a set X and a test suite τ on X, a basic term τ-check is a term

c ∈ T τ

A term t ∈ T X passes a basic term τ-check c, if t can be obtained from c by replacing every V ∈ τ by some x ∈ V.

The set of terms passing a given basic term τ-check c is denoted υ(c). Sets of this kind will be called basic term τ-tests on T X.

Lemma 28. For any Σ, ⟨X, τ⟩, every test in T_{X}τ is a union of basic term τ-tests on T X.

Proof. Recall from Corollary ?? that T_{X}τ is the greatest fix point of the operator Ψ:

Ψτ′ = (ψ^{−1})^{∗}(τ ⊕ Σ_{T X}τ′)

The proof proceeds by constructing for all n and for any test V ∈ Ψ^{n}(PT X), a family Γ_{n}(V) of basic term τ-checks from T_{n}τ such that

V ∩ T_{n}X = ⋃_{γ∈Γ_{n}(V)} υ(γ)

where T_{n}X denotes the set of Σ-terms of depth at most n.

Given this construction, for any test V ∈ T_{X}τ we have

V = ⋃_{n∈N} ⋃_{γ∈Γ_{n}(V)} υ(γ)

which will complete the proof.

The families Γ_{n}(V) are constructed by induction on n. For the base case, take Γ_{0}(V) = ∅ for any V. Indeed,

V ∩ T_{0}X = V ∩ ∅ = ⋃_{γ∈∅} υ(γ)

For the induction step, take a test V ∈ Ψ^{n}(PT X). By definition, V = V′ + V′′ (+ denotes disjoint union of sets), where V′ ∈ τ, and V′′ ∈ Σ_{T X}Ψ^{n−1}(PT X). By Lemma 26, for some indexing set I

V′′ = ⋃_{i∈I} υ(δ_{i})

where each δ_{i} is a basic flat Ψ^{n−1}(PT X)-check on ΣT X, i.e.

δ_{i} ∈ Σ(Ψ^{n−1}(PT X))

By the inductive assumption, for every test U ∈ Ψ^{n−1}(PT X) there exist a family Γ_{n−1}(U) of basic term τ-checks such that

U ∩ T_{n−1}X = ⋃_{u∈Γ_{n−1}(U)} υ(u)

Now for any δ_{i} as above, take δ′_{i} = δ_{i}[σ], where

σ(U) = ⋃_{u∈Γ_{n−1}(U)} υ(u)

is a substitution from Ψ^{n−1}(PT X) to PT X. Obviously, each δ′_{i} is a basic flat (PT X)-check and

\begin{matrix}υ(δ′_{i}) = υ(δ_{i}) ∩ ΣT_{n−1}X \\ ι_{2}(υ(δ′_{i})) = ι_{2}(υ(δ_{i})) ∩ T_{n}X \end{matrix}

where ι_{2} : ΣT X → T X is the coproduct inclusion.

Moreover, for any δ_{i} as above, consider the family of basic term τ-checks:

Θ(δ_{i}) = { ι_{2}(δ_{i}[σ′]) : σ′(U) ∈ Γ_{n−1}(U) } ⊆ T_{n}τ

where ι_{2} : ΣT_{n−1}τ → T_{n}τ is the coproduct inclusion, and σ′ ranges on substitutions from Ψ^{n−1}(PT X) to T_{n−1}τ.

From definition of υ, it is easy to see that

⋃_{γ∈Θ(δ_{i})} υ(γ) = ι_{2}(υ(δ′_{i}))

Now take

Γ_{n}(V) = {ι_{1}(V′)} ∪ ⋃_{i∈I} Θ(γ_{i})

and check that

V ∩ T_{n}X = (V′ + V′′) ∩ T_{n}X

= (ι_{1}(V′) ∪ ι_{2}(V′′)) ∩ T_{n}X

= (ι_{1}(V′) ∩ T_{n}X) ∪ (ι_{2}(V′′) ∩ T_{n}X)

= ι_{1}(V′) ∪ ( ⋃_{i∈I} ι_{2}(υ(δ_{i})) ∩ T_{n}X)

= υ(ι_{1}(V′)) ∪ ( ⋃_{i∈I} ι_{2}(υ(γ′_{i})))

= υ(ι_{1}(V′)) ∪ ( ⋃_{i∈I} ⋃_{γ∈Θ(δ_{i})} υ(γ))

This completes the induction step, and the proof of Lemma 28.

Definition 29. For a given ⟨X, τ⟩, a basic positive τ-check on BX is an expression of the form ^{a} ▶ V, where a ∈ A and V ∈ τ. A set β ∈ BX passes such a check, if there is some ⟨a, x⟩ ∈ β such that x ∈ V. As usual, the test on BX associated to a basic positive τ-check c is denoted υ(c) and is called a basic positive τ-test.

Similarly, for a given ⟨X, τ⟩, a basic positive term τ-check on BT X is an expression of the form ^{a} ▶ γ, where a ∈ A and γ is a basic term τ-test on T X. The definition of passing and of the basic positive term τ-test υ( ^{a} ▶ γ) is as usual.

Lemma 30. A test in B_{T X}^{Tr}T_{X}τ is either the always true test BT X, or a union of basic positive term τ-tests.

Proof. If a test V ∈ B_{T X}^{Tr}T_{X}τ is not equal to BT X, then

V = w_{⟨a⟩} ∘ BV′ = { β ∈ BT X : ⟨a, t⟩ ∈ β, t ∈ V′ }

for some V′ ∈ T_{X}τ. But then, by Lemma 28, V′ is a union of basic term τ-tests:

V′ = ⋃_{i∈I} υ(γ_{i})

hence

V = ⋃_{i∈I} { β ∈ BT X : ⟨a, t⟩ ∈ β, t ∈ υ(γ_{i}) } = ⋃_{i∈I} υ( ^{a} ▶ γ_{i})

We shall now prove Theorem 24. By Lemma 30, it is enough to show that for any ⟨X, τ⟩, and for any given basic positive term τ-check ^{a} ▶ γ, there exists a family of basic flat (τ ⋈ B_{X}^{Tr}τ)-checks δ_{1}, δ_{2}, …, δ_{m} such that

λ^{−1}υ( ^{a} ▶ γ) = ⋃_{i=1}^{m} υ(δ_{i})

To achieve this, fix a basic positive term τ-check ^{a} ▶ γ, and take any rule ρ ∈ R, which has the conclusion of the form

f(x_{1}, … x_{n}) ^{a} ▶ t

for some construct f with arity n, and such that t can be obtained from γ by replacing each V ∈ τ with some x ∈ Ξ. Since no variable occurs in t more than once, this gives a function σ : Ξ → τ such that γ = t[σ]. Without loss of generality, assume that σ(x) = X if x does not occur in

t.

Now for each 1 ≤ i ≤ n take a test V_{i} ∈ τ ⋈ B_{X}τ as follows:

• If x_{i} does not occur in any premise of ρ, then take V_{i} = σ(x_{i})×BX.

• If x_{i} occurs in a premise x_{i} ^{b_{i}} ▶ y_{i}, then take V_{i} = X×υ( ^{b_{i}} ▶ σ(y_{i}))

Note that the syntactic restrictions of the Tr-format ensure that the above definition is complete and unambiguous.

Having defined the tests V_{i}, consider a basic flat τ ⋈ B_{X}τ-check

δ_{ρ} = f ⟨V_{1}, …, V_{n}⟩

We will show that υ(δ_{ρ}) = ρ_{X}^{−1}υ( ^{a} ▶ γ). To this end, take any

r = f ⟨⟨x_{1}, β_{1}⟩ , …, ⟨x_{n}, β_{n}⟩⟩ ∈ Σ(X × BX)

and check that the following are equivalent:

r passes δ_{ρ}

⟺ ⟨x_{i}, β_{i}⟩ ∈ V_{i} for all 1 ≤ i ≤ n

⟺ For each 1 ≤ i ≤ n, either x_{i} does not occur in any premise and x_{i} ∈ σ(x_{i}), or x_{i} occurs in a premise x_{i} ^{b_{i}} ▶ y_{i} and ⟨b_{i}, y_{i}⟩ ∈ β_{i} for

some y_{i} ∈ σ(y_{i})

⟺ θ mapping each x_{i} to x_{i}, and y_{i} to y_{i} satisfies the conditions described in the proof of Theorem 9. Moreover, θ(x) ∈ σ(x) for all x ∈ Ξ.

⟺ ⟨a, t[θ]⟩ ∈ ρ_{X}r, and t[θ] passes γ.

⟺ ρ_{X}r passes ^{a} ▶ γ.

This shows that υ(δ_{ρ}) = ρ_{X}^{−1}υ( ^{a} ▶ γ).

Now by definition of λ from the family of ρ_{X} for ρ ∈ R,

λ^{−1}(υ( ^{a} ▶ γ)) = ⋃_{ρ} υ(ρ_{X})

where the summation is made over all rules ρ with the conclusion as described above.

This completes the proof of Theorem 24.

Theorem 31. If R is in CTr-format, then

λ : Σ^{∗}(Id × B^{CTr}) → B^{CTr}T^{∗}

is a natural transformation in Set^{∗}.

Proof. As before, we show that for any ⟨X, τ⟩, for every test V ∈ B_{T X}^{CTr}T_{X} there is a test V′ ∈ Σ_{X}(τ ⋈ B_{X}^{CTr}τ) such that λ^{−1}V = V′.

Definition 32. For a set of labels Q ⊆ A, the Q-failure check is denoted Q ▶̸. Instead of ^{A} ▶̸, we will sometimes write ▶̸. For any set X, a set β ∈ BX passes the Q-failure check if

β ∩ { ⟨a, t⟩ : a ∈ Q } = ∅

For any X, the test on BX associated to the Q-failure check will be denoted υ(^{Q} ▶̸), and will be called the Q-failure test.

Lemma 33. A test V ∈ B_{T X}^{CTr}T_{X} is either the always true test BT X, or the A-failure test υ( ▶̸), or a union of basic positive term τ-tests.

Proof. If a test V ∈ B_{T X}^{CTr}T_{X}τ is not equal to BT X, then either V = w_{⟨a⟩} ∘ BV′ for some V′ ∈ T_{X}τ, or V = w_{rA} ∘ BV′ for some V′ ∈ T_{X}τ. In the former case, V is a union of basic positive term τ-tests, as shown in Lemma 30. In the latter case,

w_{rA} ∘ BV′ = {∅} = υ( ▶̸)

To prove Theorem 31, it is enough to consider single basic positive term τ-tests on BT X, and the A-failure test on BT X. For the positive tests, we proceed as in the proof of Theorem 24, except that when constructing the tests V_{i} we consider one additional case:

• If x_{i} occurs in ρ in a negative premise x_{i} ^{a} ▶̸ (and hence, it occurs in a premise x_{i} ^{b} ▶̸ for any b ∈ A), then take V_{i} = X × υ( ▶̸).

The syntactic restrictions of CTr-format ensure that the definition of V_{i}’s extended this way is complete and unambiguous.

The rest of the argument remains as in the case of Tr-format.

For the A-failure test υ( ▶̸) on BT X, for any language construct f(x_{1}, …, x_{n}) take a sequence of CTr-testing sets P_{1}, …, P_{k_{m}} that satisfy the condition described in the definition of CTr-format. For each P_{i} and each variable x_{j}, define a test V_{ij} ∈ τ ⋈ B_{X}^{CTr}τ as follows:

• If, for some a ∈ A, both x_{j} ^{a} ▶ and x_{j} ^{a} ▶̸ belong to P_{i}, then take V_{ij} = ∅.

• If, for all a ∈ A, x_{j} ^{a} ▶ ∈ P_{i}, and if for all b ∈ A, x_{j} ^{b} ▶̸ ∉ P_{i}, then take V_{ij} = X × υ( ▶̸).

• If, for all a ∈ A, x_{j} ^{a} ▶ ∉ P_{i}, and if for some b ∈ A, x_{j} ^{b} ▶̸ ∈ P_{i}, then take V_{ij} = X × υ( ^{b} ▶ X).

Note that the definition of a CTr-testing set ensures that the above definition is complete and unambiguous.

Now for any P_{i} consider the basic flat τ ⋈ B_{X}^{CTr}τ-check

δ_{fi} = f ⟨V_{i1}, …, V_{in}⟩

Recall the definition of the function f_{X} in the proof of Theorem 9. We will now show that

⋃_{i=1}^{k_{f}} υ(d_{fi}) = f_{X}^{−1}υ( ▶̸)

To this end, consider any r ∈ Σ(X × BS) of the form

r = ι_{m} ⟨⟨x_{1}, β_{1}⟩ , …, ⟨x_{n}, β_{n}⟩⟩

and assume that f_{X}r does not pass ▶̸, i.e., that f_{X}r ≠ ∅. This means that there exists a rule ρ ∈ R with source f(x_{1}, …, x_{n}), and a substitution σ : Ξ → X such that

σx_{i} = x_{i}
∀i ≤ n∀j ≤ m_{i}. ⟨a_{ij}, σ(y_{ij})⟩ ∈ β_{i}
∀i ≤ n∀j ≤ n_{i}∀x ∈ X. ⟨b_{ij}, x⟩ ∉ β_{i}

where m_{i}, n_{i}, a_{ij}, b_{ij}, y_{ij} are taken from ρ.

By the first part of condition 2 of CTr-format, there exists a sequence p_{1}, …, p_{k_{f}} such that p_{i} ∈ P_{i} and each p_{i} is completed by some premise of ρ. Take any 1 ≤ i ≤ k_{f}. In ρ there is a premise that completes p_{i}. If p_{i} is a positive semiliteral x_{j} ^{c} ▶ (for some x_{j}, c), then β_{j} ≠ ∅, hence ⟨x_{j}, β_{j}⟩ ∉ V_{ij} and r does not pass d_{fi}. Similarly, if p_{i} is a negative semiliteral x_{j} ^{c} ▶̸, then β_{j} = ∅ and again ⟨x_{j}, β_{j}⟩ ∉ V_{ij} and r does not pass d_{fi}.

Conversely, assume that r does not pass d_{fi} for any 1 ≤ i ≤ k_{f}. This means that for each i, there is a j such that ⟨x_{j}, β_{j}⟩ ∉ V_{ij}. For each 1 ≤ i ≤ k_{f}, take p_{i} to be any element of P_{i} that has the respective x_{j} on the left-hand side. By the second part of condition 2 of CTr-format, there exists a rule ρ ∈ R with source f(x_{1}, …, x_{n}), such that each premise of ρ completes some p_{i}. This means that there exists a substitution σ : Ξ → X satisfying all the conditions mentioned above, hence f_{X}r ≠ ∅ and f_{X}r does not pass ▶̸.

From this, by definition of λ as in the proof of Theorem 9,

⋃_{f∈Σ} ⋃_{i=1}^{k_{f}} υ(d_{fi}) = λ^{−1}υ( ▶̸)

This completes the proof of Theorem 31.

Theorem 34. If R is in Fl-format, then

λ : Σ^{∗}(Id × B^{Fl}) → B^{Fl}T^{∗}

is a natural transformation in Set^{∗}.

Proof. As before, we show that for any ⟨X, τ⟩, for every test V ∈ B_{T X}^{Fl}T_{X} there is a test V′ ∈ Σ_{X}(τ ⋈ B_{X}^{Fl}τ) such that λ^{−1}V = V′.

As before, we begin with a characterisation of tests in B_{T X}^{Fl}T_{X}:

Lemma 35. A test V ∈ B_{T X}^{Fl}T_{X} is either the always true test BT X, or the Q-failure test υ( ▶̸) for some Q ⊆ A, or a union of basic positive term τ-tests.

Proof. As in the proof of Lemma 33.

The proof proceeds much the same as in Theorem 31. For the positive tests V, we proceed as in the proof of Theorem 24, except that when constructing the tests V_{i} we consider one additional case:

• If x_{i} occurs in ρ in some negative premises, then take V_{i} = X × υ(^{Q_{i}} ▶̸), where Q_{i} = { a ∈ A : x_{i} ^{a} ▶̸ is a premise in ρ }.

Again, the syntactic restrictions of Fl-format ensure that the definition of V_{i}’s extended this way is complete and unambiguous.

The rest of the argument remains as in the case of Tr-format.

For the Q-failure test υ(^{Q} ▶̸) for some Q ⊆ A, we proceed as in the proof of Theorem 31, except that we construct the tests V_{ij} in a slightly different manner:

• If, for some a ∈ A, both x_{j} ^{a} ▶ and x_{j} ^{a} ▶̸ belong to P_{i}, then take V_{ij} = ∅.

• If for some a ∈ A, x_{j} ^{a} ▶ ∈ P_{i}, and if for all b ∈ A, x_{j} ^{b} ▶̸ ∉ P_{i}, then take V_{ij} = X ×υ(^{Q_{j}} ▶̸), where Q_{j} = { a ∈ A : x_{j} ^{a} ▶ ∈ P_{i} }.

• If, for all a ∈ A, x_{j} ^{a} ▶ ∉ P_{i}, and if for some b ∈ A, x_{j} ^{b} ▶̸ ∈ P_{i}, then take V_{ij} = X × υ( ^{b} ▶ X).

(note that the first and the third case are as in the case of CTr-format).

Note that the definition of a Fl-testing set ensures that the above definition is complete and unambiguous.

The rest of the argument remains the same as in the case of CTr-format.

8 Conclusions

We have presented an abstract coalgebraic approach to the description of various operational preorders, via a fibration of test suites. In Theorems 16, 17 and 18 we illustrated this approach on the trace preorder, the completed trace preorder and the failures preorder. Combined with bialgebraic methods, this framework allows the derivation of syntactic subformats of GSOS which guarantee that the aforementioned operational preorders are precongruences. Theorem 23 is a guideline in the search for such formats, and Theorems 24, 31 and 34 are applications of the framework.

The generality and abstractness of Theorem 23 prompted us to coin the expression ‘precongruence format for free’. However, it must be stressed that to derive a syntactic format for a given operational preorder remains a non-trivial task. Indeed, the proofs of Theorems 24, 31 and 34 are quite long and technical. The expression ‘for free’ reflects the fact that Theorem 23 lets us prove precongruence properties without considering the global behaviour (e.g. traces) of processes. Instead, one considers only simple tests on processes, corresponding intuitively to single modalities.

Related abstract approaches to operational preorders and equivalences include those based on modal characterisations [10] and quantales [1]. In the latter framework, no syntactic issues have been addressed. In the former, some general precongruence formats have been obtained by attempting to decompose modal formulae according to given operational rules [7]. This technique bears some resemblance to our approach, and the precise connections have to be investigated.

There are several possible directions of future work. Firstly, the approach presented here can be extended to deal with other operational preorders and equivalences described in literature. Secondly, one can move from the GSOS format (and its subformats) to the more general (safe) ntree format [9], which can also be formalised in the bialgebraic framework [30]. Thirdly, the abstract framework of test suites seems to be general enough to cover other notions of process behaviour (e.g. involving store), or even other underlying categories (e.g. complete partial orders instead of sets). It may prove interesting to formalise various operational preorders in such cases and to find precongruence formats for them.

References

[1] S. Abramsky and S. Vickers. Quantales, observational logic and process semantics. Math. Struct. in Comp. Sci., 3:161–227, 1993.

[2] L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra. Elsevier, 1999.

[3] P. Aczel and N. Mendler. A final coalgebra theorem. In D. H. Pitt et al., editors, Proc. CTCS’89, volume 389 of LNCS, pages 357–365, 1989.

[4] M. Barr. Terminal coalgebras in well-founded set theory. Theoretical Computer Science, 114:299–315, 1993.

[5] B. Bloom. When is partial trace equivalence adequate? Formal Aspects of Computing, 6:25–68, 1994.

[6] B. Bloom, W. Fokkink, and R. J. van Glabbeek. Precongruence formats for decorated trace preorders. In Logic in Computer Science, pages 107– 118, 2000.

[7] B. Bloom, W.J Fokkink, and R.J van Glabbeek. Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic. To appear.

[8] B. Bloom, S. Istrail, and A. Meyer. Bisimulation can’t be traced. Journal of the ACM, 42:232–268, 1995.

[9] W. Fokkink and R. van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126:1–10, 1996.

[10] R. J. van Glabbeek. The linear time-branching time spectrum I. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra. Elsevier, 1999.

[11] J. F. Groote. Transition system specifications with negative premises. Theoret. Comput. Sci., 118:263–299, 1993.

[12] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137–161, 1985.

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

[14] B. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. North Holland, Elsevier, 1999.

[15] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996.

[16] S. Mac Lane. Categories for the Working Matematician. Springer-Verlag, second edition, 1998.

[17] J. Leifer and R. Milner. Deriving bisimulation congruences for reactive systems. In Int. Conf. on Concurrency Theory, CONCUR 00, Lecture Notes in Computer Science, pages 243–258. Springer Verlag, 2000.

[18] R. Milner and D. Sangiorgi. Barbed bisimulation. In Proceedings of ICALP 92’: Automata, Languages and Programming, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

[19] D. M. Park. Concurrency on automata and infinite sequences. In P. Deussen, editor, Conf. on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science. Springer Verlag, 1981.

[20] G. Plotkin. Bialgebraic semantics (and recursion). Unpublished notes.

[21] G. Plotkin. A structural approach to operational semantics. DAIMI Report FN-19, Computer Science Department, Aarhus University, 1981.

[22] G. Plotkin. Bialgebraic semantics and recursion (extended abstract). In A. Corradini, M. Lenisa, and U. Montanari, editors, Electronic Notes in Theoretical Computer Science, volume 44. Elsevier Science Publishers, 2001.

[23] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997.

[24] J. Rutten and D. Turi. Initial algebra and final coalgebra semantics for concurrency. In J. de Bakker et al., editors, Proc. of the REX workshop A Decade of Concurrency – Reflections and Perspectives, volume 803 of LNCS, pages 530–582. Springer-Verlag, 1994.

[25] V. Sassone and P. Sobociński. Deriving bisimulation congruences: A 2categorical approach. Electronic Notes in Theoretical Computer Science, 68(2), 2002.

[26] P. Sewell. From rewrite rules to bisimulation congruences. Lecture Notes in Computer Science, 1466:269–284, 1998.

[27] R. de Simone. Higher-level synchronising devices in Meije-SCCS. Theoret. Comput. Sci., 37:245–267, 1985.

[28] D. Turi. Fibrations and bisimulation. Unpublished notes.

[29] D. Turi. Functorial Operational Semantics and its Denotational Dual. PhD thesis, Vrije Universiteit, Amsterdam, 1996.

[30] D. Turi and G. Plotkin. Towards a mathematical operational semantics. In Proceedings 12th Ann. IEEE Symp. on Logic in Computer Science, LICS’97, Warsaw, Poland, 29 June – 2 July 1997, pages 280–291. IEEE Computer Society Press, 1997.

[31] Frits W. Vaandrager. On the relationship between process algebra and input/output automata. In Logic in Computer Science, pages 387–398, 1991.

Recent BRICS Report Series Publications

RS-03-18 Bartek Klin and Pawe� Sobociński. Syntactic Formats for Free: An Abstract Approach to Process Equivalence. April 2003. 41 pp.

RS-03-17 Luca Aceto, Jens Alsted Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. The Complexity of Checking Consistency of Pedigree Information and Related Problems. 2003.

RS-03-16 Ivan B. Damgård and Mads J. Jurik. A Length-Flexible Threshold Cryptosystem with Applications. March 2003. 19 pp.

RS-03-15 Anna Ingólfsdóttir. A Semantic Theory for Value–Passing Processes Based on the Late Approach. March 2003. 49 pp.

RS-03-14 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From Interpreter to Compiler and Virtual Machine: A Functional Derivation. March 2003. 36 pp.

RS-03-13 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Evaluators and Abstract Machines. March 2003. 28 pp.

RS-03-12 Mircea-Dan Hernest and Ulrich Kohlenbach. A Complexity Analysis of Functional Interpretations. February 2003. 70 pp.

RS-03-11 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. February 2003. 14 pp. To appear in Leuschel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’03 Proceedings, 2003.

RS-03-10 Federico Crazzolara and Giuseppe Milicia. Wireless Authentication in χ-Spaces. February 2003. 20 pp.

RS-03-9 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average and Worst Case Error Estimates. February 2003. 53 pp.

RS-03-8 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. Efficient Algorithms for gcd and Cubic Residuosity in the Ring of Eisenstein Integers. February 2003. 11 pp.

RS-03-7 Claus Brabrand, Michael I. Schwartzbach, and Mads Vanggaard. The METAFRONT System: Extensible Parsing and Transformation. February 2003. 24 pp.