Concurrency Theory 2011/2012
We offer a 4+2 first years Master's course on Concurrency Theory with the following content. It can be chosen as a theory course or specialisation on- Algorithmics
- Verification
- Embedded Systems.
News
- The oral exams will take place in the office of Roland Meyer: Geb. 34, Raum 428.
- Correcting clarification: the first sentence of problem 2.(a) in the last exercise sheet should be: "Define a domain of limits for Petri nets with an arbitrarily fixed number of places."
- There is a last exercise sheet. It will help you in the preparation for the exam.
- These slides give a good overview of the results on pi-Calculus.
- The lecture notes on siphons and traps, the basic verification system, and the first part on the enhanced verification system are now available for download from the lecture notes section.
- There will be an oral exam. The dates are still to be fixed.
- To be admitted to the final exam (we decide next week if written or oral) you must have at least 60% of the overall exercises marked "+" and you must have presented at least two of them at the board during the tutorial. Please try to solve and turn in the exercises in groups of 2-3 people.
Lecture Notes
The lecture comes with
lecture notes (ebook version, thanks to Matteo Settenvini, 17/02/2012)
Recall that we excluded SAT for the exam. The following notes are not yet part of the above document.
- Started with an overview of the topics presented in this lecture.
- Finished the overview of the topics presented in this lecture.
Exercises
The exercises are out on Tuesdays. Please hand them in the following Mondays before noon so that they can be discussed during the Wednesday tutorials. A mailbox where you can drop your soulutions can be found in building 34, 4th floor, close to room 401 and SoftTech AG. If you have questions or encounter problems with the exercises, please contact us — just pass by our offices or drop us a mail.- Download Exercise Sheet 1 here. This online version corrects a typo in Exercise 1.(b) in the text given in class.
- Download Exercise Sheet 2 here. From this second exercise sheet on you must hand in your solutions on Mondays. In problem 1b it should be assumed that M≥0.
- Download Exercise Sheet 3 here. The definition of transition invariants required for Exercise 4(a) was given in the tutorial.
- Download Exercise Sheet 4 here.
- Download Exercise Sheet 5 here. The statement of the 2nd problem had a typo corrected.
- Download Exercise Sheet 6 here.
- Download Exercise Sheet 7 here.
- Download Exercise Sheet 8 here.
- Download Exercise Sheet 9 here.
- Download Exercise Sheet 10 here.
- Download Exercise Sheet 11 here.
- Download Exercise Sheet 12 here.
- Download Exercise Sheet 13 here.
- A final (not graded) preparatory exercise sheet can be downloaded here. The linked exercises are taken from Stefan Schwoon.
- Correcting clarification: the first sentence of problem 2.(a) in the last exercise sheet should be: "Define a domain of limits for Petri nets with an arbitrarily fixed number of places."
Content
- Multi-threaded programs and Petri nets
- Petri net specific analyses
- Karp and Miller coverability graphs
- Invariants
- Unfoldings + SAT
- Static networks and lossy channel systems (lcs)
- Analysis of well-structured transition systems (wsts), with lcs as an example
- Wsts and Finkel's finite reachability tree
- Abdulla's backwards algorithm
- Geeraert's EEC algorithm
- Reconfigurable networks and process algebras
- Analysability
- Structural stationarity, depth, and breadth
- Well-structuredness in bounded depth
- Turing completeness in bounded breadth
- Bisimilarity, an alternative correctness notion
- Analysis and its limits
- Fixed points in the finite
- Communication freedom and prime elements in the infinite
- Undecidability following Jančar
Literature
The lectures will be based upon the following books and articles. Most of them are available online, the remaining ones can be found in the library.- L. Priese and H. Wimmel. Petri-Netze. Springer-Verlag, 2003.
- W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 1985.
- P. H. Starke. Analyse von Petri-Netz-Modellen. Leitfäden und Monographien der Informatik. Teubner, 1990.
- J. Esparza and M. Nielsen. Decibility issues for Petri nets-a survey. Journal of Information Processing and Cybernetics EIK, 30(3):143-160, 1994. Free version can be found here.
- J. Esparza. Decidability and complexity of Petri net problems - an introduction. In Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, volume 1491 of LNCS, pages 374-428, Springer-Verlag, 1998. Free version can be found here.
- J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159-189, 2000. Free version can be found here.
- J. Esparza and K. Heljanko. Unfoldings. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 2008. Free version can be found here.
- A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. Free version can be found here.
- G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1):180-203, 2005. Free version can be found here.
- P. Abdulla, A. Bouajjani, B. Jonsson. On-the-Fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In Proc. of the 10th International Conference on Computer Aided Verification, CAV, volume 1427 of LNCS, pages 305-318, Springer-Verlag, 1998. Free version can be found here.
- R. Meyer. Structural Stationarity in the pi-Calculus. PhD thesis, Department of Computing Science, University of Oldenburg, 2008. Free version can be found here.