Special Issue of

Information & Computation

on Structural Operational Semantics

Information & Computation 207(2)

Accepted Papers

Preface	Rob van Glabbeek and Peter Mosses

Author(s) Title/Abstract

MohammadReza Mousavi,
Iain C.C. Phillips,
Michel A. Reniers
& Irek Ulidowski Semantics and Expressiveness of Ordered SOS
Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications.
Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their relative suitability. We also give semantics-preserving transformations between the two paradigms, namely SOS with negative premises and SOS with orderings. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.

Irek Ulidowski
& Shoji Yuen Generating Priority Rewrite Systems for Ordered SOS Process Languages
We propose an algorithm for generating a Priority Rewrite System (PRS) for an arbitrary process language in the Ordered SOS (OSOS) format such that rewriting of process terms is sound for bisimulation and head normalising. The algorithm is inspired by a procedure which was developed by Aceto, Bloom and Vaandrager and presented in the paper titled ``Turning SOS Rules into Equations''.
For a subclass of OSOS process languages representing finite behaviours the PRSs that are generated by our algorithm are strongly normalising (terminating) and confluent, where termination is proved using the dependency pair and dependency graph techniques. Additionally, such PRSs are complete for bisimulation on closed process terms modulo associativity and commutativity of the choice operator of CCS. We illustrate the usefulness of our results, and the benefits of rewriting with priorities in general, with several examples.

David de Frutos Escrig
& Carlos Gregorio Rodríguez (Bi)Simulations Up-to Characterise Process Semantics
In this paper we define simulations up-to a preorder and show how we can use them to provide a coinductive, simulation-like, characterisation of semantic preorders for processes. The result applies to a wide class of preorders, in particular to all the semantic preorders for reactive systems that appear under the ready simulation in the linear time-branching time spectrum. An interesting but unexpected result was that when starting from an equivalence relation the simulation up-to it is a canonical preorder whose kernel is the given equivalence relation. These canonical preorders have several nice properties, the main of which is that since all of them are defined in an homogeneous way, we can prove their properties in a generic way. In particular, we present an axiomatic characterisation of each of these canonical preorders, that is obtained simply by adding a single axiom to the axiomatization of the original equivalence relation. This gives us an alternative axiomatization for any axiomatizable preorder in the linear time-branching time spectrum, whose correctness and completeness can be proved once and for all.
Besides, if we compare the classic axiomatizations we already had with the one provided by our general theorem, it is very easy to conclude the completeness of them from that of the new axiomatization, thus getting a quite shorter proof of it than the original one.

Samuel Hym Mobility control via passports
Dπ is a simple distributed extension of the π-calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations.
In this paper we introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes.
Passports allow locations to control incoming processes. This induces a major modification to the possible observations which can be made of agent-based systems. Using the type system we describe these observations, and use them to build a loyal notion of observational equivalence for this setting. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.

Massimo Merro An Observation Theory for Mobile Ad Hoc Networks
We propose a process calculus to study the observational theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of simulation and bisimulation for ad hoc networks. As a main result, we prove that the (weak) labelled bisimilarity completely characterises (weak) reduction barbed congruence, a standard, branching-time, contextually-defined program equivalence. We then use our (bi)simulation proof methods to formally prove a number of non-trivial properties of ad hoc networks.

Marcelo Fiore
& Sam Staton A Congruence Rule Format for Name-Passing Process Calculi
We introduce a GSOS-like rule format for name-passing process calculi. Specifications in this format correspond to theories in nominal logic. The intended models of such specifications arise by initiality from a general categorical model theory. For operational semantics given in this rule format, a natural behavioural equivalence --- a form of open bisimilarity --- is a congruence.

Bartek Klin Bialgebraic Methods and Modal Logic in Structural Operational Semantics
Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of syntax and system behaviour, thus treating various kinds of operational descriptions in a uniform fashion.
In this paper, bialgebraic semantics is combined with a coalgebraic approach to modal logic in a novel, general approach to proving the compositionality of process equivalences for languages defined by structural operational semantics. To prove compositionality, one provides a notion of behaviour for logical formulas, and defines an SOS-like specification of modal operators which reflects the original SOS specification of the language. This approach can be used to define SOS congruence formats as well as to prove compositionality for specific languages and equivalences.

Patrick Cousot
& Radhia Cousot Bi-inductive Structural Semantics
We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structured operational semantics to describe simultaneously the finite and infinite behaviors of programs. This is illustrated on grammars and the call-by-value λ-calculus.

Xavier Leroy
& Hervé Grall Coinductive big-step operational semantics
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers.
A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results.

Traian Florin Serbanuta,
Grigore Rosu
& José Meseguer A Rewriting Logic Approach to Operational Semantics
This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.

Janis Voigtlaender
& Patricia Johann A Family of Syntactic Logical Relations for the Semantics of Haskell-like Languages
Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.

