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.

Setup

If it were possible we would be meeting physically about once per week in a pandemia compliant setup. The precise weekly time slot will be fixed once the participants' constraints are known. Remote participation via Zoom will be default until further notice.

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

• Kickoff- November 5 at 09:15: We discuss the setup and potential topics.
  0% of the final grade
• Selection - by November 12: You bid for the topics using this doodle link, afterwards you are assigned one of them.
  0% of the final grade
• Calibration - November 19 at 08:15: 8 minutes presentations explaining either "What is Branching Bisimulation?" or "What is the pi-calculus?". You will present to half of the audience (the one with the other topic assigned).
  15% of the final grade
• Scope - by early December: You explore the topic assigned. You are invited to come with suggestions how to shape or adjust the scope of your upcoming presentation.
  0% of the final grade
• Contents - by December 17: You have settled scanning the relevant literature, and have sent over a draft story line of your presentation, to be discussed with the instructor.
  10% of the final grade - failing to meet the deadline implies failing the seminar.
• Slides - by January 20: You deliver the full slide set to the instructor, and defend it at an individual appointment.
  15% of the final grade - failing to meet the deadline implies failing the seminar.
• Presentation - March 15-17: 45 minutes presentations each. You need to construct a good story and explain it properly therein.
  40% 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
   

Topics

Below is a selection of entry points for topics that

• are of foundational nature, or
• are of anecdotical nature, or
• are selected from the most recent edition of the International Conference on Concurrency Theory, CONCUR 2020.
   

1. Axiomatising Parallel Composition -- JH on March 17
   Entry point:
   Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, Mathias Ruggaard Pedersen: On the Axiomatisability of Parallel Composition: A Journey in the Spectrum. CONCUR 2020, 18:1-18:22.
    

2. 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)
   and
   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
    

3. Timed Automata Expressiveness
   Entry point:
   Lorenzo Clemente, Slawomir Lasota, Radoslaw Piórkowski: Determinisability of One-Clock Timed Automata. CONCUR 2020, 42:1-42:171
    

4. Distributed Consensus -- YS on March 17
   Entry point:
   A. R. Balasubramanian, Igor Walukiewicz: Characterizing Consensus in the Heard-Of Model. CONCUR 2020, 9:1-9:18.
    

5. Actors -- SH on March 15
   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.
    

6. Coupled Similarity -- TR on March 16
   Entry point:
   Benjamin Bisping, Uwe Nestmann, Kirstin Peters: Coupled similarity --  the first 32 years. Acta Informatica 57(3-5): 439-463 (2020)
    

7. Shielding -- NL on March 17
   Entry point:
   Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, Roderick Bloem: Safe Reinforcement Learning Using Probabilistic Shields. CONCUR 2020, 3:1-3:16
    

8. Session Types - Quantitatively -- MK on March 15
   Entry point:
   Omar Inverso, Hernán C. Melgratti, Luca Padovani, Catia Trubiani, Emilio Tuosto: Probabilistic Analysis of Binary Sessions. CONCUR 2020, 14:1-14:21.
    
9. Session-Type Based Reasoning in Seperation Logic -- JL on March 16
   Entry point:
   Jonas Kastberg Hinrichsen, Jesper Bengtson and Robbert Krebbers. Actris: Session-Type Based Reasoning in Separation Logic. POPL 2020, Article 6.
    

10. Markov Chain Bisimilarity -- TG on March 16 
    Entry point:
    David N. Jansen, Jan Friso Groote, Ferry Timmers, Pengfei Yang: A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. CONCUR 2020, 8:1-8:20.