Module also offered within study programmes:
General information:
Name:
Combinatorial explosion in analysis of concurrent systems
Course of study:
2019/2020
Code:
ZSDA-3-0075-s
Faculty of:
Szkoła Doktorska AGH
Study level:
Third-cycle studies
Specialty:
-
Field of study:
Szkoła Doktorska AGH
Semester:
0
Profile of education:
Academic (A)
Lecture language:
Polski i Angielski
Form and type of study:
Full-time studies
Course homepage:
 
Responsible teacher:
dr hab. inż. Karatkevich Andrei (karatkevich@agh.edu.pl)
Dyscypliny:
informatyka techniczna i telekomunikacja
Module summary

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.

Description of learning outcomes for module
MLO code Student after module completion has the knowledge/ knows how to/is able to Connections with FLO Method of learning outcomes verification (form of completion)
Social competence: is able to
M_K001 The student is able to analyze critically the known achievements in the field and his on results SDA3A_K01 Activity during classes
Skills: he can
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 Activity during classes
Knowledge: he knows and understands
M_W001 The student knows theoretical aspects of combinatorial explosion problem and the main notions and concepts of this field. SDA3A_W01 Test
M_W002 He knows the main approaches and methods allowing to analyze the parallel discrete systems limiting the state explosion SDA3A_W01 Activity during classes
Number of hours for each form of classes:
Sum (hours)
Lecture
Audit. classes
Lab. classes
Project classes
Conv. seminar
Seminar classes
Pract. classes
Zaj. terenowe
Zaj. warsztatowe
Prace kontr. przejść.
Lektorat
30 20 0 0 0 0 10 0 0 0 0 0
FLO matrix in relation to forms of classes
MLO code Student after module completion has the knowledge/ knows how to/is able to Form of classes
Lecture
Audit. classes
Lab. classes
Project classes
Conv. seminar
Seminar classes
Pract. classes
Zaj. terenowe
Zaj. warsztatowe
Prace kontr. przejść.
Lektorat
Social competence
M_K001 The student is able to analyze critically the known achievements in the field and his on results - - - - - + - - - - -
Skills
M_U001 The student is able to analyze formal models of the parallel discrete systems using the advanced state space methods. - - - - - + - - - - -
Knowledge
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 + - - - - - - - - - -
Student workload (ECTS credits balance)
Student activity form Student workload
Summary student workload 85 h
Module ECTS credits 3 ECTS
Udział w zajęciach dydaktycznych/praktyka 30 h
Preparation for classes 10 h
przygotowanie projektu, prezentacji, pracy pisemnej, sprawozdania 20 h
Realization of independently performed tasks 20 h
Contact hours 5 h
Module content
Lectures (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.

Seminar classes (10h):

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

Additional information
Teaching methods and techniques:
  • Lectures: Classical lectures with using the multimediate presentations and discussion with the listeners
  • Seminar classes: 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,

Participation rules in classes:
  • Lectures:
    – Attendance is mandatory: No
    – Participation rules in classes: Nie określono
  • Seminar classes:
    – Attendance is mandatory: Yes
    – Participation rules in classes: Activity of the students during the seminars
Method of calculating the final grade:

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

Prerequisites and additional requirements:

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

Recommended literature and teaching resources:

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.

Scientific publications of module course instructors related to the topic of the module:

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)

Additional information:

None