for students of computer studies (2 year, master).
kod kursu: INEA12103W

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.

The course in the winter semester 2021/2022 takes place remotely (not in the campus). Lectures on Temporal Logic and Timed Automata are on-line video presentations, prerecorded to be watched when needed. They show slides with voice comments and explain automata construction and analysis on the tools used in the laboratories.

If You have any questions to the lectures, you may consult the teacher in the time of the lecture by e-mails (at pawel.gluchowski(at)pwr.edu.pl) or by Skype (at dr.inz.pawel.gluchowski@gmail.com).

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

Petri nets and queing networks

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 6:
  1. Introduction to temporal logic: slides, slajdy, lecture, wykład
  2. LTL logic: slides, slajdy, lecture, wykład
  3. CTL logic: slides, slajdy, lecture, wykład
• lecture 7:
  1. System model verification: slides, slajdy, lecture, wykład
  2. UPPAAL timed automata: slides, slajdy, lecture, wykład
  3. System model verification in UPPAAL: slides, slajdy, lecture, wykład
• lecture 8:
  1. NuSMV timed automata: slides, slajdy, lecture, wykład
  2. System model verification in NuSMV: slides, slajdy, lecture, wykład
• extras:
  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.