Scope and Topics

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.

This year marks the 25th edition of EXPRESS and the 15th edition of SOS.

Topics of interest for this combined workshop include (but are not limited to):

• expressiveness and comparison of models of computation (process algebras, event structures, Petri nets, rewrite systems),
• expressiveness and comparison of programming languages and models (distributed, component-based, object-oriented, and service-oriented computing);
• logics for concurrency (modal logics, probabilistic and stochastic logics, temporal logics and resource logics);
• analysis techniques for concurrent systems;
• theory of structural operational semantics (metatheory, category-theoretic approaches, congruence results);
• comparison of structural operational semantics to other forms of semantics;
• applications of structural operational semantics;
• software tools that automate, or are based on, structural operational semantics.

Contributions bridging the gap between the above topics and emerging and/or neighbouring areas (such as, for instance, computer security, multi-agent systems, knowledge representation, reversible computation) are particularly welcome.

Invited Speakers

Adrian Francalanza (University of Malta)

Wan Fokkink (Vrije Universiteit Amsterdam)

Programme

9:00-9:20	Registration
9:20-9:30	Opening
9.30-10.30	Adrian Francalanza (invited presentation)
	Adventures in Monitorability
	Runtime Verification is a lightweight technique that checks at runtime whether a program satisfies (or violates) a correctness property. It synthesises monitors from properties specified in some formal logic, which are then instrumented to run alongside the executing program so as to analyse its behaviour and flag detected satisfactions or violations. The joint research group at Reykjavik University and the University of Malta has been challenging the commonly held assumption that only linear-time properties can be monitored at runtime. In particular, the group has established maximality results for the monitorability of the modal mu-calculus with a branching-time interpretation. These results, however, remain quite disconnected from the rich theory of linear-time monitoring that has been developed over the years. In this presentation I will overview ongoing work that aims to bridge this gap. By considering a linear-time interpretation of modal mu-calculus, this study extends the methods used for the branching-time setting to establish missing results on the path towards a unified theory of monitorability.
10.30-11.00	Kirstin Peters and Uwe Nestmann
	On the Distributability of Mobile Ambients
	We analyse the level of distribution in mobile ambients. Therefore, we rely on earlier established synchronisation patterns. It turns out that mobile ambients are not fully distributed, because they can express enough synchronisation to express a synchronisation pattern called M. But they can express strictly less synchronisation than the standard pi-calculus. With that we show that there is no good and distributability-preserving encoding from the join-calculus into mobile ambients and also no such encoding from mobile ambients into the standard pi-calculus. Finally, we discuss how these results can be used to obtain a fully distributed variant of mobile ambients.
11:00-11:30	Coffee Break
11.30-12.00	Doriana Medic, Claudio Antares Mezzina, Iain Phillips and Nobuko Yoshida.
	A Parametric Framework for Reversible Pi-Calculi
	This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in Pi-calculus, which differ in the treatment of parallel extrusions of the same name. In this paper, we present a uniform framework for reversible Pi-calculi that is parametric with respect to a data structure that stores information about an extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We show that the (parametric) reversibility induced by our framework is causally-consistent and prove a causal correspondence between an appropriate instance of the framework and Boreale and Sangiorgi’s causal semantics. We define a causal bisimulation which abstracts away from the notion of causality used and does not distinguish object from subject causality.
12:00-12:30	James Hoey, Irek Ulidowski and Shoji Yuen.
	Reversing Parallel Programs with Blocks and Procedures
	We show how to reverse a while language extended with blocks, local variables, procedures and the interleaving parallel composition. Annotation is defined along with a set of operational semantics capable of storing necessary reversal information, and identifiers are introduced to capture the interleaving order of an execution. Inversion is defined with a set of operational semantics that use saved information to undo an execution. We prove that annotation does not alter the behaviour of the original program, and that inversion correctly restores the initial program state.
12.30-13.00	Hans Hüttel, Jens Aagard, Mathias Jakobsen and Mikkel Kettunen
	Context-Free Session Types for Applied Pi-Calculus
	We present a binary session type system using context-free session types to a version of the applied Pi-calculus of Abadi et. al. where only base terms, constants and channels can be sent. Session types resemble process terms from BPA and we use a version of bisimulation equivalence to characterize type equivalence. We present a quotiented type system defined on type equivalence classes for which type equivalence is built into the type system. Both type systems satisfy general soundness properties; this is established by an appeal to a generic session type system for psi-calculi.
13:00-14:30	Lunch Break
14.30-15.30	Wan Fokkink (invited presentation)
	On Milner's Axiomatization for Regular Expressions
	In 1984, Robin Milner formulated an axiomatization for regular expressions in bisimulation semantics. It is still an open question whether this axiomatization is ground-complete. I will explain some ideas behind an ongoing attempt to provide an affirmative answer to this question.
