Moduł oferowany także w ramach programów studiów:
Informacje ogólne:
Nazwa:
Eksplozja kombinatoryczna w analizie systemów współbieżnych
Tok studiów:
2019/2020
Kod:
ZSDA-3-0075-s
Wydział:
Szkoła Doktorska AGH
Poziom studiów:
Studia III stopnia
Specjalność:
-
Kierunek:
Szkoła Doktorska AGH
Semestr:
0
Profil:
Ogólnoakademicki (A)
Język wykładowy:
Polski i Angielski
Forma studiów:
Stacjonarne
Strona www:
 
Prowadzący moduł:
dr hab. inż. Karatkevich Andrei (karatkevich@agh.edu.pl)
Dyscypliny:
informatyka techniczna i telekomunikacja
Treści programowe zapewniające uzyskanie efektów uczenia się dla modułu zajęć

State explosion problem, its causes, examples, related notions and concepts. Methods of handling the combinatorial expolsion, such as partial state space explosion, system decomposition and abstraction, symbolic model checking. The analysis problems which can be solved without explicite enumeration of the system state space.

Opis efektów uczenia się dla modułu zajęć
Kod MEU Student, który zaliczył moduł zajęć zna i rozumie/potrafi/jest gotów do Powiązania z KEU Sposób weryfikacji i oceny efektów uczenia się osiągniętych przez studenta w ramach poszczególnych form zajęć i dla całego modułu zajęć
Wiedza: zna i rozumie
M_W001 The student knows theoretical aspects of combinatorial explosion problem and the main notions and concepts of this field. SDA3A_W01 Kolokwium
M_W002 He knows the main approaches and methods allowing to analyze the parallel discrete systems limiting the state explosion SDA3A_W01 Aktywność na zajęciach
Umiejętności: potrafi
M_U001 The student is able to analyze formal models of the parallel discrete systems using the advanced state space methods. SDA3A_U01, SDA3A_U02 Aktywność na zajęciach
Kompetencje społeczne: jest gotów do
M_K001 The student is able to analyze critically the known achievements in the field and his on results SDA3A_K01 Aktywność na zajęciach
Liczba godzin zajęć w ramach poszczególnych form zajęć:
SUMA (godz.)
Wykład
Ćwicz. aud
Ćwicz. lab
Ćw. proj.
Konw.
Zaj. sem.
Zaj. prakt
Zaj. terenowe
Zaj. warsztatowe
Prace kontr. przejść.
Lektorat
30 20 0 0 0 0 10 0 0 0 0 0
Matryca kierunkowych efektów uczenia się w odniesieniu do form zajęć i sposobu zaliczenia, które pozwalają na ich uzyskanie
Kod MEU Student, który zaliczył moduł zajęć zna i rozumie/potrafi/jest gotów do Forma zajęć dydaktycznych
Wykład
Ćwicz. aud
Ćwicz. lab
Ćw. proj.
Konw.
Zaj. sem.
Zaj. prakt
Zaj. terenowe
Zaj. warsztatowe
Prace kontr. przejść.
Lektorat
Wiedza
M_W001 The student knows theoretical aspects of combinatorial explosion problem and the main notions and concepts of this field. + - - - - - - - - - -
M_W002 He knows the main approaches and methods allowing to analyze the parallel discrete systems limiting the state explosion + - - - - - - - - - -
Umiejętności
M_U001 The student is able to analyze formal models of the parallel discrete systems using the advanced state space methods. - - - - - + - - - - -
Kompetencje społeczne
M_K001 The student is able to analyze critically the known achievements in the field and his on results - - - - - + - - - - -
Nakład pracy studenta (bilans punktów ECTS)
Forma aktywności studenta Obciążenie studenta
Sumaryczne obciążenie pracą studenta 85 godz
Punkty ECTS za moduł 3 ECTS
Udział w zajęciach dydaktycznych/praktyka 30 godz
Przygotowanie do zajęć 10 godz
przygotowanie projektu, prezentacji, pracy pisemnej, sprawozdania 20 godz
Samodzielne studiowanie tematyki zajęć 20 godz
Dodatkowe godziny kontaktowe 5 godz
Szczegółowe treści kształcenia w ramach poszczególnych form zajęć (szczegółowy program wykładów i pozostałych zajęć)
Wykład (20h):
  1. Main notions and examples of combinatorial explosion

    Rapid growth of complexity of certain cases of problems. Examples using games, quickly growing functions using in combinatorics, the Ackermann function. State space explosion in parallel systems

  2. Parallel discrete systems and the tasks of their analysis

    Liveness and safeness properties, deadlocks, livelocks. Properties expressed by temporal logic. Reachability graphs and interleaving.

  3. Persistent set approach

    Theoretical background: Mazurkiewicz traces, persistent sets. The stubborn set method in its basic form.

  4. More possibilities of the stubborn set method

    Application of the stubborn set method to special cases of parallel systems and applying its modifications for analysis of different properties.

  5. The ignoring problem

    How the persistent set approach may lead to eternal ignoring of possible transitions and how it can be avoided.

  6. Parallel simulation approach

    Janicki and Koutny’s method and other possibilities of concurrent simulation. Combining the persistent set approach and the concurrent simulation.

  7. On-the-fly minimization of the state spaces

    Dynamic reduction of the reachability graphs and its applying to analysis tasks.

  8. Abstraction approach to analysis

    Unfolding and different kinds of decomposition decreasing the state explosion.

  9. Symbolic model checking

    Characteristic functions using BDDs representing the state spaces, analysis methods using such representations instead of explicit enumeration of reachable states.

  10. Bounded model checking

    Model checking using iterative deepening search to limit the numer of explored states.

