• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Modeling of information systems and analysis of their behavior on the basis of the event history

Priority areas of development: IT and mathematics
2018
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 expand and investigate the methods for system verification, as well as to develop new approaches for simulation, visualization, repair and synthesis of process models from information systems’ event logs.

Methodology

The theory of finite state machines-converters and temporal logic were used to expand and analyze the methods for system verification. The theory of finite automata and formal languages, Petri nets, and machine learning methods were used to create new methods for the analysis and synthesis of process models.

Empirical base of research

Both information systems and their event logs serve as an empirical base.

Results of research

The following results were obtained in the field of verification of information system models and information security properties:

A language of LP-CTL* specifications was developed. The formulas of this language can describe the properties of finite automata-converters over semigroups.

An algorithm for the verification of reactive systems modeled by automata-transducers against the LP-CTL* specifications for was proposed. The correctness and completeness of this algorithm were proven.

Two fragments of the LP-CTL* language allowing to set specifications of the Kripke model were investigated. Algorithms for verification of Kripke models with respect to these specifications were constructed.

The complexity of the problem of verification of automata-converters over commutative semigroups was estimated.

The existence of a polynomial algorithm for checking the equivalence of deterministic 2-tape automata was proven.

co-NP-completeness of the problem of verification of information security properties of non-recursive cryptographic protocols models was investigated.

The following results were obtained in the field of simulation, visualization, synthesis and repair of process models using the information systems’ event logs:

Patterns for the compositional synthesis of correct formal models of multi-agent systems in the form of Petri nets were proposed. On the basis of these patterns, a composite approach for the construction of correct and complete models of distributed systems based on the models of the individual components behavior was developed.

A general modular approach for the synthesis of process models for multi-agent systems based on event logs was proposed. System event logs are filtered against the behavior of specific agents. Further, networks of workflows for each specific agent are synthesized using existing algorithms of automatic discovery. Only asynchronous interactions between two agents are considered. The organization of asynchronous interaction of agents with the help of channel-composition of two networks of workflows was investigated.

A novel approach for the synthesis of transition systems from event logs using recurrent neural networks was developed. It was implemented and tested on real-life event logs generated by information systems. A parametric synthesis method is developed to vary the degree of accuracy and complexity of the model in the form of a finite state machine, assuming the precision metric as the target. The developed method was tested on a set of artificial and real-life event logs.

A novel approach for the synthesis of compact regular expressions from finite automata based on the event logs of information systems was developed. The algorithm was applied to real-life information systems’ event logs. The size (length) of obtained regular expressions was estimated, both using the proposed heuristics and without it. It was shown that the proposed algorithm can significantly reduce the size of the resulting regular expressions.

A greedy algorithm for correcting process models based on event logs was created. This algorithm can be used to correct non-local inconsistencies between the process model and the event log.

An algorithm for simulation of process models for multi-agent systems in accordance with declarative interface constraints was developed. This approach is proposed to be used in assessing the quality of algorithms for extracting process models from event logs in terms of the structural characteristics of the obtained models.

A novel approach for the visualization of complex hierarchical and multidimensional software models was created. The software implementing this approach for visualization of hierarchical and multi-agent software systems using nested Petri nets was developed.

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

The proposed theoretical methods are focused primarily on the possibility of their practical application. The developed methods of synthesis and repair of process models were tested on real-life event logs of information systems.

Additional results

In 2018, under the supervision of the head of the PAIS Lab Lomazova I.A., 2 PhD theses related to the scope of research of the PAIS Lab were defended:

- On June 5, 2018 senior researcher at the PAIS Lab  Kalenkova A.A. defended the thesis "Learning high-level models from event data" at the Technical University of Eindhoven (Netherlands);

- On October 10, 2018, researcher at the PAIS Lab Dworzanski L.W. defended the thesis "Nested Petri Nets: behaviour analysis and time semantics” at the Humboldt University of Berlin (Germany).

