Theoretical Computer Science

Concurrency Theory 2010/2011

News

• The results of the 2nd exam can be found on the board next to 34/424. You can have a look at your results (exam review, Klausureinsicht) next Friday, April 29th 2011, from 9.30 to 11.00 in 34/419.
• The results of the exam can be found on the board next to 34/424. You can have a look at your results (exam review, Klausureinsicht) this Friday, March 18th 2011, from 9.30 to 11.00 in 34/419.
• The results of the exam will be available on March 15th 2011.
• An example for verification with evs can be found here. Thanks to those who spotted a bug. For the ERV algorithm, this is an example. Note that I updated the terminology and that the token is back. We compute a finite and complete prefix of the unfolding. I omitted some potential extensions in the end that contained cut off events. Here is an example for the EEC algorithm. Its actually an example from exercise sheet 11 that raised some questions. I answered them in an accompanying text. Examples for the structural semantics can be found here and here. They are taken from my thesis.
• On Monday, February 21st 2011, there will be an extra tutorial from 11.45 to 13.15. We will meet in room 34-420 and recapitulate exercises as they are relevant for the exam.
• The part on dynamic networks is based on this thesis.
• The chapter on lossy channel systems will be based on this paper. The formalism and simple regular expressions are taken from this article. The theory of well-structured transition systems is here and here. The eec algorithm is presented here. Some comments on well-quasi orderings can be found in Chapter 12 of this book.
• It seems the registration dates can be found in this document.
• On Monday, November 29th 2010, there will be an extra tutorial instead of a lecture. We will recapitulate exercises as they are relevant for the exam and discuss questions.
• There will be a written exam on February 28th 2011 from 08.30 to 11.00 in 46-210. The second exam will take place on April 13th 2011 from 13.30 to 16.00 in 46-110.

Lecture Notes

• The lecture notes are now available from KIS. Hope all of you have access to the system. The linear programming part of the lecture was inspired by this article.

Exercises

• Download Exercise 1 here.
• Download Exercise 2 here.
• Download Exercise 3 here.
• Download Exercise 4 here. In Problem 3, arcs with two heads stand for two arcs. The exercise is a bit of work but demonstrates the power of the analysis technique. The example is taken from J. Esparza, S. Melzer: Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design 16(2): 159-189 (2000).
• Download Exercise 5 here.
• Download Exercise 6 here.
• Download Exercise 7 here.
• Download Exercise 8 here.
• Download Exercise 9 here. Exercise 4 is taken from 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.

  Merry Christmas and Happy New Year!

• Download Exercise 10 here.
• Download Exercise 11 here.
• Download Exercise 12 here.
• Download Exercise 13 here.

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

• 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.