Mathematical Methods in Computer Science (DAT7, Autumn'07)
Lecturers:
Participants:
Axiomatizations of bisimilarity
Assignment 0 - Weighted LTS
Models of Concurrency
Session on Friday, 21.9 at 12:30; meeting point in front of Jiri's office
Introduction to process rewrite systems.
Before the meeting, read quickly the following short text:
A Note on Game
Characterization of Strong and Weak Bisimilarity by J. Srba.
- Compulsary Reading
- Recommended Reading
- Papers for Presentation (in the first week of October)
- 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
Reachability in pushdown automata; bisimilarity on Petri nets.
- Compulsary Reading
- Recommended Reading
Session on Thursday, 4.10 from 12:30 to 15:30,
meeting point at Jiri's office
Tool jMoped: presentation by Joakim;
well-structured transition systems and decidability of coverability; examples
on Petri nets.
- Compulsary reading:
- 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
Presentations by Jesper, Simon and Mads.
Session on Thursday, 11.10 from 12:30 to 15:30,
meeting point at Jiri's office
Presentations by Anders, Uffe and Claus.
Computability Theory
Session on Thursday, 15.10 from 8:55 (sharp) to 12:00,
meeting point at Jiri's office
Decidability and Undecidability of First Order Logics on
Natural Numbers; Godel's First Incompleteness Theorem; speaker Jiri
Reading: Section 6.2 and 6.3 from Sipser.
Home-assignment:
Assignment 3
Session on Thursday, 15.10 from 14:00 to 16:00,
meeting point at Kim's office
Undecidable problems from Timed Automata; speaker Kim
Home-assignment:
Assignment 4
Reading:
Tuesday 20.11 from 8:30 to 11:30 (at Jiri's Office). Presentations by
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:
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.