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