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 https://www.cs.tut.fi/~ava/modelPetri.html
Suitable for postgraduate studies.
The implementation will not be executed during the academic year 2017-2018.
Person responsible
Antti Valmari
Lessons
| Implementation | Period | Person responsible | Requirements |
| MAT-74506 2017-01 | - |
Antti Valmari |
If the number of students is small, the course is passed by solving many enough weekly exercise problems. Otherwise there will be an examination. |
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