BRICS RS-94-40 Aceto & Ing� olfsd� ottir: CPO Models for GSOS Languages � Part I

BRICS

Basic Research in Computer Science

CPO Models for GSOS Languages Part I: Compact GSOS Languages

Luca Aceto Anna Ing� olfsd� ottir

BRICS Report Series RS-94-40 ISSN 0909-0878 December 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, 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 publications in the BRICS Report Series. 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@daimi.aau.dk

CPO Models for GSOS Languages Part I: Compact GSOS Languages

Luca Aceto^{∗}  Anna Ingólfsdóttir^{†}
BRICS^{‡}

Department of Mathematics and Computer Science Aalborg University Fredrik Bajersvej 7E 9220 Aalborg Ø, Denmark

Abstract In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail and Meyer. The canonical model used for this purpose will be Abramsky’s domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages.

1 Introduction

This study is part of an on-going research programme on the meta-theory of process description languages. This line of research aims at contributing to the systematic development of process theory by offering results that hold for classes of process description languages. As these languages are often equipped with a Plotkin-style Structural Operational Semantics (SOS) [70], this way of giving semantics to processes has been a natural handle to establish results that hold for all languages whose semantics is given by means of inference rules that fit a certain format. Examples of the kind of meta-theoretic results that have been systematically derived from the form of the SOS rules may be found in, e.g., [78, 79, 23, 19, 36, 35, 24, 53, 88, 13, 7, 87, 16, 90, 91, 6]. So far, this line of research has produced a wealth of results which generalize and explain several of the most important theorems and constructions in process theory. For example, given a language with an SOS semantics, an examination of the SOS rules is often all that is needed to guarantee that a notion of behavioral equivalence or preorder will be preserved by the constructs in the language [23, 36, 88, 87, 16, 21, 22], that a process equivalence can be equationally characterized [7, 5], or that a language is implementable [23, 89].

∗On leave from the School of Cognitive and Computing Sciences, University of Sussex, Brighton BN1 9QH, UK. Partially supported by HCM project express. Email: luca@iesd.auc.dk.

†Partially supported by a grant from the Danish Research Council. Email: annai@iesd.auc.dk.

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

Following a bias towards operational methods in process theory that dates back to Milner’s original development of the theory of CCS [59, 65], most of the work reported in the aforementioned references is concerned with operational, axiomatic semantics^{1} for processes and the relationships between the two. In particular, it is by now clear that it is often possible to automatically translate an operational theory of processes into an axiomatic one [7]. Moreover, in certain circumstances, it is also possible to derive an SOS semantics from an axiomatic one, as witnessed by the developments in [48, 7].

Axiomatic semantics and proof systems for programming and specification languages are often closely related to denotational semantics for them, particularly if the Scott-Strachey approach [77] is followed. A paradigmatic example of the development of a semantic theory of processes in which behavioural, axiomatic and denotational semantics coexist harmoniously, and may be used to highlight different aspects of process behaviours is the theory of testing equivalence developed by De Nicola and Hennessy [30, 41]. In this theory, a process can be characterized operationally in terms of its reaction to experiments, and denotationally as a so-called acceptance tree [40]. Acceptance trees allow one to fully describe the behaviour of a process while abstracting completely from the operational details of its interactions with all the possible testers. Moreover, the domaintheoretic properties of this model allow one to establish properties of the behavioural semantics that would be very difficult to derive using purely operational methods. (See, e.g., the results in [41, Sect. 4.5].)

To our mind, the coincidence of axiomatic, behavioural/operational and denotational semantics enjoyed by the theory of processes presented in [41] does not only reinforce the naturality of the chosen notion of program semantics, but allows one to make good use of the complementary benefits afforded by these semantic descriptions in establishing properties of processes. However, developing these three views of processes for each process description language from scratch and proving their coincidence is hard, subtle work; in addition, to quote from [54], giving denotational semantics to programming languages using the Scott-Strachey approach “involves an armamentarium of mathematical weapons otherwise unfamiliar in Computer Science”. We thus believe that it would be beneficial to develop systematic ways of giving denotational semantics to process description languages, following the Scott-Strachey approach, starting from their SOS description. Of course, this is only worthwhile if the denotational semantics produced by the proposed techniques is automatically guaranteed to be in agreement with the behavioural and axiomatic views of processes. In particular, we should like to generate a denotational semantics that matches exactly our operational intuition about process behaviour, i.e., that is fully abstract, in the sense of Milner and Plotkin [56, 68, 57, 85], with respect to a reasonable notion of behavioural semantics. This paper aims at giving a small contribution in this direction.

1In this paper, we shall use the term axiomatic semantics to denote the characterization of process semantics by means of (in)equationally based proof systems. This branch of process theory is referred to as algebraic semantics by some authors (see, e.g., the title of [63]). In this study, we prefer to reserve the term algebraic semantics for the approach to programming language semantics described in, e.g., [37, 41].

1.1 Results

In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail and Meyer [23, 19]. The canonical model used for this purpose will be Abramsky’s domain of synchronization trees D presented in [1], and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder studied in, e.g., [45, 60, 38, 92, 1]. Moreover, in the process of establishing the full abstraction result, we also present an algorithm, along the lines of those given in [7, 5], to generate a complete axiomatization of the bisimulation preorder, thus fulfilling our aim of giving behavioural, axiomatic and denotational accounts of process behaviour that are in complete agreement. As a byproduct of our denotational semantics, we shall be able to establish very general results about the behavioural bisimulation preorder that would be hard to prove using purely operational definitions. (For an example, cf. Thm 6.17.) This is one of the major theoretical advantages of having several complementary semantic views of a language; proofs of program properties that may be very involved or even hard to find in one semantics can be approached in a totally different way in another. On a more speculative note, the denotational semantics we propose may also have some practical interest. For example, powerful effective induction rules like Scott Induction (see, e.g., [52, 41] for a discussion of this proof principle) become usable to reason about process (in)equalities, and proofs about processes can, at least in principle, be carried out within the kind of axiom systems supported by a tool like LCF [34].

The class of GSOS systems we shall give denotational semantics to will have the structure of most standard process algebras (see, e.g., [64, 46, 17, 11]). They will consist of a set of operations to construct finite, acyclic process graphs, and a facility for the recursive definition of behaviours. Borrowing a terminology introduced in [47] in the context of denotational semantics, we shall refer to these languages as compact GSOS languages. Their operational semantics will be given in terms of a variation on the standard model of labelled transition systems [50] that takes divergence information into account. This will be done in such a way that the bisimulation preorder is a precongruence with respect to all the operators in the language. In order to obtain this substitutivity result, special care must be taken in interpreting negative premises in GSOS rules; in particular, negative premises will only be interpreted over convergent (or fully specified) processes. (A similarly motivated choice is made in [87], where negative premises are only interpreted over stable processes, i.e., processes that cannot perform internal transitions.) Intuitively, this is because, in order to find out what a process cannot do, we need to know precisely what its capabilities are, and the initial behaviour of a divergent process is only partially specified. A consequence of our choice is that, for example, the rule

\frac{x ↛^{a}}{f(x) →^{a} f(x)}

cannot be used to derive that the term f(Ω) has an a-labelled transition to itself, where Ω denotes the typical totally divergent process with no transitions. As a byproduct of our approach, we are able to give a simple semantics to GSOS languages in which negative premises are allowed to coexist with unguarded recursive definitions. This contrasts with the standard GSOS semantics given in [23, 19] in which the interplay between negative premises and unguarded recursion may lead to the operational specification of languages without a well-defined operational semantics. (See, e.g., [19, 35] and Sect. 4 of this paper for an example.)

Our first main result is that, with our choice of operational semantics for GSOS languages, the bisimulation preorder is substitutive with respect to all language contexts. (See Thm. 3.9 and Thm. 4.8.) Moreover, as a consequence of general results established by Abramsky in [1], we are able to give a characterization of the finitely observable (or finitary) part of the bisimulation preorder for every GSOS language. Intuitively, this is the preorder obtained by restricting the prebisimulation relation to observations of finite depth.

We then show how to automatically give a denotational semantics for a GSOS language in terms of Abramsky’s domain of synchronization trees D. To this end, following the ideas of initial algebra semantics [76, 33, 29, 58], it is sufficient to endow Abramsky’s model with an appropriate continuous algebra structure in the sense of [33, 37, 41]. This we do by showing how the GSOS rules defining the operational semantics of an operation symbol f of a compact GSOS language can be used to define a continuous function f_{D} of the appropriate arity over the domain of synchronization trees D. In defining the semantic counterparts of the operations in a compact GSOS language, we shall rely on a description of the domain D presented in [47], where it is shown how to reconstruct D from a suitable preorder over finite synchronization trees. This view of D will allow us to define each semantic operation f_{D} in stepwise fashion from monotonic operations over finite synchronization trees. We hope that this choice will make the presentation more accessible to readers who are unfamiliar with domain theory [69, 84].

As a result of our general framework, we shall then show that the denotational semantics so obtained is guaranteed to be in complete agreement with the chosen behavioural semantics. More precisely, for every compact GSOS language, the denotational semantics produced by the general approach presented in this paper is always fully abstract with respect to the finitary part of the bisimulation preorder. The key to the proof of this result is a general theorem that states that, for every compact GSOS language, the finitary part of the bisimulation preorder is completely determined by how it acts on recursion-free processes. Relations that have this property are called algebraic in [41]. The proof of the algebraicity of the behavioural preorder is rather involved, and relies on an algorithm for generating an inequational theory that is partially complete with respect to the bisimulation preorder, in the sense of [38], for arbitrary compact GSOS systems. The partially complete axiomatization generated by our methods proves exactly all the valid inequalities of the form P ≤ Q, where P is a recursion-free term and Q is any term. It can be lifted to the whole of a compact GSOS language by adding to the proof system a very powerful induction rule, called ω-induction in [41].

1.2 Outline of the Paper

The paper is organized as follows. Section 2 presents the basic notions on transition systems and prebisimulation that will be needed in this study. We then go on to present GSOS languages and rules; first we discuss recursion-free languages in Sect. 3, and present our new transition systems semantics for them. The main result of Sect. 3 is that our operational view of GSOS languages induces operations that are substitutive with respect to the bisimulation preorder. Section 4 introduces GSOS languages with recursion and their operational semantics. There we show how to apply our approach to give reasonable operational semantics to languages combining operations defined using negative premises with arbitrary recursive definitions. Section 5 is devoted to background material on algebraic and denotational semantics needed for the remainder of the paper. Compact GSOS languages are introduced in Sect. 6.1. Our method for giving a denotational semantics to arbitrary compact GSOS languages is presented in Sect. 6.2, where the proof of full abstraction of the resulting semantics is also given. Finally, we present in Sect. 7 an algorithm that, for any compact GSOS language, generates an inequational theory that is partially complete with respect to the bisimulation preorder. The paper concludes with some remarks on our work and a mention of topics for further research.

As this is not an introductory paper on the meta-theory of process description languages, we have taken the liberty of referring the readers to other publications in the literature for motivations and some of the background technical material. We hope, however, that our choice of presentation will make the paper accessible to uninitiated readers.

1.3 Related Work

The work reported in this paper is by no means the first attempt to systematically derive denotational models from SOS language specifications. The main precursors to this work in the field of the meta-theory of process description languages may be found in the work by Bloom [20], and by Rutten and Turi [72, 73, 74, 75]. In his unpublished paper [20], Bloom gives operational, logical, relational and three denotational semantics for GSOS languages without negative premises and unguarded recursion, and shows that they coincide. Bloom’s work is based on the behavioural notion of simulation [43], and two of his denotational semantics are given in terms of Scott domains based on finite synchronization trees. On the other hand, the work by Rutten presented in [72, 73, 74] gives methods for deriving a denotational semantics based on complete metric spaces and Aczel’s non-well-founded sets [9] for languages specified in terms of sub-formats of the tyft/tyxt format due to Groote and Vaandrager [36]. In particular, the reference [74] gives a detailed and clear introduction to a technique, called processes as terms by Rutten, for the definition of operations on semantic models from operational rules. Rutten’s general “processes as terms” approach could have been applied to yield an equivalent formulation of the semantic operations on finite synchronization trees we present in Sect. 6.2; in this study, however, we have plumped for the more direct construction of the operations given in Def. 6.9. The work presented in the aforementioned papers by Rutten has recently been generalized by Rutten and Turi in [75]. In that paper, the authors show how to give denotational semantics to languages specified by transition system specifications in full tyft/tyxt format [36], and investigate in a categorical perspective the essential properties of semantic domains that make their definitions possible.

In [3], various notions of process observations are considered in a uniform algebraic framework provided by the theory of quantales (see, e.g., [71]). The methods developed by Abramsky and Vickers in [3] yield, in a uniform fashion, observational logics and denotational models for each notion of process observation they consider. Their work is, however, semantic in nature, and ignores the algebraic structure of process expressions.

In the area of the semantics of functional programs, developments that are somewhat similar in spirit to those pursued in this study are presented by Smith in [80]. In that paper, Smith studies a natural notion of preorder over programs written in a simple functional programming language, and shows how any ordering on programs with certain basic properties can be extended to a term model that is fully abstract with respect to it.

Finally, it is hard to underestimate the debt that our work owes to the pioneering work of Abramsky, Hennessy, Milner, Plotkin and their coworkers in the field of denotational models for concurrency. Without the inspiration of seminal papers like [55, 44, 40, 1, 42], this work would simply not have been possible.

2 Preliminaries on Labelled Transition Systems

We begin by reviewing the basic notions on transition systems that will be needed in this study. The interested reader is invited to consult, e.g., [50, 70] for more details and extensive motivations.

The operational semantics of the languages considered in this paper will be given in terms of a variation on the model of labelled transition systems [50] that takes divergence information into account. We refer the interested readers to, e.g., [45, 38, 60, 92] for motivation and more information on (variations on) this semantic model for reactive systems.

Definition 2.1 (Labelled Transition Systems with Divergence) A labelled transition system with divergence (lts) is a quadruple (P, Lab, →, ↑), where:

• P is a set of processes, ranged over by s, t;

• Lab is a set of labels, ranged over by ℓ;

• →⊆ P × Lab × P is a transition relation. As usual, we shall use the more suggestive notation s →^{ℓ} t in lieu of (s, ℓ, t) ∈→;

• ↑⊆ P is a divergence predicate, notation s ↑.

We write s ↓, read “s definitely converges”, iff it is not the case that s ↑, and s → t iff s →^{a} t for some a ∈ Lab (→^{∗} stands for the reflexive and transitive closure of →). The sort of a process s is defined as follows:

sort(s) = {a ∈ Lab | ∃t, u : s →^{∗} t →^{a} u} .

An lts is sort-finite iff sort(s) is finite for every process s.

A useful source of examples for labelled transition systems with divergence is the set of finite synchronization trees over a set of labels Lab, denoted by ST(Lab). These are the sets generated by the following inductive definition:

\frac{\{ℓ_{i} ∈ Lab, t_{i} ∈ ST(Lab)\}_{i∈I}}{\{⟨ℓ_{i}, t_{i}⟩ | i ∈ I\}[∪\{⊥\}] ∈ ST(Lab)}

where I is a finite index set, and the notation [∪{⊥}] means optional inclusion of ⊥. As it will become clear in a moment, the symbol ⊥ will be used to represent the fact that a synchronization tree is divergent. The set of finite synchronization trees ST(Lab) can be turned into a labelled transition system with divergence by stipulating that, for t ∈ ST(Lab):

• t ↑ iff ⊥ is in t, and

• t →^{ℓ_{i}} t_{i} iff ⟨ℓ_{i}, t_{i}⟩ is in t.

The behavioural relation over processes that we shall study in this paper is that of prebisimulation [45, 60, 38, 92] (also known as partial bisimulation [1]).

Definition 2.2 (Prebisimulation) Let Λ = (P, Lab, →, ↑) be an lts. Let Rel(P) denote the set of binary relations over P. Define the functional F : Rel(P) → Rel(P) by:

F (R) = {(s, t) | ∀ℓ ∈ Lab

• s →^{ℓ} s′ ⇒ ∃t′ : t →^{ℓ} t′ and s′ R t′

• s ↓⇒ t ↓ and [t →^{ℓ} t′ ⇒ ∃s′ : s →^{ℓ} s′ and s′ R t′]}

A relation R is a prebisimulation iff R⊆ F (R). We write s_{1} ≲_{Λ} s_{2} iff there exists a prebisimulation R such that s_{1} R s_{2}. (The subscript Λ will be omitted when this causes no confusion.)

The relation ≲ is a preorder over P based on a variation on bisimulation equivalence [66, 64]. Its kernel will be denoted by ∼, i.e., ∼=≲ ∩ ≲^{−1}. Intuitively, s_{1} ≲ s_{2} if s_{2}’s behaviour is at least as specified as that of s_{1}, and s_{1} and s_{2} can simulate each other when restricted to the part of their behaviour that is fully specified. A divergent state s with no outgoing transition is a minimal element with respect to ≲, and intuitively corresponds to a process whose behaviour is totally unspecified — essentially an operational version of the bottom element ⊥ in Scott’s theory of domains [77, 69, 84].

Although the relations ≲ and ∼ have been defined over a given lts, we often want to use them to compare processes from different lts’s; for example, we shall often compare states in an lts with finite synchronization trees. This can be done in standard fashion by forming the disjoint union of the two systems, and then using ≲ and ∼ on the resulting lts. In the sequel, this will be done without further comment.

Notation 2.3 The largest prebisimulation over an lts obtained as the disjoint union of an lts Λ and the lts of finite synchronization trees will be denoted by ≲_{Λ} throughout the paper.

In this study, we shall be interested in relating the notion of prebisimulation to a preorder on processes induced by a denotational semantics given in terms of an algebraic domain [69, 84]. As such preorders are completely determined by how they act on finite processes, we shall be interested in comparing them with the “finitely observable”, or finitary, part of the bisimulation in the sense of, e.g., [37, 38]. The following definition is from [1].

Definition 2.4 The finitary preorder ≲^{F} is defined on any lts by

s ≲^{F} s′ ⇔ ∀t ∈ ST(Lab). t ≲ s ⇒ t ≲ s′ .

An alternative method for using the functional F to obtain a behavioural preorder is to apply it inductively as follows:

• ≲_{0}= Rel(P),

• ≲_{n+1}= F (≲_{n})

and finally ≲_{ω}= ⋂_{n≥0} ≲_{n}. Intuitively, the preorder ≲_{ω} is obtained by restricting the prebisimulation relation to observations of finite depth. The preorders ≲, ≲_{ω} and ≲^{F} are, in general, related thus:

≲ ⊆ ≲_{ω} ⊆ ≲^{F} .

Moreover the inclusions are, in general, strict. The interested reader is referred to [1] for a wealth of examples distinguishing these preorders, and a very deep analysis of their general relationships and properties. Here we simply state the following useful result, which is a simple consequence of [1, Lem. 5.10]:

Lemma 2.5 Let (P, Lab, →, ↑) be an lts with divergence. Then, for every t ∈ ST(Lab), s ∈ P, t ≲ s iff t ≲_{ω} s.

In what follows we shall have some use for the notion of prebisimulation up to ≲. (See Sect. 4.) Following Milner [62, 64] and Walker [92], this is defined as follows:

Definition 2.6 Let (P, Lab, →, ↑) be an lts with divergence. A relation R ⊆ P × P is a prebisimulation up to ≲ if, for all s_{1}, s_{2} ∈ P, ℓ ∈ Lab, s_{1} R s_{2} implies

1. if s_{1} →^{ℓ} s′_{1}, then for some s′_{2}, s′′_{2} ∈ P, s_{2} →^{ℓ} s′′_{2} and s′_{1} R s′_{2} ≲ s′′_{2};

2. if s_{1} ↓ then

(a) s_{2} ↓, and

(b) if s_{2} →^{ℓ} s′_{2}, then for some s′_{1}, s′′_{1} ∈ P, s_{1} →^{ℓ} s′′_{1} and s′′_{1} ≲ s′_{1} R s′_{2}.

The usefulness of the above notion is summarized by the following lemma that can be shown by simple arguments along the lines of [64, Lemma 4.5].

Lemma 2.7 Let (P, Lab, →, ↑) be an lts. Suppose that a relation R ⊆ P × P is a prebisimulation up to ≲. Then s_{1} R s_{2} implies s_{1} ≲ s_{2}.

3 GSOS Languages

We assume some familiarity with process algebra and structural operational semantics (see, e.g., [46, 41, 64, 17, 70, 36, 23, 19] for more details and extensive motivations).

Let Var be a denumerable set of meta-variables ranged over by x, y. A signature Σ consists of a set of operation symbols, disjoint from Var, together with a function arity that assigns a natural number to each operation symbol. Throughout this paper, following the standard lines of algebraic semantics (see, e.g., [37, 41]), we shall assume that signatures contain a distinguished function symbol Ω of arity zero to denote the totally unspecified, or divergent, process, i.e., a process about whose behaviour we have no information^{2}. The set (Σ, Var) of terms over Σ and Var (abbreviated to (Σ) when the set of variables is clear from the context or immaterial) is the least set such that

• Each x ∈ Var is a term.

• If f is an operation symbol of arity l, and P_{1}, …, P_{l} are terms, then f(P_{1}, …, P_{l}) is a term.

We shall use P, Q, … to range over terms and the symbol ≡ for the relation of syntactic equality on terms. T(Σ) is the set of closed terms over Σ, i.e., terms that do not contain variables. Constants, i.e. terms of the form f(), will be abbreviated as f.

A Σ-context C[x⃗] is a term in which at most the variables x⃗ appear. C[P⃗] is C[x⃗] with x_{i} replaced by P_{i} wherever it occurs. We say that a relation R ⊆ T(Σ) × T(Σ) is closed with respect to Σ-contexts iff for every Σ-context C[x⃗] and vectors of closed terms P⃗ and Q⃗ of the appropriate length

P⃗ R Q⃗ implies C[P⃗] R C[Q⃗]

where the relation R is extended pointwise to vectors of equal length.

Besides terms we have actions, elements of some given finite set Act, which is ranged over by a, b, c. A positive transition formula is a triple of two terms and an action, written P →^{a} P′. A negative transition formula is a pair of a term and an action, written P ↛^{a}. In general, the terms in the transition formula will contain variables. Transition formulae will be ranged over by φ.

Definition 3.1 (GSOS Rules) Suppose Σ is a signature. A GSOS rule r over Σ is an inference rule of the form:

\frac{⋃_{i=1}^{l} \{x_{i} →^{a_{ij}} y_{ij}|1 ≤ j ≤ m_{i}\} ∪ ⋃_{i=1}^{l} \{x_{i} ↛^{b_{ik}} |1 ≤ k ≤ n_{i}\}}{f(x_{1}, …, x_{l}) →^{c} C[x⃗, y⃗]}  (1)

where all the variables are distinct, m_{i}, n_{i} ≥ 0, f is an operation symbol from Σ with arity l, C[x⃗, y⃗] is a Σ-context, and the a_{ij}, b_{ik}, and c are actions in Act.

2In fact, as it will become clear in the remainder of this paper, Ω is just syntactic sugar for the recursive term fix(X = X). See Sect. 4 for details.

It is useful to name components of rules of the form (1). The operation symbol f is the principal operation of the rule, and the term f(x⃗) is the source. C[x⃗, y⃗] is the target (sometimes denoted by target(r)); c is the action (sometimes denoted by action(r)); the formulae above the line are the antecedents; and the formula below the line is the consequent. If, for some i, m_{i} > 0 then we say that r tests its i-th argument positively. Similarly if n_{i} > 0 then we say that r tests its i-th argument negatively. An operation f tests its i-th argument positively (resp. negatively) if it occurs as principal operation of a rule that tests its i-th argument positively (resp. negatively). We say that an operation f tests its i-th argument if it tests it either positively or negatively.

