Dr. Igor Valerievich Tarasyuk


Description of Research

Last years, computing machines and systems with parallel and distributed architecture became widespread, since they provide a possibility to solve a permanently growing volume of computation problems. But the problem of behavioral analysis for such concurrent systems appeared to be more complex than that for usual sequential systems, because some components of the former can work with partial of complete independence each of another. Therefore, such a branch of computer science as theory of parallel systems and processes becomes more and more important. It deals with an investigation of behavior of concurrent systems with the use of different mathematical formalisms.

In concurrency theory, from the very beginning, a great attention was to a development of formal models for specification and analysis of systems with independent occurrence of actions. In addition to such standard models as languages, automata and transition systems, also that like Petri nets, process algebras, Hoare traces, Mazurkiewicz traces , synchronization trees, event structures and many others have been introduced.

A classification of such a model diversity can be arranged via the following dichotomies:

  1. structure / behavior;
  2. interleaving / true concurrency;
  3. linear time / branching time.

In structure models, the states of systems are clearly described, and behavioral aspects are hidden. In behavior models, the actions fulfilled by systems are explicit ones, and the states can be derived from behavior.

In interleaving models, concurrency of actions is simulated by their nondeterministic interleaving (i.e occurrence in all possible orders). In true concurrency models, it is interpreted as causal independence of actions.

In linear time models, conflict is not respected, i.e. the moment of behavior when nondeterministic choice among several ways of further computations ("futures" or "branches") happens. In branching time models, this information is completely represented.

Changing a particular model corresponds to the choice of an abstraction level of behavior, i.e. to the changing of semantics.

An alternative (and more convenient) approach consists in the choice of an expressive enough (structural or behavioral) formal model and consideration of different equivalences which provide one with a semantics or an equality criteria for a proper abstraction level corresponding to the two remaining dichotomies.

Among these formalisms, a structural model of Petri nets and a behavioral model of process algebras became most popular. The main advantages of Petri nets are in their ability for clear description of concurrency and long experience in both specification and analysis of parallel systems. In addition, the have useful graph representation. The main advantages of process algebras are in their modular nature, well developed equivalence notions, algebraic rules and complete proof systems. A considering these models together (in particular, a definition of a net semantics for algebraic formulas) provides one with a possibility to combine the best properties of both the formalisms.

A notion of equivalence is central in any theory of systems. Behavioral equivalences allow to compare systems taking into account particular aspects of their behavior and abstract from the peculiarities of a model used for their specification. Hence it constitutes a part of the semantics of formal models. In particular, it provides a basis for the correct (i.e. semantics-preserving) simplification of systems. At the verification level, equivalences give a possibility to check whether an implementation satisfy a specification, and whether two implementations correspond to the same specification.

