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

August 27, 2016, Quebec City, Canada

A satellite event of CONCUR 2016

  

Description

TRENDS 2016 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 in the morning of August 27, 2016 and will consist of three invited talks, followed by the yearly WG 1.8 business meeting.

 

Invited Speakers

  • Franck van Breugel, York University, Canada
  • Dana Fisman, Ben-Gurion University, Israel
  • Philippa Gardner, Imperial College, UK

 

Program (Slides and Abstract)

  • 9:00-09:45 Invited talk: Franck van Breugel, Towards a Quantitative Theory of Concurrent Probabilistic Systems

    For the last three and a half decades behavioural equivalences such as bisimilarity,
    due to Milner and Park, have been a cornerstone of concurrency theory.  As this
    theory matured, more detailed models of concurrent systems have been developed, some
    including quantitative data such as cost, probabilities and time.  For these models
    with quantitative information, behavioural equivalences were proposed, such as
    probabilistic bisimilarity, due to Larsen and Skou.  Although these behavioural
    equivalences allow us to reason about the behaviour of concurrent systems, they have
    one drawback: they are not robust.  That is, small changes in the quantitative data
    may cause equivalent states to becomes inequivalent or vice versa.  Since the
    quantitative data is usually is obtained experimentally and, therefore is often just
    an approximation, this lack of robustness is a serious limitation of behavioural
    equivalences for concurrent systems with quantitative information.  This lack of
    robustness was first pointed out by Giacalone, Jou and Smolka.  They suggested
    generalizing behavioural equivalences, which assign to each  pair of states a Boolean,
    to behavioural pseudometrics, which assign to each pair of states a nonnegative real
    number.  Behavioural pseudometrics play an increasingly important role in concurrency
    theory, as is reflected, for example, by the fact that four papers on this topic are
    part of this year's program of CONCUR.

    In this talk, I will focus on behavioural pseudometrics for concurrent probabilistic
    systems.  These systems are often modelled by Segala's probabilistic automata.  During
    the last decade several behavioural pseudometrics have been introduced for these
    automata.  Here, I will concentrate on the one put forward by Deng, Chothia, Palamidessi,
    and Pang.  I will use this behavioural pseudometric to illustrate two trends.  Firstly,
    I will show how games can be used to characterize and compute behavioural pseudometrics.
    Secondly, I will show that it is often beneficial to decide the behavioural equivalence
    before computing the behavioural pseudometric.
     
  • 9:45-10:30 Invited talk: Dana Fisman, Inferring Regular Languages and omega-Languages

    In the last decade the problem of inferring an unknown regular language using membership and equivalence queries, solved by Angluin in 87, has found many application in verification and synthesis, e.g., in black-box checking, assume-guarantee reasoning, error localization, regular model checking, and more. These new applications challenge the state-of-the art solutions in various directions, in particular, scaling or working with more succinct representations, and dealing with omega-languages, the main model for reactive systems.

     

    Inference algorithms typically rely on the correspondence between the automata states and the right congruence, henceforth, the residuality property. DFAs enjoy the residuality property (as stated by the Myhill-Nerode Theorem) but more succinct representations such as non-deterministic and alternating finite automata (NFAs and AFAs) in general do not. The situation in the omega-languages realm is even worse, since none of the traditional automata that can express all regular omega-languages enjoys the residuality property.

     

    In this talk I will survey residual models for regular languages and omega-languages, the simple learning algorithms that can infer these, and many related open questions.

     

    The talk is based on joint works with Dana Angluin, Udi Boker and Sarah Eisenstat.

 

  • 10:30-11:00 Coffee Break 

  • 11:00-11:45 Invited talk: Philippa Gardner, A Concurrent Specification of POSIX

    POSIX is a standard for operating systems, with a substantial part
    devoted to specifying file-system operations. File-system operations
    exhibit complex concurrent behaviour, comprising multiple actions
    affecting different parts of the state: typically, multiple atomic
    reads followed by an atomic update. However, the standard’s
    description of concurrent behaviour is unsatisfactory: it is
    fragmented; contains ambiguities; and is generally under-specified. We
    provide a formal concurrent specification of POSIX file systems and
    demonstrate scalable reasoning for clients. Our specification is based
    on a concurrent specification language, which combines a refinement
    calculus with  recent developments in concurrent separation logics for
    reasoning about abstract atomic operations.

    In this talk, I will give an overview of  recent work on concurrent
    separation logics in general and describe our  work on the concurrent
    specification of POSIX in particular. This work is joint with Gian Ntzik and
    Pedro da Rocha Pinto. Details of  our work on concurrent verification can
    be found at  http://psvg.doc.ic.ac.uk/research/concurrency.html.


  • 11:45-13:00 IFIP WG 1.8 Business Meeting (Open to all)

  • 13:00-14:00 Lunch

  

Participation

Participation, both to the workshop and to the IFIP WG 1.8 meeting, is open to everybody. For registration, please consult the CONCUR 2016 registration page

 

Organizers

Ilaria Castellani (INRIA Sophia Antipolis, France)

Mohammad Mousavi (Halmstad University, Sweden)

 

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.