Definition 3.2 (GSOS Systems) A GSOS system is a pair G = (Σ_{G}, R_{G}), where Σ_{G} is a finite signature and R_{G} is a finite set of GSOS rules over Σ_{G} containing no rules with Ω as principal operation.

Example: An example of GSOS system, the language preACP_{Ωθ}^{3}, is presented in Fig. 1. We shall use this concrete language as a running example throughout the paper to illustrate our definitions and results.

The language preACP_{Ωθ} is a subset of ACP [17] with action prefixing in lieu of general sequential composition. Its parallel composition operator, denoted by ∥, is parameterized with respect to a partial, commutative and associative communication function γ : Act × Act ⇀ Act. An operation in preACP_{Ωθ} that uses the power of negative premises, at least in the presence of a non-trivial priority structure on actions, is the priority operation θ of Baeten, Bergstra and Klop [15]. In order to define this operation, we assume a given partial ordering relation > on Act. Intuitively, b > a is interpreted as “action b has priority over action a”.

The sub-language of preACP_{Ωθ} consisting only of the operations Ω, δ, a. and + will be denoted by FINTREE_{Ω}. We shall use the standard process algebra conventions for the FINTREE_{Ω} language. For example, for I = {i_{1}, …, i_{n}} a finite index set, we write ∑_{i∈I} P_{i} for P_{i_{1}} + ⋯ + P_{i_{n}}. By convention, ∑_{i∈∅} P_{i} stands for δ.

□

GSOS systems have been introduced and studied in depth in [23, 19]. Intuitively, a GSOS system gives a language, whose constructs are the operations in the signature Σ_{G}, together with a Plotkin-style structural operational semantics [70] for it defined by the set of conditional rules R_{G}. In this study, the operational semantics of a GSOS system will be given in terms of labelled transition systems with divergence. In order to obtain this non-standard interpretation, we aim at using the rules in a GSOS system G to define a divergence predicate over terms and a transition relation in such a way that our definitions:

1. specialize to those originally given by Bloom, Istrail and Meyer in their seminal studies [23, 19] when divergence is not taken into account;

2. give results that are in agreement with those already presented in the literature when applied to known process description languages; and

3Here we follow the spirit of the terminology suggested in [14].

Signature  Arity Rules
δ  0 no rules
Ω  0 no rules
a. (a ∈ Act) 1 a.x →^{a} x
+  2 \frac{x→^{a}x′}{x+y→^{a}x′}  \frac{y→^{a}y′}{x+y→^{a}y′}
∥  2 \frac{x→^{a}x′}{x∥y→^{a}x′∥y} \frac{y→^{a}y′}{x∥y→^{a}x∥y′}

\frac{x→^{a}x′,y→^{b}y′}{x∥y→^{c}x′∥y′} γ(a, b) ≃ c

θ  1 \frac{x→^{a}x′,(∀b>a)x↛^{b}}{θ(x)→^{a}θ(x′)}

Figure 1: The language preACP_{Ωθ}

3. produce operators that are well-behaved with respect to the notion of prebisimulation, i.e., operations for which prebisimulation is a precongruence.

First of all, we shall use the rules in a GSOS systems to define a divergence (or underspecification) predicate on the set of closed terms over Σ_{G}. In fact, as is common practice in the literature on process algebras, we shall define the notion of convergence, and use it to define the divergence predicate we are after. Intuitively, a term P is convergent if the set of its initial transitions is fully specified. The basic divergent term is Ω, the totally unspecified process. A term of the form f(P⃗) is convergent iff the set of its initial transitions only depends on those arguments P_{i}s whose initial behaviour is completely known. This informal discussion motivates the following definition.

Definition 3.3 (Convergence) Let G = (Σ_{G}, R_{G}) be a GSOS system. The convergence predicate ↓_{G} (abbreviated to ↓ when the GSOS system G is clear from the context) is the least predicate over T(Σ_{G}) that satisfies the following clause:

f(P_{1}, …, P_{l}) ↓_{G} if

1. f ≠ Ω, and

2. for every argument i of f, if f tests i then P_{i} ↓_{G}.

We write P ↑_{G} iff it is not the case that P ↓_{G}.

When applied to the language preACP_{Ωθ}, Def. 3.3 gives the following convergence predicate:

• δ ↓,

• if P ↓ and Q ↓, then P + Q ↓ and P ∥Q ↓,

• if P ↓ then θ(P) ↓.

The reader familiar with the literature on prebisimulation over CCS-like languages will have noted that the above definition generalizes those given in, e.g., [45, 38, 30]. For instance, when applied to the recursion-free fragment of the version of Milner’s SCCS considered in [38], it delivers exactly Hennessy’s converge predicate.

We shall now present our non-standard operational semantics for GSOS languages. As stated above, we take as our starting point the original theory developed by Bloom, Istrail and Meyer. Informally, the original intent of a GSOS rule is as follows. Suppose that we are wondering whether f(P⃗) is capable of taking a c-step. We look at each rule with principal operation f and action c in turn. We inspect each positive antecedent x_{i} →^{a_{ij}} y_{ij}, checking if P_{i} is capable of taking an a_{ij}-step for each j and if so calling the a_{ij}-children Q_{ij}. We also check the negative antecedents; if P_{i} is incapable of taking a b_{ik}-step for each k. If so, then the rule fires and f(P⃗) →^{c} C[P⃗ , Q⃗]. Roughly, this means that the transition relation associated with a GSOS system in [23] is the one defined by structural induction on terms using the rules in R_{G}.

In the presence of divergence information, we shall define the transition relation over terms in a similar vein. However, we shall interpret negative transition formulae over convergent processes only. Intuitively, to know that a process cannot initially perform a given action, we need to find out precisely all the actions that it can perform. If a process is divergent, its set of initial actions is not fully specified; thus we cannot be sure whether such a process satisfies a negative transition formula or not.

For the sake of completeness, we shall now formally define the lts with divergence induced by a GSOS system following [23, 19, 7]. (Our presentation follows the one given in [7] more closely.)

Definition 3.4 A closed Σ-substitution is a function σ from variables to closed terms over the signature Σ. For each term P, P σ will denote the result of substituting σ(x) for each x occurring in P. For t a term, transition formula, GSOS rule, etc., we write tσ for the result of substituting σ(x) for each x occurring in t.

The notation {P_{1}/x_{1}, …, P_{n}/x_{n}}, where the P_{i}s are terms and the x_{i}s are distinct variables, will often be used to denote the substitution that maps each x_{i} to P_{i}, and leaves all the other variables unchanged.

Definition 3.5 Let G be a GSOS system. A transition relation over the signature Σ_{G} is a relation ⇝ ⊆ T(Σ_{G}) × Act × T(Σ_{G}).

Let ⇝ be a transition relation and σ a closed substitution. For each transition formula φ, the predicate ⇝, σ ⊧ φ is defined by

⇝, σ ⊧ P →^{a} Q =^{Δ} P σ ⇝^{a} Qσ
⇝, σ ⊧ P ↛^{a} =^{Δ} P σ ↓_{G} and ∄Q : P σ ⇝^{a} Q

For H a set of transition formulae, we define

⇝, σ ⊧ H =^{Δ} ∀φ ∈ H : ⇝, σ ⊧ φ

and for r = \frac{H}{φ} a GSOS rule of the form (1),

⇝, σ ⊧ \frac{H}{φ} =^{Δ} (⇝, σ ⊧ H ⇒ ⇝, σ ⊧ φ).

The reader familiar with the literature on Hennessy-Milner logics [43] for prebisimulationlike relations will have noted that our notion of satisfaction for negative transition formulae is akin to that for formulae of the form [a]F given in, e.g., [60, 82, 83, 1, 8]. In those references, the new interpretation is necessary to obtain monotonicity of the satisfaction relation with respect to the appropriate notion of prebisimulation. In this study, our interpretation of negative premises will be crucial to obtain operations that are monotonic with respect to the notion of prebisimulation. (See, e.g., Thm. 3.9). Basically, it will ensure that, for a closed term P, the transition formula P ↛^{a} holds iff Q ↛^{a} holds for every closed term with P ≲ Q.

Definition 3.6 Suppose G is a GSOS system and ⇝ is a transition relation over Σ_{G}. Then ⇝ is sound for G iff for every rule r ∈ R_{G} and every closed Σ_{G}-substitution σ, we

have ⇝, σ ⊧ r. A transition P ⇝^{a} Q is supported by some rule \frac{H}{φ} ∈ R_{G} iff there exists

a substitution σ such that ⇝, σ ⊧ H and φσ = (P →^{a} Q). The relation ⇝ is supported by G iff each transition in ⇝ is supported by a rule in R_{G}.

The requirements of soundness and supportedness are sufficient to associate a unique transition relation with each GSOS system.

Lemma 3.7 For each GSOS system G there is a unique sound and supported transition relation.

Proof: The unique sound and supported transition relation associated with a GSOS system G is the one defined by structural recursion on terms using the rules in R_{G}, with the proviso that, as formalized in Def. 3.5, negative transition formulae can only be satisfied by convergent terms. The interested reader is referred to the proof of Propn. 4.3 for details. □

We write →_{G} for the unique sound and supported transition relation for G.

Lemma 3.8 Suppose G is a GSOS system. Then the transition relation →_{G} is finitely branching, i.e., for every P ∈ T(Σ_{G}), the set Der(P) = {(a, Q) | P →^{a}_{G} Q} is finite.

Proof: A minor modification of the proof of the standard result for GSOS languages in [19]. □

The lts with divergence specified by a GSOS system G is then given by

lts(G) = (T(Σ_{G}), →_{G}, ↑_{G}) .

The largest prebisimulation over lts(G) will be denoted by ≲_{G}, and its kernel by ∼_{G}. (The subscript G will be omitted from these relations when this causes no confusion).

Example: We exemplify our approach using our running example, the language in Fig. 1, by considering some identities involving simple terms that use the priority operation θ.

The term θ(Ω) is divergent, as Ω is. Moreover it does not have any transition because Ω has none. We thus have that θ(Ω) ∼ Ω.

Consider a term of the form P ≡ a.δ + Ω, with a a maximal element in the poset (Act, >), i.e., with a an action with maximal priority. Then the rule for θ with action a has no negative antecedents, and it can be used to establish the transition θ(P) →^{a} θ(δ). Indeed, this is the only transition that is possible from θ(P). As θ(P) is divergent, as P is, it is easy to see that θ(P) ∼ a.δ + Ω.

On the other hand, if a is not maximal in the poset (Act, >), the rule for θ with action a will have at least one negative antecedent. As P is divergent, that rule cannot be used to derive a transition from the term θ(P). It thus follows that θ(P) ∼ Ω, if a is not maximal in the poset (Act, >). □

3.1 Prebisimulation is a Precongruence

We are now ready to establish the first main result of this paper. Namely, we shall prove that the operations of a GSOS system preserve the semantic notion of prebisimulation. This is the import of the following theorem.

Theorem 3.9 Let G be a GSOS system. Then ≲_{G} is a precongruence for all operation symbols f of G, i.e., (∀i : P_{i} ≲_{G} Q_{i}) ⇒ f(P⃗) ≲_{G} f(Q⃗).

Proof: Consider the least relation R satisfying the following conditions:

1. ≲_{G} ⊆ R, and

2. if P_{i} R Q_{i} for 1 ≤ i ≤ l, then f(P⃗) R f(Q⃗).

Note that R so defined is the smallest relation that contains ≲_{G} and is closed with respect to all Σ_{G}-contexts.

The statement of the theorem follows immediately if we prove that R is a prebisimulation. This we show by induction on the definition of the relation R. Assume thus that P R Q. By the definition of R, we have that either

1. P ≲_{G} Q, or

2. P ≡ f(P⃗), Q ≡ f(Q⃗) and P_{i} R Q_{i}, for some P⃗, Q⃗.

If P ≲_{G} Q, then the clauses of Definition 2.1 are trivially met as ≲_{G} is itself a prebisimulation included in R. We shall thus concentrate on showing that they are met when P ≡ f(P⃗), Q ≡ f(Q⃗) and P_{i} R Q_{i}, for some P⃗, Q⃗, under the inductive hypothesis that they are met for each pair of terms P_{i} R Q_{i}.

We check that each clause of the definition of prebisimulation is met in turn.

• Assume that P ≡ f(P⃗) →^{c}_{G} R for some R ∈ T(Σ_{G}). We shall show that Q ≡ f(Q⃗) →^{c}_{G} S for some S such that R R S.

As f(P⃗) →^{c}_{G} R and →_{G} is supported by R_{G}, there exist a rule r for f of the form (1), and a closed substitution σ such that:

1. f(x⃗)σ = f(P⃗), i.e., σ(x_{i}) = P_{i} for very i ∈ {1, …, l};

2. C[x⃗, y⃗]σ = R;

3. for every 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, σ(x_{i}) = P_{i} →^{a_{ij}}_{G} σ(y_{ij}), and

4. for every 1 ≤ i ≤ l with n_{i} > 0, σ(x_{i}) = P_{i} ↓_{G} and, for every 1 ≤ k ≤ n_{i},

P_{i} ↛^{b_{ik}}_{G}.

We aim at using r to construct a matching transition from f(Q⃗) with respect to R. This requires checking that all the antecedents of rule r are suitably met by Q⃗.

We examine the positive antecedents first. As P_{i} R Q_{i} for each 1 ≤ i ≤ l, by induction we have that for every 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, there exists a term S_{ij} such that

– Q_{i} →^{a_{ij}}_{G} S_{ij}, and

– σ(y_{ij}) R S_{ij}.

This implies that the positive antecedents of r can be met by using the substitution τ = {Q⃗/x⃗, S⃗/y⃗}.

As P_{i} R Q_{i} and P_{i} ↓_{G} if n_{i} > 0 (1 ≤ i ≤ l), another application of the inductive hypothesis gives that for every 1 ≤ i ≤ l with n_{i} > 0, τ(x_{i}) = Q_{i} ↓_{G} and τ(x_{i}) = Q_{i} ↛^{b_{ik}}_{G}, 1 ≤ k ≤ n_{i}, i.e., all the negative antecedents of rule r can also be met by the substitution τ.

Thus the substitution τ and the rule r can be used to derive the transition

f(Q⃗) →^{c}_{G} C[x⃗, y⃗]τ .

We are now left to show that R = C[x⃗, y⃗]σ R C[x⃗, y⃗]τ. However, this is immediate from the fact that, by construction, R is closed with respect to all Σ_{G}-contexts.

• We now show that f(P⃗) ↓_{G} implies f(Q⃗) ↓_{G}. Assume that f(P⃗) ↓_{G}. By the definition of the predicate ↓_{G}, this is because f ≠ Ω and, for every argument i of f, f tests i implies that P_{i} ↓_{G}. As P_{i} R Q_{i}, the induction hypothesis gives that Q_{i} ↓_{G} for every i tested by f. Thus f(Q⃗) ↓_{G}.

• Assume that f(P⃗) ↓_{G}, f(Q⃗) ↓_{G} and f(Q⃗) →^{c}_{G} S. We shall show that f(P⃗) →^{c}_{G} R for some term R such that R R S. As f(Q⃗) →^{c}_{G} S and →_{G} is supported by R_{G}, there exist a rule r for f of the form (1), and a closed substitution τ such that:

1. f(x⃗)τ = f(Q⃗), i.e., τ(x_{i}) = Q_{i} for very i ∈ {1, …, l};

2. C[x⃗, y⃗]τ = S;

3. for every 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, τ(x_{i}) = Q_{i} →^{a_{ij}}_{G} τ(y_{ij}), and

4. for every 1 ≤ i ≤ l with n_{i} > 0, τ(x_{i}) = Q_{i} ↓_{G} and τ(x_{i}) = Q_{i} ↛^{b_{ik}}_{G}, for 1 ≤ k ≤ n_{i}.

As before, we aim at using r to construct a matching transition from f(P⃗) with respect to R. This requires checking that all the antecedents of rule r are suitably met by P⃗.

First of all, note that, as f(P⃗) ↓_{G}, we have that P_{i} ↓_{G} for every argument i that is tested by f. In particular, it follows that P_{i} ↓_{G} for every argument i that is tested by r. Thus, by the fact that P_{i} R Q_{i} for 1 ≤ i ≤ n and induction, we obtain that:

– for every 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, there exists a term R_{ij} such that P_{i} →^{a_{ij}}_{G} R_{ij}

and R_{ij} R τ(y_{ij}); and

– for every 1 ≤ i ≤ l with n_{i} > 0, P_{i} ↓_{G} and P_{i} ↛^{b_{ik}}_{G}, for 1 ≤ k ≤ n_{i}.

Consider now the substitution σ = {P⃗ /x⃗, R⃗/y⃗}. By construction, the substitution σ satisfies the antecedents of rule r; σ and r can therefore be used to derive the transition

f(P⃗) →^{c}_{G} C[x⃗, y⃗]σ .

We are now left to show that C[x⃗, y⃗]σ R C[x⃗, y⃗]τ. Again, this follows easily from the fact that the relation R is closed with respect to Σ_{G}-contexts.

This proves that R is a prebisimulation. □

It is interesting to remark here that the above theorem would not hold if we allowed negative premises to be satisfied by divergent terms. As a simple example of this fact, consider the operation θ in our running example, and let us assume that the poset (Act, >) is non-trivial. Let a be an action that is not maximal in the poset (Act, >), and consider the term P ≡ a.δ + Ω. If we were allowed to interpret negative premises over divergent terms, then the rule for θ with action a could be used to derive the transition θ(P) →^{a} θ(δ). However, any term of the form a.δ + b.δ with b > a (these terms exist as a is not maximal in (Act, >)) would have the properties that:

1. P ≲ a.δ + b.δ, and

2. θ(a.δ + b.δ) ↛^{a}.

This would imply that θ(P) ≴ θ(a.δ + b.δ).

4 GSOS Systems with Recursion

In this section we consider GSOS languages that include explicit recursive definitions of processes. Let G = (Σ_{G}, R_{G}) be a GSOS system, and let PVar be a fresh denumerable set of process variables (X, Y ∈ PVar). The set of recursive terms over Σ_{G} and PVar, denoted by REC(Σ_{G}, PVar), is given by the following BNF syntax:

P ::= X | f(P_{1}, …, P_{l}) | fix(X = P)

where X ∈ PVar, f is an operation symbol in Σ_{G} of arity l and fix is a binding construct. This gives rise to the usual notions of free and bound variables in terms. The set of closed recursive terms (or programs) will be denoted by CREC(Σ_{G}, PVar). We shall assume a standard notion of substitution of terms for free process variables, and use, with abuse of notation, P {Q/X} to denote term P in which each free occurrence of X has been replaced by Q, after possibly renaming bound variables in P. (The details of the operation of substitution in the presence of binders like fix are standard, and will not be important in this study. The interested reader is invited to consult, e.g., [86] for details). General substitutions mapping process variables to programs in CREC(Σ_{G}, PVar) will be denoted by boldface Greek letters like σ.

We shall now define an operational semantics for the set of programs CREC(Σ_{G}, PVar) in terms of an lts with divergence, following the techniques presented in Sect. 3. Again, our aim is to give an operational semantics for recursive terms which is, as much as possible, in the spirit of the standard GSOS approach. One of the corner-stones of the GSOS philosophy is the use of structural recursion on terms to define the transition relation associated with a GSOS system. (Note that, for recursive terms, this requires defining the transition relation for arbitrary open terms in REC(Σ_{G}, PVar).) This suggests the following rule schemata to give the operational semantics of recursion:

\frac{x →^{a} y}{fix(X = x) →^{a} y\{fix(X = x)/X\}}  (2)

Such a variation on the rule for recursion used in, e.g., CCS [59] has been applied in, e.g., [27], and is discussed in detail in [12]. As argued in [12], for guarded recursive terms^{4}, this rule for recursion gives the same results as the standard one based on unfoldings, namely:

\frac{x\{fix(X = x)/X\} →^{a} y}{fix(X = x) →^{a} y}  (3)

Moreover, rule (2) has the benefit of leading to an effective operational semantics that associates a finitely branching lts with each program [12]. However, in this paper, our main desideratum of a recursion rule is that it allows us to interpret recursive terms as fixed-points, i.e., we should like the following equation to hold:

fix(X = P) = P {fix(X = P)/X} .  (4)

This requirement rules out the use of rule (2), as, in general, (4) does not hold for unguarded recursive terms if their semantics is given using it. As an example, consider the GSOS system obtained by adding to FINTREE_{Ω} the operation f given by the rule:

\frac{x →^{a} y}{f(x) →^{b} δ}  (5)

Then, as process variables have no transitions, the open term f(X)+a.δ can only exhibit one transition, namely f(X)+a.δ →^{a} δ. Therefore, the only transition that can be inferred for the term P ≡ fix(X = f(X) + a.δ) using rule (2) is

4In Milner’s CCS, a program P is guarded if every occurrence of a process variable in P is within the scope of an a. operation. Generalizations of this idea are presented in [12, 89, 6].

fix(X = f(X) + a.δ) →^{a} δ .

On the other hand, the term f(P) + a.δ, obtained by unwinding the recursive definition of P once, has also the possibility of performing a b-transition. This implies that P ≁ f(P) + a.δ. For this reason, the semantics of recursive terms will be given in this study by means of the standard recursion rule (3).

In order to define the operational semantics of CREC(Σ_{G}, PVar), we need, first of all, to extend the convergence predicate to CREC(Σ_{G}, PVar). This can be done in standard fashion following, e.g., [45, 38, 8].

Definition 4.1 The convergence predicate ↓Grec (abbreviated to ↓ when the GSOS system G is clear from the context) is the least predicate over CREC(Σ_{G}, PVar) that satisfies the following clauses:

1. f(P_{1}, …, P_{l}) ↓Grec if

(a) f ≠ Ω, and

(b) for every argument i of f, if f tests i then P_{i} ↓Grec.

2. fix(X = P) ↓Grec if P {fix(X = P)/X} ↓Grec.

Again, we write P ↑Grec iff it is not the case that P ↓Grec.

The motivation for the above definition is the following: a term P is divergent if its initial transitions are not fully specified. This occurs either when the initial behaviour of term P depends on under-specified arguments like Ω or in the presence of unguarded recursive definitions. For example, the terms fix(X = X) and fix(X = f(X)), where f is the operation given by rule (5) are not convergent as the initial behaviour of these processes depends on itself. It is immediate to see that the predicates ↓_{G} and ↓_{Grec} coincide over T(Σ_{G}), the set of recursion-free terms in CREC(Σ_{G}, PVar). We remark here that, when applied to SCCS [62] and the version of CCS considered in [92], the above definition delivers exactly the convergence predicates given by Hennessy in [38] and Walker in [92], respectively.

We shall now show how to associate a transition relation with a GSOS language with recursion. Of course, we should like the transition relation to be at least sound and supported in the sense of Def. 3.6^{5}. Moreover, as it is the case for languages defined by rules without negative premises, we should like to associate the least such relation with a GSOS language with recursion. We shall now show that this can indeed be done, and that the extra structure given by the convergence predicate can be put to good use in giving a simple way of constructing the transition relation determined by a GSOS language with recursion. (The interested reader may wish to compare what follows with the techniques presented in the beautiful study [24].) The basic idea of the construction given in the proof of the following proposition is to build the transition relation associated with CREC(Σ_{G}, PVar) in two steps. In the first step of the construction, we derive the transitions emanating from convergent terms by induction on the convergence predicate following the approach outlined in the previous section, and using the rule schemata (3) to derive the transitions of recursive terms. In the second, we use the information about the transitions that are possible for convergent terms to determine the outgoing transitions for all the terms in CREC(Σ_{G}, PVar).

