Title
Concurrency Theory (contents see below)
Time
Tuesdays, 16:00, Room 4201b
News
When
What
8 Jan 2010
The evaluation results are available
3 Dec 2009
The papers are now available from here.
30 Nov 2009
The presentation from 1 Dec is moved to 2 Dec, 15:00!
10 Nov 2009
The Presentation on 17 November is cancelled.
16 Oct 2009
The presentation on Mazurkiewicz traces is on again, at the planned day. Instead, the first presentation on Process Terms is cancelled. This means that the first presentation will be on 3. November!
13 Oct 2009
The presentation on Mazurkiewicz traces has been cancelled.
Sep 2009
The first presentation will now take place on 27. October. The presentation of 20. October will take place at 22. December.
21 July 2009
The Advisers for the different topics are now added to the list of topics below.
16 July 2009
Assignment of topics and tentative dates are online. Names of advisers will follow.
16 July 2009
The slides of the introduction are online.
15 July 2009
The seminar presentations are planned to take place on Tuesdays, 16.00, starting 20 October 2009.
15 July 2009
The kick-off meeting will take place on 16 July, 16:30, Room 4201b, Building E1.
2 June 2009
We are online!
Ausarbeitungen / Papers
Topics and Literature
Nr | Date | Topic | Student | Adviser |
|---|---|---|---|---|
4 | 10.11. | CSP. | Freiberg | |
7 | 24.11. | Hennessy-Milner logic. | Maleki-Fard | |
8 | 2.12. 15:00 | Branching Processes of Petri nets. | Himber | |
9 | 8.12. | Petri Nets, Event Structures and Domains. | Lindt | |
11 | 15.12. | Trace-oriented models of concurrency: Finite Traces. | de Carolis | |
1 | (entf舁lt) | Petri Nets. | - | |
13 | (entf舁lt) | Mazurkiewicz-Traces. | - | |
14 | 19.1.10 | Modeling Concurrency with Partial Orders. | Fonteyn | |
15 | (entf舁lt) | The Pi-Calculus. | - | |
17 | 2.2.10 | A calculus for cryptographic protocols: the spi calculus. | Falak Sher |
Dates are tentative.
Literature
Many papers can be found in
- J.A. Bergstra, A. Ponse, S.A. Smolka (Eds.) Handbook of Process Algebra. Elsevier, 2001.
We abbreviate this book in the list below as PA.
Topic(s) | Literature |
|---|---|
1,2 | E.-R. Olderog. Nets, Terms and Formulas. Cambridge University Press, 1991. |
3 | W.J. Fokkink, Introduction to Process Algebra (2nd edition), April 2007 (pdf, postscript) |
4 | A. W. Roscoe. Theory and Practice of Concurrency. Prentice-Hall, 2005. Chapter 1-3 and 6.<cite> Available here. </cite> |
5,6 | Rob van Glabbeek: The Linear Time-Branching Time Spectrum I, Ch.1 PA. |
7 | Matthew Hennessy, Robin Milner: Algebraic Laws for Nondeterminism and Concurrency J. ACM 32(1): 137-161 (1985) |
8 | Joost Engelfriet, Branching Processes of Petri nets, Acta Informatica 28, 1991, p 575-591. |
9 | Mogens Nielsen, Gordon D. Plotkin, Glynn Winskel: Petri Nets, Event Structures and Domains, Part I. Theor. Comput. Sci. 13: 85-108 (1981) |
10 | Christel Baier, Mila E. Majster-Cederbaum: The Connection be- tween an Event Structure Semantics and an Operational Seman- tics for TCSP. Acta Inf. 31(1): 81-104 (1994) |
11,12 | M. Broy and E.-R. Olderog: Trace-oriented models of concur- rency. Ch. 2 PA. |
13 | Antoni W. Mazurkiewicz: Trace Theory. Advances in Petri Nets 1986: 279-324 |
14 | Vaughan Pratt: Modeling Concurrency with Partial Orders. Int. J. on Parallel Programming vol. 15(1), 33-71 (1986) |
15 | Joachim Parrow: An Introduction to the Pi-Calculus. Ch. 8 PA. |
16 | Cardelli, L.; A.D. Gordon. "Mobile Ambients". Proceedings of the First international Conference on Foundations of Software Science and Computation Structure (March 28 - April 4, 1998). M. Nivat, Ed. Lecture Notes in Computer Science (Springer-Verlag) 1378: 140--155 |
17 | Abadi, Martin and Gordon, Andrew D. A calculus for cryptographic protocols: the spi calculus. Proceedings of the 4th ACM conference on Computer and Communications Security (CCS '97). pp. 36-47. ACM, 1997. |
Type
Weekly Seminar (Hauptseminar) in Theoretical CS for Bachelor and Diplom students
People involved
- Henrik Bohnenkamp (Contact person for questions, henrik at cs dot rwth-aachen dot de)
- Martin Neuh舫?er
- Thomas Noll
- Joost-Pieter Katoen
First Meeting
The first meeting will take place 16 July, 16:30, in the seminar room of I2, Room 4201b, Building E1.
Attending this meeting is mandatory, i.e., selected students need a good reason if they cannot attend and want to keep their spot in the seminar (waiting lists are usually long). Participants who know beforehand that they can not attend should inform Henrik Bohnenkamp before the meeting.
Contents
Concurrency is a phenomenon that can be found in nearly all areas of
computer science. Multi-Core processors, distributed systems, network
protocols, multi-threaded programs, operating systems... in all these
examples concurrency is present, i.e., the fact that different events,
which are are somehow depending on each other, can happen at the same
time, and can influence each other in different (negative ) ways.
Concurrency can lead to baffling, obviously incorrect behavior even of
simple systems, but with the mistakes very well hidden and extremely
difficult to find. Livelock and deadlock are the best-known errors
that can be introduced during the design and programming of concurrent
systems. A plethora of protocols and mechanisms have been developed
over the decades to solve the problem of mutual exclusion and process
synchronisation (see "The Little Book of Semaphores" for an overview),
but to actually show that they do what they are supposed to do is most
difficult.
Already in the 60s there was the insight that concurrency is a
phenomenon that is in need of rigorous analysis. The first, seminal
approach to describe concurrent systems in a formal way was published
by Petri in 1962. Petri nets are a graph-based formalism to describe
concurrency. Research on has lead to a vast number of papers and to
many extensions of the original concept.
Others prefer to describe concurrent systems in a way more structured
than Petri nets allow, by using languages. In the 80s, the idea was
developed to describe concurrent systems with a compositional
specification language, where complex processes are described by
combining simpler processes with simple operators. This approach has
led to process algebra, and the three major approaches to describe its
semantics: operational, denotational, and axiomatic.
Milner formulated the goal to find a calculus of processes which would
become all-encompassing and would be able to describe all aspects of
concurrency, in the same way as the lambda-calculus is able to
describe all aspects of computable functions.
Whereas this goal seems to be as far away as it was at the beginning,
research on concurrency has produced a rich theory in process calculi,
process algebras, semantics for concurrency and applications in
verification and model-checking.
This seminar picks some interesting topics from concurrency theory. Among others, the following questions will be adressed:
computer science. Multi-Core processors, distributed systems, network
protocols, multi-threaded programs, operating systems... in all these
examples concurrency is present, i.e., the fact that different events,
which are are somehow depending on each other, can happen at the same
time, and can influence each other in different (negative ) ways.
Concurrency can lead to baffling, obviously incorrect behavior even of
simple systems, but with the mistakes very well hidden and extremely
difficult to find. Livelock and deadlock are the best-known errors
that can be introduced during the design and programming of concurrent
systems. A plethora of protocols and mechanisms have been developed
over the decades to solve the problem of mutual exclusion and process
synchronisation (see "The Little Book of Semaphores" for an overview),
but to actually show that they do what they are supposed to do is most
difficult.
Already in the 60s there was the insight that concurrency is a
phenomenon that is in need of rigorous analysis. The first, seminal
approach to describe concurrent systems in a formal way was published
by Petri in 1962. Petri nets are a graph-based formalism to describe
concurrency. Research on has lead to a vast number of papers and to
many extensions of the original concept.
Others prefer to describe concurrent systems in a way more structured
than Petri nets allow, by using languages. In the 80s, the idea was
developed to describe concurrent systems with a compositional
specification language, where complex processes are described by
combining simpler processes with simple operators. This approach has
led to process algebra, and the three major approaches to describe its
semantics: operational, denotational, and axiomatic.
Milner formulated the goal to find a calculus of processes which would
become all-encompassing and would be able to describe all aspects of
concurrency, in the same way as the lambda-calculus is able to
describe all aspects of computable functions.
Whereas this goal seems to be as far away as it was at the beginning,
research on concurrency has produced a rich theory in process calculi,
process algebras, semantics for concurrency and applications in
verification and model-checking.
This seminar picks some interesting topics from concurrency theory. Among others, the following questions will be adressed:
- How can we describe concurrent systems?
- What kind of semantic formalisms exist, and how can they be compared?
- How can the behavior of different processes be compared?
- How can we reason about concurrent systems?
- What is the "algebra" in process algebra?
- ...
The following links lead to some short pdf files which illuminate the subject area some more.
- Samson Abramsky has some opinions on Concurrency Theory.
- The Introduction to the Handbook of Process Algebra gives a very short overview over the area and introduces also some of the topics of the seminar.
- The Introduction of Petersons Book " Petri Net Theory and the Modeling of Systems", Prentice Hall (1981), reviews some basic facts of Petri nets.
- The Frontmatter of Sangiorgi's and Walker's book "The π-calculus", Cambridge University Press (2001), discusses mobility in the context of concurrent systems.
Rules
- Every participant works on one subject.
- Written report, $\approx$ 15-20 pages.
- 45 min presentation
- German or English
- One presentation weekly
Deliverables:
- immediately: get literature from web or from library, learn all that seems to be important about the subject. Contact advisor if there are problems.
- 6 weeks prior to talk (or earlier): contact advisor and discuss your ideas about the presentation and report. Bring a 2-3-page draft of your report.
- 2 weeks prior to talk (preferably earlier): final version of report due.
- 1 week prior to talk: discuss presentation (have slides prepared).
Note that these deadlines describe only the tightest-possible case. In general it is much better and more relaxed for everbody if students and advisor meet earlier than indicated.