Madhavan Mukund

Automata, Concurrency and Timed Systems

January-April, 2010

Reading material

Distributed Automata

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

• Determinizing Asynchronous Automata, (PDF),
  Nils Klarlund, Madhavan Mukund and Milind Sohoni,
  TR TCS-93-5, CMI
  (abridged version appeared in Proc. ICALP 1994)

Regularity and Trace Closure

• The "last" decision problem for rational trace languages (PDF),
  Jacques Sakarovitch,
  Proc LATIN 1992, Springer LNCS 583, (1992) 460-473.

• A Note on the Commutative Closure of Star-Free Languages, (PDF),
  Anca Muscholl and Holger Petersen,
  Information Processing Letters (IPL), 57(2), (1996) 71-74.

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.

• 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 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.

Timed Systems

• A Theory of Timed Automata (PDF),
  Rajeev Alur and David Dill,
  Theoretical Computer Science 126(2) (1994) 183-235.

• Decision problems for timed automata: A survey (PDF),
  Rajeev Alur and P. Madhusudan,
  4th Intl. School on Formal Methods for Computer, Communication, and Software Systems: Real Time (2004).

• Foundations for Timed Systems (PDF),
  Patricia Bouyer,
  Tutorial (2005).

• Clocks, DBMs and States in Timed Systems (PDF),
  Johan Bengtsson,
  PhD Thesis, Uppsala University (2002).

Hybrid Systems

• An Introduction to Hybrid Automata (PDF),
  Jean-Francois Raskin,
  in Dimitros Hristu-Varsakelis, William S. Levine (Eds.), Handbook of Networked and Embedded Control Systems Birkhauser (2005), 491-518.

• What's Decidable about Hybrid Automata? (PDF),
  Thomas A. Henzinger, Peter W. Kopke, Anuj Puri and Pravin Varaiya,
  Journal of Computer and Systems Sciences 57(1), (1998) 94-124.

• Lazy Rectangular Hybrid Automata (PDF),
  Manindra Agrawal and P. S. Thiagarajan,
  Proc HSCC 2004

Regular event structures

• Regular Trace Event Structures (PDF),
  P. S. Thiagarajan,
  BRICS Research Report RS-96-32, Aarhus University (1996).

Material from the lectures

• Lecture 1, 11 January 2010

  • Distributed alphabets, direct and synchronized products of automata
  • Mazukiewicz traces, asynchronous automata, statement of Zielonka's theorem

• Lecture 2, 18 January 2010

  • Regular trace languages
  • Gossip protocol for traces
  • Proof idea for Zielonka's theorem

• Lecture 3, 27 January 2010

  • Proof of Zielonka's Theorem (blackboard)

• Lecture 4, 08 February 2010

  • Subset construction (determinization) for asynchronous automata

• Lecture 5, 15 February 2010

  • Lower bound for determinization of asynchronous automata
  • Undecidability of regularity of trace closure
  • Introduction to Petri nets

• Lecture 6, 22 February 2010

  • Petri nets: basic definitions
  • P/T nets, elementary net systems
  • Markings, firing rule
  • Conflict, concurrency, confusion

• Lecture 7, 01 March 2010

  • Nonsequential behaviours of elementary net systems: traces, branching processes, prime event structures

• Lecture 8, 08 March 2010

  • Place/transition nets: boundedness, coverability, reachability, unfoldings for safe nets

• Lecture 9, 15 March 2010

  • Place/transition nets: finite unfolding prefix for safe nets
  • Timed automta: basic definitions, closure under union and intersection, non-closure under complementation

• Lecture 10, 22 March 2010

  • Timed automata: region constructiona and decidability of emptiness

• Lecture 11, 29 March 2010

  • Time automata: zones and DBMs
  • Hybrid automata: basic definitions, rectangular hybrid automata

• Lecture 12, 05 April 2010

  • Hybrid automata: decidable and undecidable subclasses

• Lecture 13, 12 April 2010

  • Lazy hybrid automata

• Lecture 14, 19 April 2010

  • Regular event structures and Thiagarajan's conjecture