Concurrent Automata

Concurrent Automata Seminar

Audience

This Seminar addresses Master and Bachelor students in Computer Science, or possibly in Mathematics, Bioinformatics, CuK or Computerlinguistics. Space permitting we might run it as a combined Seminar/Proseminar.

The first meeting

The first meeting takes place on Tuesday April 15, at 14:00 (sharp), in room SR 016 in E1 3. More details about the organisation will be discussed there. The default option is that the regular meetings will then also be on Tuesdays, from 14:00 to 16:00. All further meetings will take place at 14:00 (sharp) in SR 016 in E1 3.

Structure

• casting - April 29: 5 minutes presentation on timed automata, for papers to start from, see Materials in this system.
  (you will only present without any audience, you are not admitted to listen to the talks of the others; we will aks the author of the presentation that we consider the best to redo the presentation in the following meeting)
  10% of the final grade
• presentations - May 20 - July 08 15: 45 minutes presentations, one presentations per week,
  you probably cannot present all the material in these 45 minutes - you need to select a good story out of the material
  31% of the final grade
• writeup - draft until July 15 22, final version until September 15 22: writeup of your presentation in a book chapter style
  like in your presentation, you need to select a good story and explain it properly then (examples, exercises, etc.)
  29% of the final grade
• reviews - until August 15 22: you will be assigned two write-ups of you colleagues, you need to read them and give a written feedback
  10% 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
  20% of the final grade 
   

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 automata models.

Automata models play an important role in computer science. On one hand they build the foundation for theoretical aspects such as computability or the Chomsky hieararchy of languages. On the other hand they are foundational in the analysis of software systems, hardware, business processes, internet protocols, and wireless networks. In particular, the automatic verification of properties of a system, called model-checking, is based on automata models.

In this seminar, we deal with various automata models which in different senses extend finite automata. Every such extension is motivated by a concrete practical application area. This way, we can reason about timed behaviour of real-time systems; describe behaviour of reactive systems using languages composed not of finite but of infinite words; specify classes of models using a modal automata; or reason about randomness using probabilistic automata. We will see how these modelling feature are crucial for the respective application areas.

List of papers

• Comparison of CSP, CCS, and LOTOS
  Colin Fidge: A Comparative Introduction to CSP, CCS and LOTOS
  R.J. van Glabbeek: Notes on the methodology of CCS and CSP

• Event-structures (and non-interleaving semantics of CCS)
  Bowman, Gomez: Calculi and Automata for Modelling Untimed and Timed Concurrent Systems, Chapter 4.

• Interface Automata
  Luca de Alfaro, Thomas A. Henzinger: Interface Automata
  (for further context, see also: Luca de Alfaro: Game Models for Open Systems)

• TSO memory models
  M. F. Atig, A. Bouajjani, S. Burckhart, M. Musuvathi: On the Verification Problem for Weak Memory Models

• Probabilistic automata and PCCS
  Marielle Stoelinga: An introduction to probabilistic automata. Bulletin of the European Association for Theoretical Computer Science, 2002

• Model checking of probabilistic automata
  Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, and David Parker: Automated Verification Techniques for Probabilistic Systems
  (a lot of material, you cannot present all in 45 minutes, some Sections need to be omitted in the presentation; we can discuss)

• Energy timed automata (and closely related priced TA / weighted TA)
  an overview of priced TA models: P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey. Quantitative analysis of real-time systems using priced timed automata
  more technical content for energy TA: P. Bouyer, K. G. Larsen, N. Markey. Lower-Bound Constrained Runs in Weighted Timed Automata
  (it also possible to present only the overview, and search for some technical parts in research papers cited in the overview)

• Battery transition systems
  U. Boker, T. A. Henzinger, A. Radhakrishna. Battery transition systems
  (additional material: R. Alur, C. Courcoubetisb, N. Halbwachs, T.A. Henzinger, P.-H. Hod, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine: The algorithmic analysis of hybrid systems)