Concurrency Theory

Course Overview

This course introduces the theoretical foundations of concurrency. We study mathematical models for concurrent and distributed systems, including process calculi, transition systems, and petri-nets. Emphasis is placed on formal reasoning of these models.

Learning Objectives

• Understand formal models of concurrency and interaction
• Reason about equivalence, refinement, and behavioral semantics
• Analyze expressiveness, decidability and complexity boundaries
• Gain exposure to verification and model-checking techniques

Course Information

Topics Covered

• Introduction to Concurrency
• Process Calculi (CCS) Syntax and Operational Semantivs
• Bisimulation, Weak Bisimulation, Simulation Equivalence and Trace Equivalences
• Revisiting Computability
• Process Calculi with mobility (π-calculus)
• Process Calculi (CSP)
• Introduction to Trace Theory: Mazurkiewicz Traces and Related Theorems
• Well-Structured Transition Systems
• Petrinets/Vector Addition Systems with States
• Expressiveness and Decidability Results
• Temporal Logic, Model Checking and Verification Techniques

Assessment Structure (before the potluck grading)

• Problem Sets: 15%
• Mini Project / Reading Project: 15%
• Mid-Semester Exam: 20%
• End-Semester Exam: 45%
• Class Paticipation:5%

Lecture Slides and Details

• Lecture 1: Introduction to Concurrency Theory Course
• Lecture 2 and 3: Process Algebra — Calculus of Communicating Systems (CCS): Syntax and Operational Semantics
• Lecture 4: CCS Toy Examples
• Lecture 5: Behavioral Equivalences (CCS)
• A brief detour into the Theory of Computation:
  Lecture 6 — Introduction to Complexity Classes P, NP, PSPACE (board)
  Lecture 7 — Revisiting Turing Machines & Halting Problem Undecidability (board)
  Lecture 8 — Counter Machines (board)
• Pi Calculus: Introduction and Undecidability of Equivalence

References

• Robin Milner, Communication and Concurrency
  Foundational text for CCS and behavioral equivalences.
• C. A. R. Hoare, Communicating Sequential Processes
  Original monograph introducing CSP.
• A. W. Roscoe, The Theory and Practice of Concurrency
  Definitive modern reference for CSP, refinement, failures and divergences.
• Davide Sangiorgi and David Walker, The π-Calculus: A Theory of Mobile Processes
  Standard reference for the π-calculus, expressiveness, and encodings.
• Volker Diekert and Grzegorz Rozenberg (eds.), The Book of Traces
  Authoritative reference on trace theory and partial-order semantics.
• Selected research papers on Petri Nets
  Coverability, Reachability, Non-Elementary Behaviour of Petrinets, Reversal Bounded Counter Machines, Semilinear Sets.
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking
  Temporal logics (LTL, CTL, μ-calculus) and model checking techniques.