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.
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), and programming 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.
Joost-Pieter Katoen (RWTH Aachen University, Germany)
|09:45 – 10:00||Welcome|
|10:00 – 11:00||Joost-Pieter Katoen (invited presentation)|
|What Do Probabilistic Programs Mean?
Probabilistic programming is en vogue. It is used to describe complex Bayesian networks, quantum programs, security protocols and biological systems. Programming languages like C, C#, Java, Prolog, Scala, etc. all have their probabilistic version. Key features are random sampling and means to adjust distributions based on obtained information from measurements, system observations, and the like. We discuss some semantic intricacies, present a wp-style and an operational semantics, and show that termination is a more involved notion than for ordinary programs.
|11:00 – 11:30||Coffee Break
|11:30 – 12:00||Eduard Baranov and Simon Bliudze|
|A Note on the Expressiveness of BIP
We extend our previous algebraic formalisation of the notion of component-based framework in order to formally define two forms—strong and weak—of the notion of full expressiveness. Our earlier result shows that the BIP (Behaviour-Interaction-Priority) framework does not possess the strong full expressiveness. In this paper, we show that BIP has the weak form of this notion and provide results detailing weak and strong full expressiveness for classical BIP and several modifications, obtained by relaxing the constraints imposed on priority models.
|12:00 – 12:30||Xian Xu|
|Higher-order Processes with Parameterization over Names and Processes
Parameterization extends higher-order processes with the capability of abstraction and application (like those in lambda-calculus). This extension is strict, i.e., higher-order processes equipped with parameterization is computationally more powerful. This paper studies higher-order processes with two kinds of parameterization: one on names and the other on processes themselves. We present two results. One is that in presence of parameterization, higher-order processes can encode first-order (name-passing) processes in a quite neat fashion, in contrast to the fact that higher-order processes without parameterization cannot encode first-order processes at all. In the other result, we provide a simpler characterization of the (standard) context bisimulation for higher-order processes with parameterization, in terms of the normal bisimulation that stems from the well-known normal characterization for higher-order calculus. These two results demonstrate more essence of the parameterization method in the higher-order paradigm toward expressiveness and behavioural equivalence.
|12:30 – 14:30||Lunch Break
|14:30 – 15:00||Sanjiva Prasad and Lenore Zuck|
|Self-Similarity breeds Resilience
Self-similarity is the property of a system being similar to a part of itself. We posit that a special class of behaviourally self-similar systems exhibits a degree of resilience to adversarial behaviour. We formalise the notions of system, adversary and resilience in operational terms, based on transition systems and observations. While the general problem of proving systems to be behaviourally self-similar is undecidable, we show, by casting them in the framework of well-structured transition systems, that there is an interesting class of systems for which the problem is decidable. We illustrate our prescriptive framework for resilience with some small examples, e.g., systems robust to failures in a fail-stop model, and those avoiding side-channel attacks.
|15:00 – 15:30||Matias David Lee and Bas Luttik|
|Unique Parallel Decomposition for the Pi-calculus
A (fragment of a) process algebra satisfies unique parallel decomposition if the behaviors definable admit a unique decomposition into decomposable parallel components. In this paper we prove that finite processes of the Pi-calculus, processes that perform no infinite executions, satisfy this property modulo strong bisimilarity and bisimilarity. Our results rely on the general technique for establishing unique parallel decomposition introduced by Luttik and Oostrom (2005).
|15:30 – 16:00||Paola Giannini and Mariangiola Dezani-Ciancaglini|
|Reversible Multiparty Sessions with Checkpoints
Reversible interactions model different scenarios, like biochemical systems and human as well as automatic negotiations. We abstract interactions via multiparty sessions enriched with named checkpoints. Computations can either go forward or roll back to some checkpoint, where different choices may be taken. In this way communications can be undone and different conversations can be tried. Interactions are typed with global types, which control also rollbacks. Typability of session participants in agreement with global types assures session fidelity and progress of reversible communications.
|16:00 – 16:30||Coffee Break
The workshop proceedings are available as EPTCS 222.
Please register for EXPRESS/SOS 2016 via the registration page of CONCUR 2016.
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. The programme committee will select submissions for presentation at the workshop.
The final versions of the accepted papers will be published in the EPTCS (Electronic Proceedings in Theoretical Computer Science). There is limited time between the notification of acceptance of submissions and the deadline for submission of camera-ready versions. Submissions are therefore requested to adhere to the EPTCS-style format. Please also note that after submitting the camera-ready version to EPTCS, usually some interaction between authors, editors and EPTCS staff is needed. At least one author should therefore be available in the week after submitting the camera-ready version. It is recommended that the final version of the paper includes as much as possible proofs and technical material.
June 06, 2016 June 17, 2016
June 13, 2016 June 17, 2016
Notification date: July 18, 2016
Camera ready version: July 29, 2016
|Daniel Gebler (VU University Amsterdam, The Nederlands)
Kirstin Peters (TU Berlin, Germany)
Ilaria Castellani (INRIA Sophia Antipolis, France)
Matteo Cimini (Indiana University, Bloomington, Indiana)
Ornela Dardha (University of Glasgow, UK)
Pedro R. D’Argenio (University of Córdoba, Argentina)
Simone Tini (Università degli Studi dell’Insubria, Italia)
Daniel Gebler (VU University Amsterdam, The Netherlands)
Tobias Heindel (IT University of Copenhagen, Denmark)
Thomas T. Hildebrandt (IT University of Copenhagen, Denmark)
Daniel Hirschkoff (ENS Lyon, France)
Jorge A. Pérez (University of Groningen, The Netherlands)
Kirstin Peters (Technische Universität Berlin, Germany)
Alexandra Silva (University College London, UK)
Pawel Sobocinski (University of Southampton, UK)
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’98was 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. The combined EXPRESS/SOS 2014 workshop was co-located with CONCUR 2014 in Rome, Italy and was co-chaired by Johannes Borgstrom 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.