In 2018, the research work of Davydova K.V. "Method for constructing hybrid UML models from event logs of systems with service-oriented architecture", performed under the supervision of PAIS Lab researcher Shershakov S.A., won the third place at the competition of the NIRS in the category "Best research work in computer science for master students and graduates of 2017".

Publications:


Roman A. Nesterov, Irina A. Lomazova. Compositional Process Model Synthesis based on Interface Patterns, in: Tools and Methods of Program Analysis: 4th International Conference, TMPA 2017, Moscow, Russia, March 3-4, 2017, Revised Selected Papers Vol. 779: Communications in Computer and Information Science. Cham: Springer, 2018. doi P. 151-162. doi
Гнатенко А. Р., Захаров В. А. О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. 2018. Т. 25. № 5. С. 506-524. doi
Bernardinello L., Irina Lomazova, Roman Nesterov, Pomello L. Compositional Discovery of Workflow Nets from Event Logs Using Morphisms, in: Proceedings of the International Workshop on Algorithms & Theories for the Analysis of Event Data 2018 Vol. 2115: CEUR Workshop Proceedings. CEUR-WS.org, 2018. P. 23-38.
Nesterov R.A., Mitsyuk A.A., Lomazova I.A. Simulating Behavior of Multi-Agent Systems with Acyclic Interactions of Agents // Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 285-302. doi
Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018.
Захаров В. А., Гнатенко А. Р. Языки спецификаций моделей Крипке на основе темпоральных логик и их выразительные возможности С. 131-133.
Kalenkova A. A., Агеев А. А., Lomazova I. A., van der Aalst W. E-Government Services: Comparing Real and Expected User Behavior, in: BPM 2017 International Workshops, Barcelona, Spain, September 10-11, 2017, Revised Papers Vol. 308. Springer, 2018. P. 484-496. doi
Mitsyuk A. A., Котылев Я. В. Layered Layouts for Software Systems Visualization Using Nested Petri Nets, in: Tools and Methods of Program Analysis: 4th International Conference, TMPA 2017, Moscow, Russia, March 3-4, 2017, Revised Selected Papers Vol. 779: Communications in Computer and Information Science. Cham: Springer, 2018. doi Ch. 11. P. 127-138. doi
Mitsyuk A. A. Non-Local Correction of Process Models Using Event Logs, in: Proceedings of the 2017 Ivannikov ISPRAS Open Conference. Los Alamitos : IEEE Computer Society, 2017. Ch. 2. P. 6-11. doi
Захаров В. А., Аббас М. М. Даже простые процессы pi-исчисления трудны для анализа // Моделирование и анализ информационных систем. 2018. Т. 25. № 6. С. 589-606. doi
Tarantsova P. D., Kalenkova A. A. Constructing Regular Expressions from Real-life Event Logs, in: Analysis of Images, Social Networks and Texts. 7th International Conference AIST 2018 / Ed. by W. van der Aalst, D. I. Ignatov. Springer, 2018. P. 274-280.
Гнатенко А. Р., Захаров В. А. Языки спецификаций моделей Крипке на основе темпоральных логик и их выразительные возможности // В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018. С. 131-133.
Захаров В. А. Полиномиальный алгоритм проверки эквивалентности детерминированных двухленточных автоматов // В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018. С. 128-130.
Shunin T., Zubkova N., Sergey Shershakov. Neural Approach to the Discovery Problem in Process Mining, in: Analysis of Images, Social Networks and Texts. 7th International Conference AIST 2018 / Ed. by W. van der Aalst, D. I. Ignatov. Springer, 2018. P. 261-273. doi
Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018 / Ed. by V. Zakharov, Н. В. Шилов. Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018.
Zakharov V., Gnatenko A. On the expressive power of some extensions of Linear Temporal Logic, in: Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018 / Ed. by V. Zakharov, Н. В. Шилов. Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29-36.
Gnatenko A., Zakharov V. On the Model Checking of Finite State Transducers over Semigroups // Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 303-324. doi