EXPRESS/SOS 2014Combined 21th International Workshop on
Expressiveness in Concurrencyand 11th Workshop on
Structural Operational Semantics
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 object-oriented 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 middle-ware and coordination languages, programming language semantics and implementation, static analysis software and hardware verification, semantics for domain-specific languages and model-based 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.00-10.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:30-11:00||Johannes Aman Pohjola and Joachim Parrow|
|Priorities Without Priorities: Representing Preemption in Psi-Calculi|
|Psi-calculi is a parametric framework for extensions of the pi-calculus 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 psi-calculi parameters can be chosen such that the effect of action priorities can be encoded. To accomplish this we define an extension of psi-calculi with action priorities, and show that for every calculus in the extended framework there is a corresponding ordinary psi-calculus, 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 psi-calculi extended with priorities.|
|11.00-11.30:||Kirstin Peters, Tsvetelina Yonova-Karbe and Uwe Nestmann|
|Matching in the Pi-Calculus|
We study whether, in the pi-calculus, 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 widely-tested 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 non-expressibility of matching using only Gorla's relaxed requirements.
|On the Expressiveness of Intensional Communication|
|The expressiveness of communication primitives has been explored in a common framework based on the pi-calculus by considering four features: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (shared dataspaces vs channel-based), and pattern-matching (binding to a name vs testing name equality). Here pattern-matching 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, communication-medium, and pattern-matching, yet no combination of these without intensionality can encode any intensional language.|
|12.00-12.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 "types-as-processes", providing dedicated type algebras for particular properties, ranging from protocol compatibility to race-freedom, lock-freedom, 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 pi-calculus with sessions and session types (the system of Gay and Hole) into a pi-calculus with process types (the Generic Type System of Igarashi and Kobayashi). We encode session type environments, polarities (which distinguish session channels end-points), 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 pi-calculus, taking advantage in particular of the framework provided by the Generic Type System.|
|14:00-14.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 state-based style. This is in contrast to the traditional action-based reasoning of process calculi. Nevertheless, we use domain-specific 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, domain-specific 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 state-informative 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:30-15:00||Daniel Gebler and Simone Tini|
|Fixed-point 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:00-15:30||Bartek Klin and Beata Nachyla|
|Distributive Laws and Decidable Properties of SOS Specifications|
|Some formats of well-behaved 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.|
|16:00-16:30||Sonja Franke-Arnold, 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.30-16.50:||Harsh Beohar, and Mohammad Reza Mousavi|
|Two Logical Characterizations for Input-Output Conformance (Short Paper)|
|Input-output conformance (ioco) is a behavioral relation on input-output 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 input-output labeled transition systems.|
|16:50-17:10||Daniel Hirschkoff, Jean-Marie Madiot and Xian Xu|
|A Behavioural Theory for a Pi-calculus with Preorders (Short Paper)|
|We study the behavioural theory of piP, a pi-calculus 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:10-17: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 non-sequential processes, by drawing from the laws of physics, and especially from the theory of relativity. Among other properties, Petri introduced K-density, which requires that any maximal antichain (or cut) in the partial order and any maximal chain (or line) have a non-empty 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 non-empty intersection with a given line in the poset form what is called a two-valued state in quantum logics. Intuitively, a two-valued 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 two-valued states is full, which means that it allows to reconstruct in a unique way the lattice.
The workshop proceedings are available as EPTCS 160.
We intend to organise a special issue of a high-quality 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 peer-reviewed and selected according to the standard journal policy.
|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 Erlangen-Nurnberg, 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, co-chaired by Ursula Goltz and Rocco De Nicola). EXPRESS'97, which took place in Santa Margherita Ligure and was co-chaired 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, co-chaired by Ilaria Castellani and Catuscia Palamidessi, and like on that occasion EXPRESS'99 was hosted by the CONCUR'99 conference in Eindhoven, co-chaired by Ilaria Castellani and Björn Victor. The EXPRESS'00 workshop was held as a satellite workshop of CONCUR 2000, Pennsylvania State University, co-chaired by Luca Aceto and Björn Victor. The EXPRESS'01 workshop was held at Aalborg University as a satellite of CONCUR'01 and was co-chaired by Luca Aceto and Prakash Panangaden. The EXPRESS'02 workshop was held at Brno University as a satellite of CONCUR'02 and was co-chaired by Uwe Nestmann and Prakash Panangaden. The EXPRESS'03 workshop was co-located with CONCUR 2003 in Marseille and was co-chaired by Flavio Corradini and Uwe Nestmann. The EXPRESS'04 workshop was co-located with CONCUR 2004 in London and was co-chaired by Jos Baeten and Flavio Corradini. The EXPRESS'05 workshop was co-located with CONCUR 2005 in San Francisco and was co-chaired by Jos Baeten and Iain Phillips. The EXPRESS'06 workshop was co-located with CONCUR 2006 in Bonn and was co-chaired by Roberto Amadio and Iain Phillips. The EXPRESS'07 workshop was co-located with CONCUR 2007 in Lisbon and was co-chaired by Roberto Amadio and Thomas Hildebrandt. The EXPRESS'08 workshop was co-located with CONCUR 2008 in Toronto and was co-chaired by Daniele Gorla and Thomas Hildebrandt. The EXPRESS'09 workshop was co-located with CONCUR 2009 in Bologna and was co-chaired by Sibylle Fröschle and Daniele Gorla. The EXPRESS'10 workshop was co-located with CONCUR 2010 in Paris and was co-chaired by Sibylle Fröschle and Frank Valencia. The EXPRESS'11 workshop was co-located with CONCUR 2011 in Aachen and was co-chaired 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 2006-2007 appeared in 2009.
The first combined EXPRESS/SOS workshop (EXPRESS/SOS 2012) was co-located with CONCUR 2012 in Newcastle upon Tyne, UK and was co-chaired by Bas Luttik and Michel Reniers. The second combined EXPRESS/SOS 2013 workshop was co-located with CONCUR 2013 in Buenos Aires, Argentina and was co-chaired by Johannes Borgström and Bas Luttik.
|Page maintained by Silvia Crafa|