Mathematical Methods in Computer Science (DAT7, Autumn'07)

• Kim G. Larsen
• Jiri Srba

• Anders Franz Terkelsen
• Claus Thrane
• Jesper B. Rosenkilde
• Mads Chr. Olesen
• Simon Kongshoj
• Uffe Soerensen

Axiomatizations of bisimilarity

Models of Concurrency

Session on Friday, 21.9 at 12:30; meeting point in front of Jiri's office

• Compulsary Reading
  • Grammars as Processes by J. Esparza. Section 1, 2, 3, 4 and 5.
  • Infinite Results by F. Moller. Sections 1 and 2.
• Recommended Reading
  • On the Computational Complexity of Bisimulation, Redux by F. Moller, S. Smolka and J. Srba.
  • Roadmap of Infinite Results by J. Srba.
• Papers for Presentation (in the first week of October)
  • Speaker: Jesper; An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis by J. Esparza and J. Knoop.
  • Speaker: Simon; Visibly Pushdown Languages by R. Alur and P. Madhusudan.
  • Speaker: Mads; Visibly Pushdown Epxression Effects for XML Stream Processing by C. Pitcher.
  • Speaker: Joakim; jMoped - A Test Environment for Java Programs. Tool presentation based on the papers from TACAS'05 and CAV'07.
  • Speaker: Anders; SAT-Based Verification of Safe Petri Nets by S. Ogata, T. Tsuchiya and T. Kikuno.
  • Speaker: Uffe; On Non-Decidability of Reachability for Timed-Arc Petri Nets by V.V. Ruiz, D. de F. Escrig and F.C. Gomez.
  • Speaker: Claus; The Regular Viewpoint on PA-Processes by D. Lugiez and Ph. Schnoebelen.
  
  
• Home-assignment: Assignment 1 (containing exercises for both the current and the following session)

Session of Thursday, 27.9 from 9:00 to 12:00, meeting point at Jiri's office

• Compulsary Reading
  • Model-Checking Pushdown Systems by S. Schwoon. Chapter 3, pages 32-41.
  • Undecidability of Bisimilarity for Petri Nets and Some Related Problems by P. Jancar. Section 1,2 and 3.
• Recommended Reading
  • Reachability Analysis of Pushdown Automata: Application to Model-Checking by A. Bouajjani, J. Esparza and O. Maler.

Session on Thursday, 4.10 from 12:30 to 15:30, meeting point at Jiri's office

• Compulsary reading:
  • Well-Structured Transition Systems Everywhere! by A. Finkel and Ph. Schnoebelen. Parts I and II.
  
  
• Home-assignment 2: Prove Dickson's Lemma: Every infinite sequence of vectors of natural numbers (of dimention k) has an infinite nondecreasing subsequence w.r.t. component-wise ordering.
  
  Hint: use mathematical induction on k.

Session on Wednesday, 10.10 from 12:30 to 15:30, meeting point at Jiri's office

Session on Thursday, 11.10 from 12:30 to 15:30, meeting point at Jiri's office

Computability Theory

Session on Thursday, 15.10 from 8:55 (sharp) to 12:00, meeting point at Jiri's office

Session on Thursday, 15.10 from 14:00 to 16:00, meeting point at Kim's office

• A Theory of Timed Automata by R. Alur and D. Dill (emphasis on Section 5).
• Are Timed Automata Updatable? by Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury and Antoine Petit.

Tuesday 20.11 from 8:30 to 11:30 (at Jiri's Office). Presentations by

• Claus: Undecidable Problems in Context-Free Grammars from the book Languages and Machines by Thomas A. Sudkamp.
• Jesper: The convenience of Tilings by Peter van Emde Boas (focus on the master reduction and undecidability results).
• Uffe: Folk Theorems on the Determinization and Minimization of Timed Automata by S. Tripakis.

Deadline for Assignments 2 and 3 is this Friday (30/11)! Deadline for Assignment 4 is by the middle of the next week.

Complexity Theory

Wednesday 5.12 from 13:30 to 16:00 (meeting at Jiri's Office)

• Ovierview of time/space complexity classes, completeness and logspace reductions. Alternation, AP=PSPACE, APSPACE=EXPTIME, AEXPTIME=EXPSPACE, polynomial hierarchy.
• Reading about alternation and polynomial hierarchy: Sipser's book, Section 10.3.

Friday 7.12 from 12:30 to 15:00 (meeting at Kim's Office)

• Hardness results from timed automata theory.
• Reading:
  • A Theory of Timed Automata by R. Alur and D. Dill (Sections 4.5 and 6).
  • Is Your Model Checker on Time? by L. Aceto and F. Laroussinie.

Wednesday 12.12 from 12:30 to 16:00 (meeting at Jiri's office)

• Presentations by Anders, Mads and Simon.
• Mads: QBF, Formula-Game, Generalized Geography from Sipser Section 8.3.
• Anders: PSPACE-hardness of strong bisimilarity on BPP by J. Srba.
• Simon: Strong NP-Completeness and Pseudo-Polynomial Algorithms from Ch. Papadimitriou (hand-out).
• Assignment 5

Exam Questions

• Axiomatization of strong bisimilarity on a fragment of CCS.
  Reading material: Complete Axiomatization of Strong and Observational Congruence for Finite Agent by Robin Milner. Pages 1-1 to 4-1.
  
  
• Process Rewrite System hierarchy.
  Definition of the classes (FS, BPA, BPP, PN, PA, PDA, ...), strictness of the hierarchy, relationship to control-flow analysis.
  Reading material: Grammars as Processes by J. Esparza.
  
  
• Decidability of forward and backward reachability in pushdown automata.
  Pre* and Post* construction, complexity analysis, applications.
  Reading material: Model-Checking Pushdown Systems by S. Schwoon. Chapter 3, pages 32-41. (Regarding the complexity analysis, you should be able to argue that the algorithms run in polynomial time.)
  
  
• Minsky machine and undecidability of bisimilarity for Petri nets.
  Definition of Minsky machine, reduction of the halting problem to strong bisimilarity on PN.
  Reading material: Undecidability of Bisimilarity for Petri Nets and Some Related Problems by P. Jancar. Section 1,2 and 3.
  
  
• Undecidability of universality and inclusion for timed automata.
  Definitions of the problems, proof.
  Reading material: A Theory of Timed Automata by R. Alur and D. Dill (Section 5).
  
  
• Alternating Turing machines and alternating complexity classes.
  Alternation, AP, APSPACE, AEXPTIME, relationship to standard complexity classes, proof ideas.
  Reading material: Sipser Section 10.3.