5To be precise, we should extend Def. 3.6 to arbitrary transition formulae. This is straightforward in light of Def. 3.5. See also [24].

The second step of the construction outlined informally above will use a notion of proof of a transition from a set of inference rules which is a slight modification of the standard one presented in, e.g., [36]. This we now present for the sake of completeness.

Definition 4.2 Let G be a GSOS system. An oracle for G is a set O of transitions of the form P →^{a} Q, where P, Q ∈ CREC(Σ_{G}, PVar) and P ↓_{Grec}.

Let O be an oracle for G. Let P, Q ∈ CREC(Σ_{G}, PVar) and a ∈ Act. A proof with oracle O of the transition formula P →^{a} Q from G is a well-founded, upwardly branching tree whose nodes are labelled by positive transition formulae of the form P′ →^{b} Q′ with P′, Q′ ∈ CREC(Σ_{G}, PVar) and b ∈ Act, such that:

• the root is labelled with P →^{a} Q,

• if P′ →^{c} Q′ is the label of a node, and Children is the set of labels of the nodes directly above it, then:

– either, there are an instance \frac{ψ}{φ} of rule (3) and a substitution σ : Var → CREC(Σ_{G}, PVar) such that {ψσ} = Children and φσ = P′ →^{c} Q′,

– or, Children = {P_{i} →^{a_{ij}} Q_{ij} | 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}}, and there are a rule r ∈ R_{G} of the form (1) and a substitution σ : Var → CREC(Σ_{G}, PVar) such that:

∗ Children = ⋃_{i=1}^{l} {σ(x_{i}) →^{a_{ij}} σ(y_{ij})|1 ≤ j ≤ m_{i}};

∗ for every 1 ≤ i ≤ l with n_{i} > 0, σ(x_{i}) ↓_{Grec} and σ(x_{i}) →^{b_{ik}} R ∈ O (1 ≤ k ≤

n_{i}) for no R ∈ CREC(Σ_{G}, PVar); and

∗ P′ →^{c} Q′ = (f(x⃗) →^{c} C[x⃗, y⃗])σ.

Proposition 4.3 For every GSOS language with recursion CREC(Σ_{G}, PVar), there exists a smallest sound and supported transition relation over CREC(Σ_{G}, PVar). This transition relation will be denoted by →_{Grec}. Moreover, for every P ∈ T(Σ_{G}),

P →^{a}_{Grec} Q ⇔ Q ∈ T(Σ_{G}) and P →^{a}_{G} Q .  (6)

Proof: First of all, we show how to construct a sound and supported transition relation →_{Grec} over CREC(Σ_{G}, PVar). We then proceed to prove that →_{Grec} is indeed the smallest relation with these properties.

• Construction of →_{Grec}. We shall construct the relation →_{Grec} over CREC(Σ_{G}, PVar) in two steps, and the construction outlined below will guarantee that the result is sound and supported. In the first step of the construction, we derive the transitions emanating from convergent terms only. In the second step, we use the information about the transitions that are possible for convergent terms to determine the outgoing transitions for all the terms in CREC(Σ_{G}, PVar).

– Step 1. We determine the transitions that are possible for convergent terms by induction on the predicate ↓_{Grec}. To this end, let us assume that P ↓_{Grec}. We shall now show how to construct the set

Der(P) = {(a, Q) | P →^{a}_{Grec} Q}

by examining the possible forms P may take.

∗ Case P ≡ f(P⃗). As P ↓_{Grec}, it must be the case that f ≠ Ω and, for every argument i that is tested by f, P_{i} ↓_{Grec}. By the inductive hypothesis, we may then assume that we have already constructed the set Der(P_{i}) for each such i. Note that this means that we have complete information about the transitions that are possible from every argument tested by any rule for f. We now stipulate that (a, Q) ∈ Der(P) iff there exist a rule r ∈ R_{G} for f of the form (1), and a substitution σ such that:

1. σ(x_{i}) = P_{i} for every i,

2. C[x⃗, y⃗]σ ≡ Q,

3. for every positive transition formula x_{i} →^{a_{ij}} y_{ij} in H, we have that (a_{ij}, σ(y_{ij})) ∈ Der(P_{i}), and

4. for every negative transition formula x_{i} ↛^{b_{ik}} in H, we have that for no

R, (b_{ik}, R) ∈ Der(P_{i}).

∗ Case P ≡ fix(X = R). As P ↓_{Grec}, it must be the case that

R{fix(X = R)/X} ↓_{Grec} .

By the inductive hypothesis, we may assume that we have already constructed the set Der(R{fix(X = R)/X}). We now stipulate that

Der(P) = Der(R{fix(X = R)/X}) .

It is immediate to see that, by construction, the transition relation for convergent terms defined above is indeed sound and supported. Moreover, it assigns a transition to a convergent recursion-free term iff →_{G} does.

– Step 2. Let O = {P →^{a}_{Grec} Q | P ↓_{Grec} and (a, Q) ∈ Der(P)}. The transition relation is extended to divergent terms as follows: For a divergent term P, the transition P →^{a}_{Grec} Q holds iff it has a proof with oracle O from G in the sense of Def. 4.2.

Again, the soundness and supportedness of the resulting transition relation is immediate by construction, and so is the agreement with →_{G} for recursion-free terms.

• Leastness of →_{Grec}. First of all, it is easy to show, by induction on the convergence predicate, that any sound and supported transition relation ⇒ must coincide with →_{Grec} for convergent processes, i.e., that for every convergent P, action a and Q ∈ CREC(Σ_{G}, PVar),

P →^{a}_{Grec} Q ⇔ P ⇒^{a} Q .

The leastness of →_{Grec} is then ensured by Step 2 of the above construction, and can be proven by a simple induction on the depth of the proof of transitions.

□

To exemplify the construction in the above proof on a pathological example, let us consider the term fix(X = odd(X)), where the operation odd is given by the rule:

\frac{x ↛^{a}}{odd(x) →^{a} δ}

This operation is standardly used in the literature to show that negative premises and unguarded recursive definitions can lead to inconsistent specifications. (See, e.g., [19]). The reason for this phenomenon is that, if we follow the standard GSOS approach, the equation

X = odd(X)  (7)

cannot have any solution. In fact, with the standard operational interpretation of GSOS systems and general transition system specifications with negative premises [35, 24], a process P solving the above equation would have to exhibit an a-transition iff it does not have one. In our approach, instead, the above equation has a unique solution modulo ∼. To see that this is indeed the case, note, first of all, that fix(X = odd(X)) is a divergent term. It is then easy to see that, because of our requirement that negative premises in rules be interpreted over convergent terms only, the above rule can never be applied to derive a transition for fix(X = odd(X)). Thus we have that this term has no transition and is divergent, i.e., that fix(X = odd(X)) ∼ Ω. It is easy to see that, modulo ∼, Ω is the unique solution of Eqn. (7).

When applied to the languages considered in [38, 92], the theory that we have so far presented delivers exactly the transition system semantics for SCCS and CCS given in those references.

With the above definitions, the operational semantics of a GSOS language with recursion CREC(Σ_{G}, PVar) is given by the lts with divergence

lts(G_{rec}) = (CREC(Σ_{G}, PVar), Act, →_{Grec}, ↑_{Grec}) .

This lts is in general neither finitely branching nor image finite [43]. For example, the term fix(X = a.δ∥X) in our running example has a countably infinite set of a-derivatives. However, the lts associated with a GSOS system with recursion is guaranteed to be weakly finitely branching in the sense of [1]. This is the import of the following result:

Proposition 4.4 (Weak Finite Branching) Let G be a GSOS system. Then, for every P ∈ CREC(Σ_{G}, PVar), P ↓_{Grec} implies Der(P) is finite.

Proof: By induction on the relation ↓_{Grec}. □

Fact 4.5 Let G be a GSOS system. Then equation (4) is sound with respect to ≲_{Grec}, i.e., for every P ∈ REC(Σ_{G}, PVar) containing at most X free,

fix(X = P) ∼_{Hrec} P {fix(X = P)/X} .

Because Act is assumed to be finite, the lts with divergence giving semantics to a GSOS system with recursion is a fortiori sort-finite. As a corollary of general results by Abramsky, we then have the following characterization of the finitary bisimulation preorder over lts(G_{rec}) for any GSOS language G:

Proposition 4.6 Let G be a GSOS system. Then the preorders ≲^{F} and ≲_{ω} coincide over lts(G_{rec}).

Proof: By Proposition 4.4, the lts (CREC(Σ_{G}, PVar), Act, →_{Grec}, ↑_{Grec}) is weakly finitely branching. By [1, Prop. 5.23], any weakly finitely branching lts satisfies Abramsky’s axiom scheme of bounded non-determinacy (BN) (cf. [1, Page 193]). The claim then follows immediately by [1, Prop. 6.13], as our lts is sort-finite. □

We end this section with a result showing that prebisimulation is preserved by recursion. The techniques that we shall employ are modifications of those developed by Milner [62, 64] and adapted by Walker to the setting of prebisimulation [92].

Definition 4.7 Let P, Q ∈ REC(Σ_{G}, PVar) contain at most X_{1}, …, X_{n} as free variables. Then P ≲_{Grec} Q iff, for every vector of programs R_{1}, …, R_{n} ∈ CREC(Σ_{G}, PVar),

P {R_{1}/X_{1}, …, R_{n}/X_{n}} ≲_{Grec} Q{R_{1}/X_{1}, …, R_{n}/X_{n}} .

Theorem 4.8 Let G be a GSOS system. Let P, Q ∈ REC(Σ_{G}, PVar) contain at most X as a free variable. Then P ≲_{Grec} Q implies that fix(X = P) ≲_{Grec} fix(X = Q).

Proof: (Following Milner.) Let P, Q ∈ REC(Σ_{G}, PVar) contain at most X as a free variable, and assume that P ≲_{Grec} Q. To prove that fix(X = P) ≲_{Grec} fix(X = Q), it is sufficient to show that the relation

R= {(E{fix(X = P)/X}, E{fix(X = Q)/X}) | E contains at most X free}

is a prebisimulation up to ≲_{Grec}. For then, by taking E ≡ X, it follows by Lemma 2.7 that fix(X = P) ≲_{Grec} fix(X = Q). We remark here that, by definition, the relation R is closed with respect to Σ_{G}-contexts.

To prove that the relation R is a bisimulation up to ≲_{Grec}, it is sufficient to show that, for every pair of closed terms (E{fix(X = P)/X}, E{fix(X = Q)/X}) ∈R, the following three claims hold:

1. If E{fix(X = P)/X} →^{a}_{Grec} P′, then there exist Q′, Q′′ such that

E{fix(X = Q)/X} →^{a}_{Grec} Q′′ and P′ R Q′ ≲_{Grec} Q′′;

2. If E{fix(X = P)/X} ↓_{Grec} then E{fix(X = Q)/X} ↓_{Grec}; and

3. If E{fix(X = P)/X} ↓_{Grec}, E{fix(X = Q)/X} ↓_{Grec} and E{fix(X = Q)/X} →^{a}_{Grec}

Q′, then there exist P′, P′′ such that

E{fix(X = P)/X} →^{a}_{Grec} P′′ and P′′ ≲_{Grec} P′ R Q′.

To prove that these claims do hold, we proceed as follows. First of all, we establish their validity for convergent terms simultaneously by induction on the convergence predicate. This will prove claims 2 and 3. We then prove that claim 1 holds for all terms by induction on the proof of the transition E{fix(X = P)/X} →^{a}_{Grec} P′. This part of the proof uses the validity of claims 2 and 3 for convergent terms.

• Proof of the claims for convergent terms. Assume that E{fix(X = P)/X} ↓_{Grec}. We show that claims 1–3 above hold simultaneously by induction on the convergence predicate.

– Proof of claim 1. Assume that E{fix(X = P)/X} →^{a}_{Grec} P′ and E has at most X free. We prove that, for some Q′, Q′′, E{fix(X = Q)/X} →^{a}_{Grec} Q′′ and P′ R Q′ ≲_{Grec} Q′′ arguing by cases on the form E takes.

∗ Case E ≡ X. In this case, by the definition of the convergence predicate, it follows that E{fix(X = P)/X} ≡ fix(X = P) ↓_{Grec} because P {fix(X = P)/X} ↓_{Grec}. By the operational semantics,

E{fix(X = P)/X} ≡ fix(X = P) →^{a}_{Grec} P′

because P {fix(X = P)/X} →^{a}_{Grec} P′. As P has at most X free, we can now apply the inductive hypothesis for claim 1 to derive that, for some

Q′, Q^{∗}, P {fix(X = Q)/X} →^{a}_{Grec} Q^{∗} and P′ R Q′ ≲_{Grec} Q^{∗}. As P ≲_{Grec}

Q, it follows that, in particular,

P {fix(X = Q)/X} ≲_{Grec} Q{fix(X = Q)/X} .

Thus there exists Q′′ such that Q{fix(X = Q)/X} →^{a}_{Grec} Q′′ and Q^{∗} ≲_{Grec} Q′′. By the definition of the operational semantics and the transitivity of

≲_{Grec}, we then have that fix(X = Q) →^{a}_{Grec} Q′′ and P′ R Q′ ≲_{Grec} Q′′.

∗ Case E ≡ f(E⃗). In this case, by the definition of the convergence predicate, we have that E{fix(X = P)/X} ≡ f(E⃗{fix(X = P)/X}) ↓_{Grec} because f ≠ Ω and E_{i}{fix(X = P)/X} ↓_{Grec} for every argument i tested by f. Assume now that E{fix(X = P)/X} →^{a}_{Grec} P′. By the definition of the transition relation, this is because there exist a rule r of the form (1) and a substitution σ : Var → CREC(Σ_{G}, PVar) such that:

· for every 1 ≤ i ≤ l, σ(x_{i}) = E_{i}{fix(X = P)/X},

· for every 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, E_{i}{fix(X = P)/X} →^{a_{ij}}_{Grec} σ(y_{ij}),

· for every 1 ≤ i ≤ l with n_{i} > 0, E_{i}{fix(X = P)/X} ↓_{Grec} and, for

1 ≤ k ≤ n_{i}, E_{i}{fix(X = P)/X} ↛^{b_{ik}}_{Grec}, and, finally,

· P′ ≡ C[E⃗{fix(X = P)/X}, σ(y⃗)], where we use σ(y⃗) to stand for the vector of the σ(y_{ij})s.

We aim at using the same rule r to find the required matching transition from E{fix(X = Q)/X}. First of all, note that each E_{i} has at most X free. Moreover, for every argument i that is tested by f, E_{i}{fix(X = P)/X} ↓_{Grec}. We may thus apply the inductive hypothesis for claim 1 to infer that, for every 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, there exist closed terms Q′_{ij}, Q′′_{ij} such that

E_{i}{fix(X = Q)/X} →^{a_{ij}}_{Grec} Q′′_{ij} and σ(y_{ij}) R Q′_{ij} ≲_{Grec} Q′′_{ij} . (8)

An application of the inductive hypothesis for claims 2 and 3 allows us to derive that, for every 1 ≤ i ≤ l with n_{i} > 0, and 1 ≤ k ≤ n_{i},

E_{i}{fix(X = Q)/X} ↓_{Grec} and E_{i}{fix(X = Q)/X} ↛^{b_{ik}}_{Grec} . (9)

Thus, by the definition of the transition relation, (8) and (9), rule r gives that

E{fix(X = Q)/X} →^{a}_{Grec} C[E⃗{fix(X = Q)/X}, Q⃗′′] .

By setting

Q′ ≡ C[E⃗{fix(X = Q)/X}, Q⃗′]
Q′′ ≡ C[E⃗{fix(X = Q)/X}, Q⃗′′]

we now have that:

P′ R Q′ (R is substitutive)
≲_{Grec} Q′′ (Thm. 3.9)

The proof for this case is then complete.

∗ Case E ≡ fix(Y = F), for some F with at most X and Y free. The claim is trivially seen to hold if X = Y, as in this case X is not free in E. Assume then that X ≠ Y, that E{fix(X = P)/X} ↓_{Grec} and E{fix(X = P)/X} →^{a}_{Grec} P′. By the definition of the convergence predicate and simple properties of substitution, we have that

F {E/Y }{fix(X = P)/X} ↓_{Grec}

by a shorter inference. Similarly, by the definition of the transition relation, we have that

F {E/Y }{fix(X = P)/X} →^{a}_{Grec} P′ .  (10)

Note now that the term F {E/Y } has at most X free. An application of the inductive hypothesis for claim 1 to (10) now gives that there exist Q′, Q′′ such that

F {E/Y }{fix(X = Q)/X} →^{a}_{Grec} Q′′ and P′ R Q′ ≲_{Grec} Q′′ .

By the definition of the transition relation and simple properties of substitution, it then follows that

E{fix(X = Q)/X} →^{a}_{Grec} Q′′ .

This completes the proof of claim 1 for convergent processes.

– Proof of claim 2. Assume that E{fix(X = P)/X} ↓_{Grec} and E has at most X free. We prove that E{fix(X = Q)/X} ↓_{Grec} arguing by cases on the form E takes. The proof is straightforward and we only give one case as an example.

∗ Case E ≡ X. We argue as follows:

E{fix(X = P)/X} ↓_{Grec} ⇔ fix(X = P) ↓_{Grec}

(E ≡ X)

⇔ P {fix(X = P)/X} ↓_{Grec}

(Definition of ↓_{Grec})

⇒ P {fix(X = Q)/X} ↓_{Grec}

(By induction)

⇒ Q{fix(X = Q)/X} ↓_{Grec}

(P ≲_{Grec} Q)

⇔ fix(X = Q) ↓_{Grec}

(Definition of ↓_{Grec})

⇔ E{fix(X = Q)/X} ↓_{Grec}

(E ≡ X)

– Proof of claim 3. Similar to the proof for claim 1.

• Proof of claim 1 for all closed terms. We now show that claim 1 holds for all closed terms by induction on the proof of the transition E{fix(X = P)/X} →^{a}_{Grec} P′. The proof proceeds by cases on the form of E, and the details are very similar to those of the proof of claim 1 for convergent processes spelled out above. The interested reader will have no difficulty in filling the details.

□

By Thm. 4.8 and an easy adaptation of the proof of Thm. 3.9 to CREC(Σ_{G}, PVar), we then have that:

Corollary 4.9 Let G be a GSOS system. Then ≲_{Grec} is a precongruence over the language CREC(Σ_{G}, PVar).

5 Background on Denotational Semantics

In this section, we review the basic notions of algebraic semantics and domain theory that will be needed in the remainder of this study. The interested reader is invited to consult, e.g., [29, 33, 37, 41, 67, 69, 1, 84] for more details and extensive motivation.

5.1 Preliminaries on Algebraic Semantics

We assume that the reader is familiar with the basic notions of ordered and continuous algebras (see, e.g., [37, 41, 47]); however, in what follows we give a quick overview of the way a denotational semantics can be given to a recursive language like REC(Σ_{G}, PVar) following the standard lines of algebraic semantics [37]. The interested reader is invited to consult [41] for an explanation of the theory.

In what follows, we let Σ denote a signature in the sense of Sect. 3. A Σ-algebra is a pair (A, Σ_{A}), where A is the carrier set and Σ_{A} is a set of operators f_{A} : A^{l} → A, where f ∈ Σ and l = arity(f). We call f_{A} the interpretation of the function symbol f in the structure A. Let (A, Σ_{A}) and (B, Σ_{B}) be Σ-algebras. A mapping φ : A → B is a Σ-homomorphism if it preserves the Σ-structure, i.e., if for every f ∈ Σ and vector a⃗ of elements of A of the appropriate length:

φ(f_{A}(a⃗)) = f_{B}(φ(a⃗)) .

The term algebra T(Σ) is the initial Σ-algebra, i.e., if (A, Σ_{A}) is a Σ-algebra then there is a unique Σ-homomorphism ι_{A} : T(Σ) → A. We refer to this homomorphism as the interpretation of T(Σ) in A.

A Σ-domain (A, ⊑_{A}, Σ_{A}) is a Σ-algebra whose carrier (A, ⊑_{A}) is an algebraic complete partial order (cpo) (see, e.g., [69]) and whose operations are interpreted as continuous functions. The notion of Σ-poset (respectively Σ-preorder) may be defined in a similar way by requiring that (A, ⊑_{A}) be a partially ordered (resp. preordered) set and that the operators be monotonic. The notion of Σ-homomorphism extends to the ordered Σ-structures in the obvious way by requiring that such maps preserve the underlying topological structure as well as the Σ-structure.

For any Σ-structure A, be it ordered or not, the set [PVar → A] of A-environments will be denoted by ENV_{A}, and ranged over by the meta-variable ρ. The (unique) interpretation of T(Σ, PVar) in A is the mapping A[[·]] : T(Σ, PVar) → [ENV_{A} → A] defined recursively by:

A[[x]]ρ =^{Δ} ρ(x)
A[[f(P_{1}, …, P_{l})]]ρ =^{Δ} f_{A}(A[[P_{1}]]ρ, …, A[[P_{l}]]ρ)

If A is a Σ-domain the interpretation extends to the set REC(Σ, PVar) of recursive terms over Σ by setting

A[[fix(X = P)]]ρ =^{Δ} Yλa. A[[P]]ρ[X → a]

where Y denotes the least fixed-point operator. As usual, ρ[X → a] denotes the environment which is defined as follows:

