Wroclaw, Poland, 9th July 2007
Editors: Rob van Glabbeek and Matthew Hennessy
|Preface||Rob van Glabbeek and Matthew Hennessy|
|Pawel Sobocinski||A well-behaved LTS for the Pi-calculus (abstract)|
The pi-calculus and its many variations have received much attention in the literature. We discuss the standard early labelled transition system (LTS) and outline an approach which decomposes the system into two components, one of which is presented in detail. The advantages of using the decomposition include a more complete understanding of the treatment of bound outputs in Pi as well as an LTS which is more robust with respect to the addition and removal of language features. The present paper serves as an overview of some of the techniques involved and some of the goals of the ongoing work.
|David Frutos Escrig and Carlos Gregorio Rodríguez||Simulations up-to and Canonical Preorders (extended abstract)|
In this paper we define simulations up-to a preorder and show how we can use them to provide a coinductive, simulation-like, characterization of semantic preorders for processes. The result applies to a wide class of preorders, in particular to all semantic preorders coarser than the ready simulation preorder in the linear time-branching time spectrum. An interesting but unexpected result is that, when built from an equivalence relation, the simulation up-to is a canonical preorder whose kernel is the given equivalence relation. These canonical preorders have several nice properties, the main being that since all of them are defined in a homogeneous way, their properties can be proved in a generic way. In particular, we present an axiomatic characterization of each of these canonical preorders, that is obtained just by adding a single axiom to the axiomatization of the original equivalence relation. This gives us an alternative axiomatization for every axiomatizable preorder in the linear time-branching time spectrum, whose correctness and completeness can be proved once and for all.
|Patrick Cousot and Radhia Cousot||Bi-inductive Structural Semantics (extended abstract)|
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 structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value λ-calculus.
|Harald Fecher and Heiko Schmidt||Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems|
Process algebras are standard formalisms for compositionally describing systems by the dependencies of their observable synchronous communication. In concurrent systems, parallel composition introduces resolvable nondeterminism, i.e., nondeterminism that will be resolved in later design phases or by the operating system. Sometimes it is also important to express inherent nondeterminism for equal (communication) labels. Here, we give operational and axiomatic semantics to a process algebra having a parallel operator interpreted as concurrent and having a choice operator interpreted as inherent, not only with respect to different, but also with respect to equal next-step actions. In order to handle the different kinds of nondeterminism, the operational semantics uses mu-automata as underlying semantical model. Soundness and completeness of our axiom system with respect to the operational semantics is shown.
|Jesper Bengtson and Joachim Parrow||A completeness proof for bisimulation in the pi-calculus using Isabelle|
We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt; rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.
|Astrid Kiehn||An Operational Semantics for Shared Messaging Communication|
Shared Messaging Communication (SMC) has been introduced by Kiran et.al. as a model of communication which reduces communication costs (both in terms of communication latency and memory usage) by allowing tasks to communicate data through special shared memory regions. Sending a reference to an otherwise inaccessible memory regions rather than the data itself, the model combines the advantages of message passing and shared memories. Experimental results have shown that SMC in case of large data payloads clearly outperforms the classical message passing. In this paper we give a formal operational semantics to SMC exhibiting unambiguously the effect of executing an SMC command on local and shared memories. Based on this semantics we show that any program using message passing can be proved to be weakly bisimilar to one based on SMC and that with respect to communication costs the latter is amortised cheaper.
|Iain Phillips and Irek Ulidowski||Reversibility and Models for Concurrency|
There is a growing interest in models of reversible computation driven by exciting application areas such as bio-systems and quantum computing. Reversible process algebras RCCS (Danos and Krivine) and CCSK (Phillips and Ulidowski) were developed and general techniques for reversing other process operators were proposed. The paper shows that the notion of reversibility can bridge the gap between some interleaving models and non-interleaving models of concurrency, and makes them interchangeable. We prove that transition systems associated with reversible process algebras are equivalent as models to labelled prime event structures. Furthermore, we show that forward-reverse bisimulation corresponds to hereditary history-preserving bisimulation in the setting with no auto-concurrency and no auto-causation.
|MohammadReza Mousavi and Michel Reniers||A Congruence Rule Format with Universal Quantification|
We investigate the addition of universal quantification to the meta-theory of Structural Operational Semantics (SOS). We study the syntax and semantics of SOS rules extended with universal quantification and propose a congruence rule format for strong bisimilarity that supports this new feature.
|Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer||A Rewriting Logic Approach to Operational Semantics (extended abstract)|
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.