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

Päivittäjä: Ikonen Suvi-Päivikki, 13.04.2016