Zajęcia seminaryjne (10h):

Discussions and experiments on the algorithms and methods presented in the lectures. Student’s presentations on the selected topics.

Pozostałe informacje
Metody i techniki kształcenia:
  • Wykład: Classical lectures with using the multimediate presentations and discussion with the listeners
  • Zajęcia seminaryjne: Nie określono
Warunki i sposób zaliczenia poszczególnych form zajęć, w tym zasady zaliczeń poprawkowych, a także warunki dopuszczenia do egzaminu:

Activity at the seminars or presentation of a selected topic by the student,

Zasady udziału w zajęciach:
  • Wykład:
    – Obecność obowiązkowa: Nie
    – Zasady udziału w zajęciach: Nie określono
  • Zajęcia seminaryjne:
    – Obecność obowiązkowa: Tak
    – Zasady udziału w zajęciach: Activity of the students during the seminars
Sposób obliczania oceny końcowej:

Evaluation of the activity at the seminar classes and/or presentation.

Sposób i tryb wyrównywania zaległości powstałych wskutek nieobecności studenta na zajęciach:

A student who has not attained at two or more seminar classes has to prepare a presentation on a topic defined together with the lecturer

Wymagania wstępne i dodatkowe, z uwzględnieniem sekwencyjności modułów :

Basic knowledge on discrete mathematics, including combinatorics, Boolean algebra and temporal logic

Zalecana literatura i pomoce naukowe:

1. Valmari A., “State of the Art Report: Stubborn Sets”, Petri Net Newsletter, no. 46, April, pp. 6-14, 1994
2. Diekert V, Metivier Y., “Partial Commutation and Traces”, In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, Vol. 3, Beyond Words. Springer-Verlag, Berlin, 1997.
3. Valmari A.: “The State Explosion Problem”, ACPN 1996: Lectures on Petri Nets I: Basic Models pp 429-528, Springer, 1998.
4. Clarke E. M., Grumberg O., Peled D. A., Model Checking. MIT Press, 1999.
5. Flanagan C., Godefroid P., “Dynamic partial-order reduction for model checking software”. Proceedings of POPL ’05, 32nd ACM Symp. on Principles of Programming Languages. pp. 110–121, 2005.
6. Baier C., Katoen J.: Principles of Model Checking, 2008.

Publikacje naukowe osób prowadzących zajęcia związane z tematyką modułu:

1. Karatkevich A., “Memory-saving Analysis of Petri Nets”. In: Design of Embedded Control Systems, Springer, 2005.- pp. 63-72.
2. Karatkevich A., “Dynamic Analysis of Petri Net-Based Discrete Systems”, Lecture Notes in Control and Information Sciences, Vol. 356, Springer, 2007.
3. Karatkevich A., “Analysis of Parallel Discrete Systems: Persistent Sets vs. Concurrent Simulation”, Przegląd Elektrotechniczny R 85 № 7, 2009, pp. 182-184.
4. Karatkevich A., “Analysis of concurrent discrete systems by means of reduced reachability graphs”. In: Preprints of the IFAC Workshop DESDes’09, Gandia Beach, 2009.- pp. 51-56.
5. Karatkevich A., Łabiak G., “Deadlock-preserving reduction of Petri nets”. In: Materiały konferencji naukowej KNWS’14, Karpacz, 2014, pp. 60-61.
6. Karatkevich A., Grobelna I., “Deadlock detection in Petri nets: one trace for one deadlock?” In: Proceedings of the 2014 7th International Conference on Human System Interactions (HSI), Lisbon, 2014, pp. 227-231 (electronic edition)

Informacje dodatkowe:

Brak