Concurrency Theory

Concurrency Theory

Audience

This Seminar addresses Master and Bachelor students in Computer Science and related study programs that mandate participation in at least one Seminar.

The first meeting

The first meeting takes place on Monday October 28, at 14:05 in room 401 of E1 3.

Overview of the seminar

This Seminar has two goals:

1. to practice and to refine the skills of "scientific presentation", "scientific argumentation", and "scientific reflection";
2. to learn more about various theoretically challenging and practically relevant concurrency models, especially process algebra.

Despite its importance and more than three decades of highly active research, concurrent systems are still less understood than sequential systems. A comprehensive model of concurrency, comparable to Turing machines and the lambda calculus for sequential programs, is yet to be established for concurrency. In our seminar we will study some of the most important models and results for concurrency, and we will see why concurrency is so difficult to understand.

The scientific goal of the seminar is to provide a broad overview of the theoretical underpinnings of concurrency theory.

Structure

• Calibration - November 11 starting 08:45: 10 minutes presentations explaining either "What is Branching Bisimulation?" or "What are BPA, BPP, and BCCSP?". You will present to half of the audience (the one with the other topic assigned).
• 10% of the final grade
• Reading Phase - November/December:  We jointly study chapters from this book. Everyone will have read the respective material upfront, each student will be assigned a part of the matter as moderator to guide through the discussion. 
  21% of the final grade
• Presentation contents - by December 17: You will have settled scanning the relevant literature, and have sent over a draft story line of your presentation, to be discussed with the instructor. 
  5% of the final grade - failing to meet the deadline implies failing the seminar.
• Presentation slides - by January 20: You deliver the full slide set to the instructor, and defend it at an individual appointment.
  11% of the final grade - failing to meet the deadline implies failing the seminar.
• Presentation - February (or in a block): 35 minutes presentations. You need to construct a good story and explain it properly therein.
  33% of the final grade 
• Active participation: this involves feedback to the presentations of your colleagues and, most importantly, participation in the "scientific" discussions during and after the presentations, as well as in the reading phase.
  20% of the final grade

Topic Selection

We selected one or two papers from the arguably most intriguing areas of concurrency theory as entry points for deeper self-study of the topics.

1. Axiomatising Parallel Composition

   Entry points:
   Luca Aceto, Anna Ingólfsdóttir: The Saga of the Axiomatization of Parallel Composition. CONCUR 2007: 2-16

    

   Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, Bas Luttik: A Finite Equational Base for CCS with Left Merge and Communication Merge. ICALP (2) 2006: 492-503

    

2. Rule formats

   Entry point:
   Bard Bloom, Sorin Istrail, Albert R. Meyer: Bisimulation Can't be Traced. J. ACM 42(1): 232-268 (1995)

    

   Luca Aceto, Eugen-Ioan Goriac, Anna Ingolfsdottir, Mohammad Reza Mousavi, Michel A. Reniers. Exploiting Algebraic Laws to Improve Mechanized Axiomatizations. CALCO 2013: 36–50

3. Flavors of I/O Automata

   Entry points:
   Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Moses D. Liskov, Nancy A. Lynch, Olivier Pereira, Roberto Segala:Task-structured probabilistic I/O automata. J. Comput. Syst. Sci. 94: 63-97 (2018)

    

   Dilsun Kirli Kaynar, Nancy A. Lynch, Roberto Segala, Frits W. Vaandrager: The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science, Morgan & Claypool Publishers 2006

4. Axiomatising Priority

   Entry point:
   Luca Aceto, Taolue Chen, Anna Ingolfsdottir, Bas Luttik and Jaco van de Pol. On the Axiomatizability of Priority II. Theoretical Computer Science 412(28):3035–3044, 2011.

    

5. Monitorability

   Entry point:
   Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen: Adventures in monitorability: from branching to linear time and back again. PACMPL 3(POPL): 52:1-52:29 (2019)

    

6. Petri Nets, CCS, and Nested Units

   Entry points:
   Hubert Garavel: Nested-unit Petri nets. J. Log. Algebr. Meth. Program. 104: 60-85 (2019)

    

   Dirk Taubner: Representing CCS Programs by Finite Predicate/Transition Nets. Acta Inf. 27(6): 533-565 (1990)

    

7. Divergence

   Entry point:

   Markus Lohrey, Pedro R. D'Argenio, Holger Hermanns: Axiomatising divergence. Inf. Comput. 203(2): 115-144 (2005)

    

8. Actors

   Entry point:
   Gul A. Agha, Prasannaa Thati, and Reza Ziaei. Actors: A model for reasoning about open distributed systems.  Formal Methods for Distributed Processing - An Object Oriented Approach, chapter 8, pages 155–176. Cambridge University Press, New York, NY, USA, 2001.

    

9. Branching bisimilarity

   Entry point:
   Petr Jancar: Branching Bisimilarity of Normed BPA Processes as a Rational Monoid. Logical Methods in Computer Science 13(4) (2017)

    

10. Coupled simulation

    Entry point:
    Benjamin Bisping, Uwe Nestmann: Computing Coupled Similarity. TACAS (1) 2019: 244-261

     

11. Iteration
    Entry points:
    Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir: A Menagerie of Non finitely Based Process Semantics over BPA* - From Ready Simulation to Completed Traces. Mathematical Structures in Computer Science 8(3): 193-230 (1998)

     

    Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir: The max-plus algebra of the natural numbers has no finite equational basis. Theor. Comput. Sci. 293(1): 169-188 (2003)