Proceedings of the 3rd Workshop on
Structural Operational Semantics

Bonn, Germany, 26th August 2006

Editors: Rob van Glabbeek and Peter D. Mosses

in ENTCS 175(1).

Preface Rob van Glabbeek and Peter Mosses

Invited Speaker Title/Abstract
Bartek Klin Bialgebraic Methods 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 specifications. 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 talk, the current state of the art in the area of bialgebraic semantics is presented, and its prospects for the future are sketched. In particular, a combination of basic bialgebraic techniques with a categorical approach to modal logics is described, as an abstract approach to proving compositionality by decomposing modal logics over structural operational specifications.

Robin Milner
(a joint Express-Infinity-SOS talk) 		Bigraphs, Multi-local Names and Confluence
(Appears in EXPRESS proceedings - not in these SOS proceedings)

The first test of bigraphs has been on the uniform generation of labelled transition systems (LTSs) whose labels are simple contexts. More recently they are being explored as a way of describing and programming realistic systems, which often involve movement in physical space as well as in the virtual space of (collections of) programs. In this talk I explain two aspects of such work.

First, we need to explore how names can have a definite scope, but still allow useful forms of mobility. In pure bigraphs all names are global (unlimited scope); in local bigraphs, all names are local (confined to one or more regions). One may need a combination of local and global names, but we should first clarify the expressive power of local names alone.

Second, an important aspect of dynamics --at least as important as LTSs-- is the study of confluent reactive systems. Real systems are likely to resolve into confluent and non-confluent parts. We would therefore like to extend techniques for handling confluence (e.g. in lambda calculus) to the more unruly domain of bigraphs. It is strictly more unruly: for example, redexes are no longer either independent or nested; they can intertwine!

In this talk, I shall

  1. introduce local bigraphs and some new operations upon them;
  2. give general conditions which guarantee weak confluence in a bigraphical reactive system, illustrating them for a simple encoding of lambda calculus (which indeed satisfies them).
I shall also ask: are bigraphs amenable to methods (such as the finiteness of developments) that strengthen weak confluence? If so, then work on the lambda calculus finds a new sphere of application.

Accepted Papers

Author(s) Title/Abstract
Simone Tini Notes on Generative Probabilistic Bisimulation

We consider the model of Generative Probabilistic Transition Systems, and Baier and Hermanns' notion of weak bisimulation defined over them. We prove that, if we consider any process algebra giving rise to a Generative Probabilistic Transition System satisfying the condition of regularity and offering prefixing, interleaving, and guarded recursion, then the coarsest congruence that is contained in weak bisimulation is strong bisimulation.

Vincent Danos, Jean Krivine
& Fabien Tarissan 		Self-assembling Trees

RCCS is a variant of Milner's CCS where processes are allowed a controlled form of backtracking. It turns out that the RCCS reinterpretation of a CCS process is equivalent, in the sense of weak bisimilarity, to its causal transition system in CCS. This can be used to develop an efficient method for designing distributed algorithms, which we illustrate here by deriving a distributed algorithm for assembling trees. Such a problem requires solving a highly distributed consensus, and a comparison with a traditional CCS-based solution shows that the code we obtain is shorter, easier to understand, and easier to prove correct by hand, or even to verify.

Henrik Pilegaard, Flemming Nielson & Hanne Riis Nielson Active Evaluation Contexts for Reaction Semantics

In the context of process algebras it is customary to define semantics in the form of a reaction relation supported by a structural congruence relation. Recently process algebras have grown more expressive in order to meet the modelling demands of fields as diverse as business modelling and systems biology. This leads to combining various features, such as general choice and parallelism that were previously studied separately, and it often becomes difficult to define the reaction semantics. We present a general approach based on Active Evaluation Contexts that allows the reaction semantics to be easily constructed.

Christiano Braga
& Alberto Verdejo 		Modular Structural Operational Semantics with Strategies

Strategies are a powerful mechanism to control rule application in rule-based systems. For instance, different transition relations can be defined and then combined by means of strategies, giving rise to an effective tool to define the semantics of programming languages. We have endowed the Maude MSOS Tool (MMT), an executable environment for modular structural operational semantics, with the possibility of defining strategies over its transition rules, by combining MMT with the Maude strategy language interpreter prototype. The combination was possible due to Maude\'s reflective capabilities. One possible use of MMT with strategies is to execute Ordered SOS specifications. We show how a particular form of strategy can be defined to represent an OSOS order and therefore execute, for instance, SOS specifications with negative premises. In this context, we also discuss how two known techniques for the representation of negative premises in OSOS become simplified in our setting.

MohammadReza Mousavi
& Michel A. Reniers 		On Well-Foundedness and Expressiveness of Promoted Tyft

In this paper, we solve two open problems posed by Karen L. Bernstein regarding her promoted tyft format for structured operational semantics. We show that, unlike formats with closed terms as labels, such as the tyft format, the well-foundedness assumption cannot be dropped for the promoted tyft format while preserving the congruence result. We also show that the well-founded promoted tyft format is incomparable to the tyft format with closed terms as labels, i.e., there are transition relations that can be specified by the promoted tyft format but not by the tyft format, and vice versa.

Adrian Pop & Peter Fritzson An Eclipse-based Integrated Environment for Developing Executable Structural Operational Semantics Specifications
(tool demonstration)

The Structural Operational Semantics Development Tooling (SOSDT) Eclipse Plugin integrates the Relational Meta-Language (RML) compiler and debugger with the Eclipse Integrated Development Environment Framework. SOSDT, together with the RML compiler and debugger, provides an environment for developing and maintaining executable Structural Operational Semantics specifications, including the Natural Semantics big step variant of SOS specifications. The RML language is successfully used at our department for writing large specifications for a range of languages like Java, Modelica, Pascal, MiniML etc. The SOSDT environment includes support for browsing, code completion through menus or popups, code checking, automatic indentation, and debugging of specifications.

Rob van Glabbeek, Formal Methods Group, National ICT Australia.