Seminar in Theoretical CS, Summer Semester 2014
News
- 10.01.2014: we are online
Schedule
Thu, 20 Feb 2014, 15:00 |
Introduction at seminar room of i2 |
-8 weeks | Table of contents due |
-6 weeks | Preliminary version of report due |
-4 weeks | Final version of report due |
-2 weeks | Preliminary version of slides due |
-1 week | Final version of slides due |
Overview
Today, concurrent programming has become mainstream, dictated by need for ever increasing performance which, having reached the end of Moore’s law, can only be achieved by parallelism. Indeed, application software from areas such as medicine or natural sciences heavily relies on parallel hardware infrastructure like (GP)GPU accelerators, FPGAs, and multi- and many-core machines.
However, it is also today that we see concurrency faults coming up every day. The simple reason is that writing concurrent programs is difficult. Most programmers “think sequentially” and therefore make mistakes when writing concurrent software. Notorious programming errors include deadlock and violations of atomicity or order of operations, which are mainly caused by the wrong use of synchronization primitives like semaphores or locks. Even worse, the inherent non-deterministic behavior of concurrent software makes bugs difficult to reproduce. Addressing these challenges requires efforts from multiple related disciplines, involving concurrency bug detection, program testing and validation, and programming language design.
Another important area of computer science where concurrency naturally arises is that of reactive systems, which maintain an ongoing interaction with their environment. In contrast to sequential systems whose meaning is defined by the results of finite computations, the behavior of reactive systems is mainly determined by concurrent execution, communication, interaction, and mobility of non-terminating processes. Typical examples include operating systems, control systems for production lines, power plants, or vehicles. As many of such systems are safety critical, their development calls for rigorous formal techniques for design, implementation, and validation.
The aim of this seminar is to deepen some of the topics that have been introduced in the Concurrency Theory Course in the preceding semester, and to study alternative modeling approaches that have not been discussed before. With respect to the former, additional topics related to process algebras will be studied, which provide a formal apparatus for reasoning about structure and behavior of systems in a compositional way. Also, the seminar will feature additional material on Petri Nets, which are well suited for explicitly modeling the concurrent behavior of distributed systems.
Each of the topics is addressed in a scientific journal or conference article (please refer to the references below). These research articles are the basis on which students have to prepare their report and presentation.
Prerequisites
Basic knowledge in the following areas is expected:
- Essential concepts of operating systems
- Formal languages and automata theory
- Mathematical logic
- Previous knowledge in Concurrency Theory is helpful but not mandatory
Dates
(all presentations on Tuesdays 16:00-17:00 at I2 seminar room)
Date | Topic(s) |
22 April | 1 |
13 May | 5 |
27 May | 8 |
3 June | 9 |
24 June | 12 |
1 July | 14 |
8 July | 3, 15 |
15 July | 4 |
Topics
Process Algebras
- Timed CCS
- Literature: W. Yi: CCS + Time = an Interleaving Model for Real Time Systems
- Supervisor: Thomas Noll
- Student: Thomas Osterland
- Date: 22.04.2014
- Synchronous and Asynchronous CCS
- Literature: R. Milner: Calculi for synchrony and asynchrony
- Supervisor: –
- Student: –
- Date: –
- ACP Process Algebra
- Literature: J.A. Bergstra, J.W. Klop: Process algebra for synchronous communication
- Supervisor: Thomas Noll
- Student: Christian Plewnia
- Date: 08.07.2014
- Decidable Subsets of CCS
- Literature: S. Christensen, Y. Hirshfeld, F. Moller: Decidable Subsets of CCS
- Supervisor: Benjamin Kaminski
- Student: Yanjie Wang
- Date: 15.07.2014
- The Linear Time-Branching Time Spectrum
- Literature: R. van Glabbeek: The linear time – branching time spectrum
- Supervisor: Christina Jansen
- Student: Philip Martzok
- Date: 13.05.2014
- Axiomatization of Bisimilarity
- Literature: R. van Glabbeek. A complete axiomatization for branching bisimulation congruence of finite-state behaviours
- Supervisor: –
- Student: –
- Date: –
Petri Nets
- Reachability in Petri Nets
- Literature: E.W. Mayr: An Algorithm for the General Petri Net Reachability Problem
- Supervisor: –
- Student: –
- Date: –
- Undecidability of Bisimilarity for Petri Nets
- Literature: P. Jancar: Undecidability of bisimilarity for Petri nets and some related problems
- Supervisor: Kevin van der Pol
- Student: Oxana Khamidova
- Date: 27.05.2014
- Liveness and Safeness of Petri Nets
- Literature: E. Best, P.S. Tiagarajan: Some Classes of Live and Safe Petri Nets
- Supervisor: Kevin van der Pol
- Student: Sharif Md Khairul Hossain
- Date: 03.06.2014
- Efficient Net Unfolding
- Literature: J. Esparza, S. Römer, W. Vogler: An Improvement of McMillan’s Unfolding Algorithm
- Supervisor: –
- Student: –
- Date: –
- Applications of Net Unfolding
- Literature1: J. Esparza, C. Schröter: Unfolding Based Algorithms for the Reachability Problem
- Literature2: K. Heljanko: Model Checking with Finite Complete Prefixes Is PSPACE-Complete
- Supervisor: –
- Student: –
- Date: –
- Timed Nets
- Literature: W.M. Zuberek: Timed Petri nets definitions, properties, and applications
- Supervisor: Sabrina von Styp
- Student: Nicolas Osterloh
- Date: 24.06.2014
- Generalized Stochastic Petri Nets
- Literature: M.A. Marsan, G. Conte, G. Balbo: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems
- Supervisor: –
- Student: –
- Date: –
Other Concurrency Models
- Mazurkiewicz Traces
- Literature: A.W. Mazurkiewicz: Introduction to Trace Theory
- Supervisor: Benjamin Kaminski
- Student: Paul Gageik
- Date: 01.07.2014
- Event Structures
- Literature: G. Winskel: An introduction to event structures
- Supervisor: Christina Jansen
- Student: Manuel Sascha Weiand
- Date: 08.07.2014 (two presentations!)
- Modeling Concurrency with Partial Orders
- Literature: V. Pratt: Modeling Concurrency with Partial Orders
- Supervisor: –
- Student: –
- Date: –
Additional Material
Registration
Registration to the seminar is handled between January 14 and 26, 2014, via the central online form at www.graphics.rwth-aachen.de/apse
Contact
Thomas Noll <noll at cs.rwth-aachen.de>