MAT-74506 Model Checking and Petri Nets, 7 cr
Additional information
The course is given every second year. The local homepage of the course is http://www.cs.tut.fi/~ava/modelPetri.html
Suitable for postgraduate studies
Will not be lectured year 2015-2016
Person responsible
Antti Valmari
-->Requirements
If the number of students is small, the course is passed by solving many enough weekly exercise problems. Otherwise there will be an examination.
Completion parts must belong to the same implementation
Learning Outcomes
The student can read scientific literature on model checking and on Petri nets. (S)he can model concurrent systems and knows the basic correctness properties and verification methods.
Content
| Content | Core content | Complementary knowledge | Specialist knowledge |
| 1. | Petri nets. Reachability graph. Coloured Petri nets and their unfolding. | ||
| 2. | Boundedness. Invariants. Coverability set. | Symmetry method. | Structure theory of Petri nets. |
| 3. | State-based concurrent systems and their state spaces. Deadlock, livelock and reachability. | ||
| 4. | Linear temporal logic. Model checking with Büchi automata. Computation tree logic and its main verification algorithm. | Computational complexity of model checking. | |
| 5. | Binary decision diagrams. | Bounded model checking. |
Study material
| Type | Name | Author | ISBN | URL | Additional information | Examination material |
| Lecture slides | Antti Valmari | Yes | ||||
| Other literature | Scientific papers in the field | Will be delivered to the students. | No |
Prerequisites
| Course | Mandatory/Advisable | Description |
| MAT-02650 Algoritmimatematiikka | Mandatory | |
| MAT-71000 Tieto ja laskenta | Advisable | |
| TIE-02200 Ohjelmoinnin peruskurssi | Mandatory |
Correspondence of content
There is no equivalence with any other courses