Author(s)	Title/Abstract
MohammadReza Mousavi, Iain C.C. Phillips, Michel A. Reniers & Irek Ulidowski	Semantics and Expressiveness of Ordered SOS
Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications. Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their relative suitability. We also give semantics-preserving transformations between the two paradigms, namely SOS with negative premises and SOS with orderings. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.
Irek Ulidowski & Shoji Yuen	Generating Priority Rewrite Systems for Ordered SOS Process Languages
We propose an algorithm for generating a Priority Rewrite System (PRS) for an arbitrary process language in the Ordered SOS (OSOS) format such that rewriting of process terms is sound for bisimulation and head normalising. The algorithm is inspired by a procedure which was developed by Aceto, Bloom and Vaandrager and presented in the paper titled ``Turning SOS Rules into Equations''. For a subclass of OSOS process languages representing finite behaviours the PRSs that are generated by our algorithm are strongly normalising (terminating) and confluent, where termination is proved using the dependency pair and dependency graph techniques. Additionally, such PRSs are complete for bisimulation on closed process terms modulo associativity and commutativity of the choice operator of CCS. We illustrate the usefulness of our results, and the benefits of rewriting with priorities in general, with several examples.
David de Frutos Escrig & Carlos Gregorio Rodríguez	(Bi)Simulations Up-to Characterise Process Semantics
In this paper we define simulations up-to a preorder and show how we can use them to provide a coinductive, simulation-like, characterisation of semantic preorders for processes. The result applies to a wide class of preorders, in particular to all the semantic preorders for reactive systems that appear under the ready simulation in the linear time-branching time spectrum. An interesting but unexpected result was that when starting from an equivalence relation the simulation up-to it is a canonical preorder whose kernel is the given equivalence relation. These canonical preorders have several nice properties, the main of which is that since all of them are defined in an homogeneous way, we can prove their properties in a generic way. In particular, we present an axiomatic characterisation of each of these canonical preorders, that is obtained simply by adding a single axiom to the axiomatization of the original equivalence relation. This gives us an alternative axiomatization for any axiomatizable preorder in the linear time-branching time spectrum, whose correctness and completeness can be proved once and for all. Besides, if we compare the classic axiomatizations we already had with the one provided by our general theorem, it is very easy to conclude the completeness of them from that of the new axiomatization, thus getting a quite shorter proof of it than the original one.
Samuel Hym	Mobility control via passports
Dπ is a simple distributed extension of the π-calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations. In this paper we introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes. Passports allow locations to control incoming processes. This induces a major modification to the possible observations which can be made of agent-based systems. Using the type system we describe these observations, and use them to build a loyal notion of observational equivalence for this setting. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.
Massimo Merro	An Observation Theory for Mobile Ad Hoc Networks
We propose a process calculus to study the observational theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of simulation and bisimulation for ad hoc networks. As a main result, we prove that the (weak) labelled bisimilarity completely characterises (weak) reduction barbed congruence, a standard, branching-time, contextually-defined program equivalence. We then use our (bi)simulation proof methods to formally prove a number of non-trivial properties of ad hoc networks.
Marcelo Fiore & Sam Staton	A Congruence Rule Format for Name-Passing Process Calculi
We introduce a GSOS-like rule format for name-passing process calculi. Specifications in this format correspond to theories in nominal logic. The intended models of such specifications arise by initiality from a general categorical model theory. For operational semantics given in this rule format, a natural behavioural equivalence --- a form of open bisimilarity --- is a congruence.
Bartek Klin	Bialgebraic Methods and Modal Logic in Structural Operational Semantics
Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to formal reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of syntax and system behaviour, thus treating various kinds of operational descriptions in a uniform fashion. In this paper, bialgebraic semantics is combined with a coalgebraic approach to modal logic in a novel, general approach to proving the compositionality of process equivalences for languages defined by structural operational semantics. To prove compositionality, one provides a notion of behaviour for logical formulas, and defines an SOS-like specification of modal operators which reflects the original SOS specification of the language. This approach can be used to define SOS congruence formats as well as to prove compositionality for specific languages and equivalences.
Patrick Cousot & Radhia Cousot	Bi-inductive Structural Semantics
We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structured operational semantics to describe simultaneously the finite and infinite behaviors of programs. This is illustrated on grammars and the call-by-value λ-calculus.
Xavier Leroy & Hervé Grall	Coinductive big-step operational semantics
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results.
Traian Florin Serbanuta, Grigore Rosu & José Meseguer	A Rewriting Logic Approach to Operational Semantics
This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.
Janis Voigtlaender & Patricia Johann	A Family of Syntactic Logical Relations for the Semantics of Haskell-like Languages
Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.

Rob van Glabbeek, National ICT Australia.
Peter D. Mosses,