|
Published: 24th August 2018 DOI: 10.4204/EPTCS.276 ISSN: 2075-2180 |
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 specific goal 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: modeling and analysis of biological systems, security of computer systems programming, modeling 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 organized an annual combined EXPRESS/SOS workshop on the expressiveness of mathematical models of computation and the formal semantics of systems and programming concepts.
This volume contains eight papers selected by the program committee for publication and presentation at the workshop. The workshop program included also two invited presentations:
Jorge A. Pérez and Simone Tini, August 2018
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.
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.