Course Catalog 2013-2014
Postgraduate

Basic Pori International Postgraduate Open University

|Degrees|     |Study blocks|     |Courses|    

Course Catalog 2013-2014

MAT-74506 Model Checking and Petri Nets, 7 cr

Additional information

The course is given every second year.
Suitable for postgraduate studies
Will not be lectured year 2013-2014

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.  Structural 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 Edition, availability, ... Examination material Language
Lecture slides     Antti Valmari         Yes    English  
Other literature   Scientific papers in the field         Will be delivered to the students.   No    English  

Prerequisites

Course Mandatory/Advisable Description
MAT-02650 Algoritmimatematiikka Mandatory    
MAT-71000 Tieto ja laskenta Advisable    
TIE-02200 Ohjelmoinnin peruskurssi Mandatory    

Prerequisite relations (Requires logging in to POP)

Correspondence of content

There is no equivalence with any other courses

Last modified21.02.2013