Our results in this scientific area are the following.

  1. On Petri nets both without and with silent transitions a wide set of behavioral equivalences has been proposed and investigated. It provides one with an ability to abstract from structural and behavioral properties of modeled systems. These relations are distributed in the semantics from interleaving to true concurrency and from linear to branching time ones.
    • A diagram of interrelations of the mentioned equivalences has been obtained. A logical characterization of a number of equivalence notions has been proposed which can be used for treating behavior of concurrent systems in terms of temporal formulas. A method of effective net reduction has been designed that preserves their behavior modulo the equivalences.
    • Compositional aspects of behavior properties preservation for modeled systems have been investigated.
    • Interrelation of equivalence notions on subclasses of nets has been established to simplify comparing their behavior and better understanding a nature of the relations.
  2. On time Petri nets both without and with silent transitions a number of time, untime and regional equivalences have been investigated, which are able in different degree to take into account time aspects of behavior of modeled systems.
    • A correlation of the mentioned equivalences has been clarified. A regional characterization of time equivalences has been proposed, which simplifies check of the latter.
    • A compositional approach to the check of equivalences has been investigated.
    • Interrelations of equivalences on subclasses of time nets have been established.
  3. On a new class of Discrete Time Weighted Stochastic Petri Nets (DTWSPNs) with concurrent transition firings proposed by Prof. Dr. Peter Buchholz a number of equivalence relations has been introduced. They extend the well-known trace and bisimulation ones for systems with step semantics to DTWSPNs.
    • A lattice of interrelations for the equivalence notions has been established.
    • A logical characterization of the equivalences has been presented via formulas of the new probabilistic modal logics.
    • It has been demonstrated how the equivalences can be used to compare stationary behavior of stochastic nets.
  4. Semantic equivalences of algebraic calculi and their extensions have been treated as well as their connections with net equivalence relations.
    • A new calculus of labeled nondeterministic concurrent processes AFLP_2 has been proposed, which is an extension of the known algebra AFP_2 (introduced by Prof. Dr. Vadim E. Kotov and Dr. Ludmila A. Cherkasova) by labeling function. This labeling has offered a possibility of specifying much wider class of processes that of AFP_2.
    • A complete and correct axiomatization of the equivalences w.r.t. denotational semantics of the mentioned algebras has been proposed as well as operational characterization of these equivalences which can be used for comparing these notions with behavioral relations.
    • Interrelations of the algebraic and net equivalences have been established. The result is the translation net specifications into algebraic and vice versa with preservation of behavior. It has integrated the advantages both nets and algebras.
    • A term rewrite system to arrange automatic check of semantic equivalences has been defined. On its basis, a computer program CANON for check of formulas for equivalence has been designed.
  5. Semantic equivalences of stochastic extensions of well-known process algebras have been defined and investigated.
    • A discrete time stochastic extension StAFP_0 of Algebra of Finite Processes AFP_0 (introduced by Prof. Dr. Vadim E. Kotov and Dr. Ludmila A. Cherkasova) has been proposed. Formulas of StAFP_0 specify Stochastic A-nets (SANs), a subclass of DTWSPN's.
    • A sound axiomatization of the net equivalence of StAFP_0 (an isomorphism of net representations of formulas) has been presented.
    • A discrete time stochastic extension dtsPBC of finite Petri Box Calculus PBC enriched with iteration has been constructed.
    • Step operational semantics of dtsPBC has been defined in terms of labeled transition systems based on action and inaction rules. Denotational semantics has been defined in terms of a subclass of labeled DTSPNs (LDTSPNs) called discrete time stochastic Petri boxes (dts-boxes).
    • Algebraic stochastic equivalences of dtsPBC have been introduced which allow one to identify stochastic processes with similar behaviour. The interrelations of all the introduced probabilistic equivalences have been investigated.
    • It is explained how the equivalences we proposed can be used to reduce transition systems of expressions of dtsPBC.
    • A logical characterization of the equivalences of dtsPBC has been presented via formulas of the new probabilistic modal logics.
    • It has been demonstrated how to apply the equivalences of dtsPBC to compare stationary behaviour.
    • A problem of preservation of the equivalences by algebraic operations of dtsPBC has been discussed.
    • It has been explained how to analyze performance of systems within dtsPBC.
    • The algebraic models of shared memory system and dining philosophers one as well as their reductions have been presented and analyzed in dtsPBC.
    • An extension dtsiPBC of dtsPBC with immediate multiactions has been proposed.
    • Step operational semantics of dtsiPBC has been constructed via labeled probabilistic transition systems. Denotational semantics of dtsiPBC has been defined on the basis of a subclass of labeled discrete time stochastic Petri nets with immediate transitions.
    • The corresponding stochastic process which is a semi-Markov chain has been analyzed to evaluate performance in dtsiPBC.
    • Step stochastic bisimulation equivalence is defined and used to reduce transition systems and underlying semi-Markov chains of expressions as well as to compare the stationary behaviour.
    • A case study of the shared memory system has been considered as an example of specification, modeling, behaviour analysis and performance evaluation in dtsiPBC.