Teaching assistant: Ritam Raha, Rajarshi Roy
Evaluation:
Assignments, 35%
Mid-semeseter exam, 25%
Final exam, 40%
Copying is fatal.
Textbook:
We won't follow any one book. References will be put up under "Reading Material" as we go along.
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.
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.
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.
Petri Net Synthesis, Part I
(PDF),
E. Badouel and P. Darondeau, draft (2011)
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.
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.
On Communicating Finite-State Machines
(PDF),
Daniel Brand and Pitro Zafiropulo,
Journal of the ACM, 30(2), (1983) 323-342.
The Theory of Message Sequence Charts
(PDF),
K. Narayan Kumar,
in Deepak D'Souza and Priti Shankar (eds),
Modern Applications of Automata Theory, World
Scientific (2012) 289-324.
The Theory of Message Sequence Charts
(PDF),
K. Narayan Kumar,
Slides from a talk at TIFR, April 2009.
Realizability and Verification of MSC Graphs
(PDF),
Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis,
Theoretical Cmputer Science, 331,
(2005) 97-114.
Verifying Programs with Unreliable Channels
(PDF),
Parosh Aziz Abdulla and Bengt Jonsson,
Information and Computation, 127,
(1996) 91-101.
Well-Structured Transition Systems Everywhere!
(PDF),
Alain Finkel and Philippe Schnoebelen,
Theoretical Computer Science, 256,
(2001) 63-92.
Parallel and distributed computing, concurrency, introduction to Petri nets
Petri nets, reachable markings, boundedness, elementary net systems, fundamental situations (concurrency, conflict, causality), contact and complementary places, diamonds in marking graph, confusion.
Reference: Rozenberg-Engelfriet, Sections 1-3
Confusion, free-choice property, deadlock and liveness, reachability, vector addition systems, coverability, omega-markings and coverability tree
Reference: Rozenberg-Engelfriet, Section 3.5, Desel-Reisig, Sections 1-4 (upto 4.5)
Coverability tree, arc weights, place capacities, inhibitor arcs, undecidability of reachability for inhibitor arcs
Reference: Desel-Reisig, Section 4 (4.6-4.8), Section 7
Place invariants
Reference: Desel-Reisig, Section 5.1-5.2
Petri net languages
Unlabelled Petri net languages and unsolvable words
Introduction to Mazurkiewicz traces
Mazurkiewicz traces: trace languages, partial order representation, trace inclusion
Building a "canonical" partial order representation of [w] for a firing sequence w via causal nets
References: Thiagarajan, Sections 1-4, Nielsen, Rozenberg, Thiagarajan, Sections 1-3
Firing sequences to causal nets and traces; causal nets to occurrence nets and event structures
References: Thiagarajan, and Nielsen, Rozenberg, Thiagarajan
Event structures, prime configurations, algebraic characterization of prime event structures
References: Nielsen, Plotkin, Winskel.
Algorithm for constructing an unfolding, complete finite prefixes, local configurations, cutoff events, adequate orders, improved adequate orders
Reference: Esparza, Roemer and Vogler, sections 1-5, pages 1-17
Distributed alphabets, direct product automata, characterization in terms of shuffle closure
Reference: Mukund Sections 1.1-1.3, 1.6
Synchronized product automata
Reference: Mukund Section 1.4
Asynchronous automata. Traces: local views, latest information, time-stamps.
Reference: Mukund Section 1.5-1.7.2 (upto Lemma 1.19)
Traces: updating latest information with primary graphs, secondary information and reusing labels, gossip automaton
Reference: Mukund Section 1.7.2-1.7.4
Zielonka's theorem: distributed simulation, process residues.
Reference: Mukund Section 1.8, 1.8.1
Zielonka's theorem: primary residues, updating residues, complexity.
Reference: Mukund Section 1.8.2-1.8.4
Synthesis: from behaviours to automata. Elementary net systems and theory of regions
Reference: Badouel and Darondeau Sections 1.1-1.4
Failure equivalence
Failures, testing, simulation, bisimulation: basic definitions
Equivalience of failures and testing.
Failures, bisimulation: decidability issues
Silent actions and weak equivalence.
Concurrency preserving bisimulation
The case for hereditary history preserving bisimulation.
Message passing systems
Communicating finite-state machines with reliable unbounded, FIFO channels; message-passing languages; undecidability of all forms of reachability; the bounded channel case and regularity
MSCs and MSGs
References: K. Narayan Kumar, Talk slides and IISc survey, 10.1–10.2.1
MSCs and MSGs
MSGs cannot represent all regular MSC languages: atomic MSC decomposition, alternating bit protocol.
Implied scenarios, undecidability of weak realizability
References: K. Narayan Kumar, IISc survey, 10.4–10.4.1 ; Alur, Etessami and Yannakakis, Sections 1-3.1.
Lossy channel systems
Decidability of reachability, safety
Reference: Abdulla and Jonsson
Well structured transition systems
Basic definitions, set saturation methods, tree saturation methods
Reference: Finkel and Schnoebelen, Sections 1-4.