• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
  • HSE University
  • Research projects
  • Synthesis, recovery, conformance checking, and other methods for the analysis of process models and distributed information systems

Synthesis, recovery, conformance checking, and other methods for the analysis of process models and distributed information systems

Priority areas of development: IT and mathematics
2019
The project has been carried out as part of the HSE Program of Fundamental Studies.

Goal of research

The aim of the work is to develop and study new methods for the analysis and verification of automata-based models of information systems as well as new approaches to simulation, visualization, synthesis, repair and conformance checking of complex information system models according to examples of their observed behavior registered in event logs.

Methodology

Theory of finite transducers and computation tree logic (CTL) fragments and extensions are used to develop new methods for the analysis and verification of automata-based information system models. Theory of formal languages, Petri nets and their extensions are used to develop new approaches to analyze the observed behavior of distributed information systems.

Empirical base of research

The specific examples of real distributed information systems and event logs containing history of their execution constitute the empirical base within this research project.

Results of research

The following results have been achieved in the area of the analysis and verification of automata-based information system models:

The transducer equivalence problem has been studied. Within this problem, a class of prefix transducers has been identified. It has been proven that there exists an algorithm of checking the equivalence of real-time transducers. This algorithm has the quadratic complexity with respect to the size of automata. It has also been proven that there exists an algorithm of checking the equivalence of transducers with epsilon-transitions. This algorithm has the cubic complexity with respect to the size of automata. In addition, a linear translation of deterministic two-tape automata into prefix transducers has been shown. Thus, there exists an algorithm of checking the equivalence of deterministic two-tape automata. The proposed algorithms are based on the new method for solving systems of linear language equations.

The problem of checking the equivalence of non-deterministic transducers operating over a unary input alphabet has been studied. It has been proven that if projections of transducers on the input alphabet are deterministic automata, then the problem of checking the equivalence of transducers is decidable.

The satisfiability problem for the regular extension of the computation tree logic Reg‑CTL* has been examined within sequential reactive systems. It has been proven that this problem is PSPACE-complete.

The following results have been achieved in the area of simulation, visualization, synthesis, repair and conformance checking of complex information system models according to examples of their observed behavior registered in event logs:

The problem of comparing BPMN (Business Process Model and Notation) process models has been studied. Within this task, the existing heuristic algorithms, including tabu search algorithm, colony optimization algorithm and simulated annealing algorithm, have been adapted. It has been shown that these algorithms allow to find the minimal editing distance between two BPMN-models. Experimental evaluation results show that these algorithms work significantly faster in comparison with the exact algorithms of finding the minimal editing distance.

A new algorithm for simulating Petri nets with reset and inhibitor arcs has been proposed. This algorithm has been implemented within an open-source prototype software that records the observed behavior of a Petri net with reset and inhibitor arcs in a corresponding event log.

Transition firing priorities are one of the techniques to control Petri net behavior to provide their liveness and boundedness. These properties are necessary since most of real information systems are characterized with a limited number of available resources. The existing algorithm for computing transition priorities has been implemented. This algorithm has been tested with models of complex distributed information systems.

Typical asynchronous agent interaction patterns have been identified to model multi-agent systems. These patterns have been modeled using Petri net composition. Semantic properties of a corresponding composition have also been investigated. It has been shown how to apply these asynchronous interaction patterns to discover structured models of multi-agent information systems from their event logs.

A new technique to check conformance between information system models and event logs has been proposed. This technique evaluates not only complete, but also partial correspondence between sequences of observed and model behavior. Within this technique a special conformance checking measure has also been developed. It has been proven that this measure meets the monotonicity property, i.e. the more the level of partial correspondence between observed and model behavior is, the bigger the value of the conformance checking measure is.

Exploitation of information systems often results in changes to the organization of its processes. There has been studied a problem of identifying fragments of BPMN-models that still conform with the observed behavior from event logs. The proposed methods is based on the identification and analysis of dependencies between process events.

There has been made an improvement to the existing method of Petri net decomposition for repairing its fragments with respect to event logs. The proposed improvement is based on constructing decomposition graph, showing the maximal Petri net decomposition, and on the minimal spanning tree including all fragments to be repaired.

