Probabilistic Models for Concurrency [PMC]

Summer Term 2006
Lehrstuhl für Informatik II
Hauptstudium / Master Programme

The precise dates of the lectures and exercises will be announced during the first lecture. See also the table under overhead transparancies and exercises. On July 7th, the exercise class will be at 10:00-11:30.

News

The new version of Exercise 5 is updated on June 30, where in Problem 3, it should be ~m instead of ~p.

Motivation and background

Traditionally, models and methods for the analysis of the functional correctness of reactive systems and those for the analysis of their performance and dependability aspects, have been studied by different research communities. This has resulted in the development of successful, but distinct and largely unrelated modeling and analysis techniques for both domains. In many modern systems, however, the difference between their functional features and their performance properties has become blurred, as relevant functionalities become inextricably linked to performance aspects. The strong relationship between functionality and performance aspects calls for a modeling and analysis approach in which qualitative and quantitative aspects are studied from an integrated perspective.

This need has resulted in combining insights and results from process algebra with techniques for performance modeling and analysis such as Markov chains. Process algebra provides a formal apparatus for reasoning about structure and behavior of systems in a compositional way. Probabilistic extensions to process algebras are aimed to overcome the lack of hierarchical, compositional facilities in performance modeling and form the central theme of this course.

Content

• basic principles of Markov processes
  • discrete-time and continuous-time Markov chains
  • Markov decision processes
  • transient-state and steady-state probabilities, lumping
• probabilistic process algebra
  • probabilistic choice, synchronous interaction, asynchronous interaction
  • probabilistic bisimulation vs. lumping, simulation relations
• Markovian process algebra
  • exponentially delayed actions, semantics of concurrency and interaction
  • equivalence and pre-order relations, equational reasoning
  • algebra of Markov chains, abstraction
• general distributions in process algebra
  • generalized semi-Markov processes
  • timed automata, stochastic automata
  • expansion law, equivalences
• alternative modeling formalisms for reactive systems
  • stochastic Statecharts, Petri nets, and probabilistic Protocol Metalanguage (Promela)
• case studies and tools
  • modeling randomized distributed algorithms, plain-old telephone system
  • SCSI bus interface, plug-and-play networks, peer-to-peer network protocols
  • IPv4 address assignment protocol

Prior knowledge

Apart from the standard courses in the first two years (like Automata Theory and Probability Theory), there are no mandatory courses required.

It is helpful (though not required) when the course on Models for Concurrency (by Dr. Noll) has been followed and successfully passed.

Language

The lectures will be given in English.
All course material (i.e., slides and papers) will be in English.

Excercises

There will be 6 exercise series. Exercises can be worked on in groups of at most two students. To achieve a certificate for this course, half of the exercises has to be reasonably dealt with and the final exam has to be passed. The exercise sheets will be issued every other week.

Overhead transparencies and exercises

The reference solutions are available here, but only for the students attending the lecture. They may be accessed only from within Aachen university and with the password given in the lecture on April 26th.

Literature

Several sources will be used as basis for this course. The most relevant sources are listed here:

• R. Milner: Communicating and Mobile Systems: the Pi-calculus. Cambridge University Press, 1999
(Chapter 1 through 7)
• H. Hermanns: Interactive Markov Chains: The Quest for Quantified Quality. LNCS 2428, Springer 2002
• H. Hermanns, U. Herzog, J.-P. Katoen: Process algebra for performance evaluation. Theor. Comput. Sci. 274(1-2): 43-87 (2002)
• E. Brinksma, H. Hermanns, J.-P. Katoen: Lectures on Formal Methods and Performance Analysis. LNCS 2090, Springer 2001
• J. Hillston: A Compositional Approach to Performance Modelling. Cambridge University Press, 1996
• J. Bergstra, A. Ponse and S.A. Smolka: Handbook of Process Algebra. Elsevier, 2001
(Chapters 6 and 11)
• M. Stoelinga: An introduction to probabilistic automata. Bull. of the EATCS, number 78, 2002
• H. Hermanns and J.-P. Katoen. Automated compositional Markov chain generation for a plain-old telephone system, Science of Computer Proghramming 36: 97-127 (2000)