ρ[X → a](Y) =^{Δ} \{ \begin{matrix}a & if X = Y \\ ρ(Y) & otherwise \end{matrix}

Note that, for each closed recursive term P ∈ CREC(Σ, PVar), A[[P]]ρ does not depend on the environment ρ. The denotation of a closed term P will be denoted by A[[P]].

In what follows, we shall make use of some general results about the semantic mappings defined above, which may be found in [29, 37, 41]. The first states that for any P ∈ REC(Σ, PVar) there is a sequence of finite approximations P^{n} ∈ T(Σ, PVar) (n ∈ ℕ) such that, for any Σ-domain A,

A[[P]] = ⨆_{n≥0}A[[P^{n}]] .  (11)

The second states that there is a syntactically defined relation between P and every finite approximation P^{n}. Let ≤_{Ω} be the least Σ-precongruence which satisfies Eqn. 4 and the inequation

Ω ≤ X .  (12)

Then, for every n ≥ 0, P^{n} ≤_{Ω} P. (Note that the relation ≤_{Ω} is contained in the behavioural preorders ≲ and ≲_{ω}.)

For any binary relation R over CREC(Σ, PVar), the algebraic part of R, denoted by R^{A}, is defined as follows [41]:

P R^{A} Q ⇔ ∀n∃m. P^{n} R Q^{m} .

We say that R is algebraic iff R=R^{A}. Intuitively, a relation is algebraic if it is completely determined by how it behaves on recursion-free terms. Every denotational interpretation A[[·]] induces a preorder ⊑_{A} over terms by:

P ⊑_{A} Q ⇔ A[[P]] ⊑_{A} A[[Q]] .

The following result characterizes a class of denotational interpretations which induce relations over terms that are algebraic.

Lemma 5.1 Let A be a Σ-domain. Then the following statements hold:

1. For all P, Q ∈ CREC(Σ, PVar), P ⊑_{A}^{A} Q implies P ⊑_{A} Q.

2. Assume that, for every P ∈ T(Σ), A[[P]] is a compact element in A. Then ⊑_{A} is algebraic.

Proof: Let Σ be a signature, and A be a Σ-domain. We prove the two statements separately.

1. Let P, Q ∈ CREC(Σ, PVar) and assume that P ⊑_{A}^{A} Q. We prove that P ⊑_{A} Q as follows:

P ⊑_{A}^{A} Q ⇔ ∀n ≥ 0∃m ≥ 0 : P^{n} ⊑_{A} Q^{m}  (By the definition of ⊑_{A}^{A})
⇔ ∀n ≥ 0∃m ≥ 0 : A[[P^{n}]] ⊑_{A} A[[Q^{m}]] (By the definition of ⊑_{A})
⇒^{1} ∀n ≥ 0 : A[[P^{n}]] ⊑_{A} ⨆_{m≥0}A[[Q^{m}]]
⇔ ⨆_{n≥0}A[[P^{n}]] ⊑_{A} ⨆_{m≥0}A[[Q^{m}]]
⇔ A[[P]] ⊑_{A} A[[Q]]  (By Eqn. (11))
⇔ P ⊑_{A} Q.

2. To prove this statement we note that if A[[P^{n}]] is a compact element in A then the implication ⇒^{1} in the proof above may be replaced by a bi-implication, ⇔.

□

In view of the above general lemma, the relations over terms induced by a denotational semantics are always algebraic, provided that the denotations of recursion-free terms are compact elements in the cpo A. We shall make use of this fact in the technical developments to follow.

5.2 A Domain Equation for Synchronization Trees

In this section we recall Abramsky’s domain equation for synchronization trees, and introduce the background in domain theory that is necessary to understand the paper. The interested reader is referred to, e.g., [69, 84, 37, 41, 85] for more general information on the theory of domains and denotational semantics, and to [1, Sect. 3] for a quick reference to some of the results mentioned in this section.

The canonical domain we shall use to give a denotational semantics to a class of GSOS languages is the domain of synchronization trees over a countable set of labels Lab considered by Abramsky in his seminal paper [1]. This is defined to be the initial solution D(Lab) in the category SFP (cf. [67]) of the domain equation

D(Lab) = (1)_{⊥} ⊕ P [ ∑_{ℓ∈Lab} D(Lab)]  (13)

where 1 is the one point domain, (·)_{⊥} is lifting, ⊕ is coalesced sum, ∑ is separated sum, and P [D] denotes the Plotkin powerdomain of D (cf. [67, 69] for details on these domaintheoretic operations). We henceforth omit the parameter Lab as it will be always clear from the context.

To streamline the presentation and make our results more accessible to uninitiated readers, in this study we shall abstract completely from the domain-theoretic description of D given by (13). Our description of the domain of synchronization trees D will follow the one given in [47], and we shall rely on results presented in that reference that show how to construct D starting from a suitable preorder on the set of finite synchronization trees ST(Lab). Our reconstruction of D will be given in three steps:

1. First of all, we shall define a preorder ⊑ on the set of finite synchronization trees ST(Lab). This preorder will be a reformulation of the Egli-Milner preorder over ST(Lab) presented in [47]. (See Fact 5.5 below.)

2. Secondly, we shall relate the poset of compact elements of D to the poset of equivalence classes induced by (ST(Lab), ⊑).

3. Finally, we shall use the fact that D is the ideal completion of its poset of compact elements to relate it to (ST(Lab), ⊑).

The approach outlined above will allow us to factor the definition of the continuous algebra structure [33, 37, 41] on D given in Sect. 5 in three similar steps, hopefully making it simpler to understand.

Definition 5.2 We define ⊑ as the least binary relation over ST(Lab) satisfying:

t ⊑ u if (1) ⟨ℓ, t′⟩ ∈ t ⇒ ∃⟨ℓ, u′⟩ ∈ u : t′ ⊑ u′ and
(2) ⊥ ∈ u ⇒ ⊥ ∈ t and
(3) ⟨ℓ, u′⟩ ∈ u ⇒ (⊥ ∈ t or ∃⟨ℓ, t′⟩ ∈ t : t′ ⊑ u′)

The relation ⊑ so defined is easily seen to be a preorder over ST(Lab). Its kernel will be denoted by ≃. Moreover, it has the following useful property:

Fact 5.3 For all t, u ∈ ST(Lab), t ⊑ u iff t ≲ u.

Proof: The “only if” implication follows because ≲ satisfies the defining constraints of ⊑, and ⊑ is the smallest such relation. The proof of the “if” implication is an easy induction on the combined size of the trees t and u. □

Definition 5.4 (ST(Lab)/ ≃, ⊑_{≃}) stands for the poset whose elements are ≃-equivalence classes of synchronization trees (denoted by [t]), and whose partial ordering ⊑_{≃} is given by:

[t] ⊑_{≃} [u] ⇔ t ⊑ u .

We can now relate the preorder of synchronization trees (ST(Lab), ⊑) with the poset of compact elements of D in a way that will allow us to define, in a canonical way, continuous operations on D from monotonic ones on (ST(Lab), ⊑).

First of all, we recall from [1] that D is, up to isomorphism, the algebraic complete partial order (cpo) whose poset of compact elements (K(D), ⊑_{K(D)}) is given in [1] by:

• K(D) is defined inductively as follows:

– ∅ ∈ K(D)

– {⊥} ∈ K(D)

– ℓ ∈ Lab, d ∈ K(D) ⇒ {⟨ℓ, d⟩} ∈ K(D)

– d_{1}, d_{2} ∈ K(D) ⇒ Con(d_{1}∪d_{2}) ∈ K(D), where Con denotes the convex closure operation (see, e.g., [1, page 170]);

• ⊑_{K(D)} is defined by:

d ⊑_{K(D)} e ⇔ d = {⊥} or d ⊑_{EM} e

where ⊑_{EM} denotes the standard Egli-Milner ordering (see, e.g., [1, Def. 3.3]).

From the above definitions, it follows that K(D) is a subset of the set of finite synchronization trees ST(Lab). Hence it makes sense to compare the relations ⊑ and ⊑_{K(D)} over it. The following small result lends credence to our previous claims:

Fact 5.5 For all d, e ∈ K(D), d ⊑ e iff d ⊑_{K(D)} e.

Proof: From Abramsky’s results (see [1, Prop. 3.11]), we have that D is “internally fully abstract”, i.e., that for all d_{1}, d_{2} ∈ D,

d_{1} ≲ d_{2} ⇔ d_{1} ⊑_{D} d_{2} .

The result now follows from Fact 5.3 and the fact that each compact element of D is in ST(Lab). □ As a consequence of this result, to ease the presentation of the technical results to follow, from now on we shall always use ⊑ as our notion of preorder on K(D). Using it, we may rephrase the definition of convex-closure of a synchronization tree as follows: Fact 5.6 Let t = {⟨ℓ_{i}, t_{i}⟩ | 1 ≤ i ≤ n}[∪{⊥}] be a synchronization tree in ST(Lab). Then its convex-closure Con(t) is given by:

• ⊥ ∈ Con(t) iff ⊥ ∈ t;

• ⟨ℓ, t′⟩ ∈ Con(t) iff one of the following holds: – there exist ⟨ℓ_{i}, t_{i}⟩, ⟨ℓ_{j}, t_{j}⟩ ∈ t such that ℓ_{i} = ℓ_{j} = ℓ and t_{i} ⊑ t′ ⊑ t_{j}; or – ⊥ ∈ t and, for some ⟨ℓ_{i}, t_{i}⟩ ∈ t, ℓ_{i} = ℓ and t′ ⊑ t_{i}.

For a synchronization tree t = {⟨ℓ_{i}, t_{i}⟩ | 1 ≤ i ≤ n}[∪{⊥}], its recursive convex-closure t^{c} is inductively defined as follows:

t^{c} =^{Δ} Con({⟨ℓ_{i}, t_{i}^{c}⟩ | 1 ≤ i ≤ n}[∪{⊥}]) .  (14)

It is not difficult to see that, for every t ∈ ST(Lab), t^{c} is a compact element of D. Moreover, the function (·)^{c} : (ST(Lab), ⊑) → (K(D), ⊑) enjoys the following properties: Lemma 5.7

1. For every t ∈ ST(Lab), t ≃ t^{c}.

2. For all t, u ∈ ST(Lab), t ⊑ u iff t^{c} ⊑ u^{c}.

3. For all t, u ∈ ST(Lab), t ≃ u iff t^{c} = u^{c}, i.e., t^{c} and u^{c} are equal as sets.

4. For all t ∈ ST(Lab), t^{c} = (t^{c})^{c}. As an immediate consequence of the lemma above we have the following: Corollary 5.8 The poset (ST(Lab)/ ≃, ⊑_{≃}) is isomorphic to (K(D), ⊑_{K(D)}) under the isomorphism given by φ([t]) = t^{c}. Assume now that fST : (ST(Lab), ⊑)^{l} → (ST(Lab), ⊑) is a monotonic function. We may naturally use fST to define a function f_{K(D)} : (K(D), ⊑)^{l} → (K(D), ⊑) as follows:

f_{K(D)}(t⃗^{c}) =^{Δ} (fST(t⃗))^{c} .  (15)

It is easy to see that the function is well defined in this way. To see that it is monotonic, assume that t⃗^{c} ⊑ u^{c}. Then:

t⃗^{c} ⊑ u^{c} ⇔ t⃗ ⊑ u⃗  (Lem. 5.7(2))
⇒ fST(t⃗) ⊑ fST(u⃗)  (fST is monotonic)
⇔ (fST(t⃗))^{c} ⊑ (fST(u⃗))^{c} (Lem. 5.7(2))
⇔ f_{K(D)}(t⃗^{c}) ⊑ f_{K(D)}(u^{c}) (15)

In what follows we refer to the function f_{K(D)} defined above as fST^{c}. We extend this notation to a set of operators Σ_{ST(Lab)} in the standard way.

An easy consequence of the previous theory is that, for any signature Σ, Eqn. (15) can be used to induce a Σ-poset structure on the poset of compact elements from a Σ-preorder structure on finite synchronization trees. This is formalized in the following result, that also relates the unique meaning maps from T(Σ) to the resulting algebraic structures, denoted by ST[[·]] and K(D)[[·]] respectively.

Corollary 5.9 For any signature Σ, if (ST(Lab), ⊑, Σ_{ST(Lab)}) is a Σ-preorder then (K(D), ⊑_{K(D)}, Σ_{ST(Lab)}^{c}) is a Σ-poset. Moreover, for every P ∈ T(Σ),

K(D)[[P]] = (ST[[P]])^{c}.

Proof: The first statement follows immediately from the previous theory. The second follows from the initiality of T(Σ), because the mappings K(D)[[cot]] and (·)^{c} ∘ ST[[·]] are both Σ-homomorphisms. □

The corollary above implies that we can lift any Σ-preorder structure on (ST(Lab), ⊑) to a Σ-poset structure on (K(D), ⊑), in the sense of [41], in a canonical way. In Sect. 6.2 we shall take advantage of this fact. Finally, from the theory of powerdomains [67, 81, 47], we know that the domain of synchronization trees D is, up to isomorphism, the ideal completion of the poset of compact elements K(D). As a result of this observation, we can extend any monotonic function f_{K(D)} : (K(D), ⊑)^{l} → (K(D), ⊑) to a continuous function f_{D} : (D, ⊑_{D})^{l} → (D, ⊑_{D}) by:

f_{D}(k⃗) =^{Δ} ⨆{f_{K(D)}(d⃗) | d⃗ ∈ K(D) and d⃗ ⊑_{D} k⃗} .  (16)

The interested reader is invited to consult, e.g., [41, sect. 3.3] for a discussion of the properties afforded by this canonical extension. Thus (16) can be used to conservatively extend any Σ-poset algebra structure on (K(D), ⊑) to a continuous algebra structure on D, in the sense of [33, 37, 41].

6 Denotational Semantics for Compact GSOS Languages with Recursion

In this section we shall present a general technique to give denotational semantics in terms of the Plotkin powerdomain of synchronization trees (see Sect. 5.2) for a class of GSOS languages with recursion. The denotational semantics will be guaranteed to be fully abstract, in the sense of Milner and Plotkin [56, 57, 68, 85], with respect to the finitary part of the prebisimulation relation. The languages that we shall consider have the structure of most standard process calculi (see, e.g., [64, 46, 17, 11]); they will consist of a set of operations to build finite, acyclic labelled transition systems and a facility for recursive definitions of behaviours. Thus we shall consider GSOS languages with recursion in which infinite behaviours can only be defined by means of recursive definitions.

6.1 Compact GSOS Systems

The following notion from [7] will allow us to pin down precisely a class of GSOS operations that map finite processes to finite processes. The semantic counterparts of these operations will have the property of being compact in the sense of [47], i.e., of mapping compact elements in the Plotkin powerdomain of synchronization trees to compact elements. In view of Lem. 5.1, denotational interpretations for the resulting languages will induce algebraic preorders over terms.

Definition 6.1 A GSOS rule of the general form (1) is linear if each variable occurs at most once in the target and, for each argument i that is tested positively, x_{i} does not occur in the target and at most one of the y_{ij}’s does. An operation from a GSOS system G is linear iff all rules for it are linear. Finally, G itself is linear iff it only contains linear rules.

The format of linear rules is a restriction of the general GSOS format in that no copying of arguments is allowed and no argument for which there is a positive antecedent may appear in the target of a rule. Moreover, there may be possibly many positive antecedents for an argument x_{i} in a rule, but at most one of the y_{ij}’s may appear in its target. As far as we know, all the operations occurring in the standard process algebras are linear. An example of a non-linear operation is the Kleene star operation [51] given by the rules (one pair of rules for each a ∈ Act):

\frac{x →^{a} x′}{x^{∗}y →^{a} x′; (x^{∗}y)}  \frac{y →^{a} y′}{x^{∗}y →^{a} y′}

Modulo a different treatment of termination, these rules may be found in [18], where the Kleene star operation is considered in the setting of ACP.

Definition 6.2 ([7]) A GSOS system G is syntactically well-founded iff there exists a function w from operation symbols in Σ_{G} to natural numbers such that, for each rule r ∈ R_{G} with principal operation symbol f and target C[x⃗, y⃗] the following conditions hold:

• if r has no positive antecedents then W (C[x⃗, y⃗]) < w(f), and

• W (C[x⃗, y⃗]) ≤ w(f) otherwise,

where W : (Σ_{G}) → ℕ is given by

\begin{matrix}W (x) & =^{Δ} & 0 \\ W (f(P_{1}, …, P_{l})) & =^{Δ} & w(f) + W (P_{1}) + ⋯ + W (P_{l}). \end{matrix}

For example, the GSOS system in Fig. 1 is linear and syntactically well-founded. In fact, it is sufficient to assign weight 1 to the action prefixing operations and weight 0 to all the other operations. On the other hand, no GSOS system containing a constant a^{ω} with rule

\overline{a^{ω} →^{a} a^{ω}}  (17)

can be syntactically well-founded. Syntactic well-foundedness is decidable over GSOS systems (cf. [7, Thm. 6.8]), and, for linear GSOS systems, it is sufficient to guarantee that terms are semantically well-founded in the sense of [7].

Definition 6.3 (Compact GSOS Systems) A GSOS system is said to be compact iff it is linear and syntactically well-founded.

An example of a compact GSOS system is our running example, the language preACP_{Ωθ} in Fig. 1. Other examples are the finite alphabet versions of standard process algebras like CCS [64], CSP [46] and ACP [17]. The following proposition, that can be proven following the lines of [7, Prop. 6.7], states the key property of compact GSOS systems, namely that no term in a compact GSOS system exhibits infinite derivations.

Proposition 6.4 Let G be a compact GSOS system. Then G is well-founded, i.e., for every P ∈ T(Σ_{G}) there exists no infinite sequence P_{0}, a_{0}, P_{1}, a_{1}, P_{2}, … of terms in T(Σ_{G}) and actions in Act with P ≡ P_{0} and P_{i} →^{a_{i}}_{G} P_{i+1} for all i ≥ 0.

As an immediate corollary of the above result and of Lem. 3.8, if G is a compact GSOS system, then we can unfold the finite, acyclic process graph giving the operational semantics of a term P ∈ T(Σ_{G}) to obtain that:

Corollary 6.5 Let G be a compact GSOS system. Then, for every P ∈ T(Σ_{G}), there exists a synchronization tree t_{P} ∈ ST(Act) such that P ∼ t_{P}.

In what follows, we shall give a denotational semantics for GSOS systems with recursion built on top of compact GSOS systems. In view of Cor. 5.9, in order to endow D with a structure of a continuous (aka complete ordered Σ_{G}-magma or Σ_{G}-cpo) algebra [29, 33, 37, 41], it is sufficient to define a monotonic Σ-structure on ST(Act). An interpretation for the GSOS language with recursion CREC(Σ_{G}, PVar) built on top of G can then be given in standard fashion, and will be shown to induce a fully abstract semantics for CREC(Σ_{G}, PVar) with respect to ≲_{ω}.

6.2 A Fully Abstract Denotational Semantics for Compact GSOS Systems

We shall now present a general method to give a denotational semantics in terms of the Plotkin powerdomain of synchronization trees to compact GSOS systems. We shall then show how to extend the results in this section to GSOS languages with recursion built on top of such systems.

Let G be a compact GSOS language. We shall now give a way of defining, for each Σ_{G}-context C[x⃗], a function CST over ST(Act) of the appropriate arity. The definition of CST will be given using the rules in R_{G} as a guideline. First of all, note that it is sufficient to define semantic operations fST for each f ∈ Σ_{G}, as derived semantic operations can then be obtained by function composition. The definition of the functions fST is given by the inductive construction in Def. 6.9. Intuitively, the inductive construction of the synchronization tree fST(t⃗) given in Def. 6.9 is well-founded because, by the compactness of G, whenever the premises of a rule of the form (1) can be met by a vector of finite synchronization trees t⃗, then either the weight of C[x⃗, y⃗] is strictly smaller than that of f, or the weight of C[x⃗, y⃗] is the same as that of f, and the sum of the sizes of the arguments of CST has decreased.

Before presenting the inductive definition of the synchronization tree fST(t⃗), we now put the intuitive justification of its well-foundedness on firmer ground. First of all, we associate with a class of relevant Σ_{G}-contexts of the form C[x⃗] a measure of the complexity of the synchronization tree CST[t⃗], where t⃗ is a vector of synchronization trees of the appropriate length.

Definition 6.6 The height of a synchronization tree t = {⟨a_{1}, t_{1}⟩, …, ⟨a_{n}, t_{n}⟩}[∪{⊥}] ∈ ST(Act) is inductively defined by

ht({⟨a_{1}, t_{1}⟩, …, ⟨a_{n}, t_{n}⟩}[∪{⊥}]) = sup {ht(t_{i}) | 1 ≤ i ≤ n} + 1 .

Definition 6.7 Let G be a compact GSOS system, and let w : Σ_{G} → ℕ be a weight function for G in the sense of Def. 6.2. For each Σ_{G}-context C[x⃗] in which each variable occurs at most once, and vector of synchronization trees t⃗ of the appropriate length we define the pair of natural numbers norm(C[x⃗], t⃗) as

norm(C[x⃗], t⃗) = (W (C[x⃗]), ∑ {ht(t_{i}) | x_{i} occurs in C[x⃗]}) .

Following [7, Prop. 6.7], it can now be shown that:

Proposition 6.8 Let G be a compact GSOS system. Then, for every rule r in R_{G} of the form (1), and vectors of trees t⃗ = t_{1}, …, t_{l}, u⃗ = u_{11} … u_{1m_{1}} … u_{l1} … u_{lm_{l}} such that, for all 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, ⟨a_{ij}, u_{ij}⟩ ∈ t_{i},

norm(C[x⃗, y⃗], t⃗u⃗) ≺ norm(f(x⃗), t⃗)

where ≺ denotes the lexicographic ordering over ℕ×ℕ, and t⃗u⃗ denotes the vector obtained by concatenating t⃗ and u⃗.

Proof: As G is compact, there exist functions w and W satisfying the requirements in Def. 6.2. We proceed to prove the claim by distinguishing two cases, depending on whether the rule r has positive hypotheses or not.

• If r has no positive premise, then, as G is syntactically well-founded, it follows that W (C[x⃗]) < w(f). The claim then follows immediately as w(f) = W (f(x⃗)).

• Assume that r has at least one positive premise of the form x_{i} →^{a_{ij}} y_{ij}. As for all 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, ⟨a_{ij}, u_{ij}⟩ ∈ t_{i}, it follows that ht(u_{ij}) < ht(t_{i}) for each such transition formula.

As G is syntactically well-founded, we have that W (C[x⃗, y⃗]) ≤ w(f) = W (f(x⃗)). We claim that the sum of the heights of the trees corresponding to variables occurring in C[x⃗, y⃗] is strictly smaller than the combined heights of the trees in the vector t⃗. To see that this is the case, let

k =^{Δ} ∑ {ht(t_{i}) | x_{i} occurs in C[x⃗, y⃗]} + ∑ {ht(u_{ij}) | y_{ij} occurs in C[x⃗, y⃗]} .

Then, we argue as follows:

k ≤ ∑_{{i|m_{i}>0}}[max_{1≤j≤m_{i}} ht(u_{ij})] + ∑_{{i|m_{i}=0}} ht(t_{i})

(by linearity of r)

< ∑_{{i|m_{i}>0}} ht(t_{i}) + ∑_{{i|m_{i}>0}} ht(t_{i})

(as ht(u_{ij}) < ht(t_{i}) for each x_{i} →^{a_{ij}} y_{ij}, using ∃i : m_{i} > 0)

= ∑_{{x_{i} | x_{i} occurs in f(x⃗)}} ht(t_{i}) .

This completes the proof of the claim. □

By the above result, we are now in a position to define, for each l-ary operation f in a compact GSOS system, the effect of applying the function fST : ST(Act)^{l} → ST(Act) to a vector of trees t⃗ by induction on the relation ≺ over the norm given in Def. 6.7. This is done in the following definition.

Definition 6.9 Let G = (Σ_{G}, R_{G}) be a compact GSOS system, and let f be an l-ary operation in Σ_{G}. We define the operation fST : ST(Act)^{l} → ST(Act) inductively by stipulating that, for every t_{1}, …, t_{l} ∈ ST(Act):

• ⊥ ∈ fST(t_{1}, …, t_{l}) iff f = Ω or there is an argument i for f such that f tests its i-th argument and ⊥ ∈ t_{i};

• ⟨c, t⟩ ∈ fST(t_{1}, …, t_{l}) iff there exist a rule for f of the form (1) and a vector of trees u⃗ = u_{11} … u_{1m_{1}} … u_{l1} … u_{lm_{l}} such that:

1. for all 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, ⟨a_{ij}, u_{ij}⟩ ∈ t_{i};

2. for all 1 ≤ i ≤ l with n_{i} > 0, ⊥ ∉ t_{i} and, for all 1 ≤ k ≤ n_{i}, ⟨b_{ik}, u⟩ ∈ t_{i} for no u ∈ ST(Act); and

3. CST[t⃗, u⃗] = t, where CST denotes the derived semantic operation associated with the Σ_{G}-context C[x⃗, y⃗]. If C[x⃗] is a variable x_{i}, then CST[t⃗] = t_{i}.

In the above definition, we have inductively defined the synchronization tree corresponding to fST(t⃗) assuming that we have already constructed the compact element CST[t⃗, u⃗] needed in clause 3 above. This is justified by Propn. 6.8.

The reader might wonder about the basis of our inductive construction of the synchronization tree CST[t⃗], i.e., about the results it produces when norm(C[x⃗], t⃗) = (0, 1). In this case, it is not difficult to see that CST[t⃗] is either the empty tree, or it is the completely unspecified tree {⊥}. To see that this is the case, note, first of all, that if C[x⃗] then either C[x⃗] is a variable x_{i}, or C[x⃗] = f(C_{1}[x⃗], …, C_{l}[x⃗]) for some operation f and contexts C_{1}[x⃗], …, C_{l}[x⃗] of zero weight. Let us examine the form the tree CST[t⃗] may take in these cases:

1. If C[x⃗] = x_{i}, then, as norm(C[x⃗], t⃗) = (0, 1), it must be the case that ht(t_{i}) = 1. There are only two trees with height 1, namely ∅ and {⊥}. Thus CST[t⃗] = t_{i} is of the postulated form in this case.

2. If C[x⃗] = f(C_{1}[x⃗], …, C_{l}[x⃗]), then, again as norm(C[x⃗], t⃗) = (0, 1), it must be the case that ht(t_{i}) = 1 for every x_{i} occurring in C[x⃗]. By structural induction this means that, for each 1 ≤ i ≤ l, C_{i}ST[t⃗] is either ∅ or {⊥}. Moreover, as G is syntactically well-founded and the context C[x⃗] has zero weight, f has no rule without positive antecedents. As every argument tested by f has no transition, it is then immediate to see that no rule for f can be applied to derive that a pair ⟨a, t⟩ ∈ CST[t⃗]. This again means that CST[t⃗] is either ∅ or {⊥}.

We hope that the above discussion makes the aforementioned inductive construction more understandable. The following example will, hopefully, also shed some light on it.

Example: When applied to the language preACP_{Ωθ}, the construction in Def. 6.9 produces the following functions:

• δST = ∅,

• ΩST = {⊥},

• for every t ∈ ST(Act), aST(t) = {⟨a, t⟩},

• for every t_{1}, t_{2} ∈ ST(Act), t_{1}+STt_{2} = t_{1} ∪ t_{2},

• for every t_{1}, t_{2} ∈ ST(Act), t_{1}∥STt_{2} is given by:

1. ⊥ ∈ t_{1}∥STt_{2} iff ⊥ ∈ t_{1} or ⊥ ∈ t_{2};

2. ⟨c, t⟩ ∈ t_{1}∥STt_{2} iff one of the following holds:

(a) there exists ⟨c, t′_{1}⟩ ∈ t_{1} such that t = t′_{1}∥STt_{2}, or

(b) there exists ⟨c, t′_{2}⟩ ∈ t_{2} such that t = t_{1}∥STt′_{2}, or

(c) there exist ⟨a, t′_{1}⟩ ∈ t_{1} and ⟨b, t′_{2}⟩ ∈ t_{2} such that c = γ(a, b) and t = t′_{1}∥STt′_{2}.

• for every t ∈ ST(Act), θST(t) is given by:

1. ⊥ ∈ θST(t) iff ⊥ ∈ t,

2. ⟨c, t_{1}⟩ ∈ θST(t) iff there exists ⟨c, t′⟩ ∈ t such that:

(a) either c is maximal in (Act, >) and θST(t′) = t_{1},

(b) or c is not maximal in (Act, >), for no action b > c and t_{2} ⟨b, t_{2}⟩ ∈ d, ⊥ ∉ t, and θST(t′) = t_{1}.

The reader familiar with [47] will notice the similarity of these definitions with those given in that reference. □

We shall now prove that the definition of the operations given in Def. 6.9 endows the preorder of synchronization trees ST(Act) with a Σ_{G}-preorder structure. To this end, it is sufficient to prove that each operation fST is monotonic with respect to the preorder ⊑.

Theorem 6.10 (Monotonicity) Let G be a compact GSOS system, and f be an l-ary operation in Σ_{G}. Then the function fST given by the construction in Def. 6.9 is monotonic with respect to ⊑.

Proof: We prove that for each Σ_{G}-context C[x⃗] in which each variable occurs at most once, and vectors of synchronization trees t⃗ and u⃗ of the appropriate length

t⃗ ⊑ u⃗ ⇒ CST[t⃗] ⊑ CST[u⃗] .  (18)

To show the above statement, we associate with each triple (C[x⃗], t⃗, u⃗) the pair of natural numbers

(W (C[x⃗]), ∑ {ht(t_{i}) + ht(u_{i}) | x_{i} occurs in C[x⃗]}) .

We then prove that (18) holds by well-founded induction on such pairs ordered lexicographically. Let us assume that (18) holds for every triple (D[y⃗], w⃗, v⃗) which is strictly smaller than (C[x⃗], t⃗, u⃗) with respect to our chosen notion of ordering. We then prove that, under this assumption, if t⃗ ⊑ u⃗, then CST[t⃗] ⊑ CST[u⃗]. In fact, it is easy to see that it is sufficient to prove that (18) holds when C[x⃗] = f(x⃗) as compositions of monotonic functions are monotonic.

In order to show that if t⃗ ⊑ u⃗, then fST(t⃗) ⊑ fST(u⃗), it is sufficient to establish the following claims:

1. if ⊥ ∈ fST(u⃗) then ⊥ ∈ fST(t⃗);

2. if ⟨c, t⟩ ∈ fST(t⃗) then ⟨c, u⟩ ∈ fST(u⃗), for some u ∈ ST(Act) such that t ⊑ u;

3. if ⟨c, u⟩ ∈ fST(u⃗), then either ⊥ ∈ fST(t⃗) or ⟨c, t⟩ ∈ fST(t⃗) for some t ∈ ST(Act) such that t ⊑ u.

We proceed by showing these three claims separately.

1. Assume that ⊥ ∈ fST(u⃗). By the definition of the function fST, this is because either f = Ω or there is an argument i for f such that f tests its i-th argument and ⊥ ∈ u_{i}. If f = Ω, then Def. 6.9 immediately gives that ⊥ ∈ fST(t⃗). Otherwise, assume that there is an argument i for f such that f tests its i-th argument and ⊥ ∈ u_{i}. As t_{i} ⊑ u_{i}, it follows that ⊥ ∈ t_{i}. Def. 6.9 then gives that ⊥ ∈ fST(t⃗).

2. Assume that ⟨c, t⟩ ∈ fST(t⃗). By Def. 6.9 this is because there exist a rule r for f of the form (1) and a vector of trees v⃗ = v_{11} … v_{1m_{1}} … v_{l1} … v_{lm_{l}} such that:

(a) for all 1 ≤ i ≤ l, 1 ≤ j ≤ m_{i}, ⟨a_{ij}, v_{ij}⟩ ∈ t_{i}; (b) for all 1 ≤ i ≤ l with n_{i} > 0, ⊥ ∉ t_{i} and, for all 1 ≤ k ≤ n_{i}, ⟨b_{ik}, v⟩ ∈ t_{i} for no

v ∈ ST(Act); and

(c) CST[t⃗, u⃗] = t, where CST denotes the derived semantic operation associated with the Σ_{G}-context C[x⃗, y⃗].

By (a) and (b) above, we have that:

• for every positive transition formula x_{i} →^{a_{ij}} y_{ij} in the antecedents of r, as t_{i} ⊑ u_{i},

it follows that ⟨a_{ij}, w_{ij}⟩ ∈ u for some w_{ij} such that v_{ij} ⊑ w_{ij};

• for every negative transition formula x_{i} ↛^{b_{ik}} in the antecedents of r, as t_{i} ⊑ u_{i}

and ⊥ ∉ t_{i}, it follows that ⊥ ∉ u_{i} and for no w ∈ ST(Act), ⟨b_{ik}, w⟩ ∈ u_{i}.

Thus rule r can be used, in conjunction with the vector of trees w⃗, to show that ⟨c, u⟩ ∈ fST(u⃗), where u = CST[u⃗, w⃗]. We are now left to prove that t ⊑ u. However, this follows immediately by the inductive hypothesis because, by linearity, C[x⃗, y⃗] is a context in which each variable occurs at most once, and, as G is compact, we have that either W (C[x⃗, y⃗]) < w(f), or r has at least one positive hypothesis, W (C[x⃗, y⃗]) ≤ w(f) and the sum of the heights of the arguments of C[x⃗, y⃗] has decreased. (Cf. Propn. 6.8).

3. Assume that ⟨c, u⟩ ∈ fST(u⃗) and that ⊥ ∉ fST(t⃗). Following the proof of the previous claim, we can then show that ⟨c, t⟩ ∈ fST(t⃗) for some t ∈ ST(Act) such that t ⊑ u. The details are omitted.

This completes the proof of (18). □

Because of the above result, the construction of Def. 6.9 allows us to define, for each operation symbol f in the signature of a compact GSOS system, a monotonic function fST over the preorder of finite synchronization trees ST(Act) of the appropriate arity. This is exactly what is needed to endow the preorder (ST(Act), ⊑) with the structure of a Σ_{G}-preorder. We now proceed to show that, for any compact GSOS system G, the denotational semantics induced by K(D)[[·]] for recursion-free terms in CREC(Σ_{G}, PVar) is fully abstract with respect to the bisimulation preorder, i.e., that, for all P, Q ∈ T(Σ_{G}),

P ≲ Q ⇔ K(D)[[P]] ⊑ K(D)[[Q]] .

First of all, we relate the operational semantics of recursion-free terms to the transition system view of ST(Act).

Lemma 6.11 Let G = (Σ_{G}, R_{G}) be a compact GSOS system. Then, for all P ∈ T(Σ_{G}), the following statements hold:

1. P ↓_{G} iff ST[[P]] ↓;

2. if P →^{a}_{G} Q then ST[[P]] →^{a} ST[[Q]];

3. if ST[[P]] →^{a} t then P →^{a}_{G} Q for some Q such that ST[[Q]] = t.

Proof: All the statements can be easily seen to hold by structural induction on P. Statements 2 and 3 must be proven simultaneously. The details are standard, and therefore we omit them. □

Proposition 6.12 Let G = (Σ_{G}, R_{G}) be a compact GSOS system. Then, for all P ∈ T(Σ_{G}), P ∼ ST[[P]].

Proof: Lemma 6.11 tells us that the symmetric closure of the relation

R= {(P, ST[[P]]) | P ∈ T(Σ_{G})}

is a prebisimulation. □

The results we have established so far allow us to prove that our denotational semantics is fully abstract with respect to the bisimulation preorder for recursion-free terms.

Theorem 6.13 (Full Abstraction for Recursion-free Terms) Let G be a compact GSOS system. Then, for all P, Q ∈ T(Σ_{G}), P ≲ Q iff K(D)[[P]] ⊑ K(D)[[Q]].

Proof: We reason as follows:

P ≲ Q ⇔ ST[[P]] ≲ ST[[Q]]  (Prop. 6.12)
⇔ ST[[P]] ⊑ ST[[Q]]  (Fact. 5.3)
⇔ (ST[[P]])^{c} ⊑ (ST[[Q]])^{c} (Lem. 5.7(2))
⇔ K(D)[[P]] ⊑ K(D)[[Q]] (Cor. 5.9)
□

Our aim in the remainder of this section will be to extend the above full abstraction result to the whole of CREC(Σ_{G}, PVar), for any compact GSOS system G. First of all, in order to define an interpretation of programs in CREC(Σ_{G}, PVar) as elements of D, we need to define a continuous Σ_{G}-algebra structure on D. As (D, ⊑_{D}) is, up to isomorphism, the unique algebraic cpo with (K(D), ⊑) as poset of compact elements, this is easily done by using Eqn. (16) to define a continuous function f_{D} for each f ∈ Σ_{G}. By the general theory of algebraic semantics (see, e.g., [41]), we then have that, for all P, Q ∈ T(Σ_{G}),

D[[P]] ⊑_{D} D[[Q]] ⇔ K(D)[[P]] ⊑ K(D)[[Q]] .  (19)

In view of Thm. 6.13, our desired full abstraction result will follow if we prove that the behavioural preorder ≲_{ω} is algebraic. This is because, from Lem. 5.1 and the fact that, by our constructions, each term P ∈ T(Σ_{G}) is interpreted as a compact element of D, the relation ⊑_{D} is algebraic, and two algebraic relations that coincide over T(Σ_{G}) do, in fact, coincide over the whole of CREC(Σ_{G}, PVar). The key to the proof of the algebraicity of ≲_{ω} is the following general theorem providing a partial completeness result for ≲ in the sense of Hennessy [38, 8] for arbitrary compact GSOS systems.

Before stating the partial completeness theorem, we introduce a technical notion from [7] which will be useful in the remainder of this paper.

Definition 6.14 A GSOS system H is a disjoint extension of a GSOS system G if the signature and rules of H include those of G, and H introduces no new rules for operations of G.

Note that the relation “is a disjoint extension of” is a partial order over the set of GSOS systems. Moreover, if H disjointly extends G then it is not hard to see that:

• for every program P in CREC(Σ_{G}, PVar), P ↓_{Grec} iff P ↓_{Hrec};

• for all P, Q ∈ CREC(Σ_{G}, PVar), P →^{a}_{Grec} Q implies P →^{a}_{Hrec} Q; and

• for all P ∈ CREC(Σ_{G}, PVar), Q ∈ CREC(Σ_{H}, PVar), P →^{a}_{Hrec} Q implies Q ∈ CREC(Σ_{G}, PVar) and P →^{a}_{Grec} Q.

This means in particular that, for P, Q ∈ CREC(Σ_{G}, PVar), P ≲_{Grec} Q ⇔ P ≲_{Hrec} Q.

Theorem 6.15 (Partial Completeness) Let G be a compact GSOS system. Then there exist a compact GSOS system H and a set of Σ_{H}-inequations T such that:

• H disjointly extends G and FINTREE_{Ω}, and

• for all P ∈ T(Σ_{H}), Q ∈ CREC(Σ_{H}, PVar), P ≲_{H} Q iff T ∪ {(4)} ⊢ P ≤ Q.

The proof of this theorem is rather involved and occupies the whole of the next section. It involves giving an algorithm for finding a complete axiomatization of the relation ≲ over a disjoint extension of our original language following the lines of [7]. As the details of the proof are not necessary to understand the developments of this section, we feel free to assume Thm. 6.15 in what follows and defer its proof. Apart from its intrinsic interest, the main consequence of Thm. 6.15 is the following key result that essentially states that, for any compact GSOS system, finite trees are compact elements with respect to the preorder ≲.

Theorem 6.16 Let G be a compact GSOS system. Suppose that t is a synchronization tree in ST(Act) and that P ∈ CREC(Σ_{G}, PVar). Then t ≲_{Grec} P iff there exists a finite approximation P^{n} of P such that t ≲_{Grec} P^{n}.

Proof: The “if” implication follows immediately from the fact that P^{n} ≤_{Ω} P implies P^{n} ≲_{Grec} P; so we concentrate on the proof of the “only if” implication. The proof relies on general properties of initial continuous algebras in inequational varieties that may be found in, e.g., [41].

Let G be a compact GSOS system. Then, by Thm. 6.15, there exist a compact GSOS H that disjointly extends G and FINTREE_{Ω}, and a collection T of Σ_{H}-inequations such that, for all P ∈ T(Σ_{H}), Q ∈ CREC(Σ_{H}, PVar), P ≲_{Hrec} Q iff T ∪ {(4)} ⊢ P ≤ Q. Let CI_{T} denote the initial continuous Σ_{H}-algebra that satisfies the set of Σ_{H}-inequations T. Then, from the general theory of algebraic semantics, we have that, for all P ∈ T(H), Q ∈ CREC(Σ_{H}, PVar),

CI_{T} [[P]] ≤ CI_{T} [[Q]] ⇔ T ∪ {(4)} ⊢ P ≤ Q .  (20)

Let t ∈ ST(Act) and P ∈ CREC(Σ_{G}, PVar). Assume that t ≲_{Grec} P. As H is a disjoint extension of G, we have that t ≲_{Hrec} P. Moreover, as H disjointly extends FINTREE_{Ω}, there exists a term Q_{t} ∈ T(Σ_{H}) such that Q_{t} ∼_{Hrec} t ≲_{Hrec} P. By Thm. 6.15, it follows that T ∪ {(4)} ⊢ Q_{t} ≤ P. By (20), we then have that CI_{T} [[Q_{t}]] ≤ CI_{T} [[P]]. By the construction of CI_{T}, the denotation of every recursion-free term in CREC(Σ_{Σ_{H}}, PVar) is a compact element in CI_{T}. Using (11), this implies that CI_{T} [[Q_{t}]] ≤ CI_{T} [[P^{n}]] for some finite approximation P^{n} of P. Applying (20) and the soundness of the inequations in T with respect to ≲_{Hrec}, we have that t ∼_{Hrec} Q_{t} ≲_{Hrec} P^{n}. As P^{n} is a Σ_{G}-term, and H disjointly extends G, we finally conclude that t ≲_{Grec} P^{n}, as required. □

The above result, in conjunction with Propn. 4.6, allows us to prove that ≲_{ω} is indeed algebraic.

Theorem 6.17 Let G be a compact GSOS system. Then the relation ≲_{ω} over lts(Grec) is algebraic.

Proof: We prove that, for all P, Q ∈ CREC(Σ_{G}, PVar), P ≲_{ω} Q iff P ≲_{ω}^{A} Q.

• Assume that P ≲_{ω} Q. We prove that P ≲_{ω}^{A} Q, i.e., that for every finite approximation P^{n} of P there exists a finite approximation Q^{m} of Q such that P^{n} ≲_{ω} Q^{m}.

Let P^{n} be a finite approximation of P. Then, as ≲_{ω} is a Σ_{G}-precongruence and the defining laws for ≤_{Ω} are sound with respect to it, we have that P^{n} ≲_{ω} P. As G is compact and P^{n} ∈ T(Σ_{G}), by Lem. 6.5, there exists a finite synchronization tree t_{P^{n}} such that t_{P^{n}} ∼ P^{n}. Thus, by transitivity of ≲_{ω}, t_{P^{n}} ≲_{ω} Q. We may now apply Thm. 6.16 to conclude that, for some finite approximant Q^{m} of Q, t_{P^{n}} ≲ Q^{m}. By Lem. 2.5, it follows that P^{n} ≲_{ω} Q^{m}, as required.

• Assume that P ≲_{ω}^{A} Q. We prove that P ≲_{ω} Q. In fact, as ≲_{ω} coincides with the finitary part of ≲ by Propn. 4.6, it is sufficient to show that P ≲^{F} Q. Assume to this end that t ≲ P for some t ∈ ST(Act). We then reason as follows:

t ≲ P ⇔ ∃P^{n} : t ≲ P^{n}  (By Thm. 6.16)
⇔ ∃P^{n} : t ≲_{ω} P^{n}  (By Lem. 2.5)
⇒ ∃Q^{m} : t ≲_{ω} P^{n} ≲_{ω} Q^{m} (P ≲_{ω}^{A} Q)
⇒ t ≲_{ω} Q  (≤_{Ω} ⊆ ≲_{ω})
⇔ t ≲ Q  (By Lem. 2.5)

Thus P ≲^{F} Q, as required.

□

It is interesting to note that the relation ≲_{ω} is, in general, not algebraic for arbitrary GSOS systems. Consider, for instance, the GSOS system obtained by adding the constant a^{ω} given by the rule (17) to our running example preACP_{Ωθ}. Because of the presence of a^{ω}, the resulting GSOS system is not compact. We claim that the relation ≲_{ω} is not algebraic over this language. In fact, consider the terms a^{ω} and fix(X = a.X). It is easy to see that a^{ω} ≲_{ω} fix(X = a.X). Moreover, for every n ≥ 1, (a^{ω})^{n} ≡ a^{ω}. However, for no finite approximation (fix(X = a.X))^{n} of fix(X = a.X), it holds that a^{ω} ≲_{ω} (fix(X = a.X))^{n}. This is because each (fix(X = a.X))^{n} has the form a^{n}.Ω and a^{ω} ≴_{n+1} a^{n}.Ω.

In light of the above results, we can now show that, for any compact GSOS system G, the denotational semantics for CREC(Σ_{G}, PVar) is fully abstract with respect to ≲_{ω}.

Theorem 6.18 (Full Abstraction) Let G be a compact GSOS system. Then, for every P, Q ∈ CREC(Σ_{G}, PVar), P ≲_{ω} Q iff D[[P]] ⊑_{D} D[[Q]].

Proof: Let G be a compact GSOS system and P, Q ∈ CREC(Σ_{G}, PVar). We proceed as follows:

P ≲_{ω} Q ⇔ ∀n∃m : P^{n} ≲_{ω} Q^{m}  By Lem.6.17
⇔ ∀n∃m : D[[P^{n}]] ⊑_{D} D[[Q^{m}]] By Thm. 6.13
⇔ P ≲_{ω} Q  by property (11).
□

When applied to the version of SCCS considered by Abramsky in [1], the techniques we have presented deliver a denotational semantics that is exactly the one given by Abramsky in that paper. This is an easy consequence of Thm. 6.18, Abramsky’s full abstraction theorem [1, Thm. 6.19] and the fact that, as remarked in Sect. 4, the operational semantics for SCCS generated by our methods is exactly the standard one given in [38].

7 Partial Completeness for Compact GSOS Languages

Our aim in this section is to give a proof of Thm. 6.15. The main ideas underlying the proof of this partial completeness result are a generalization of those used, e.g., by Hennessy in [38] to establish a similar result for Milner’s SCCS [62]. This generalization of Hennessy’s approach is achieved along the lines of the developments in [7, 5], but the details are quite different from the ones in the aforementioned references.

Let G be a compact GSOS system. We present an algorithm that can be used to generate a compact GSOS system H that disjointly extends G and FINTREE_{Ω}, and a set of Σ_{H}-inequations such that, for all P ∈ T(Σ_{H}) and Q ∈ CREC(Σ_{H}, PVar),

P ≲_{H} Q ⇔ T ∪ {(Rec)} ⊢ P ≤ Q  (21)

where (Rec) stands for equation (4), stating that a recursive term is equivalent to its unwinding. As H is a disjoint extension of the GSOS system G we started from, we have that ≲_{G} coincides with ≲_{H} over CREC(Σ_{G}, PVar). A solution to (21) thus solves, in particular, the partial completeness problem for the original language G.

The equational theory T generated by the methods presented in this section will include the following set of inequations^{6}, which will be henceforth referred to as T_{FINTREE_{Ω}}:

x + y = y + x  (22)
(x + y) + z = x + (y + z)  (23)

6As usual, an equation P = Q should be read as a shorthand for the pair of inequations P ≤ Q and Q ≤ P.

x + x = x  (24)
x + δ = x  (25)
Ω ≤ x  (26)

It is not difficult to see that the above inequations are sound in any GSOS system that disjointly extends FINTREE_{Ω}. Moreover, it is well-known that they are complete with respect to ≲ over FINTREE_{Ω}. (See, e.g., the results in [38, 8]).

Lemma 7.1 Let G be a GSOS system that disjointly extends FINTREE_{Ω}. Then the inequational theory T_{FINTREE_{Ω}} is sound with respect to ≲_{Grec}.

In order to prove Thm. 6.15, we aim at generating GSOS system H that disjointly extends G and FINTREE_{Ω}, and an inequational theory T over Σ_{H} that includes T_{FINTREE_{Ω}} and has the following properties:

• T is Ω-head normalizing for terms in T(Σ_{H}). Adapting the terminology in [41], a Ω-head normal form is a term of the form ∑_{i∈I} a_{i}.P_{i}[+Ω], where the notation [+Ω] means that Ω is an optional summand. The inequational theory generated by our methods will have the property that every recursion-free term in CREC(Σ_{H}, PVar) is provably equal to a Ω-head normal form, i.e.,

∀P ∈ T(Σ_{H})∃ ∑_{i∈I} a_{i}.P_{i}[+Ω] : T ⊢ P = ∑_{i∈I} a_{i}.P_{i}[+Ω] .  (27)

• T is head normalizing for convergent terms in CREC(Σ_{H}, PVar). A head normal form is a term of the form ∑_{i∈I} a_{i}.P_{i}. The inequational theory generated by our methods will have the property that every convergent term in CREC(Σ_{H}, PVar) is provably equal to a head normal form, i.e., for every P ∈ CREC(Σ_{H}, PVar),

P ↓_{Hrec} ⇒ ∃ ∑_{i∈I} a_{i}.P_{i} : T ∪ {(Rec)} ⊢ P = ∑_{i∈I} a_{i}.P_{i} .  (28)

• T absorbes transitions. The inequational theory generated by our methods will be such that for all P ∈ CREC(Σ_{H}, PVar) there exists a program P^{∗} ∈ CREC(Σ_{H}, PVar) with the following properties:

T ⊢ P = P^{∗}  (29)

and, for all a ∈ Act, Q ∈ CREC(Σ_{H}, PVar),

P^{∗} →^{a}_{Hrec} Q ⇒ T ∪ {(Rec)} ⊢ P^{∗} = P^{∗} + a.Q .  (30)

Our interest in inequational theories with the aforementioned properties stems from the following result, from which, after having presented the promised algorithm, we shall be able to derive Thm. 6.15.

Theorem 7.2 Let H be a compact GSOS system that disjointly extends FINTREE_{Ω}. Suppose that T is a collection of sound inequations with respect to ≲_{Hrec} that extends T_{FINTREE_{Ω}}. Suppose further that T is Ω-head normalizing for terms in T(Σ_{H}), head normalizing for convergent terms in CREC(Σ_{H}, PVar) and that T absorbes transitions. Then (21) holds for such H and T.

Proof: Assume that H is a compact GSOS system that disjointly extends FINTREE_{Ω}, and that T is a collection of inequations over Σ_{H} that includes T_{FINTREE_{Ω}}, is sound with respect to ≲_{Hrec} and has properties (27)–(30). We prove that (21) holds for such an H and T.

The soundness part of the statement is guaranteed to hold by the proviso of the theorem, by Fact. 4.5 and by Corollary 4.9. Therefore, we focus on the proof of partial completeness. To this end, note, first of all, that, by Lem. 3.8 and (6), Der(P) is finite for every P ∈ T(Σ_{H}). Moreover, as H is compact, by Propn. 6.4 no term P ∈ T(Σ_{H}) can have infinite derivations. Thus we can associate with each P ∈ T(Σ_{H}) a natural number depth(P), denoting the maximum number of consecutive transitions possible from P. Note further that, for any two terms P_{1}, P_{2} ∈ T(Σ_{H}) that are related by ∼_{Hrec}, depth(P_{1}) = depth(P_{2}).

Assume now that P ∈ T(Σ_{H}) and that Q ∈ CREC(Σ_{H}, PVar). Suppose further that P ≲_{Hrec} Q. We prove, using properties (27)–(30) above that

T ∪ {(Rec)} ⊢ P ≤ Q .  (31)

The proof is by induction on depth(P). We assume, as inductive hypothesis, that the claim holds for all P′ ∈ T(Σ_{H}), Q′ ∈ CREC(Σ_{H}, PVar) with P′ ≲_{Hrec} Q′ and depth(P′) < depth(P), and show that it holds for P and Q.

To show (31), by transitivity, it is sufficient to establish the following two claims:

1. T ∪ {(Rec)} ⊢ P ≤ P + Q, and

2. T ∪ {(Rec)} ⊢ P + Q ≤ Q.

We now proceed by proving the above claims separately. First of all, note that, as P ∈ T(Σ_{H}), by (27) we have that P is provably equal to a Ω-head normal form ∑_{i∈I} a_{i}.P_{i}[+Ω], i.e.,

T ⊢ P = ∑_{i∈I} a_{i}.P_{i}[+Ω] .  (32)

Proof of Claim 1. We prove that T ∪ {(Rec)} ⊢ P ≤ P + Q by distinguishing two cases, depending on whether the Ω-head normal form for P has a Ω summand or not.

• Assume that the Ω-head normal form for P has a Ω summand. Then we simply reason as follows:

T ⊢ P = ∑_{i∈I} a_{i}.P_{i} + Ω
≤ ∑_{i∈I} a_{i}.P_{i} + Ω + Q (By (24) and (26))
= P + Q .

• Assume that the Ω-head normal form for P does not have a Ω summand. Then, by the soundness of T, we have that

P ∼_{Hrec} ∑_{i∈I} a_{i}.P_{i} .

It follows that P ↓_{Hrec}. As P ≲_{Hrec} Q, it must also be the case that Q ↓_{Hrec}.

By (28), Q is provably equal to a head normal form ∑_{j∈J} b_{j}.Q_{j}, i.e.,

T ∪ {(Rec)} ⊢ Q = ∑_{j∈J} b_{j}.Q_{j} .

As P ≲_{Hrec} Q, P ↓_{Hrec} and Q ↓_{Hrec}, for every j ∈ J there exists i_{j} ∈ I such that a_{i_{j}} = b_{j} and P_{i_{j}} ≲_{Hrec} Q_{j}. Now note that depth(P_{i}) < depth(∑_{i∈I} a_{i}.P_{i}) = depth(P). Thus the inductive hypothesis can be applied to infer that

T ∪ {(Rec)} ⊢ P_{i_{j}} ≤ Q_{j} .

Therefore,

T ∪ {(Rec)} ⊢ P = ∑_{i∈I} a_{i}.P_{i}
= ∑_{i∈I} a_{i}.P_{i} + ∑_{j∈J} a_{i_{j}}.P_{i_{j}} (By repeated use of (24))
≤ ∑_{i∈I} a_{i}.P_{i} + ∑_{j∈J} b_{j}.Q_{j} (By the inductive hypothesis)
= P + Q .

This completes the proof of the first claim.

Proof of Claim 2. We now complete the proof by showing that T ∪{(Rec)} ⊢ P +Q ≤ Q. First of all, note that, as T absorbes transitions, there exists a program Q^{∗} ∈ CREC(Σ_{H}, PVar) such that:

T ⊢ Q = Q^{∗}  (33)

and, for all a ∈ Act and Q ∈ CREC(Σ_{H}, PVar),

Q^{∗} →^{a}_{Hrec} Q′ ⇒ T ∪ {(Rec)} ⊢ Q^{∗} = Q^{∗} + a.Q′ .  (34)

By the soundness of the inequations in T and (32), we have that

∑_{i∈I} a_{i}.P_{i}[+Ω] ∼_{Hrec} P ≲_{Hrec} Q ∼_{Hrec} Q^{∗} .

Thus, for every i ∈ I there exists a term Q_{i} such that Q^{∗} →^{a_{i}}_{Hrec} Q_{i} and P_{i} ≲_{Hrec} Q_{i}. By induction, we infer that, for each such pair of processes (P_{i}, Q_{i}),

T ∪ {(Rec)} ⊢ P_{i} ≤ Q_{i} .  (35)

Therefore,

T ∪ {(Rec)} ⊢ P + Q = P + Q^{∗} (By (33))
= ∑_{i∈I} a_{i}.P_{i}[+Ω] + Q^{∗}

≤ ∑_{i∈I} a_{i}.P_{i}[+Q^{∗}] + Q^{∗} (By possibly using (26))
≤ ∑_{i∈I} a_{i}.Q_{i} + Q^{∗} (By (35) and possibly using (24))
= Q^{∗} (By repeated use of (34))
= Q (Again by (33))

The proof of the theorem is now complete. □

By the above theorem, all that is needed to show Theorem 6.15 is an algorithm that, starting from a compact GSOS system G, allows us to generate a suitable disjoint extension H of G, and an inequational theory T that enjoys properties (27)–(30). This we now present following the developments in [7, 5] closely. We take the liberty of referring the reader to those references for detailed motivations for some of the technical definitions to follow.

We now present the core of our strategy for axiomatizing GSOS operations. Following [7], we proceed in two steps: first, we shall show how to axiomatize a class of particularly well-behaved operations, the smooth operations introduced in Section 7.1. Secondly, we shall extend our results to arbitrary GSOS operations in Section 7.2.

Notation 7.3 For any term P in a GSOS system G that disjointly extends FINTREE_{Ω}, the notation P [+Ω ⇔ Condition] will stand for P + Ω if Condition is true, and P otherwise.

7.1 Smooth Operations

In this subsection we give a way of generating an inequational theory that enjoys properties (27)–(30) for the class of smooth operations, using the still simpler weakly distinctive operations [22, 5] as a base case. The following definition is from [7], where motivation and examples of smooth operations may be found.

Definition 7.4 A GSOS rule is smooth if it takes the form

\frac{\{x_{i} →^{a_{i}} y_{i}|i ∈ I\} ∪ \{x_{i} ↛^{b_{ij}} |i ∈ K, 1 ≤ j ≤ n_{i}\}}{f(x_{1}, …, x_{l}) →^{c} C[x⃗, y⃗]}  (36)

where I, K are disjoint sets such that I ∪ K = {1, …, l}, and no x_{i} with i ∈ I appears in C[x⃗, y⃗]. An operation from a GSOS system G is smooth if all the rules for this operation are smooth.

For example, the operations in the language preACP_{Ωθ} are smooth, with the possible exception of the priority operation θ which is only smooth if the priority structure on actions is trivial.

In order to obtain an inequational theory for smooth operations with the required properties, we shall first show how to obtain equations that describe the interplay between such operations and the FINTREE_{Ω} combinators. Lemmas 7.5–7.11 hold for arbitrary GSOS systems, and will be stated in full generality even though, in the remainder of the paper, we shall only apply them to obtain equations for smooth operations in compact GSOS systems.

Lemma 7.5 (Distributivity Laws) Let f be an l-ary smooth operation of a GSOS system G that disjointly extends FINTREE_{Ω}, and suppose i is an argument of f for which each rule for f has a positive antecedent. Then f distributes over + in its i-th argument, i.e., for every GSOS system H that disjointly extends G,

f(X_{1}, …, X_{i} + Y_{i}, …, X_{l}) ∼_{Hrec} f(X_{1}, …, X_{i}, …, X_{l}) + f(X_{1}, …, Y_{i}, …, X_{l}) . (37)

Proof: A minor adaptation of the proof of [4, Lem. 5.2]. □

When applied to the communication-merge operation from ACP [17] given by the rules (one such rule for each triple of actions (a, b, c) with γ(a, b) ≃ c):

\frac{x →^{a} x′, y →^{b} y′}{x|y →^{c} x′|y′}

the above lemma gives the equations:

(X + Y)|Z = X|Z + Y |Z
X|(Y + Z) = X|Y + X|Z

We now present lemmas that give divergence laws and inaction laws to describe the interaction between arbitrary operations and the FINTREE_{Ω} constants Ω and δ, respectively; that is, laws which say when a term f(P⃗) is equivalent to Ω or δ. The following lemmas can certainly be generalized to yield more laws, but they will be enough for our purposes in this study.

Lemma 7.6 (Divergence Laws) Suppose f is an l-ary smooth operation of a GSOS system G that disjointly extends FINTREE_{Ω}, and suppose that, for 1 ≤ i ≤ l, term P_{i} is of the form δ, Ω, X_{i} or X_{i} + Ω. Suppose further that the following conditions are met:

1. for each rule for f of the form (36) there is an index i such that:

• either i ∈ I, and P_{i} ≡ δ or P_{i} ≡ Ω,

• or i ∈ K, n_{i} > 0 and P_{i} ≡ Ω or P_{i} ≡ X_{i} + Ω;

and

2. for some argument i tested by f, P_{i} ≡ Ω or P_{i} ≡ X_{i} + Ω.

Then, for every GSOS system H that disjointly extends G,

f(P⃗) ∼_{Hrec} Ω .  (38)

Proof: Assume that H is a disjoint extension of G, and consider a substitution σ : PVar → CREC(Σ_{H}, PVar). Then condition 1 of the lemma ensures that f(P⃗)σ does not have any transition, and condition 2 ensures that f(P⃗)σ ↑_{Hrec}. Therefore f(P⃗)σ ∼_{Hrec} Ω, as required. □

To give the reader an idea of the laws that are generated by the above lemma, we consider the binary smooth operation △ introduced in [7] to axiomatize the priority operation θ. The definition of this operation, as that of θ, assumes the presence of a partially ordered set of actions (Act, >). The operation △ has rules (one for each a ∈ Act):

\frac{x →^{a} x′, y ↛^{b} (for all b > a)}{x△y →^{a} θ(x′)}  (39)

We apply the above lemma to generate divergence laws for △ by considering the possible forms that its arguments can take.

• Divergence laws when the first argument is δ: In this case, the first condition of the statement of Lem. 7.6 is met regardless of the form of the second argument. However, condition 2 must also be met. This is not possible if the partial order on actions is flat, i.e., if no two actions are related by >. In that case, no divergence laws are generated by the lemma when the first argument of △ is the inactive, convergent term δ. Otherwise, Lem. 7.6 gives the following laws:

δ△Ω = Ω
δ△(Y + Ω) = Ω

Note that, in the presence of law (24), the first law is redundant as it is provably equal to a substitution instance of the second.

• Divergence laws when the first argument is Ω: In this case, the second argument can be arbitrary, and every law generated by Lem. 7.6 can be obtained as a substitution instance of the law:

Ω△Y = Ω .

• Divergence laws when the first argument is a process variable X: In this case, Lem. 7.6 produces no divergence law. In fact, as Act is finite, there is at least one action a which is maximal with respect to >. The instance of rule (39) for a has no negative premise and condition 1(2) in the statement of the lemma cannot be met for it, no matter what the form of the second argument of △ is. We remark here that the requirement n_{i} > 0 in condition 1(2) of the statement of the lemma is vital for the soundness of the generated equations. Without it, Lem. 7.6 could be used to derive the unsound equation:

X△Ω = Ω .

This equation is unsound because, if a is an action in Act which is maximal with respect to >, then

a.δ△Ω ∼ a.δ[+Ω⇔(Act, >) is not flat] ≁ Ω .

• Divergence laws when the first argument is of the form X + Ω: Reasoning as in the previous case, it is not hard to argue that Lem. 7.6 produces no divergence law.

Lemma 7.7 (Inaction Laws) Suppose f is an l-ary smooth operation of a GSOS system G that disjointly extends FINTREE_{Ω}, and suppose that, for 1 ≤ i ≤ l, term P_{i} is of the form δ, X_{i} or ∑_{n∈N} c_{n}.X_{n}. Suppose further that the following conditions are met:

1. for each rule for f of the form (36) there is an index i such that either (1) i ∈ I and P_{i} ≡ δ or P_{i} ≡ ∑_{n∈N} c_{n}.X_{n} and a_{i} ∉ {c_{n} | n ∈ N}, or (2) i ∈ K, P_{i} ≡ ∑_{n∈N} c_{n}.X_{n} and there exist n ∈ N and 1 ≤ j ≤ n_{i} with c_{n} = b_{ij}; and

2. for no argument i tested by f, P_{i} is a process variable.

Then, for every GSOS system H that disjointly extends G,

f(P⃗) ∼_{Hrec} δ .  (40)

Proof: Assume that H is a disjoint extension of G, and consider a substitution σ : PVar → CREC(Σ_{H}, PVar). Then condition 1 of the lemma ensures that f(P⃗)σ does not have any transition, and condition 2 ensures that f(P⃗)σ ↓_{Hrec}. Therefore f(P⃗)σ ∼_{Hrec} δ, as required. □

Again, we show the above lemma in action by applying it to generate inaction laws for the △ operation. As before, we proceed by considering the possible forms the arguments of △ may take.

• Inaction laws when the first argument of △ is δ: In this case, condition 1 in the statement of the lemma is always satisfied. If the partial ordering on Act is flat, then △ does not test its second argument, which may take any of the forms specified in Lem. 7.7; all the equations generated by the lemma in this case may be obtained as substitution instances of the law:

δ△Y = δ .

Otherwise, △ does test its second argument, and, by condition 2, the second argument must be of the form ∑_{n∈N} a_{n}.X_{n}. (Recall that δ ≡ ∑_{n∈∅} a_{n}.X_{n}.) The corresponding law is:

δ△ ∑_{n∈N} a_{n}.X_{n} = δ .

• Inaction laws when the first argument of △ is a process variable X: This case is ruled out by condition 2 of the lemma, and no equations are generated.

• Inaction laws when the first argument of △ is of the form ∑_{n∈N} a_{n}.X_{n} for nonempty N: In this case, in order to meet condition 1 in the statement of the lemma, the second argument must be of the form ∑_{m∈M} b_{m}.Y_{m} and for every n ∈ N there exists m ∈ M with b_{m} > a_{n}. For every pair of such terms, Lem. 40 generates the equation:

∑_{n∈N} a_{n}.X_{n}△ ∑_{m∈M} b_{m}.Y_{m} = δ .

We now derive action laws, which tell when a process can take an action. These laws will be given for a sub-class of smooth GSOS operations that test their arguments positively in a consistent way. This class of smooth operations is characterized in the following definition.

Definition 7.8 Let f be an l-ary smooth operation in a GSOS system G. We say that f is weakly distinctive iff every rule for f tests the same arguments positively.

For a weakly distinctive, smooth operation f in a GSOS system G, we write Test^{+}(f) for the set of arguments tested positively by every rule for f, and Test^{−}(f) for the set of arguments tested negatively by some rule for f.

For example, the operation a. for preACP_{Ωθ}, and the left-merge and communicationmerge operations from ACP [17] are weakly distinctive. As remarked previously, the priority operation θ is smooth iff the poset of actions (Act, >) is flat. In that case, θ is also weakly distinctive, and uninteresting. Note also that, for a smooth operation f, Test^{+}(f) and Test^{−}(f) are disjoint.

The notion of weak distinctiveness given above is a weakening of the notion of distinctiveness introduced in [7]. Its definition differs slightly from that given in [4] in that we do not require that the operation f is positive, i.e. that rules for f do not have negative antecedents, and consistent in the sense of [4, Def. 7.1].

Notation 7.9 We write Act_{⊥} for the set Act ∪ {⊥}, where ⊥ is a symbol not occurring in Act.

For a term P of the form ∑_{i∈I} a_{i}.P_{i}[+Ω], Initials(P) will denote the subset of Act_{⊥} given by {a_{i} | i ∈ I}[∪{⊥}], where ⊥ ∈ Initials(P) iff Ω is a summand of P.

Definition 7.10 Let f be an l-ary weakly distinctive, smooth operation in a GSOS system G. We say that a vector ⟨e_{1}, …, e_{l}⟩ over Act ∪ 2^{Act^{⊥}} is consistent with f iff for every argument i of f, if i ∈ Test^{+}(f) then e_{i} ∈ Act, and e_{i} ⊆ Act_{⊥} otherwise.

Let f be an l-ary weakly distinctive, smooth operation in a GSOS system G, and let the vector ⟨e_{1}, …, e_{l}⟩ be consistent with f. Then R_{G}(f, ⟨e_{1}, …, e_{l}⟩) will denote the set of rules r ∈ R_{G} of the form (36) with f as principal operation such that:

r ∈ R_{G}(f, ⟨e_{1}, …, e_{l}⟩) ⇔
(1) ∀i ∈ Test^{+}(f). a_{i} = e_{i}, and
(2) ∀i ∈ K. n_{i} > 0 ⇒ (e_{i} ∩ {b_{ij} | 1 ≤ j ≤ n_{i}} = ∅ and ⊥ ∉ e_{i}) .

Intuitively, R_{G}(f, ⟨e_{1}, …, e_{l}⟩) is the set of rules for f that can be possibly used to derive outgoing transitions from a term of the form f(P⃗) where, for each argument i for f:

1. if i ∈ Test^{+}(f), then P_{i} can initially perform an e_{i}-action, and

2. if i ∈ Test^{−}(f), then P_{i} converges (encoded by the absence of ⊥ in the set e_{i}) and the set of initial actions that P_{i} can perform is exactly e_{i}.

For example, any tuple of the form ⟨a, B⟩, where a ∈ Act and B ⊆ Act_{⊥} is consistent with the △ operation. For any GSOS system G containing this operation, the set R_{G}(△, ⟨a, B⟩) is a singleton if a is maximal in the poset (Act, >) or ⊥ ∉ B and B does not contain any b > a, and it is empty otherwise. In fact, for any operation f that, like △, is smooth and distinctive in the sense of [7], the set R_{G}(f, ⟨e_{1}, …, e_{l}⟩) is either empty or it contains a single rule. This property does not hold in general for weakly distinctive operations. As an example, consider a GSOS system G that contains the smooth, distinctive operation ⊕ [25, 39, 31, 41] given by the rules:

\overline{x ⊕ y →^{τ} x}  \overline{x ⊕ y →^{τ} y}

Then the vector ⟨∅, ∅⟩ is consistent with ⊕, and R_{G}(⊕, ⟨∅, ∅⟩) contains both the above rules.

Lemma 7.11 Suppose that f is a weakly distinctive smooth operation of arity l of a disjoint extension G of FINTREE_{Ω}. Let ⟨e_{1}, …, e_{l}⟩ be a vector over Act ∪ 2^{Act^{⊥}} that is consistent with f. Finally, let P⃗ be the vector of terms given by:

P_{i} ≡ \{ \begin{matrix}e_{i}.Y_{i} & i ∈ Test^{+}(f) \\ ∑ \{b.Z_{b} | b ∈ e_{i}\}[+Ω ⇔ ⊥ ∈ e_{i}] & i ∈ Test^{−}(f) \\ X_{i} & otherwise \end{matrix}

where all the process variables are distinct. Then, for every disjoint extension H of G,

f(P⃗) ∼_{Hrec} ∑_{r∈R_{G}(f,⟨e_{1},...,e_{l}⟩)} action(r).target(r){P⃗ /x⃗, Y⃗ /y⃗}
[+Ω ⇔ (∃i ∈ Test^{−}(f) : ⊥ ∈ e_{i}) ∨ f = Ω] .  (41)

Proof: Assume that H is a disjoint extension of G, and consider a substitution σ : PVar → CREC(Σ_{H}, PVar). By the definition of P⃗ and the fact that f is smooth, it follows immediately that a transition of the form f(P⃗)σ →^{c}_{Hrec} Q holds iff there exists a rule r in R_{G}(f, ⟨e_{1}, …, e_{l}⟩) with action c such that target(r){P⃗ /x⃗, Y⃗ /y⃗}σ = Q. Similarly, the

form of Eqn. (41) ensures that f(P⃗)σ converges iff the instantiated right-hand side of the equation does. □

As an example, we apply the above lemma to derive action laws for the △ operation specified by (39). As remarked previously, any vector over Act ∪ 2^{Act^{⊥}} that is consistent with △ has the form ⟨a, B⟩ for some a ∈ Act and B ⊆ Act_{⊥}. We proceed to generate the corresponding action law for △ by distinguishing two cases, depending on whether a is maximal in (Act, >) or not.

• If a is maximal in (Act, >), then R_{G}(△, ⟨a, B⟩) is the singleton set containing the only rule for △ with action a. The equation generated by Lem. 7.11 then takes the form:

a.Y △ ∑_{b∈B} b.Z_{b}[+Ω] = a.θ(Y)[+Ω]

where Ω is a summand of the right-hand side of the equation iff it appears as a summand of the second argument iff ⊥ ∈ B.

• If a is not maximal in (Act, >), then the form of the equation produced by Lem. 7.11 depends on whether there is a reason in the set B that prevents the application of the only rule for △ to derive a transition from the term a.Y △ ∑_{b∈B} b.Z_{b}[+Ω], or not.

– If b > a for some b ∈ B or ⊥ ∈ B, then R_{G}(△, ⟨a, B⟩) is empty. The equation given by Lem. 7.11 in this case is then:

a.Y △ ∑_{b∈B} b.Z_{b}[+Ω] = δ[+Ω]

where Ω is a summand of the right-hand side of the equation iff it appears as a summand of the second argument iff ⊥ ∈ B ^{7}.

– Otherwise, R_{G}(△, ⟨a, B⟩) is the singleton set containing the only rule for △ with action a, and Lem. 7.11 gives the equation:

a.Y △ ∑_{b∈B} b.Z_{b} = a.θ(Y) .

The equations given by the above lemmas provide us with an equational theory that is strong enough to establish properties (27)–(30) for terms built from the FINTREE_{Ω} operations and weakly distinctive smooth operations. For the sake of clarity, we reiterate below the definitions of the types of head normal forms we shall be interested in in the remainder of the paper.

Definition 7.12 A term P over a signature Σ ⊇ Σ_{FINTREE_{Ω}} is in Ω-head normal form if it is of the form ∑ a_{i}.P_{i}[+Ω]. We say that P is in head normal form if it is of the form ∑ a_{i}.P_{i}.

We prove, first of all, that the equations generated by Lemmas 7.5–7.11 allow us to associate a Ω-head normal form with each recursion-free program built from the FINTREE_{Ω} operations and weakly distinctive smooth operations.

Theorem 7.13 Suppose G is a GSOS system that disjointly extends FINTREE_{Ω}. Let Σ ⊆ Σ_{G} − Σ_{FINTREE_{Ω}} be a collection of weakly distinctive smooth operations of G. Let T be the equational theory that extends T_{FINTREE_{Ω}} \ {(26)} with the following axioms, for each operation f from Σ,

1. for each argument i of f that is tested positively by f, a distributivity axiom (37),

2. for each vector ⟨e_{1}, …, e_{l}⟩ over Act ∪ 2^{Act^{⊥}} consistent with f an action law (41),

3. all the divergence laws (38) for f, and

7As shown by this example, Lem. 7.11 also delivers inaction and divergence laws. For this reason, the name “action lemma” we have used for it is a bit misleading. We hope that this does not cause any confusion in the reader.

4. all the inaction laws (40) for f.

Then the following statements hold:

• If T ⊢ P = Q then, for every disjoint extension H of G, P ∼_{Hrec} Q.

• For every P ∈ T(Σ ∪ Σ_{FINTREE_{Ω}}), there exists a Ω-head normal form Ω-hnf(P)

such that

T ⊢ P = Ω-hnf(P) .

Proof: The fact that if T ⊢ P = Q then, for every disjoint extension H of G, P ∼_{Hrec} Q follows immediately from Lem. 7.1 and Lemmas 7.5–7.11. We are thus left to show that, for every P ∈ T(Σ∪Σ_{FINTREE_{Ω}}), there exists a Ω-head normal form Ω-hnf(P) such that:

T ⊢ P = Ω-hnf(P) .  (42)

This we will follow via a straightforward structural induction on P from the following claim. Claim: Suppose f is an l-ary operation symbol from Σ, and P_{1}, …, P_{l} ∈ (Σ_{G}) are all in Ω-head normal form. Then there exists a term P ∈ (Σ_{G}) in Ω-head normal form such that T ⊢ f(P_{1}, …, P_{l}) = P. The proof of the claim proceeds by induction on the combined size of P_{1}, …, P_{l}. There are four cases to examine.

Case 1. There is an argument i that is tested positively by f and for which P_{i} is of the form P′_{i} + P′′_{i}. As f is weakly distinctive, all rules for f test i positively. In this case we can apply one of the distributivity laws (37) to infer

T ⊢ f(P_{1}, …, P_{l}) = f(P_{1}, …, P′_{i} + P′′_{i}, …, P_{l})
= f(P_{1}, …, P′_{i}, …, P_{l}) + f(P_{1}, …, P′′_{i}, …, P_{l}) .

Next the induction hypothesis gives that there exist Ω-head normal forms P′ and P′′ such that T ⊢ f(P_{1}, …, P′_{i}, …, P_{l}) = P′ and T ⊢ f(P_{1}, …, P′′_{i}, …, P_{l}) = P′′. Hence T ⊢ f(P_{1}, …, P_{l}) = P′ + P′′ and the induction step follows, after possibly using (24) once to eliminate duplicate Ωs in P′ + P′′.

Case 2. There is an argument i that is tested positively by f and for which P_{i} ≡ Ω. Since f is weakly distinctive, all rules for f test i positively. Thus T contains a divergence law f(X_{1}, …, X_{i−1}, Ω, X_{i+1}, …, X_{l}) = Ω. Instantiation of this law gives T ⊢ f(P⃗) = Ω, and the induction step follows.

Case 3. There is an argument i that is tested positively by f and for which P_{i} ≡ δ. We proceed by considering two sub-cases.

Case 3.1. There is an an argument j that is tested negatively by f and for which P_{j} is of the form P′_{j} + Ω. Since f is weakly distinctive, all rules for f test i positively. Thus T contains a divergence law f(Q⃗) = Ω, where Q_{i} ≡ δ, Q_{j} ≡ X_{j} + Ω and Q_{h} ≡ X_{h} otherwise. Instantiation of this law gives T ⊢ f(P⃗) = Ω, and the induction step follows.

Case 3.2. For every argument j that is tested negatively by f, P_{j} does not have an Ω summand. Since f is weakly distinctive, all rules for f test i positively. Thus T contains an inaction law T ⊢ f(P⃗) = δ, and the induction step follows.

Case 4. For all arguments k that are tested positively by f, P_{k} is of the form a_{k}.P′_{k}. Then an application of the action law in T associated with the vector ⟨e_{1}, …, e_{l}⟩, where

e_{k} = \{ \begin{matrix}a_{k} & if k is tested positively by f \\ Initials(P_{i}) & otherwise \end{matrix}

gives the required Ω-head normal form.

□

We now prove that (28) holds for convergent terms built from weakly distinctive operations and the FINTREE_{Ω} operations only, provided we add (Rec) to the equational theory given by the previous theorem.

Theorem 7.14 Suppose G is a GSOS system that disjointly extends FINTREE_{Ω}. Let Σ ⊆ Σ_{G}−Σ_{FINTREE_{Ω}} be a collection of weakly distinctive smooth operations of G. Let T be the equational theory given by Thm. 7.13. Then, for every P ∈ CREC(Σ∪Σ_{FINTREE_{Ω}}, PVar), if P ↓_{Grec} then there exists a head normal form hnf(P) such that

T ∪ {(Rec)} ⊢ P = hnf(P) .

Proof: By induction on the convergence predicate ↓_{Grec}. The details are very similar to those of the proof of Thm. 7.13, and are therefore omitted. We just remark here that no divergence law need be used in the proof, and that the inductive hypothesis and equation (Rec) are all that is needed to deal with the case P ≡ fix(X = Q), for some Q. □

We complete our analysis of terms built from weakly distinctive, smooth operations and the FINTREE_{Ω} operations only by showing that the equational theory used in Thm. 7.14 is strong enough to prove property (30) for these terms.

Theorem 7.15 Suppose G is a GSOS system that disjointly extends FINTREE_{Ω}. Let Σ ⊆ Σ_{G}−Σ_{FINTREE_{Ω}} be a collection of weakly distinctive smooth operations of G. Let T be the equational theory given by Thm. 7.13. Then, for every P ∈ CREC(Σ∪Σ_{FINTREE_{Ω}}, PVar) and Q ∈ CREC(Σ_{G}, PVar),

P →^{c}_{Grec} Q ⇒ T ∪ {(Rec)} ⊢ P = P + c.Q .

Proof: Assume that P ∈ CREC(Σ ∪ Σ_{FINTREE_{Ω}}, PVar), and that P →^{c}_{Grec} Q for some Q ∈ CREC(Σ_{G}, PVar). We show that T ∪{(Rec)} ⊢ P = P +c.Q, where T is the equational theory given by Thm. 7.13. The proof of this claim is delivered in two steps, which mimic the construction of the transition relation →_{Grec} given in the proof of Propn. 4.3. First of all, we show that the claim holds when P ↓_{Grec} by induction on the convergence predicate. Next we prove that the property holds in general by induction on the depth of the proof of the transition P →^{c}_{Grec} Q.

Case P ↓_{Grec}. We show, by induction on the convergence predicate, that if P →^{c}_{Grec} Q, then T ∪ {(Rec)} ⊢ P = P + c.Q. We proceed by a case analysis on the form P takes, and only consider the two non-trivial cases.

Case P = f(P⃗), for some f ∈ Σ and vector P⃗ of programs in CREC(Σ ∪ Σ_{FINTREE_{Ω}}, PVar). As the transition relation →_{Grec} is supported, the transition P →^{c}_{Grec} Q holds because there exist a rule r ∈ R_{G} of the form (36), and a substitution σ : Var → CREC(Σ_{G}, PVar) such that:

1. f(x⃗)σ = f(P⃗), i.e., σ(x_{i}) = P_{i}, for every 1 ≤ i ≤ l,

2. P_{i} →^{a_{i}}_{Grec} σ(y_{i}), for every i ∈ I = Test^{+}(f),

3. P_{i} ↓_{Grec} and P_{i} ↛^{b_{ij}} (1 ≤ j ≤ n_{i}), for every i ∈ K such that n_{i} > 0, and 4. Q = C[x⃗, y⃗]σ. As P is convergent, for each argument i tested by f, P_{i} ↓_{Grec}. By the inductive hypothesis, we thus have that, for each i ∈ I,

T ∪ {(Rec)} ⊢ P_{i} = P_{i} + a_{i}.σ(y_{i}) .  (43)

By Thm. 7.14, it follows that, for every i ∈ K with n_{i} > 0, there exists a head normal form hnf(P_{i}) such that:

T ∪ {(Rec)} ⊢ P_{i} = hnf(P_{i}) .  (44)

Consider now the substitutions τ, τ′ : Var → CREC(Σ_{G}, PVar) given by:

τ(x) = \{ \begin{matrix}P_{i} + a_{i}.σ(y_{i}) & if x = x_{i} for some i ∈ I \\ hnf(P_{i}) & if x = x_{i} for some i ∈ K with n_{i} > 0 \\ σ(x) & otherwise \end{matrix}

and

τ′(x) = \{ \begin{matrix}a_{i}.σ(y_{i}) & if x = x_{i} for some i ∈ I \\ τ(x) & otherwise \end{matrix}

Note that, as f is smooth, for no i ∈ I, x_{i} occurs in the context C[x⃗, y⃗]. Thus, for every meta-variable x occurring in C[x⃗, y⃗],

T ∪ {(Rec)} ⊢ σ(x) = τ′(x) .  (45)

Now, by (43) and (44):

T ∪ {(Rec)} ⊢ f(P⃗) = f(x⃗)σ
= f(x⃗)τ .

As f is weakly distinctive, T contains a distributive law for f of the form (37) for each i ∈ I. Applying these laws repeatedly to the term f(x⃗)τ, we obtain that:

T ∪ {(Rec)} ⊢ f(P⃗) = f(x⃗)τ
= f(x⃗)σ + f(x⃗)τ′
= f(P⃗) + f(x⃗)τ′ .

To prove the claim, it is thus sufficient to show that:

T ∪ {(Rec)} ⊢ f(x⃗)τ′ = f(x⃗)τ′ + c.Q .  (46)

Consider now the vector ⟨e_{1}, …, e_{l}⟩ over Act ∪ 2^{Act^{⊥}} with

e_{i} = \{ \begin{matrix}a_{i} & if i ∈ I \\ Initials(hnf(P_{i})) & if i ∈ K and n_{i} > 0 \\ ∅ & otherwise \end{matrix}

By construction, this vector is consistent with f, and r ∈ R_{G}(f, ⟨e_{1}, …, e_{l}⟩). Thus f contains the instance of law (41) associated with f and ⟨e_{1}, …, e_{l}⟩. Using this law and equations (22)–(24), we derive that:

T ∪ {(Rec)} ⊢ f(x⃗)τ′ = f(x⃗)τ′ + c.C[x⃗, y⃗]τ′
= f(x⃗)τ′ + c.C[x⃗, y⃗]σ (By (45))
= f(x⃗)τ′ + c.Q .

The proof for this case is therefore complete.

Case P ≡ fix(X = S), for some X ∈ PVar and some term S ∈ REC(Σ ∪ Σ_{FINTREE_{Ω}}, PVar) containing at most X free. As P →^{c}_{Grec} Q and P ↓_{Grec}, it must be the case that S{P/X} →^{c}_{Grec} Q and S{P/X} ↓_{Grec}. By the inductive hypothesis, we then have that

T ∪ {(Rec)} ⊢ S{P/X} = S{P/X} + c.Q .

The claim now follows immediately by law (Rec).

General case. The proof is by induction on the depth of the proof of the transition P →^{c}_{Grec} Q. The details are identical to those given above, and are therefore omitted.

□

We now extend the above results to handle general smooth operations. This is achieved by expressing these operations as a sum of weakly distinctive operations, in very much the same way as the merge operation of ACP is expressed as a sum of the auxiliary operations of left-merge and communication merge (see, e.g., [17] for a textbook presentation). In particular, the following proposition allows for the “discovery” of, e.g., the auxiliary operations of ACP. See [7] for details and examples.

Proposition 7.16 Let G be a GSOS system that disjointly extends FINTREE_{Ω}. Assume that f is an l-ary smooth operation of G. Then there exists a disjoint extension G′ of G with l-ary weakly distinctive, smooth operations f_{1}, …, f_{n} such that the following statements hold:

1. if G is compact, then G′ is also compact; 2. for every disjoint extension H of G′, and every vector of process variables X⃗ of

length l,

f(X⃗) ∼_{Hrec} f_{1}(X⃗) + ⋯ + f_{n}(X⃗) .  (47)

Proof: Assume that f is an l-ary smooth operation of G. We show how to partition the set R of rules for f in R_{G} into sets R_{1}, …, R_{n} in such a way that that, for all 1 ≤ i ≤ n, f is weakly distinctive in the GSOS system obtained from G by removing all the rules in R − R_{i}. This can be done by partitioning the set of rules for f according to the following equivalence relation:

r ≡_{f} r′ ⇔ r, r′ are rules for f that test the same arguments positively.

Let R_{1}, …, R_{n} be the equivalence classes of rules for f determined by ≡_{f}. Define Σ_{G′} to be the signature obtained by extending Σ_{G} with fresh l-ary operation symbols f_{1}, …, f_{n}. Next define R_{G′} to be the set of rules obtained by extending R_{G}, for each i, with rules derived from the rules in R_{i} by replacing the operation symbol in the source by f_{i}. It is immediate to see that each operation f_{i} so defined is weakly distinctive, and that (47) holds. Moreover, if G is compact then G′ also is, as we may assign to each new operation f_{i} the same weight as f. □

7.2 General GSOS Operations

In this subsection we show how to axiomatize non-smooth operations, thus lifting properties (27)–(30) to arbitrary GSOS languages with recursion.

First of all, we give a result that allows us to reduce the problem of axiomatizing arbitrary GSOS operations to that of axiomatizing smooth ones. The proof of the following proposition is an easy adaptation of those of [7, Lem. 4.13] and [4, Propn. 5.13].

Proposition 7.17 Suppose G is a GSOS system containing a non-smooth operation f with arity l. Then there exists a disjoint extension G′ of G with a smooth operation f′ with arity l′ (possibly different from l), and there exist vectors Z⃗ of l distinct process variables, and V⃗ of l′ variables in Z⃗ (possibly repeated), such that:

1. if G is compact, then so is G′;

2. for every disjoint extension H of G′, the equation f(Z⃗) = f′(V⃗) is sound with

respect to ∼_{Hrec}, i.e.,

f(Z⃗) ∼_{Hrec} f′(V⃗) .  (48)

In particular, as detailed in [7], when applied to the priority operation θ, the construction given in the proof of the above proposition generates the △ operation given by the rules (39), together with the equation:

θ(X) = X△X .

For any GSOS system G, the methods presented so far allow us to generate a disjoint extension H of G, and an inequational theory T with the required properties (27)–(30).

Theorem 7.18 Let G be a GSOS system. Then the disjoint extension H of G and inequational theory T produced by the algorithm of Figure 2 have the following properties:

1. If G is compact, then so is H.

2. For every GSOS system H′ that disjointly extends H, the inequations in T ∪{(Rec)} are sound with respect to ≲_{H′rec}.

3. T is Ω-head normalizing for every P ∈ T(Σ_{H}).

4. T is head normalizing for every P ∈ CREC(Σ_{H}, PVar) such that P ↓_{Hrec}.

5. T absorbes transitions.

Proof: Assume that G is a GSOS system. Let H and T be the GSOS system and the inequational theory generated by the algorithm in Figure 2.

First of all, it is easy to see that adding a disjoint copy of FINTREE_{Ω} to a compact GSOS system results in a compact GSOS system^{8}. Therefore, by Propn. 7.16 and Lem. 7.17, it follows that H is compact if G was.

Next, note that, by applying instances of equations (47) and (48) in T, we have that, for each P ∈ REC(H, PVar) there exists a term P^{∗} built from weakly distinctive operations and FINTREE_{Ω} operations only such that T ⊢ P = P^{∗}.

Finally, Theorems 7.13–7.15 can be applied to derive that T has properties 3–5 mentioned in the statement of the theorem. □

We are now finally in a position to prove the promised partial completeness theorem for compact GSOS languages, whose statement we reiterate below.

Theorem 6.15 Let G be a compact GSOS system. Then there exist a compact GSOS system H and a set of Σ_{H}-inequations T such that:

• H disjointly extends G and FINTREE_{Ω}, and

• for all P ∈ T(Σ_{H}), Q ∈ CREC(Σ_{H}, PVar), P ≲_{H} Q iff T ∪ {(4)} ⊢ P ≤ Q.

Proof: An immediate corollary of the above theorem and of Thm. 7.2. □

Theorem. 6.15 can be strengthened to a completeness theorem for the whole of the language CREC(Σ_{H}, PVar) with respect to ≲_{ω}, at the price of adding an infinitary proof rule to the theory T ∪ {(Rec)}. This proof rule, called ω-rule in [41], states that if every finite approximation of a program P is provably smaller than, or equal to, a program Q, then so is P. Formally:

\frac{∀n ∈ ℕ. P^{n} ≤ Q}{P ≤ Q}  (49)

where, for every n ∈ ℕ, P^{n} stands for the n-th finite approximation of P. (See Sect. 5.1 for details).

8The reader familiar with the developments in [7] might recall that the semantic well-foundedness of a GSOS system (see [7, Def. 6.1]) is in general not preserved by adding a disjoint copy of FINTREE, and a fortiori of FINTREE_{Ω}, to it. The same is true in our setting. As shown by our developments in this section, however, the kind of problem highlighted in [7, Sect. 6.1] does not arise if one considers the syntactic notion of compactness in lieu of the semantic one of well-foundedness.

Input  A GSOS system G.

Output A GSOS system H and an equational theory T with the properties mentioned in Thm. 7.18.

Step 1. If G does not disjointly extend FINTREE_{Ω} then add to it a disjoint copy of FINTREE_{Ω}.

Step 2. For each operation f that is non-smooth, apply the construction of Lemma 7.17 to extend the system with a smoothed version of f, f′. Add all the resulting instances of law (48) to T_{FINTREE_{Ω}}.

Step 3. For each smooth, non-weakly-distinctive operation f ∉ Σ_{FINTREE_{Ω}} in the resulting system, apply the construction of Propn. 7.16 to generate smooth, distinctive operations f_{1}, …, f_{n}. The system so-obtained is the H we were looking for. Add to the equational theory all the resulting instances of law (47).

Step 4. Add to the equational theory obtained in Step 3 the equations given by applying Theorem 7.13 to all the smooth, weakly distinctive operations in Σ_{H} − Σ_{FINTREE_{Ω}}. The result is the theory T we were looking for.

Figure 2: The algorithm

Theorem 7.19 (Completeness for ≲_{ω}) Let G be a compact GSOS system. Then the disjoint extension H of G and inequational theory T produced by the algorithm of Figure 2 have the property that, for every P, Q ∈ CREC(Σ_{H}, PVar),

P ≲_{ω} Q ⇔ T ∪ {(Rec)} ∪ {(49)} ⊢ P ≤ Q .

Proof: We prove the two implications separately.

• Soundness. By Thm. 7.18, we know that the inequations in T ∪ {(Rec)} are sound with respect to ≲_{Hrec}. As ≲_{Hrec}⊆≲_{ω}, they are a fortiori also sound with respect to ≲_{ω}. As H is a compact GSOS system, by Thm. 6.18 it follows that, for every P, Q ∈ CREC(Σ_{H}, PVar),

P ≲_{ω} Q ⇔ D[[P]] ⊑_{D} D[[Q]] .

As the relations induced by a denotational semantics are guaranteed to be precongruences, ≲_{ω} is a precongruence over CREC(Σ_{H}, PVar).

The only thing left to check is that the proof rule (49) is sound with respect to ≲_{ω} over CREC(Σ_{H}, PVar). To this end, assume that P, Q ∈ CREC(Σ_{H}, PVar), and that P^{n} ≲_{ω} Q for every n ∈ ℕ. We prove that P ≲_{ω} Q. In fact, as ≲_{ω} is algebraic by Thm. 6.17, the claim follows if we show that:

∀n ∈ ℕ∃m ∈ ℕ : P^{n} ≲_{ω} Q^{m} .  (50)

To prove (50), let P^{n} be a finite approximation of P. By assumption, we have that P^{n} ≲_{ω} Q. As H is compact and P^{n} is a recursion-free term, by Corollary 6.5, there exists t_{P^{n}} ∈ ST(Act) such that P^{n} ∼_{Hrec} t_{P^{n}}. By Lem. 2.5, it follows that P^{n} ≲_{Hrec} Q, and therefore that t_{P^{n}} ≲_{Hrec} Q. As H is compact, Thm. 6.16 gives that there exists a finite approximation Q^{m} of Q such that t_{P^{n}} ≲_{Hrec} Q^{m}. For such a Q^{m}, P^{n} ≲_{Hrec} Q^{m}. By Lem. 2.5, P^{n} ≲_{ω} Q^{m} follows.

We have thus shown that (50) holds. Hence P ≲_{ω} Q.

• Completeness. Let P, Q ∈ CREC(Σ_{H}, PVar) be such that P ≲_{ω} Q. We argue as

follows:

P ≲_{ω} Q ⇔ ∀n ∈ ℕ∃m ∈ ℕ : P^{n} ≲_{ω} Q^{m}

(By Thm. 6.17)

⇔ ∀n ∈ ℕ∃m ∈ ℕ : P^{n} ≲_{Hrec} Q^{m}

(By Lem. 2.5)

⇔ ∀n ∈ ℕ∃m ∈ ℕ : T ∪ {(Rec)} ⊢ P^{n} ≤ Q^{m}

(By Thm. 6.15)

⇒ ∀n ∈ ℕ. T ∪ {(Rec)} ⊢ P^{n} ≤ Q

(Q^{n} ≤_{Ω} Q implies T ⊢ Q^{n} ≤ Q)

⇒ T ∪ {(Rec)} ∪ {(49)} ⊢ P ≤ Q .

The proof of the theorem is now complete. □

8 Concluding Remarks

In this paper we have presented a general way of giving denotational semantics to compact GSOS languages [23, 19] in terms of the domain of synchronization trees D introduced by Abramsky in his seminal paper [1]. The class of compact GSOS languages consists of languages that have the structure of most standard process algebras; namely, they include a set of operations to construct finite, acyclic process graphs, and a facility for the recursive definition of behaviours. We have shown that the denotational semantics for compact GSOS languages automatically generated by our methods is guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder ≲^{F}. The relation ≲^{F} has also been shown to coincide with ≲_{ω} for arbitrary GSOS languages, as defined by Bloom, Istrail and Meyer in their original papers [23, 19].

As stepping stones towards the aforementioned fully abstract denotational semantics for compact GSOS languages, we have obtained several results of independent interest. In particular, we have offered a novel operational interpretation of GSOS languages in terms of labelled transition systems with divergence that relies heavily on a non-standard treatment of negative premises in GSOS rules. The outcome of our approach is, at least in our opinion, a simple operational semantics for GSOS languages in which negative premises are allowed to coexist with unguarded recursive definitions. In this set-up, the relations ≲ and ≲_{ω} are guaranteed to be precongruences for arbitrary GSOS systems, and a general algorithm, along the lines of those in [7], provides partially complete inequational axiomatizations for them in the sense of Hennessy [38]. Moreover, if the GSOS language under consideration is compact, our results guarantee that the preorder ≲_{ω} is algebraic, in the sense of, e.g., [41]; in this case, the partially complete axiomatization generated by our methods can be extended to a complete proof system over the whole of a compact GSOS language in standard fashion. The byproduct of the methods presented in this paper is a trinity of semantic views of processes (behavioural, axiomatic and denotational) that are guaranteed to be in complete agreement.

We hope that some of these general results, whose proofs for specific process description languages tend to be quite involved and mostly use variations on the same techniques, will turn out to be useful to some of the members of our research community.

8.1 The Benefits of Compactness

In this paper we have chosen to present in detail three different semantic theories for compact GSOS languages. The main benefit of working with this class of GSOS languages is that the whole body of results of algebraic semantics from references like [29, 33, 37, 41] has been at our disposal. This has allowed us to present general and, we hope, rather strong results on prebisimulation, denotational models and axiomatic semantics for such languages. Moreover, the class of compact GSOS languages includes many of the standard process description languages (at least in their finite alphabet versions), and the general results that rely on the compactness of the language under consideration we have been able to establish (e.g., the algebraicity of ≲_{ω} and the algorithm for generating a partially complete axiomatization for prebisimulation) apply to these languages. However, there are indeed some process description languages considered in the literature that are not compact. A notable example of a non-compact process description language is SCCS with the delay operation δ [38, 62], specified by the rules:

\overline{δ(x) →^{1} δ(x)}  \frac{x →^{a} x′}{δ(x) →^{a} x′}

The presence of this operation makes SCCS non-compact, and thus some of the results that we offer in the paper do not directly apply to it. However, the delay operation is not primitive in SCCS. In fact, for any process term P, it is easy to see that the following equality holds:

δ(P) ∼ fix(X = 1.X + P) .

(The reader familiar with [38] will have noticed that Hennessy uses the above equation to deal with the δ operation in constructing the term model for SCCS given in that reference.) Therefore restricting attention to the compact fragment of SCCS, as Abramsky does in [1], allows us to use our general results for compact GSOS languages to study properties of prebisimulation, and does not lose any expressive power. Similar considerations apply to non-compact versions of ACP obtained by adding variations on the Kleene star operation [51] to the set of core operations. (See, e.g., [18, 32].) For example, modulo a different treatment of termination, the prefix-iteration operation considered in [32] is specified by the rules:

\overline{a^{∗}x →^{a} a^{∗}x}  \frac{x →^{b} x′}{a^{∗}x →^{b} x′}

For any process term P, it can be checked that:

a^{∗}P ∼ fix(X = a.X + P) .

An example of an operation which, in conjunction with the δ operation, is responsible for the non-compactness of a language and that cannot be dealt with by reduction to a suitable recursive definition (at least in the setting considered in this paper) is the desynchronizing operation Δ given by the rules (one such rule for each a ∈ Act):

\frac{x →^{a} x′}{Δ(x) →^{a} δ(Δ(x′))}

This operation is present in the early versions of SCCS studied in [61, 38, 79]. As remarked in [79, Page 249], this operation is primitive, i.e., it cannot be expressed in terms of the other operations of SCCS.

8.2 Further Work

As suggested by the title of this paper, we plan to direct our research effort to the study of cpo-based denotational models for arbitrary GSOS languages, in such a way that many of the results we have obtained for compact languages carry over to the more general class. As mentioned in the main body of the paper, the preorder ≲_{ω} is, in general, not going to be algebraic over arbitrary GSOS languages. As highlighted by Lem. 5.1 and the discussion which follows the proof of Thm. 6.17, this essentially depends on the fact that, for such languages, the standard syntactic notion of finite approximation from [29, 37, 41] is in some sense inappropriate, as these terms may be semantically infinite. This means that more involved techniques might be needed for proofs of full abstraction. The approach to this kind of results developed in [38] might provide important hints for the solution. We think that it would also be interesting to develop the above theory for infinitary versions of GSOS languages, i.e., GSOS languages over a denumerable set of actions, and with possibly countably infinite sets of operations and rules. The work presented in, e.g., [4, 5] should provide guidelines for restricting our attention to those infinitary GSOS languages for which a continuous semantics can be given. (Cf. [10] for an example of a language without a continuous fully abstract semantics.)

On a more speculative note, the developments in [1, 2] hint at the possibility of using the machinery developed by Abramsky in the aforementioned references and our results on denotational semantics for compact GSOS languages to automatically generate compositional proof systems for variations on Hennessy-Milner logics [43]. We think that this is a very interesting avenue for future research, but much work remains to be done in this direction.

On the operational side, it would be interesting to establish substitutivity results for other prebisimulation-like relations that have been proposed in the literature, e.g., those studied by Walker in [92] and the specification preorder of Cleaveland and Steffen [28]. In particular, the study of rule formats for bisimulation-like relations that abstract from unobservable transitions in process behaviours presented in [22] should be adapted to yield substitutivity results for (some of) the preorders studied by Walker in [92].

The work we have presented in this paper represents an attempt to generalize to a class of GSOS languages a collection of deep results that have been developed for several process description languages in the literature. We believe that this kind of meta-theoretic work is, by its own nature, experimental, and we hope that the reader will bear with us for the experimental nature of the work we offer in this study. The goodness of the results we present is the result of a trade-off between simplicity of definitions and proofs, and the degree in which our work offers the results presented in the literature when applied to particular languages.

We hope that we have given our readers convincing evidence that the theory we have developed does specialize to the known ones for, e.g., SCCS [62], CCS [64] and versions of ACP [17] with action-prefixing in lieu of general sequential composition. However, we make no claim that this work is optimal in any formal sense or applies equally well to all known languages. In fact, we believe that there is much room for improvement, but that our approach will work with minor adaptations also in the improved developments. For example, our operational interpretation of GSOS languages relies on the definition of a convergence predicate over programs. As argued in the paper, the convergence predicate given in Def. 4.1 delivers results that are in agreement with those presented in the literature for several process description languages. However, the treatment of convergence afforded by Def. 4.1 is, in certain cases, too syntactic. For example, the clauses in that definition can not be used to derive that the term a; Ω is convergent, where “;” stands for the sequencing operation given in [19] by the rules:

\frac{x →^{a} x′}{x; y →^{a} x′; y}  \frac{x ↛^{b} (∀b ∈ Act), y →^{a} y′}{x; y →^{a} y′}

We believe that a more general treatment of convergence can be obtained by using ruloids, in the sense of [19], in lieu of rules in an appropriate way.

We also think that there is room for improvement in the algorithm used in the proof of the partial completeness theorem for compact GSOS languages. For example, it would be nice to make the inaction laws and the action laws generated by Lemmas 7.7 and 7.11, respectively, more aesthetically pleasing.

We plan to address these issues in our future work on the topics of this paper.

Acknowledgements: Many thanks to Matthew Hennessy and Edmund Robinson for their helpful remarks that led to the technical developments in Sect. 4. We should also like to express our gratitude to Jan Rutten for patiently answering our questions on his work, and providing pointers to the literature.

References

[1] S. Abramsky, A domain equation for bisimulation, Information and Computation, 92 (1991), pp. 161–218.

[2] , Domain theory in logical form, Annals of Pure and Applied Logic, 51 (1991), pp. 1–77.

[3] S. Abramsky and S. Vickers, Quantales, observational logic, and process semantics, Report DOC 90/1, Department of Computing, Imperial College, 1990. A journal version of this paper has appeared in Mathematical Structures in Computer Science in 1993.

[4] L. Aceto, Deriving complete inference systems for a class of GSOS languages generating regular behaviours, Report IR 93–2009, Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University, Aalborg, November 1993. Also available as Computer Science Report 1/94, University of Sussex, January 1994.

[5] , Deriving complete inference systems for a class of GSOS languages generating regular behaviours, in Jonsson and Parrow [49], pp. 449–464.

[6] , GSOS and finite labelled transition systems, Theoretical Comput. Sci., 131 (1994), pp. 181–195.

[7] L. Aceto, B. Bloom, and F. Vaandrager, Turning SOS rules into equations, Information and Computation, 111 (1994), pp. 1–52.

[8] L. Aceto and M. Hennessy, Termination, deadlock and divergence, J. Assoc. Comput. Mach., 39 (1992), pp. 147–187.

[9] P. Aczel, Non-well-founded Sets, vol. 14 of CSLI Lecture Notes, Stanford University, 1988.

[10] K. Apt and G. Plotkin, Countable nondeterminism and random assignment, J. Assoc. Comput. Mach., 33 (1986), pp. 724–767.

[11] D. Austry and G. Boudol, Algèbre de processus et synchronisations, Theoretical Comput. Sci., 30 (1984), pp. 91–131.

[12] E. Badouel and P. Darondeau, On guarded recursion (Note), Theoretical Comput. Sci., 82 (1991), pp. 403–408.

[13] , Structural operational specifications and trace automata, in Proceedings CON-CUR 92, Stony Brook, NY, USA, W. Cleaveland, ed., vol. 630 of Lecture Notes in Computer Science, Springer-Verlag, 1992, pp. 302–316.

[14] J. Baeten and J. Bergstra, A survey of axiom systems for process algebras, Report P9111, University of Amsterdam, Amsterdam, Oct. 1991.

[15] J. Baeten, J. Bergstra, and J. Klop, Syntax and defining equations for an interrupt mechanism in process algebra, Fundamenta Informaticae, IX (1986), pp. 127– 168.

[16] J. Baeten and C. Verhoef, A congruence theorem for structured operational semantics, in Proceedings CONCUR 93, Hildesheim, E. Best, ed., vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 477–492.

[17] J. Baeten and W. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

[18] J. Bergstra, I. Bethke, and A. Ponse, Process algebra with iteration and nesting, Report P9314b, University of Amsterdam, Amsterdam, February 1994.

[19] B. Bloom, Ready Simulation, Bisimulation, and the Semantics of CCS-like Languages, PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Aug. 1989.

[20] , Many meanings of monosimulation: denotational, operational, and logical characterizations of a notion of simulation of concurrent processes, 1991. Unpublished manuscript.

[21] , Ready, set, go: Structural operational semantics for linear-time process algebras, Tech. Rep. TR 93-1372, Cornell, August 1993.

[22] , Structural operational semantics for weak bisimulations, Tech. Rep. TR 93-1373, Cornell, August 1993.

[23] B. Bloom, S. Istrail, and A. Meyer, Bisimulation can’t be traced: preliminary report, in Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988, pp. 229–239. Full version available as Technical Report 90-1150, Department of Computer Science, Cornell University, Ithaca, New York, August 1990. To appear in the Journal of the ACM.

[24] R. Bol and J. Groote, The meaning of negative premises in transition system specifications (extended abstract), in Proceedings 18^{th} ICALP, Madrid, J. Leach Albert, B. Monien, and M. Rodríguez, eds., vol. 510 of Lecture Notes in Computer Science, Springer-Verlag, 1991, pp. 481–494. Full version available as Report CS-R9054, CWI, Amsterdam, 1990.

[25] S. Brookes, C. Hoare, and A. Roscoe, A theory of communicating sequential processes, J. Assoc. Comput. Mach., 31 (1984), pp. 560–599.

[26] S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, eds., Mathematical Foundations of Programming Semantics, 7^{th} International Conference, Pittsburgh, PA, USA, March 1991, vol. 598 of Lecture Notes in Computer Science, Springer-Verlag, 1992.

[27] R. Cleaveland and M. Hennessy, Priorities in process algebras, Information and Computation, 87 (1990), pp. 58–77.

[28] R. Cleaveland and B. Steffen, A preorder for partial process specification, in Proceedings CONCUR 90, Amsterdam, J. Baeten and J. Klop, eds., vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 141–151.

[29] B. Courcelle and M. Nivat, Algebraic families of interpretations, in Proceedings 17^{th} Symposium on Foundations of Computer Science, 1976.

[30] R. De Nicola and M. Hennessy, Testing equivalences for processes, Theoretical Comput. Sci., 34 (1984), pp. 83–133.

[31] , CCS without τ’s, in Proceedings TAPSOFT 87, Vol. I, H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, eds., vol. 249 of Lecture Notes in Computer Science, Springer-Verlag, 1987.

[32] W. Fokkink, A complete equational axiomatisation for prefix integration, Technical Report CS-R9415, CWI, Amsterdam, 1994.

[33] J. Goguen, J. Thatcher, E. Wagner, and J. Wright, Initial algebra semantics and continuous algebras, J. Assoc. Comput. Mach., 24 (1977), pp. 68–95.

[34] M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF, vol. 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.

[35] J. Groote, Transition system specifications with negative premises, Report CS-R8950, CWI, Amsterdam, 1989. An extended abstract appeared in J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, LNCS 458, pages 332–341. Springer-Verlag, 1990.

[36] J. Groote and F. Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, 100 (1992), pp. 202–260.

[37] I. Guessarian, Algebraic Semantics, vol. 99 of Lecture Notes in Computer Science, Springer-Verlag, 1981.

[38] M. Hennessy, A term model for synchronous processes, Information and Control, 51 (1981), pp. 58–75.

[39] , Synchronous and asynchronous experiments on processes, Information and Control, 59 (1983), pp. 36–83.

[40] , Acceptance trees, J. Assoc. Comput. Mach., 32 (1985), pp. 896–928.

[41] , Algebraic Theory of Processes, MIT Press, Cambridge, Massachusetts, 1988.

[42] M. Hennessy and A. Ingólfsdóttir, A theory of communicating processes with value-passing, Information and Computation, 107 (1993), pp. 202–236.

[43] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32 (1985), pp. 137–161.

[44] M. Hennessy and G. Plotkin, Full abstraction for a simple programming language, in 8^{th} Symposium on Mathematical Foundations of Computer Science, J. Bečvář, ed., vol. 74 of Lecture Notes in Computer Science, Springer-Verlag, 1979, pp. 108–120.

[45] , A term model for CCS, in 9^{th} Symposium on Mathematical Foundations of Computer Science, P. Dembiński, ed., vol. 88 of Lecture Notes in Computer Science, Springer-Verlag, 1980, pp. 261–274.

[46] C. Hoare, Communicating Sequential Processes, Prentice-Hall International, Englewood Cliffs, 1985.

[47] A. Ingólfsdóttir, Semantic Models for Communicating Process with Value-Passing, PhD thesis, School of Congnitive and Computing Sciences, University of Sussex, June 1994. Computer Science Report 8/94. Also available as Report R–94– 2044, Department of Mathematics and Computer Science, Aalborg University.

[48] H. Jifeng and C. Hoare, From algebra to operational semantics, Inf. Process. Lett., 45 (1993), pp. 75–80.

[49] B. Jonsson and J. Parrow, eds., Proceedings CONCUR 94, Uppsala, vol. 836 of Lecture Notes in Computer Science, Springer-Verlag, 1994.

[50] R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.

[51] S. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, C. Shannon and J. McCarthy, eds., Princeton University Press, 1956, pp. 3– 41.

[52] J. Loeckx and K. Sieber, The Foundations of Program Verification, Wiley-Teubner Series in Computer Science, John Wiley & Sons, 1987.

[53] E. Madelaine and D. Vergamini, Finiteness conditions and structural construction of automata for all process algebras, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 3 (1991), pp. 275–292.

[54] A. Meyer, Semantical paradigms: Notes for an invited lecture, in Third Annual Symposium on Logic in Computer Science Edinburgh, IEEE Computer Society Press, 1988, pp. 236–242.

[55] G. Milne and R. Milner, Concurrent processes and their syntax, J. Assoc. Comput. Mach., 26 (1979), pp. 302–321.

[56] R. Milner, Processes: A mathematical model of computing agents, in Proceedings Logic Colloquium 1973, H. Rose and J. Shepherdson, eds., North-Holland, 1973, pp. 158–173.

[57] , Fully abstract models of typed lambda-calculi, Theoretical Comput. Sci., 4 (1977), pp. 1–22.

[58] , Flowgraphs and flow algebras, J. Assoc. Comput. Mach., 26 (1979), pp. 794– 818.

[59] , A Calculus of Communicating Systems, vol. 92 of Lecture Notes in Computer Science, Springer-Verlag, 1980.

[60] , A modal characterisation of observable machine behaviour, in Proceedings CAAP 81, G. Astesiano and C. Bohm, eds., vol. 112 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 25–34.

[61] , On relating synchrony and asynchrony, Tech. Rep. CSR–75–80, Department of Computer Science, University of Edinburgh, 1981.

[62] , Calculi for synchrony and asynchrony, Theoretical Comput. Sci., 25 (1983), pp. 267–310.

[63] , Operational and algebraic semantics of concurrent processes, Tech. Rep. ECS-LFCS-88-46, Department of Computer Science, University of Edinburgh, February 1988.

[64] , Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

[65] , Elements of interaction (Turing Award Lecture), Comm. ACM, 36 (1993), pp. 78–89.

[66] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

[67] G. Plotkin, A powerdomain construction, SIAM J. Comput., 5 (1976), pp. 452–487.

[68] , LCF considered as a programming language, Theoretical Comput. Sci., 5 (1977), pp. 223–255.

[69] , Lecture notes in domain theory, 1981. University of Edinburgh.

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

[71] K. Rosenthal, Quantales and their Applications, Research Notes in Mathematics, Pitman, London, 1990.

[72] J. Rutten, Deriving denotational models for bisimulation from structured operational semantics, in Proceedings IFIP Working Conference on Programming Concepts and Methods, Sea of Gallilea, Israel, M. Broy and C. Jones, eds., North-Holland, 1990.

[73] , Nonwellfounded sets and programming language semantics, in Brookes et al. [26], pp. 193–206.

[74] , Processes as terms: non-well-founded models for bisimulation, Mathematical Structures in Computer Science, 2 (1992), pp. 257–275.

[75] J. Rutten and D. Turi, Initial algebra and final coalgebra semantics for concurrency, in A decade of concurrency, J. de Bakker, W. de Roever, and G. Rozenberg, eds., vol. 803 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp. 530– 581. Also available as Technical Report CS-R9409, CWI, Amsterdam.

[76] D. Scott, The lattice of flow diagrams, in Symposium on Semantics of Algorithmic Languages, E. Engeler, ed., vol. 188 of Lecture Notes in Mathematics, Springer-Verlag, 1971, pp. 311–366.

[77] D. Scott and C. Strachey, Towards a mathematical semantics for computer languages, in Proceedings of the Symposium on Computers and Automata, vol. 21 of Microwave Research Institute Symposia Series, 1971.

[78] R. d. Simone, Calculabilité et Expressivité dans l’Algebra de Processus Parallèles Meije, thèse de 3^{e} cycle, Univ. Paris 7, 1984.

[79] , Higher-level synchronising devices in meije–SCCS, Theoretical Comput. Sci., 37 (1985), pp. 245–267.

[80] S. Smith, From operational to denotational semantics, in Brookes et al. [26], pp. 54– 76.

[81] M. Smyth, Powerdomains, J. Comput. System Sci., 16 (1978).

[82] C. Stirling, Modal logics for communicating systems, Theoretical Comput. Sci., 49 (1987), pp. 311–347.

[83] , Modal and temporal logics, in Handbook of Logic in Computer Science, Vol I, S. Abramsky, D. Gabbay, and T. Maibaum, eds., vol. 2, Oxford University Press, 1992, pp. 477–563.

[84] V. Stoltenberg-Hansen, I. Lindström, and E. Griffor, Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science 22, Cambridge University Press, 1994.

[85] A. Stoughton, Fully abstract models of programming languages, Research Notes in Theoretical Computer Science, Pitman, London, 1988.

[86] , Substitution revisited, Theoretical Comput. Sci., 59 (1988), pp. 317–325.

[87] I. Ulidowski, Equivalences on observable processes, in Proceedings 7^{th} Annual Symposium on Logic in Computer Science, Santa Cruz, California, IEEE Computer Society Press, 1992, pp. 148–159.

[88] F. Vaandrager, On the relationship between process algebra and input/output automata (extended abstract), in Proceedings 6^{th} Annual Symposium on Logic in Computer Science, Amsterdam, IEEE Computer Society Press, 1991, pp. 387–398.

[89] , Expressiveness results for process algebras, in Proceedings REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, J. de Bakker, W. de Roever, and G. Rozenberg, eds., vol. 666 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 609–638.

[90] C. Verhoef, A general conservative extension theorem in process algebra, Report CSN 93/38, Eindhoven University of Technology, 1993.

[91] , A congruence theorem for structured operational semantics with predicates and negative premises, in Jonsson and Parrow [49], pp. 433–448.

[92] D. Walker, Bisimulation and divergence, Information and Computation, 85 (1990), pp. 202–241.

Recent Publications in the BRICS Report Series

RS-94-40 Luca Aceto and Anna Ing� olfsd� ottir. CPO Models for GSOS Languages � Part I: Compact GSOS Languages. December 1994. 70 pp. An extended abstract of the paper will appear in: Proceedings of CAAP ’95, LNCS, 1995.

RS-94-39 Ivan Damg� ard, Oded Goldreich, and Avi Wigderson. Hashing Functions can Simplify Zero-Knowledge Protocol Design (too). November 1994. 18 pp.

RS-94-38 Ivan B. Damg� ard and Lars Ramkilde Knudsen. Enhancing the Strength of Conventional Cryptosystems. November 1994. 12 pp.

RS-94-37 Jaap van Oosten. Fibrations and Calculi of Fractions. November 1994. 21 pp.

RS-94-36 Alexander A. Razborov. On provably disjoint NP-pairs. November 1994. 27 pp.

RS-94-35 Gerth St�lting Brodal. Partially Persistent Data Structures of Bounded Degree with Constant Update Time. November 1994. 24 pp.

RS-94-34 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. October 1994. 18 pp. Appears in: Proceedings of LICS ’94, IEEE Computer Society Press.

RS-94-33 Vladimiro Sassone. Strong Concatenable Processes: An Approach to the Category of Petri Net Computations. October 1994. 40 pp.

RS-94-32 Alexander Aiken, Dexter Kozen, and Ed Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. October 1994. 33 pp.

RS-94-31 Noam Nisan and Amnon Ta-Shma. Symmetric Logspace is Closed Under Complement. September 1994. 8 pp.

RS-94-30 Thore Husfeldt. Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink. September 1994. 26 pp.