Module Description
| Module: Networks and Processes | |
|---|---|
| Lecturer: Nowotka, 6 Credit Points | |
| Prerequisites | None |
| Course Outline | The first part of this course gives an introduction to the modeling and analysis of parallel and distributed systems with Petri-nets. Basic analysis techniques, like reachability- and coverability graph, place invariants, and traps are considered. The second part introduces the specification of system properties with temporal logics both linear time (with LTL) and branching time (with CTL). Suitable model-checking techniques for both LTL and CTL are given to verify properties on systems. Such techniques form the basics of computer aided verification algorithms. Finally the course ends with the consideration of binary decision diagrams (BDD) as the predominant data structure for representing sets in implementations of the verification procedures described earlier. |
| Learning Outcome | The aim of this course is to enable students to grasp and apply the basics of formally specifying and verifying parallel, distributed systems. The students shall learn how to model and analyse systems with Petri-nets. Moreover, the students are able to express system properties in the temporal logics LTL and CTL, and to model check such properties against a finite system description (Kripke structure). Finally, basic implementation issues are to be understood by an introduction to BDDs and an algorithm to identify strongest connected components in a directed graph. |
| References and Books |
|