MAT-74506 Model Checking and Petri Nets, 7 cr
Lisätiedot
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.
Vastuuhenkilö
Antti Valmari
Opetus
| Toteutuskerta | Periodi | Vastuuhenkilö | Suoritusvaatimukset |
| MAT-74506 2016-01 | 1 - 2 |
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. |
Osaamistavoitteet
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.
Sisältö
| Sisältö | Ydinsisältö | Täydentävä tietämys | Erityistietämys |
| 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. |
Oppimateriaali
| Tyyppi | Nimi | Tekijä | ISBN | URL | Lisätiedot | Tenttimateriaali |
| Lecture slides | Antti Valmari | Yes | ||||
| Other literature | Scientific papers in the field | Will be delivered to the students. | No |
Esitietovaatimukset
| Opintojakso | P/S | Selite |
| MAT-02650 Algoritmimatematiikka | Mandatory | |
| MAT-71000 Tieto ja laskenta | Advisable | |
| TIE-02200 Ohjelmoinnin peruskurssi | Mandatory |
Vastaavuudet
Opintojakso ei vastaan mitään toista opintojaksoa