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:
- structure / behavior;
- interleaving / true concurrency;
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
