The 8th IFIP WG 1.8 Workshop on Trends in Concurrency Theory
August 31, 2019, Amsterdam, The Netherlands
A satellite event of CONCUR 2019
CWI, ADA room L017
TRENDS 2019 is an event organised by IFIP WG 1.8 on Concurrency Theory. It aims at bringing together researchers interested in Concurrency Theory and its applications, to exchange ideas and discuss recent trends and open problems. The event will take place on August 31, 2019 and will consist of three invited talks and a number of highlight presentations. It will be associated with the yearly WG 1.8 business meeting.
- Laura Bocchi, University of Kent, UK
Title: Time-sensitive protocol design and implementation
In this talk I will discuss ongoing work towards establishing relationships between models for real-time asynchronous interactions and their implementations. We will consider models based on two partly related formalisms: Timed Session Types and Communicating Timed Automata (CTA). For CTA the relationship between models and (abstractions of) programs can be expressed as a refinement relation. I will discuss decidable conditions under which refinement preserves behaviour and progress properties, providing us with guidelines on how to safely implement timed protocols expressed as CTA. For Timed Session Types the model/program relationship is the type-checking of programs against (behavioural) types. I will present a theory timed asynchronous session types for a realistic calculus and discuss open challenges and future directions.
- Joost-Pieter Katoen, RWTH Aachen University, DE
Title: Towards the Automated Synthesis of Probabilistic Programs
Probabilistic model checking focuses on checking whether a given (mostly
finite) probabilistic model satisfies a given specification. Efficient
algorithms and powerful tools such as PRISM and STORM exist and have
been applied to various case studies. These techniques do require
however the existence of a probabilistic model.
In this talk, I will focus on the automatic synthesis of Markov chains
that satisfy a specification. This includes program sketching: given a
partial probabilistic program with "holes", fill these "holes" such that
the resulting program satisfies the specification.
I will outline two approaches: counterexample-guided abstraction
refinement (CEGAR) and counterexample-guided inductive synthesis
(CEGIS). The CEGAR approach iteratively partitions the design space
starting from an abstraction of this space and refines this by a
light-weight analysis of verification results. The CEGIS technique
exploits critical subsystems as counterexamples to prune all programs
behaving incorrectly on that input.
We show the applicability of these synthesis techniques to sketching of
probabilistic programs, controller synthesis of POMDPs, and analysis of
software product lines.
- Barbara König, University of Duisburg-Essen, DE
Title: Fixpoint Games
Solving fixpoint equations is a recurring problem in several domains:
the result of a dataflow analysis can be characterized as either a
least or greatest fixpoint. It is well-known that bisimilarity - the
largest bisimulation - admits a characterization as a greatest
fixpoint and furthermore mu-calculus model-checking requires to solve
systems of nested fixpoint equations.
Often, these fixpoint equations or equation systems are defined over
powerset lattices, however in several applications - such as
lattice-valued or real-valued mu-calculi - the lattice under
consideration is not a powerset.
Hence we extend the notion of fixpoint games (or unfolding games,
introduced by Venema) to games for equation systems over more general
lattices. In particular continuous lattices admit a very elegant
characterization of the solution.
We will also describe how to define progress measures which describe
winning strategies for the existential players and explain how
abstractions and up-to functions can be integrated into the
framework. Finally, we will sketch a local algorithm for showing
whether a given lattice element is below the solution.
(Joint work with Paolo Baldan, Tommaso Padoan, Christina
Rob van Glabbeek, Reward Testing Equivalences for Processes.
Hubert Garavel, Converting Safe Petri-Nets to NUPNs.
Jaco van de Pol and Laure Petrucci, Taming NDFS for Parametric Timed Automata.
Jos Baeten, Cesare Carissimo and Bas Luttik, Pushdown Automata and Context-Free Grammars in Bisimulation Semantics.
Mark Bouwman, Bas Luttik and Tim Willemse, Action-based justness for automated verification of liveness.
Mauricio Cano, Ilaria Castellani, Cinzia Di Giusto and Jorge A. Pérez, Multiparty Reactive Sessions.
10:00-10:25: --- Arrival and coffee ---
10:30-12:30: Session 1: Invited talks
10:30-11:30 Laura Bocchi, Time-sensitive protocol design and implementation.
11:30-12:30: Joost-Pieter Katoen, Towards the Automated Synthesis of Probabilistic Programs.
12:30-14:00: --- Lunch and WG 1.8 Business Meeting ---
14:00-15:00: Session 2: Invited talk
14:00-15:00 Barbara König, Fixpoint Games.
15:00-15:30: --- coffee break ---
15:30-17:30: Session 3: Highlight talks
---- Chair: Bas Luttik
15:30-15:50: Rob van Glabbeek, Reward Testing Equivalences for Processes.
15:50-16:10: Hubert Garavel, Converting Safe Petri-Nets to NUPNs.
16:10-16:30: Jaco van de Pol and Laure Petrucci, Taming NDFS for Parametric Timed Automata.
---- Chair: Kirstin Peters
16:30-16:50 Jos Baeten, Cesare Carissimo and Bas Luttik, Pushdown Automata and Context-Free Grammars in Bisimulation Semantics.
16:50-17:10: Mark Bouwman, Bas Luttik and Tim Willemse, Action-based justness for automated verification of liveness.
17:10-17:30: Mauricio Cano, Ilaria Castellani, Cinzia Di Giusto and Jorge A. Pérez, Multiparty Reactive Sessions.
Participation, both to the workshop and to the IFIP WG 1.8 meeting, is open to everybody. For registration, please consult the CONCUR 2019 registration page.
Ilaria Castellani (INRIA Sophia Antipolis, France)
Mohammad Mousavi (University of Leicester, UK)
IFIP WG 1.8 on Concurrency Theory
The aims of IFIP WG 1.8 on Concurrency Theory are:
* To develop theoretical foundations of concurrency, exploring frontiers of existing theoretical models like process algebra and process calculi, so as to obtain a deeper theoretical understanding of concurrent and parallel systems.
* To promote and coordinate the exchange of information on concurrency theory, by sharing ideas, discussing open problems, and identifying future directions of research in the area.
The activities of this WG encompass all aspects of concurrency theory and its applications.
More information on IFIP WG 1.8 can be found on its home page.
The first instalment of TRENDS (TRENDS 2012) was held on September 8, 2012 as a satellite event of CONCUR 2012, in Newcastle upon Tyne, UK.
The second instalment of TRENDS (TRENDS 2013) was held on August 31, 2013 as a satellite event of CONCUR 2013, in Buenos Aires, Argentina.
The third instalment of TRENDS (TRENDS 2014) was held on September 6, 2014 as a satellite event of CONCUR 2014, in Rome, Italy.
The fourth instalment of TRENDS (TRENDS 2015) was held on September 6, 2015 as a satellite event of CONCUR 2015, in Madrid, Spain.
The fifth instalment of TRENDS (TRENDS 2016) was held on August 27, 2016 as a satellite event of CONCUR 2016, in Quebec City, Canada.
The sixth instalment of TRENDS (TRENDS 2017) was held on September 9, 2017 as a satellite event of CONCUR 2017, in Berlin, Germany
The seventh instalment of TRENDS (TRENDS 2018) was held on September 8, 2018 as a satellite event of CONCUR 2018, in Beijing, China