The 9th IFIP WG 1.8 Workshop on Trends in Concurrency Theory

September 5, 2020, Online

A satellite event of CONCUR 2020

 

IFIP

   

Description

TRENDS 2020 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 September 5, 2020 and will consist of three invited talks. It will be associated with the yearly WG 1.8 business meeting.

 

Invited Speakers

 

  • Kostas Chatzikokolakis, University of Athens, GR


Title: Refinement relations for quantitative information flow

Abstract:


Quantitative Information Flow (QIF) studies flows of information
caused by the correlation between secret data and observable outputs,
allowing an adversary to make inferences about sensitive information.
The study is made particularly challenging by the fact that perfection
is often unachievable, in that some undesirable flows have to be
accepted for functional or practical reasons. The QIF theory provides
systematic approaches to quantifying such information "leaks" in
operationally significant ways, and then bounding them, both with
respect to the benefit of an attacking adversary and by comparisons
between alternative implementations.

In this talk I will start with an introduction to the QIF theory.
Then, I will discuss refinement relations, that is methods to
establish that a system B never leaks more than a system A in a
variety of different adversarial scenarios. This allows us, for
instance, to replace A by a newer version B, without the risk of
weakening the system's security & privacy, and without restricting the
analysis to a particular adversary.

  • Gustavo Petri, ARM, UK 


Title: Armour: Software Defined Security Policies for Networked Systems

Abstract:

In this talk I will present Armour, a language-based approach to enforcing global security policies on networked-systems. Armour provides security for multi-tenant and mutually distrusting micro-services. The benefit of Amour is that policies can be specified at a global level, and the Armour implementation ensures the correct enforcement of a global policy. I will show the design and implementation of Armour, and I will conclude with exciting open problems in this domain.

 

  • Ana Sokolova, University of Salzburg, AT

    Title:
    Tracing Probability and Nondeterminism

    Abstract:

The combination of probability and nondeterminism has been difficult to tackle and subject to a significant body of work in the past couple of decades, especially regarding understanding trace semantics. In recent work, joint with Filippo Bonchi and Valeria Vignudelli, we have managed to give a thorough and yet easy answer to the problem of combining probability and nondeterminism, which further enabled us to develop a theory of traces. This work is a nice example of the interplay between algebra and coalgebra: Systems and automata (with nondeterminism and probability) are coalgebras, but their behaviour is algebraic as we reveal in this work.

In the talk I will show how different trace semantics for systems with probability and nondeterminism can be recovered by instantiating a coalgebraic construction known as generalised determinisation. We characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.

 

 

 

Programme

 

09:00-10:00 Invited Talk: Ana Sokolova, Tracing Probability and Nondeterminism

10:00-11:00: Invited Talk: Gustavo Petri, Armour: Software Defined Security Policies for Networked Systems

11:00-11:30 Break

11:30-12:30: Invited Talk: Kostas Chatzikokolakis, Refinement relations for quantitative information flow

14:00-15:00 WG 1.8 business meeting

 

 

Participation

Participation, both to the workshop and to the IFIP WG 1.8 meeting, is open to everybody. For registration, please consult the CONCUR 2020 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

The eighth instalment of TRENDS (TRENDS 2019) was held on August 31, 2019 as a satellite event of CONCUR 2019, in Amsterdam, The Netherlands

 


 

 

 

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

 

 

 

to appear soon