Written on 07.07.14 by Jan Krčál
This week, on July 08, there is no presentation. The remaining two presentation will be on July 15.
All the deadlines regarding the writeups have been shifted by one week.
Concurrent Automata Seminar
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.
- 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
0815: 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
1522, final version until September 1522: 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
1522: 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.
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)