Software Engineering using Formal
Methods |
TDA293/DIT270, LP1, HT2012 |
Lecture Notes
|
The topics of today's lecture are:
- propositional logic
- linear temporal logic (LTL)
- Büchi automata and relation to LTL
- foundations of model checking
Remark: The slides contain two appendices: the first describes the
construction of the intersection automaton. The second appendix
describes one algorithm to construct a Büchi automaton from a
given LTL formula.
|
|
Home
| Course
| Schedule
| Exam
| Exercises
| Labs
| Eval
| Tools
|
W. Ahrendt
J. Svenningsson
M. Wang
, Sep 20, 2012
|