Preface

This volume contains the proceedings of the Combined 21^st International Workshop on Expressiveness in Concurrency and the 11^th Workshop on Structural Operational Semantics (EXPRESS/SOS 2014) which was held on 1^st September 2014 in Rome, Italy, as an affiliated workshop of CONCUR 2014, the 25^th International Conference on Concurrency Theory.

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, and semantics for domain-specific languages and model-based engineering.

Since 2012, the EXPRESS and SOS communities have organized a combined EXPRESS/SOS workshop on the expressiveness of mathematical models of computation and the formal semantics of systems and programming concepts.

We received 14 full paper submissions out of which the programme committee selected eight for publication and presentation at the workshop. These proceedings contain these selected contributions. We also received three short paper submissions, that were all selected for presentation only; their abstracts appear below. The workshop also had an invited presentation:

Towards a Computational Model for the Internet of Things
by Vladimiro Sassone (University of Southampton)

We would like to thank the authors of the submitted papers, the invited speaker, the members of the programme committee, and their subreviewers for their contribution to both the meeting and this volume. We also thank the CONCUR 2014 organizing committee for hosting EXPRESS/SOS 2014. Finally, we would like to thank our EPTCS editor Rob van Glabbeek for publishing these proceedings and his help during the preparation.

Johannes Borgström and Silvia Crafa,
August 2014.

Programme Committee

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)

Additional Reviewers

Andrea Cerone, Anuj Dawar, Wan Fokkink, Joaquim Gabarro, Helle Hvid Hansen, Matthew Hennessy, Jeroen Keiren, Bartek Klin, Tomas Masopust, Roland Meyer, Fabrizio Montesi, Iain Phillips, Jurriaan Rot, Emilio Tuosto, Benoît Valiron, Valeria Vignudelli, and Kazuya Yasuda.

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.

Two Logical Characterizations for Input-Output Conformance

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.

A Behavioural Theory for a pi-calculus with Preorders

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.

On a Logic of Observations in Occurrence Nets

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.