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.
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".