Goal of research:
The goal of the research is development of new methods for modeling and analysis of sequential programs and distributed information systems, including development of new approaches for the analysis of information system behavior based on event logs.
The basics of discrete mathematics, theory of finite state machines (including transducers), temporal logic, and abstract algebra were used for modeling and analysis of sequential programs. Temporal logic, the theory of Petri nets and finite state machines, process mining techniques were used for modeling and analysis of distributed system behavior.
Empirical base of research:
The empirical base of research is represented by sequential programs, distributed systems, and event logs of information systems.
Results of research:
In the field of sequential program analysis we obtained the following results:
The algorithmic undecidability of the satisfiability of FL-LTL logic formulas on finite state machines-transducers, operating over free commutative semigroup and Abelian groups, was proven.
It was proven that the minimization of the first-order program schemata, provided that the logic-thermal equivalence is preserved, is algorithmically solvable. An exhaustive search algorithm, based on the verification procedure of the logical-thermal equivalence of the first-order program schemata, was proposed.
It was shown that the first-order program schemata supplied with logical-thermal equivalence and finite state deterministic transducers operating over substitutions are mutually translated into each other.
In the field of modeling and analysis of distributed systems the following results were obtained:
An overview and classification of resource equivalence relations on Petri net markings is presented. Resources are defined as a part of a Petri net marking. Two resources are equivalent if and only if replacing one of them by another in any Petri net marking does not change the observable net behavior. Several types of resource equivalence are studied. It is shown that all of them can be finitely represented. Classification of resource equivalences with respect to their decidability and approximability is done.
The study on controlling Petri net behavior using priority and time constraints was continued. Controlling here means forcing a process to behave in a stable way by associating priorities, or time intervals to transitions. Earlier we have developed a partial algorithm for computing transition priorities by constructing a spin-based coverability tree. These priorities ensure liveness and safety of the net. In 2017 the algorithm was enhanced, and its applicability was extended. We have also proved decidability of a problem of finding priorities for transforming a live, but unbounded Petri net into a live and bounded net with the same structure.
Well-structured transition systems (WSTS) became a well-known tool in the study of concurrency systems for proving decidability of properties based on coverability and boundedness. The tool for behavioral analysis of such systems was developed. Two most studied algorithms for analysis of well-structured transition systems behavior (backward reachability and the Finite Reachability Tree analyses) have been implemented. The WSTSL language is developed to store and define well-structured transition systems.
In the process mining field the following results were obtained:
A real-time temporal logic was developed, suitable for formalization and formal verification of correctness requirements for event logs generated by a distributed system. Events contain a timestamp (a time when an event took place), an identifier of a sender, and a relation to other system components.
To synthesize models for multi-agent systems from event logs, a compositional approach has been suggested.
A system event log is filtered by agents. After that, agent models (in the form of Petri nets) are synthesized from filtered agent event logs. Agent interaction is also described using a Petri net called an interface. Agent models are composed via special constructs on Petri nets – morphisms. They also provide composition correctness – compositional system model inherits agent deadlock-freeness and proper termination. Interface patterns, which can be used for typical interactions, have been suggested. The preliminary experiment results on using the simple causality pattern for compositional synthesis of models for multi-agent systems have shown a significant increase in model quality, i.e. in structuredness and precision estimations.
An algorithm for discovering high-level acyclic process models from event logs and some specified partition of low-level events into subsets associated with abstract events in a high-level model is developed. Events in a high-level model are abstract events, which can be refined to low-level subprocesses, whose behavior is recorded in event logs. It is proved, that the algorithm ensures perfect fitness between the constructed high-level model and a given low-level event log.
A novel method for discovering BPMN (Business Process Model and Notation) was developed. This method allows mining hierarchical business process models with data and resource perspectives at each level of granularity.
A method for synthesizing „hybrid“ UML diagrams (a newly proposed extension of the UML standard) from event logs of service-oriented information systems was developed and implemented. Unlike the previously proposed hierarchical sequence diagrams, hybrid diagrams include different types of diagrams (sequence, activity and collaboration) for the most convenient representation of a SOA system's behavior in different perspectives.
Algorithms for the local repair of process models using information from event logs were developed. These algorithms use maximum decomposition to reduce the size of a given process model.
A novel method for the generation of event logs from BPMN models was developed. This method was implemented and verified on a variety of BPMN models from different domains.
An algorithm for finding a minimal graph edit distance between two graphs was adapted for the comparison of BPMN models. This algorithm was implemented and verified on BPMN models discovered from event logs of an e-government information system.
A novel effective technique for finding subtraces in traces of an event log was developed on the basis of the classical Aho-Corasick approach. This technique allows for searching in several traces simultaneously. It was implemented and tested on real-life event logs.
Level of implementation, recommendations on implementation or outcomes of the implementation of the results:
The proposed methods are focused on the possibility of their practical application. Methods for the behavior analysis of distributed systems have been verified on real data. For instance, using the proposed methods, various event logs of information systems automating processes in e-government, online sales, banking, and other domains were analyzed.