EXPRESS/SOS 2014
Combined 21th International Workshop onExpressiveness in Concurrency
and 11th Workshop onStructural Operational Semantics
Rome, Italy
Affiliated with CONCUR 2014
The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between programming concepts (such as concurrent, functional, imperative, logic and objectoriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, and rewrite systems) on the basis of their relative expressive power. The EXPRESS workshop series has run successfully since 1994 and over the years this focus has become broadly construed.
The SOS workshops aim at being a forum for researchers, students and practitioners interested in new developments, and directions for future investigation, in the field of structural operational semantics. One of the specific goals of the SOS workshop series is to establish synergies between the concurrency and programming language communities working on the theory and practice of SOS. Reports on applications of SOS to other fields are also most welcome, including: modelling and analysis of biological systems, security of computer systems programming, modelling and analysis of embedded systems, specification of middleware and coordination languages, programming language semantics and implementation, static analysis software and hardware verification, semantics for domainspecific languages and modelbased engineering.
Since 2012, the EXPRESS and SOS communities have joined forces and organised a combined EXPRESS/SOS workshop. The past combined workshops were a success, so this year there will again be a combined workshop on the semantics of systems and programming concepts, and on the expressiveness of mathematical models of computation.
Topics of interest for this combined workshop include (but are not limited to):
Vladimiro Sassone (University of Southampton, UK) 
9.0010.00:  Vladimiro Sassone (invited presentation, joint with BEAT 2014) 
Towards a Computational Model for the Internet of Things  
We describe the foundations of a computational model of the Internet of Things (IoT), designed from scratch with the intention of developing a framework for the analysis of cyber security in the IoT. The proposal is based on identifying the key components of a generic object as consisting of: a processing module; a sensing/actuation module; a communications module; and an energy module. The approach is mathematical in its reliance on formal definitions and its attempt to prove security properties conclusively. Our overall ambition is to build a universal model able to capture all the relevant aspects of the IoT in a simple, modular, flexible, computational framework. To the best of our knowledge, this would be the first such model for the IoT. This talk reports our first steps towards these objectives, and tries to illustrate with selected examples the potentiality of the approach. We shall describe IoT entities and their basic functions; sensing and actuation in the IoT; communication; and cyber security. Much more work is required to complete our overall research programme. Firstly, on the basis of the formal understanding of the IoT afforded by the present work, we need to formulate an comprehensive attacker model and, on the top of that, to develop a risk model for the generic IoT entity. This will allow us to deploy an hopefully realistic quantitative analysis taking into account specific risks associated with specific devices. 

10:0010:30  Coffee Break 
10:3011:00  Johannes Aman Pohjola and Joachim Parrow 
Priorities Without Priorities: Representing Preemption in PsiCalculi  
Psicalculi is a parametric framework for extensions of the picalculus with data terms and arbitrary logics. In this framework there is no direct way to represent action priorities, where an action can execute only if all other enabled actions have lower priority. We here demonstrate that the psicalculi parameters can be chosen such that the effect of action priorities can be encoded. To accomplish this we define an extension of psicalculi with action priorities, and show that for every calculus in the extended framework there is a corresponding ordinary psicalculus, without priorities, and a translation between them that satisfies strong operational correspondence. This is a significantly stronger result than for most encodings between process calculi in the literature. We also formally prove in Nominal Isabelle that the standard congruence and structural laws about strong bisimulation hold in psicalculi extended with priorities.  
11.0011.30:  Kirstin Peters, Tsvetelina YonovaKarbe and Uwe Nestmann 
Matching in the PiCalculus  
We study whether, in the picalculus, the match prefix?a conditional operator testing two names for (syntactic) equality?is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under rather strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widelytested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows comparison of calculi with respect to reachability of successful states). In this paper, we offer a considerably stronger separation result on the nonexpressibility of matching using only Gorla's relaxed requirements. 

