Madhavan Mukund

Concurrency Theory

Aug–Nov, 2019

Administrative details

  • Instructors: Aiswarya Cyriac, Madhavan Mukund

  • Teaching Assistants: Ashwani Anand, Sricharan A R

  • Evaluation:

    • Assignments, TBA

    • Mid-semeseter exam, TBA

    • Final exam, TBA

    • Copying is fatal.

  • Textbook:

    • We won't follow any one book. References will be put up under "Reading Material" as we go along.

Reading material

Elementary Net Systems

  • Elementary Net Systems (PDF),
    Grzegorz Rozenberg and Joost Engelfriet,
    Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, Springer LNCS 1491 (1998) 12-121.

Petri Nets

  • Place/Transition Nets (PDF),
    Joerg Desel and Wolfgang Reisig,
    Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, Springer LNCS 1491 (1998) 122-173.

  • An Improvement of McMillan's Unfolding Algorithm (PDF),
    Javier Esparza, Stefan Roemer and Walter Vogler,
    Formal Methods in System Design 20(3) (2002) 285-310.

Event Structures

  • Some Behavioural Aspects of Net Theory (PDF),
    P.S. Thiagarajan,
    Theoretical Computer Science, 71 (1990) 133-153.

  • Behavioural Notions for Elementary Net Systems (PDF),
    M. Nielsen, G. Rozenberg and P.S. Thiagarajan,
    Distributed Computing, 4 (1990) 45-75.

  • Petri Nets, Event Structures and Domains (PDF),
    M. Nielsen, G. Plotkin and G. Winskel,
    Theoretical Computer Science, 13 (1981) 85-108.

Theory of Regions

  • Petri Net Synthesis, Part I (PDF),
    E. Badouel and P. Darondeau, draft (2011)

Distributed Automata

  • Automata on Distributed Alphabets, (PDF),
    Madhavan Mukund,
    in Deepak D'Souza and Priti Shankar (eds),
    Modern Applications of Automata Theory, World Scientific (2012) 257-288.

Behavioural equivalences

  • The Linear Time - Branching Time Spectrum I: The Semantics of Concrete Sequential Processes, (PDF),
    Rob J. van Glabeek,
    in J.A. Bergstra, A. Ponse and S.A. Smolka (eds),
    Handbook of Process Algebra, Elsevier (2001) 3-99.

  • The Linear Time - Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves, (PDF),
    Rob J. van Glabeek,
    expanded version of article from CONCUR 1993, Springer LNCS 715 (1993) 66-81.

  • Testing Equivalences for Processes, (PDF),
    R. de Nicola and Matthew Hennessy,
    Theoretical Computer Science, 34 (1984) 83-133.

Course plan

(Subject to change!)

  • Petri nets
  • Unfoldings and event structures
  • Distributed automata
  • Mazurkiewicz traces and Zielonka's theorem
  • Program equivalences: failures, testing, bisimulation
  • Message-passing systems
  • Well-structured transition systems
  • Analysis via tree-interpretations

Lecture summaries

  • Lecture 1, 14 August 2019 (Lecture summary, Class notes)

    • Parallel and distributed computing, concurrency, introduction to Petri nets

  • Lecture 2, 16 August 2019 (Lecture summary, Class notes)

    • Petri nets, reachable markings, boundedness, elementary net systems, fundamental situations (concurrency, conflict, causality), contact and complementary places, diamonds in marking graph.

      Reference: Rozenberg-Engelfriet, Sections 1-3

  • Lecture 3, 21 August 2019 (Lecture summary, Class notes)

    • Confusion, free-choice property, deadlock and liveness, reachability, vector addition systems, coverability

      Reference: Rozenberg-Engelfriet, Section 3.5, Desel-Reisig, Sections 1-4.1

  • Lecture 4, 23 August 2019 (Lecture summary, Class notes)

    • Coverability, omega-markings and coverability tree

    • Arc weights, place capacities, inhibitor arcs

      Reference: Desel-Reisig, Section 4 (4.3-4.8), Section 7 (7.1-7.2)

  • Lecture 5, 28 August 2019 (Lecture summary, Class notes)

    • Petri nets with inhibitor arcs: undecidability of reachability

      Reference: Desel-Reisig, Section 7.3

    • Place and transition invariants

      Reference: Desel-Reisig, Sections 5.1-5.3

    • Petri net languages

  • Lecture 6, 30 August 2019 (Lecture summary, Class notes)

    • Synthesis: elementary net systems and theory of regions

      Reference: Badouel and Darondeau Sections 1.1-1.4

    • Unlabelled Petri net languages and unsolvable words

    • Petri net languages and the language hierarchy

    • Introduction to Mazurkiewicz traces

  • Lecture 7, 4 September 2019 (Lecture summary, Class notes)

    • Mazurkiewicz traces: trace languages, partial order representation, trace inclusion

    • Building a "canonical" partial order epresentation of [w] for a firing sequence w via causal nets

      References: Thiagarajan, Sections 1-4, Nielsen, Rozenberg, Thiagarajan, Sections 1-3

  • Lecture 8, 6 September 2019 (Lecture summary, Class notes)

  • Lecture 9, 11 September 2019 (Lecture summary, Class notes)

    • Wrap-up of prime event structures

    • Digression on denotational semantics and domain theory.

      An accessible account of denotational semantics is available in this book:

      Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, Joseph E. Stoy, MIT Press (1977)

      For a comprehensive survey on domain theory, see:

      Domain Theory, Samson Abramsky and Achim Jung, expanded version of a chapter in Handbook for Logic in Computer Science, Vol 3

    • Algorithm for constructing an unfolding, complete finite prefixes, local configurations, cutoff events, adequate orders, improved adequate orders

      Reference: Esparza, Roemer and Vogler