There has been studied a problem of constructing a formal model of a real stock trading system according to its description. This is a high-level Petri net model describing behavior stock trading system components regarding the way how stock exchange orders to buy and sell securities are processed. To simulate this model, a prototype software has been implemented which registers system behavior in terms of order book dynamics.

To preprocess raw data extracted form stock trading systems, a specific technique has been proposed. This technique transforms event logs making their automated processing possible in order synthesize formal models of stock trading systems.

To monitor process of managing criminal cases, an original technique has been developed. It allows to identify anomalies which are forbidden by the corresponding regulations. This method is based on event log analysis. There has been constructed a formal model of criminal case management process considering requirements imposed by the regulations. It has been shown how to identify anomalies caused by time non-compliance and looping with the help of event logs.

A new method for storing event logs in autonomous relational databases has been proposed. It is based on using SQLite RDBMS software. These event logs are called SQLite-EventLogs. This method is implemented as a component library in LDOPA and evaluated on the set of artificial and real event logs. Experiment results in comparing methods for storing event logs have shown that SQLite-EventLogs are more efficient than a conventional approach to store event logs.

The B-tree data structure has been examined, and there has been proposed a modification called B*+-trees. They are used to index tables in relational databases. There has been developed an extension to SQLite software which implements indexing with the help of B*+-trees. The main advantage to B*+-trees is the optimization of processing event logs represented by SQLite-EventLog.

There has been proposed a new method for the automated synthesis of UML activity diagrams from event logs. This methods is based on the parameterized synthesis scheme including three sequential stages of model transformation – from an event log to a UML activity diagram.

Level of implementation, recommendations on implementation or outcomes of the implementation of the results

The proposed theoretical methods of the analysis and verification of automata-based information system models are mainly focused on their practical implementation. The proposed methods of simulation, visualization, synthesis, repair and conformance checking of process models have been evaluated using event logs of real information systems.

Additional results

In 2019 the PhD thesis of the PAIS Lab researcher A.A. Mitsyuk “Structure-Preserving Process Model Repair Based on Event Logs” has been successfully defended at the National Research University Higher School of Economics, Dissertation Council in Computer Science (scientific advisor: the head of PAIS Lab I.A. Lomazova).

The paper “Monotone Conformance Checking for Partially Matching Designed and Observed Processes” by the leading PAIS Lab researcher A.A. Kalenkova and A.A. Polyvyanyy (University of Melbourne, Australia) has been awarded a best paper award at the international conference “International Conference on Process Mining (ICPM 2019)” which took place on June 24-26, 2019 in Aachen (Germany).

The paper “A Method to Improve Workflow Net Decomposition for Process Model Repair” by the PAIS Lab researcher A.A. Mitsyuk and the research assistant S.E. Tikhonov has been awarded a best paper award at the international conference “Analysis of Images, Social Networks and Texts (AIST 2019)” which took place on July 17-19, 2019 in Kazan (Russia).

Publications:


