for students of computer studies (2 year, master)

Before the course starts, please read this whole site.

Organisation of the lectures

The goal of this course is to model, simulate and verify communication and transportation systems, using Petri Nets, quening networks, temporal logic and timed automata.

The course is divided into 3 parts:

1. Petri Nets (with another lecturer).
2. Queueing models (with another lecturer).
3. Temporal Logic and Timed Automata*.

* the word „automata” is a plural form of the word „automaton”.

The following applies to the 3rd part of the course only. The 1st and the 2nd parts are taught and organised by prof Jan Magott.

This site contains the following: presentations from the lectures in slides and videos (in English and Polish), example projects used in the prersentations, and grading rules.

Presentations on Petri nets and queing networks

Insormation Systems Analysis (prof. Jan Magott, 2024)

Presentations on temporal logic and timed automata

Here are English (slides, lectures) and Polish (slajdy, wykłady) versions of the presentations. Polskie są chyba lepszej jakości.

The videos are placed in the service mega.nz, which allows to download them or watch them on-line. If the daily download quota is exhaused (which may hardly happen), please wait to the next day.

• lecture 11:
  1. Introduction to temporal logic: slides, slajdy, lecture, wykład
  2. LTL logic: slides, slajdy, lecture, wykład
• lecture 12:
  1. CTL logic: slides, slajdy, lecture, wykład
  2. System model verification: slides, slajdy, lecture, wykład
• lecture 13:
  1. UPPAAL timed automata: slides, slajdy, lecture, wykład
  2. System model verification in UPPAAL: slides, slajdy, lecture, wykład
• lecture 14:
  1. NuSMV timed automata: slides, slajdy, lecture, wykład
  2. System model verification in NuSMV: slides, slajdy, lecture, wykład
• lecture 15:
  1. Other kinds of temporal logic: slides, slajdy, lecture, wykład
  2. Temporal logic and temporal databases: slides, slajdy, lecture, wykład

Example projects used in the presentations

• Petri nets in TAPAAL
• Petri nets in Pipe
• Petri nets in Oris
• UPPAAL automata (recommended program version is 4.1.24 or newer)
• NuSMV automata

Grades

Students, who got less than 4.5 for the laboratories on Petri nets, must take the exam on this subject. Other students may take the exam, or get the grade for the laboratories.

Students, who got less than 4.5 for the laboratories on queing networks, must take the exam on this subject. Other students may take the exam, or get the grade for the laboratories.

Students, who got less than 4.5 for the laboratories on temporal logic and timed automata, must take the exam on this subject. Other students may take the exam, or get the grade for the laboratories.

The final grade is the mean value of final grades from all the 3 parts, or 2.0 if at least one of the parts ends with such a partial grade.