FORMAL
METHODS (921 U7600)
Fall 2008
每週二14：30
- 17：20
博理館114教室
Announcement
Class
Notes (under revision constantly)
Term Projects:
Examinations
Papers to
read and
present on 2007/5/29, 2007/6/5, and 2007/6/12.
Additional
course materials from the
webs:
- Introduction: (1),
(2),
(intro.alur-henzinger)
- Automata Theory: (brief
introduction) (2nd order
theory of one successor)
- Temporal Logics:
- Linear time 1
- Branching time 1,
2
- Model Checking: --
a tutorial,
(1),
(2),
(3),
(CTL model
checking), (fixed point),
(Symbolic
CTL model checking ) ( Survey on
mu-calculus)
- Binary
Decision Diagrams (BDD) ( Survey on
BDD)
- Timed
automata, Symbolic
approach, Undecidability
of multi-rate timed automata ---- (Surveys on Timed
automata, Hybrid
automata)
- State space
explosion: Intro.,
Bisimulation,
Partial
order reduction
- Some infinite
state systems: Petri nets ( 1,
2);
communicating
finite state machines
- Compositional
Verification
- Probabilistic
model checking
- Supervisory
Control
-