Skip to main content Link Menu Expand (external link) Document Search Copy Copied
Concurrency Theory

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

IFIP

Description

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.

Invited Speakers

  • 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 re fines this by a light-weight analysis of veri fication 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 Mika-Michalski)

Highlight Talks

  • 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.

Programme

10:00-10:25: — Arrival and coffee —

10:25-10:30: Opening

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

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.

Organizers

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.

History

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