15.30-16.00	Chun Tian and Davide Sangiorgi.
	Unique solutions of contractions, CCS, and their HOL formalisation
	The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The paper presents an overview of the a rather comprehensive formalisation of the core of the theory of CCS in the HOL theorem prover (HOL4), with a focus towards the theory of unique solutions of contractions. (The formalisation consists of about 20,000 lines of proof scripts in Standard ML.) Some refinements of the theory itself are obtained. In particular we remove the constraints on the occurrences of the sum operator by moving to rooted contraction, that is, the coarsest precongruence contained in the contraction preorder.
16:30-16:30	Coffee Break
16:30-17.00	Jane Hillston, Carla Piazza and Sabina Rossi.
	Persistent Stochastic Non-Interference
	In this paper we present an information flow security property for stochastic, cooperating, processes expressed as terms of the Performance Evaluation Process Algebra (PEPA). We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: the first involves a single bisimulation-like equivalence check, while the second is formulated in terms of unwinding conditions. The observation equivalence at the base of our definition relies on the notion of lumpability and ensures that, for a secure process P, the steady state probability of observing the system being in a specific state P′ is independent from its possible high level interactions.
17:00-17:30	Valentina Castiglioni.
	Trace and Testing Metrics on Nondeterministic Probabilistic Processes
	The combination of nondeterminism and probability in concurrent systems lead to the development of several interpretations of process behavior. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes wrt. trace and testing semantics. We study the properties of these metrics, like non-expansiveness, and we compare their expressive powers.
17:30-18:00	Flavio Corradini, Chiara Muzi, Barbara Re and Francesco Tiezzi.
	A Classification of BPMN Collaborations based on Safeness and Soundness Notions
	BPMN 2.0 standard has a huge uptake in modelling business processes within the same organisation or involving multiple ones. It results that providing a solid foundation to enable BPMN designers to understand their models in a consistent way is becoming more and more important. In our investigation we define and exploit a formal characterisation of the collaborations' semantics, specifically and directly given for BPMN models, to provide a classification of BPMN collaborations. In particular, we refer to collaborations involving processes with arbitrary topology, thus overcoming the well-structuredness limitations. The proposed classification is based on some of the most important correctness properties in the domain and business process domain, namely, safeness and soundness. We prove, with a uniform formal framework, some conjectured and expected results and, most of all, we achieve novel results for BPMN collaborations concerning the relationships between safeness and soundness, and their compositionality, that represent major advances in the state-of-the-art.

Proceedings

The workshop proceedings are published as volume 276 of Electronic Proceedings in Theoretical Computer Science.

Registration

Please register for EXPRESS/SOS 2018 via the registration page of CONFESTA 2018.

Submissions

We sollicit two types of submissions:

• Full papers of up to 15 pages (presented at the workshop and included in the proceedings)
• Short papers of up to 5 pages (presented at the workshop, but not included in the proceedings)

Paper submission is performed through Easychair.

Important Dates

Paper submission:	June 14, 2018 June 21, 2018
Notification of acceptance:	July 16, 2018 July 20, 2018
Final version due:	August 5, 2018

Organizers

Jorge A. Pérez (University of Groningen, NL)

Simone Tini (University of Insubria, IT)

Programme Committee

Pedro R. D'Argenio (University of Córdoba, Argentina)

Erik de Vink (Eindhoven University of Technology, The Netherlands)

Cinzia Di Giusto (Université Côte d'Azur, France)

Ignacio Fábregas (IMDEA Software Institute, Spain)

Simon Gay (University of Glasgow, United Kingdom)

Vasileios Koutavas (Trinity College Dublin, Ireland)

Bas Luttik (Eindhoven University of Technology, The Netherlands)

Claudio Antares Mezzina (IMT School for Advanced Studies Lucca, Italy)

MohammadReza Mousavi (University of Leicester, United Kingdom)

Jorge A. Pérez (University of Groningen, The Netherlands)

Jurriaan Rot (Radboud University, The Netherlands)

Simone Tini (University of Insubria, Italy)

Valeria Vignudelli (CNRS/ENS Lyon, France)

History

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.

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. The combined EXPRESS/SOS 2014 workshop was co-located with CONCUR 2014 in Rome, Italy and was co-chaired by Johannes Borgström and Silvia Crafa. The next year the combined EXPRESS/SOS 2015 workshop was co-located with CONCUR 2015 in Madrid, Spain and was co-chaired by Silvia Crafa and Daniel Gebler. The combined EXPRESS/SOS 2016 workshop was co-located with CONCUR 2016 in Québec City, Canada and was co-chaired by Daniel Gebler and Kirstin Peters. The combined EXPRESS/SOS 2017 workshop was co-located with CONCUR 2017 in Berlin, Germany and was co-chaired by Kirstin Peters and Simone Tini.

In these years some journal special issues dedicated to the mentioned events have been organised. A special issue of 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. A special issue of the Acta Informatica dedicated to EXPRESS/SOS 2016-2017 is presently in progress.