July 9, 2007, Wroclaw, Poland
Invited Speaker  Title/Abstract 

Pawel Sobocinski  A wellbehaved LTS for the Picalculus 
 
PAuL Invited Speaker  Title/Abstract 
Catuscia Palamidessi  Informationhiding protocols as opaque channels 

Author(s)  Title/Abstract 

David Frutos Escrig and Carlos Gregorio Rodríguez  Simulations upto and Canonical Preorders (extended abstract) 
In this paper we define simulations upto a preorder and show how we can use them to provide a coinductive, simulationlike, 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 timebranching time spectrum. An interesting but unexpected result is that, when built from an equivalence relation, the simulation upto 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 timebranching time spectrum, whose correctness and completeness can be proved once and for all.  
Patrick Cousot and Radhia Cousot  Biinductive Structural Semantics 
We propose a simple ordertheoretic generalization of settheoretic inductive definitions. This generalization covers inductive, coinductive and biinductive 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/bigstep trace/relational/operational semantics of the callbyvalue λ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 nextstep actions. In order to handle the different kinds of nondeterminism, the operational semantics uses muautomata 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 picalculus using Isabelle 
We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the picalculus 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 picalculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the picalculus, 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 biosystems 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 noninterleaving 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 forwardreverse bisimulation corresponds to hereditary historypreserving bisimulation in the setting with no autoconcurrency and no autocausation.  
MohammadReza Mousavi and Michel Reniers  A Congruence Rule Format with Universal Quantification 
We investigate the addition of universal quantification to the metatheory 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 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: bigstep and smallstep structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuationbased 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 onetoone 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 preimpose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles. 