Zakharov V., Abbas M. M. Even Simple Processes of Pi-calculus are Hard for Analysis / Пер. с рус. // Automatic Control and Computer Sciences, USA. 2019. Vol. 53. No. 7. P. 589-606. doi
Alexandra Kolosova, Irina Lomazova. Detection of Anomalies in the Criminal Proceedings Based on the Analysis of Event Logs, in: Analysis of Images, Social Networks and Texts. 8th International Conference, AIST 2019, Lecture Notes in Computer Science, Revised Selected Papers / Ed. by W. M. van der Aalst, V. Batagelj, D. I. Ignatov, M. Y. Khachay, V. Kuskova, A. Kutuzov, S. Kuznetsov, I. A. Lomazova, N. Loukachevitch, A. Napoli, P. M. Pardalos, M. Pelillo, A. Savchenko, E. Tutubalina. Vol. 11832. Cham : Springer, 2019. doi P. 401-410. doi
Semyon E. Tikhonov, Mitsyuk A. A. A Method to Improve Workflow Net Decomposition for Process Model Repair, in: Analysis of Images, Social Networks and Texts. 8th International Conference AIST 2019. Springer, 2019. Ch. 37. P. 411-423. doi
Skobtsov A., Kalenkova A. A. Using Heuristic Algorithms for Fast Alignment between Business Processes and Goals, in: 2019 IEEE 23rd International Enterprise Distributed Object Computing Workshop (EDOCW). IEEE, 2019. P. 85-91. doi
Zakharov V., Gnatenko A. R. On the Expressive Power of Some Extensions of Linear Temporal Logic / Пер. с рус. // Automatic Control and Computer Sciences. 2019. Vol. 53. No. 7. P. 506-524. doi
Гнатенко А. Р., Захаров В. А. Верификация моделей реагирующих систем относительно одного расширения темпоральной логики CTL* // В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019. С. 263-266.
Захаров В. А., Жайлауова Ш. Р. О проблеме эквивалентности недетерминированных автоматов-преобразователей над однобуквенным выходным алфавитом // В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019. С. 272-274.
Захаров В. А., Винарский Е. М. О задаче верификации для одного класса автоматов реального времени // В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019. С. 257-260.
Материалы XIII Международного семинара «Дискретнаяматематика и ее приложения», имени академика О.Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2019.
Roman A. Nesterov, Irina A. Lomazova. Asynchronous Interaction Patterns for Mining Multi-Agent System Models from Event Logs, in: Proceedings of the MACSPro Workshop 2019 / Ed. by Irina Lomazova, Anna Kalenkova, Р. Яворский. Vol. 2478: CEUR Workshop Proceedings. CEUR-WS.org, 2019. P. 62-73.
N. S. Zubkova, S. A. Shershakov. Method for Building UML Activity Diagrams from Event Logs // Proceedings of the Institute for System Programming of the RAS. 2019. Vol. 31. No. 4. P. 139-150. doi
Carrasquel Gamez J. C., Lomazova I. A., Itkin I. L. Towards a Formal Modelling of Order-driven Trading Systems using Petri Nets: A Multi-Agent Approach, in: Proceedings of the MACSPro Workshop 2019 / Ed. by Irina Lomazova, Anna Kalenkova, Р. Яворский. Vol. 2478: CEUR Workshop Proceedings. CEUR-WS.org, 2019. P. 92-103.
Julio C. Carrasquel, Lomazova I. A. Modelling and Validation of Trading and Multi-Agent Systems: An Approach Based on Process Mining and Petri Nets, in: ICPM Doctoral Consortium 2019. Vol. 2432: CEUR Workshop Proceedings. CEUR-WS.org, 2019. Ch. 4. P. 1-12.
Kirill Artamonov, Irina Lomazova. What Has Remained Unchanged in Your Business Process Model?, in: 21st IEEE Conference on Business Informatics (CBI). IEEE Computer Society, 2019. P. 551-558. doi
Pavel Pertsukhov, Mitsyuk A. A. Simulating Petri Nets with Inhibitor and Reset Arcs // Proceedings of the Institute for System Programming of the RAS. 2019. Vol. 31. No. 4. P. 151-162. doi
K.G. Serebrennikov. Computing Transition Priorities for Live Petri Nets // Proceedings of the Institute for System Programming of the RAS. 2019. Vol. 31. No. 4. P. 163-174. doi
Sergey A. Shershakov. Multi-Perspective Process Mining with Embedding Configurations into DB-based Event Logs, in: Proceedings of the International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA-2019). Springer, 2019.
Каленкова А. А., Колесников Д. А. Применение генетического алгоритма для нахождения редакционного расстояния между моделями процессов // Моделирование и анализ информационных систем. 2018. Т. 25. № 6. С. 711-725. doi
Kalenkova A. A., Burattin A., de Leoni M., van der Aalst W., Sperduti A. Discovering high-level BPMN process models from event data // Business Process Management Journal. 2019. Vol. 25. No. 5. P. 995-1019. doi
Skobtsov A., Kalenkova A. A. Efficient Comparison of Process Models using Tabu Search Algorithm, in: Proceedings of the MACSPro Workshop 2019 / Ed. by Irina Lomazova, Anna Kalenkova, Р. Яворский. Vol. 2478: CEUR Workshop Proceedings. CEUR-WS.org, 2019.
Polyvyanyy A., Kalenkova A. A. Monotone Conformance Checking for Partially Matching Designed and Observed Processes, in: 2019 International Conference on Process Mining (ICPM). IEEE, 2019. P. 81-88.
A.M. Rigin, S.A. Shershakov. SQLite RDBMS Extension for Data Indexing Using B-tree Modifications // Proceedings of the Institute for System Programming of the RAS. 2019. Vol. 31. No. 3. P. 203-216. doi