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


    Abstract:
    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

    Abstract:
    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