Teaching assistants: Debraj Chakraborty, Suman Sadhukhan
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
Reference: Rozenberg-Engelfriet, Sections 1-3
Symmetric and asymmetric 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, place and transition invariants, arc weights, place capacities, inhibitor arcs
Reference: Desel-Reisig, Section 4 (4.6-4.8), 5 (5.1-5.3), Section 7
Petri nets: undecidability of reachability for inhibitor arcs
Checking the opposite of coverability is hard
Petri net languages
Unlabelled Petri net languages and unsolvable words
Introduction to Mazurkiewicz traces
Mazurkiewicz traces: partial order representation, trace inclusion
Building a "canonical" partial order representation of [w] for a firing sequence w
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
Occurrence nets and event structures, prime configurations, algebraic characterization of prime event structures
References: Nielsen, Rozenberg, Thiagarajan (Section 4), 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, pages 1-17
Synthesis: from behaviours to automata. Elementary net systems and theory of regions
Reference: Badouel and Darondeau Sections 1.1-1.4
Distributed alphabets, direct product automata, characterization in terms of shuffle closure
Reference: Mukund Sections 1.1-1.3, 1.6
Synchronized product automata, introduction to asynchronous automata
Reference: Mukund Section 1.4-1.5
Asynchronous automata. Traces: local views, latest information, time-stamps.
Reference: Mukund Section 1.5-1.7.1
Traces: updating latest information with primary graphs, secondary information and reusing labels.
Reference: Mukund Section 1.7.2-1.7.3
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
Failures, testing, simulation, bisimulation: basic definitions
Reference:
Failures, testing, simulation, bisimulation
Equivalience of failures and testing, decidability issues.
Reference:
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
Reference:
MSCs and MSGs
MSGs cannot represent all regular MSC languages: atomic MSC decomposition, alternating bit protocol.
Implied scenarios, undecidability of weak realizability
References: Narayan Kumar, Proposition 10.15; 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.