11.3012.00:  Thomas GivenWilson 
On the Expressiveness of Intensional Communication  
The expressiveness of communication primitives has been explored in a common framework based on the picalculus by considering four features: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (shared dataspaces vs channelbased), and patternmatching (binding to a name vs testing name equality). Here patternmatching is generalised to account for terms with internal structure such as in recent calculi like Spi calculi, Concurrent Pattern Calculus and Psi calculi. This paper explores intensionality upon terms, in particular communication primitives that can match upon both names and structures. By means of possibility/impossibility of encodings, this paper shows that intensionality alone can encode synchronism, arity, communicationmedium, and patternmatching, yet no combination of these without intensionality can encode any intensional language.  
12.0012.30:  Simon J. Gay, Nils Gesbert and Antonio Ravara 
Session Types as Generic Process Types  
Behavioural type systems ensure more than the usual safety guarantees of static analysis. They are based on the idea of "typesasprocesses", providing dedicated type algebras for particular properties, ranging from protocol compatibility to racefreedom, lockfreedom, or even responsiveness. Two successful, although rather different, approaches, are session types and process types. The former allows to specify and verify (distributed) communication protocols using specific type (proof) systems; the latter allows to infer from a system specification a process abstraction on which it is simpler to verify properties, using a generic type (proof) system. What is the relationship between these approaches? Can the generic one subsume the specific one? At what price? And can the former be used as a compiler for the latter? The work presented herein is a step towards answers to such questions. Concretely, we define a stepwise encoding of a picalculus with sessions and session types (the system of Gay and Hole) into a picalculus with process types (the Generic Type System of Igarashi and Kobayashi). We encode session type environments, polarities (which distinguish session channels endpoints), and labelled sums. We show forward and reverse operational correspondences for the encodings, as well as typing correspondences. To faithfully encode session subtyping in process types subtyping, one needs to add to the target language record constructors and new subtyping rules. Our conclusion is that it is not difficult to instantiate the Generic Type System in a form that includes the main ideas of session types, preserving and reflecting the main properties of the typing systems. In short, the programming convenience of session types as protocol abstractions can be combined with the simplicity and power of the picalculus, taking advantage in particular of the framework provided by the Generic Type System.  
12:3014:00  Lunch Break 
14:0014.30  Christoph Wagner and Uwe Nestmann 
States in Process Calculi  
Formal reasoning about distributed algorithms (like Consensus) typically requires to analyze global states in a traditional statebased style. This is in contrast to the traditional actionbased reasoning of process calculi. Nevertheless, we use domainspecific variants of the latter, as they are convenient modeling languages in which the local code of processes can be programmed explicitly, with the local state information usually managed via parameter lists of process constants. However, domainspecific process calculi are often equipped with (unlabeled) reduction semantics, building upon a rich and convenient notion of structural congruence. Unfortunately, the price for this convenience is that the analysis is cumbersome: the set of reachable states is modulo structural congruence, and the processes' state information is very hard to identify. We extract from congruence classes of reachable states individual stateinformative representatives that we supply with a proper formal semantics. As a result, we can now freely switch between the process calculus terms and their representatives, and we can use the stateful representatives to perform assertional reasoning on process calculus models.  
14:3015:00  Daniel Gebler and Simone Tini 
Fixedpoint Characterization of Compositionality Properties of Probabilistic Processes Combinators  
Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric compositionality property. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between processes when they are combined by that operator. The compositionality property of an operator is computed by recursively counting how many times the combined processes are copied along their evolution. The compositionality properties allow to derive an upper bound on the distance between processes by purely inspecting the operators used to specify those processes.  
15:0015:30  Bartek Klin and Beata Nachyla 
Distributive Laws and Decidable Properties of SOS Specifications  
Some formats of wellbehaved operational specifications, correspond to natural transformations of certain types (for example, GSOS and coGSOS laws). These transformations have a common generalization: distributive laws of monads over comonads. We prove that this elegant theoretical generalization has limited practical benefits: it does not translate to any concrete rule format that would be complete for specifications that contain both GSOS and coGSOS rules. This is shown for the case of labeled transition systems and deterministic stream systems.  
15:3016:00  Coffee Break 
16:0016:30  Sonja FrankeArnold, Simon J. Gay and Ittoop Vergheese Puthoor 
Verification of Linear Optical Quantum Computing using Quantum Process Calculus  
We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.  
16.3016.50:  Harsh Beohar, and Mohammad Reza Mousavi 
Two Logical Characterizations for InputOutput Conformance (Short Paper)  
Inputoutput conformance (ioco) is a behavioral relation on inputoutput labeled transition systems. In this note, we propose two logical characterizations of the ioco relation in the style of Hennessy and Milner. The first one is an implicit characterization at the level of suspension automata, which are extensively used by the tools that establish the ioco relation, while the other is an explicit characterization at the level of inputoutput labeled transition systems.  
16:5017:10  Daniel Hirschkoff, JeanMarie Madiot and Xian Xu 
A Behavioural Theory for a Picalculus with Preorders (Short Paper)  
We study the behavioural theory of piP, a picalculus in the tradition of Fusions and Chi calculi. In contrast with such calculi, reduction in piP generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in piP: the first is based on a compositional LTS, and the second is an axiomatisation. This paper brings out basic properties of piP, mostly related to the interplay between the restriction operator and the preorder on names  
17:1017:30  Luca Bernardinello, Carlo Ferigato, Lucia Pomello and Stefania Rombola 
On a Logic of Observations in Occurrence Nets (Short Paper)  
Partially ordered sets are a natural framework to model concurrent processes. In this paper we consider a class of Petri nets, called occurrence nets, whose elements represent partially ordered occurrences of local states and local transitions, describing runs of concurrent systems. The partial order reflects relations of causal dependence. Petri axiomatized such partial orders, with the aim of describing the flow of information in nonsequential processes, by drawing from the laws of physics, and especially from the theory of relativity. Among other properties, Petri introduced Kdensity, which requires that any maximal antichain (or cut) in the partial order and any maximal chain (or line) have a nonempty intersection. Usually, a line represents the history of a sequential subprocess (a particle, a signal), while cuts correspond to time instants, where time is to be intended in a way analogous to the time coordinate in relativistic spacetime. In previous papers, we showed how to build an orthomodular lattice, whose elements are special subsets of elements of an occurrence net, closed with respect to a closure operator. In this contribution, we propose to consider those closed sets as propositions of a logical language. We recall that the set of propositions corresponding to closed sets having a nonempty intersection with a given line in the poset form what is called a twovalued state in quantum logics. Intuitively, a twovalued state is a maximal set of mutually consistent propositions. The resulting logic is not distributive. It is, however, locally Boolean, in the sense that the lattice of propositions can be decomposed into a family of partially overlapping Boolean algebras, and the selected subsets form an ultrafilter in each Boolean subalgebra. Here, we show that the set of twovalued states is full, which means that it allows to reconstruct in a unique way the lattice. 
The workshop proceedings are available as EPTCS 160.
Please register for EXPRESS/SOS 2014 via the registration page of CONCUR 2014. Deadline for early registration is 27th July.
We intend to organise a special issue of a highquality journal devoted to EXPRESS/SOS 2014, for which we will invite authors of a selection of the very best papers submitted to the workshop. Such papers will then be peerreviewed and selected according to the standard journal policy.
Abstract submission:  
Paper submission:  
Notification of acceptance:  July 13, 2014 
Final version due:  July 23, 2014 
Johannes Borgström (Uppsala University, SE) 
Silvia Crafa (University of Padova, Italy) 
Johannes Borgström (Uppsala University, Sweden) 
Josep Carmona Vargas (Universitat Politecnica de Catalunya, Spain) 
Matteo Cimini (Indiana University, Bloomington, Indiana) 
Silvia Crafa (University of Padova, Italy) 
Wojciech Czerwinski (University of Warsaw, Poland) 
Daniel Gebler (VU University Amsterdam, The Nederlands) 
Ivan Lanese (University of Bologna, Italy) 
Stefan Milius (University of ErlangenNurnberg, Germany) 
Kirstin Peters (Technical University of Berlin, Germany) 
Damien Pous (ENS Lyon, France) 
Pawel Sobocinski (University of Southampton, United Kingdom) 
Sam Staton (University of Nijmegen, The Nederlands) 
Irek Ulidowski (University of Leister, United Kingdom) 
The EXPRESS workshops were originally held as meetings of the HCM project EXPRESS, which was active with the same focus from January 1994 till December 1997. The first three workshops were held respectively in Amsterdam (1994, chaired by Frits Vaandrager), Tarquinia (1995, chaired by Rocco De Nicola), and Dagstuhl (1996, cochaired by Ursula Goltz and Rocco De Nicola). EXPRESS'97, which took place in Santa Margherita Ligure and was cochaired by Catuscia Palamidessi and Joachim Parrow, was organized as a conference with a call for papers and a significant attendance from outside the project. EXPRESS'98 was held as a satellite workshop of the CONCUR'98 conference in Nice, cochaired by Ilaria Castellani and Catuscia Palamidessi, and like on that occasion EXPRESS'99 was hosted by the CONCUR'99 conference in Eindhoven, cochaired by Ilaria Castellani and Björn Victor. The EXPRESS'00 workshop was held as a satellite workshop of CONCUR 2000, Pennsylvania State University, cochaired by Luca Aceto and Björn Victor. The EXPRESS'01 workshop was held at Aalborg University as a satellite of CONCUR'01 and was cochaired by Luca Aceto and Prakash Panangaden. The EXPRESS'02 workshop was held at Brno University as a satellite of CONCUR'02 and was cochaired by Uwe Nestmann and Prakash Panangaden. The EXPRESS'03 workshop was colocated with CONCUR 2003 in Marseille and was cochaired by Flavio Corradini and Uwe Nestmann. The EXPRESS'04 workshop was colocated with CONCUR 2004 in London and was cochaired by Jos Baeten and Flavio Corradini. The EXPRESS'05 workshop was colocated with CONCUR 2005 in San Francisco and was cochaired by Jos Baeten and Iain Phillips. The EXPRESS'06 workshop was colocated with CONCUR 2006 in Bonn and was cochaired by Roberto Amadio and Iain Phillips. The EXPRESS'07 workshop was colocated with CONCUR 2007 in Lisbon and was cochaired by Roberto Amadio and Thomas Hildebrandt. The EXPRESS'08 workshop was colocated with CONCUR 2008 in Toronto and was cochaired by Daniele Gorla and Thomas Hildebrandt. The EXPRESS'09 workshop was colocated with CONCUR 2009 in Bologna and was cochaired by Sibylle Fröschle and Daniele Gorla. The EXPRESS'10 workshop was colocated with CONCUR 2010 in Paris and was cochaired by Sibylle Fröschle and Frank Valencia. The EXPRESS'11 workshop was colocated with CONCUR 2011 in Aachen and was cochaired by Bas Luttik and Frank Valencia.
The first SOS Workshop took place in London as one of the satellite workshops of CONCUR 2004. Subsequently, SOS 2005 occurred in Lisbon as a satellite workshop of ICALP 2005, SOS 2006 in Bonn as a satellite workshop of CONCUR 2006, SOS 2007 in Wroclaw as a satellite workshop of LICS and ICALP 2007, and SOS 2008 in Reykjavik as a satellite workshop of ICALP 2008. SOS 2009 was held as a satellite workshop of CONCUR 2009 in Bologna. SOS 2010 was held as a satellite workshop of CONCUR 2010 in Paris. Finally, SOS 2011 was held as a satellite workshop of CONCUR 2011 in Aachen. A special issue of the Journal of Logic and Algebraic Programming on Structural Operational Semantics appeared in 2004; a special issue of Theoretical Computer Science dedicated to SOS 2005 appeared in 2007, and a special issue of Information & Computation on Structural Operational Semantics inspired by SOS 20062007 appeared in 2009.
The first combined EXPRESS/SOS workshop (EXPRESS/SOS 2012) was colocated with CONCUR 2012 in Newcastle upon Tyne, UK and was cochaired by Bas Luttik and Michel Reniers. The second combined EXPRESS/SOS 2013 workshop was colocated with CONCUR 2013 in Buenos Aires, Argentina and was cochaired by Johannes Borgström and Bas Luttik.
Page maintained by Silvia Crafa 