• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
For visually-impairedUser profile (HSE staff only)SearchMenu

New methods for solving problems of process mining and process analysis and their application to the design of information systems

Priority areas of development: IT and mathematics
2020

Goal of research

Development of new methods for equivalence checking and verification of finite automata and their extensions; development of new approaches to model behavior of information systems, to visualize process models and to check conformance with observed behavior registered in event logs of information systems.

Methodology

To develop new methods for equivalence checking and verification of finite automata models, formal grammars, theory of finite transducers and computation tree logic have bee used. To develop new methods for modeling processes and for conformance checking, formal languages, theory of Petri nets and their extensions have been used.

Empirical base of research

The empirical base includes specific examples of distributed systems and their event logs containing data on all executed activities.

Results of research

In the context of verification and equivalence checking of finite automata models of information systems the following results have been achieved:

We have proposed a new method for efficient equivalence checking of some classes of finite automata exhibiting deterministic behavior. These classes are finite transducers, two-tape automata, biautomata and push-down automata. The proposed method allows to reduce the equivalence checking to checking the solvability of the system of equations over a semi-ring of languages or binary relations. Based on this method, we have constructed an algorithm to check the equivalence of deterministic push-down automata with a single state.

We have developed an algorithm to verify finite transducers in the context the extended computation tree logic Reg-CTL*, where temporal operators are parameterized with languages over output alphabets in finite transducers. The proposed parameterization extends the expressiveness of temporal logics but preserves the decidability of formula satisfaction problems over finite models. It has also been shown that the complexity of the Reg-CTL* satisfaction problem is EXPSPACE.

We have proposed an extension to the semantics of finite transducers to model behavior of sequential reactive systems operating in real time. The extended semantics is based on using labeled transition systems, thus making possible to apply the existing verification methods for analyzing behavior of real-time reactive systems.

In the context of modeling, visualizing and checking conformance of information system behavior using data from event logs the following results have been obtained:

We have developed a system of local structural transformations for elementary net systems. It has been shown that these transformations induce morphisms over transformed models, thus proving the correctness of transformation applications. We have considered the application of the proposed structural transformation to the construction of the system with correctly interacting workflow net components.

We have proposed a new method for visualizing high-level Petri net models that takes into account their internal hierarchical structure and behavioral dynamics from event logs records. The proposed method is based on enriching the static model image of a high-level Petri net with additional information on real activity timestamps.

We have reported the development of the VTMine for Visio software that provides support for graphical modeling and automating experiments being conducted to check methods for processing information on the observed behavior from event logs of information systems.

We have proposed two new conformance checking methods that can be applied to the following Petri net extensions: colored and nested Petri nets. Information about the observed behavior is represented in event logs of multi-agent systems. Using the proposed conformance checking methods, it is possible to detect different behavioral deviation including correctness in the management of shared data sources. The proposed methods have been tested on the event logs produced by the specific stock trading system. We have also analyzed capabilities and limitations of using existing Petri net extensions to model behavior of stock trading systems. Based on that, we have proposed a scheme of a Petri net extension that allows to capture all behavioral aspects of information systems with several interacting components that operate with shared databases.

We have reported the development of the software for modeling and simulating behavior of the Petri net extension used for modeling operations with persistent data. Simulator has been development as a plugin for the existing application, whereas the implementation of persistent data management is based on using the embedded SQLite database.

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

The proposed theoretical methods for analyzing and verifying finite automata models of programs and information systems are driven to their practical implementations. The proposed methods for modeling, visualizing and conformance checking have been checked and assessed using event logs of real information systems.

Publications:


Mecheraoui K., Carrasquel G. J. C., Lomazova I. A. Compositional conformance checking of nested petri nets and event logs of multi-agent systems, in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020).: CEUR Workshop Proceedings, 2020. С. 34-45. 
Mecheraoui K., Carrasquel G. J. C., Lomazova I. A. Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems / Cornell University. Series Computer Science "arxiv.org". 2020. 
Gnatenko A., Zakharov V. Using an extension of CTL* for specification and verification of sequential reactive systems // Системная информатика. 2020. Vol. 17. P. 21-32. 
Захаров В. А. Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов // Моделирование и анализ информационных систем. 2020. Т. 27. № 3. C. 260-303. doi
Шершаков С. А. “VTMine for Visio”: инструмент графического моделирования в области Process Mining // Моделирование и анализ информационных систем. 2020. Т. 27. № 2. C. 194-217. doi
Carrasquel G. J. C., Lomazova I. A., Rivkin A. Modeling Trading Systems using Petri Net Extensions, in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020).: CEUR-WS.org, 2020. С. 118-137. 
Yaroslav V. K., Mitsyuk A. A. Software System Behavior Can Be Analyzed with Visual Analytics, in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020).: CEUR Workshop Proceedings, 2020. С. 46-56. 
Bernardinello L., Lomazova I. A., Nesterov R., Pomello L. Property-Preserving Transformations of Elementary Net Systems Based on Morphisms, in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020).: CEUR-WS.org, 2020. С. 49-67. 
Rigin A., Sergey S. Data and Reference Semantic-Based Simulator of DB-nets with the Use of Renew Tool, in: Analysis of Images, Social Networks and Texts. 9th International Conference, AIST 2020, Skolkovo, Moscow, Russia, October 15–16, 2020, Revised Selected Papers (LNCS 12602).: Springer Publishing Company, 2021. С. 453-465.