List of Publications
In the following list, there is also an information (abbreviated below the items) about foundations
supported the research with numbers of the corresponding grants, see
Scientific Projects.
List of Publications structured by kind of publication, see PDF file.
Selected publications in
Zentralblatt Math,
Scopus,
DBLP,
Web of Science,
ORCID,
German National Library,
German
National Library of Science and Technology (TIB),
ResearchGate,
Petri Nets Bibliography,
Russian Scientific Electronic Library and
MathNet.Ru.
A layout of some papers downloadable from this site can slightly differ from that of their printed versions, however,
the content is the same or improved. In particular, the page numbering may be not identical. Please, refer to the page
numbers presented at this site in such a case.
 2023
 Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives
hal02573419v4 (version 4), 142 pages, France, January 2023.
Abstract: We propose dtsdPBC, an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box
calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Macia and V. Valero. In dtsdPBC, nonnegative integers specify deterministic
multiactions with fixed (including zero) time delays. The step operational semantics is constructed via labeled probabilistic transition systems.
The Petri net denotational semantics is defined via dtsdboxes, a subclass of labeled discrete time stochastic Petri nets with deterministic
transitions. We also define step stochastic bisimulation equivalence of the process expressions, which is used to compare the qualitative and
quantitative behaviour of the specified processes. The consistency of the operational and denotational semantics of dtsdPBC up to that equivalence
is established. In order to evaluate performance in dtsdPBC, the underlying semiMarkov chains (SMCs) and (reduced) discrete time Markov chains
(DTMCs and RDTMCs) of the process expressions are analyzed. We explain how step stochastic bisimulation equivalence of the expressions can be used
for quotienting their transition systems and Markov chains, as well as to compare the stationary behaviour and residence time properties. We prove
that the equivalence guarantees coincidence of the functional and performance characteristics and therefore can be used to simplify performance
analysis of the algebraic processes. In a case study, a method of modeling, performance evaluation and behaviour reduction for concurrent systems
with discrete fixed and stochastic delays is applied to the generalized shared memory system with maintenance. We also determine the main advantages
of dtsdPBC by comparing it with other wellknown or similar SPAs.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, discrete time, stochastic multiaction, deterministic
multiaction, transition system, operational semantics, stochastic transition, deterministic transition, dtsdbox, denotational semantics, Markov
chain, performance evaluation, reduction, stochastic bisimulation, quotient, shared memory system.
 2022
 Tarasyuk I.V.
Performance preserving equivalence for stochastic process algebra dtsdPBC.
ResearchGate
Preprint 362034663, 62 pages, July 2022.
Abstract: Petri box calculus (PBC) of E. Best, R. Devillers, J.G. Hall and M. Koutny is a wellknown algebra of parallel processes with a
Petri net semantics. Discrete time stochastic and deterministic PBC (dtsdPBC) of the author extends PBC with discrete time stochastic and
deterministic delays. dtsdPBC has a step operational semantics via labeled probabilistic transition systems and a Petri net denotational semantics
via dtsdboxes, a subclass of labeled discrete time stochastic and deterministic Petri nets (LDTSDPNs). To evaluate performance in dtsdPBC, the
underlying semiMarkov chains (SMCs) and (reduced) discrete time Markov chains (DTMCs and RDTMCs) of the process expressions are analyzed. Step
stochastic bisimulation equivalence is used in dtsdPBC as to compare the qualitative and quantitative behaviour, as to establish consistency of the
operational and denotational semantics. We demonstrate how to apply step stochastic bisimulation equivalence of the process expressions for
quotienting their transition systems, SMCs, DTMCs and RDTMCs while preserving the stationary behaviour and residence time properties. We also prove
that the quotient behavioural structures (transition systems, reachability graphs and SMCs) of the process expressions and their dtsdboxes are
isomorphic. Since the equivalence guarantees identity of the functional and performance characteristics in the equivalence classes, it can be used
to simplify performance analysis within dtsdPBC due to the quotient minimization of the state space.
Keywords: Petri box calculus, discrete time, stochastic and deterministic delays, transition system, operational semantics, dtsdbox,
denotational semantics, Markov chain, performance, stochastic bisimulation, quotient.
 2021
 Tarasyuk I.V.
Performance evaluation in stochastic process algebra dtsdPBC.
Siberian Electronic Mathematical Reports 18(2), pages
11051145, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, October 2021 (ISSN 18133304). DOI:
10.33048/semi.2021.18.085. Web of Science, Scopus, Zentralblatt Math indexed.
SJR indicator (2021): 0.516 (Q2). RSCI indexed.
Abstract: We consider discrete time stochastic and deterministic Petri box calculus (dtsdPBC), recently proposed by I.V. Tarasyuk. dtsdPBC
is a discrete time extension with stochastically and deterministically timed multiactions of the wellknown Petri box calculus (PBC), presented by
E. Best, R. Devillers, J.G. Hall and M. Koutny. In dtsdPBC, stochastic multiactions have (conditional) probabilities of execution at the next time
moment while deterministic multiactions have nonnegative integers associated that specify fixed (including zero) delays. dtsdPBC features a step
operational semantics via labeled probabilistic transition systems. In order to evaluate performance in dtsdPBC, the underlying semiMarkov chains
(SMCs) are investigated, which are extracted from the transition systems corresponding to the process expressions of the calculus. It is demonstrated
that the performance analysis in dtsdPBC is alternatively possible by exploring the corresponding discrete time Markov chains (DTMCs) and their
reductions (RDTMCs), obtained by eliminating the states with zero residence time (vanishing states). The method based on DTMCs permits to avoid
building the embedded DTMC (EDTMC) and weighting the probability masses in the states by their average sojourn times. The method based on RDTMCs
simplifies performance analysis of large systems due to eliminating the nonstop transit (vanishing) states where only instantaneous activities are
executed, resulting in a smaller model that can easier be solved directly.
Keywords: stochastic process algebra, Petri box calculus, discrete time, stochastic multiaction, deterministic multiaction, transition system,
operational semantics, Markov chain, performance evaluation, reduction.
 2020
 Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives
hal02573419v1, 113 pages, France, May 2020.
Abstract: We propose dtsdPBC, an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box
calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Macia and V. Valero. In dtsdPBC, nonnegative integers specify deterministic
multiactions with fixed (including zero) time delays. The step operational semantics is constructed via labeled probabilistic transition systems.
The denotational semantics is defined on the basis of a subclass of labeled discrete time stochastic Petri nets with deterministic transitions.
The consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding semiMarkov chains and (reduced) discrete
time Markov chains are analyzed. We define step stochastic bisimulation equivalence of expressions and explain how it can be used to reduce their
transition systems and underlying semiMarkov chains, as well as to compare the stationary behaviour. We prove that the introduced equivalence
guarantees coincidence of the functional and performance characteristics and therefore can be used to simplify performance analysis of the
algebraic processes. In a case study, a method of modeling, performance evaluation and behaviour reduction for concurrent systems with discrete
fixed and stochastic delays is applied to the generalized shared memory system with with maintenance.
Keywords: stochastic Petri net, stochastic process algebra, Petri box calculus, discrete time, stochastic multiaction, deterministic
multiaction, transition system, operational semantics, stochastic transition, deterministic transition, dtsdbox, denotational semantics, Markov
chain, performance evaluation, stochastic bisimulation, reduction, shared memory system.
 Tarasyuk I.V.
Discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
Siberian Electronic Mathematical Reports 17, pages
15981679, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, October 2020 (ISSN 18133304). DOI:
10.33048/semi.2020.17.112. Web of Science, Scopus, Zentralblatt Math indexed.
SJR indicator (2020): 0.468 (Q2). RSCI indexed.
Abstract: We propose dtsdPBC, an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box
calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Macia and V. Valero. dtsdPBC enhances the expressiveness of dtsiPBC and extends the
application area of the associated specification and analysis techniques. In dtsdPBC, nonnegative integers are used to specify fixed (including
zero) time delays of deterministic multiactions. The step operational semantics of the calculus is constructed via labeled probabilistic
transition systems. The Petri net denotational semantics of the calculus is defined on the basis of dtsdboxes, a subclass of novel labeled
discrete time stochastic Petri nets with deterministic transitions (LDTSDPNs). We also define step stochastic bisimulation equivalence of the
algebraic expressions, used to compare the qualitative and quantitative behaviour of the specified processes. The consistency of the operational
and denotational semantics of dtsdPBC up to that bisimulation equivalence is established. The interrelations of the mentioned equivalence with
other behavioural notions of the calculus are investigated. A series of examples that construct the transition systems and dtsdboxes for the
expressions with different types of multiactions and operations demonstrates both the specification capabilities and semantic features of the new
calculus.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, discrete time, stochastic multiaction, deterministic
multiaction, transition system, operational semantics, stochastic transition, deterministic transition, dtsdbox, denotational semantics,
stochastic bisimulation.
 2019
 Tarasyuk I.V.
Discrete time stochastic and deterministic Petri box calculus.
CoRR abs/1905.00456 (arXiv:1905.00456), 57 pages, Computing
Research Repository, Cornell University Library, Ithaca, NY, USA, May 2019. DBLP indexed. RSCI indexed.
Abstract: We propose an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box
calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Macia and V. Valero. In dtsdPBC, nonnegative integers specify multiactions
with fixed (including zero) time delays. The step operational semantics is constructed via labeled probabilistic transition systems. The
denotational semantics is defined on the basis of a subclass of labeled discrete time stochastic Petri nets with deterministic transitions.
The consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding semiMarkov chains and (reduced)
discrete time Markov chains are analyzed.
Keywords: stochastic Petri net, stochastic process algebra, Petri box calculus, discrete time, deterministic multiaction, transition
system, operational semantics, deterministic transition, dtsdbox, denotational semantics, Markov chain, reduction, performance evaluation.
DFG BE 1267/141
 Tarasyuk I.V.,
Buchholz P.
Logical characterization of fluid equivalences.
Siberian Electronic Mathematical Reports 16, pages
826862, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, June 2019 (ISSN 18133304). DOI:
10.33048/semi.2019.16.055. Web of Science, Scopus, Zentralblatt Math indexed.
SJR indicator (2019): 0.350 (Q3). RSCI indexed.
Abstract: We investigate fluid equivalences that allow one to compare and reduce behaviour of labeled fluid stochastic Petri nets
(LFSPNs) with a single continuous place while preserving their discrete and continuous properties. We propose a lineartime relation of
fluid trace equivalence and its branchingtime counterpart, fluid bisimulation equivalence. Both fluid relations take into account the
essential features of the LFSPNs behaviour, such as functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose
continuous markings have no influence to the discrete ones, i.e. every discrete marking determines completely both the set of enabled
transitions, their firing rates and the fluid flow rates of the incoming and outgoing arcs for each continuous place. Moreover, we require
that the discrete part of the LFSPNs should be continuous time stochastic Petri nets. The underlying stochastic model for the discrete
part of the LFSPNs is continuous time Markov chains (CTMCs). The performance analysis of the continuous part of LFSPNs is accomplished via
the associated stochastic fluid models (SFMs). We characterize logically fluid trace and bisimulation equivalences with two novel fluid
modal logics HML_flt and HML_flb, constructed on the basis of the wellknown HennessyMilner Logic (HML). These characterizations
guarantee that two LFSPNs are fluid (trace or bisimulation) equivalent iff they satisfy the same formulas of the respective logic, i.e.
they are logically equivalent. The results imply operational characterizations of the logical equivalences.
Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid
model, transient and stationary behaviour, fluid trace and bisimulation equivalences, fluid modal logic, logical and operational
characterizations.
DFG BE 1267/141
 2018
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Bisimulation equivalence for functional and performance analysis of concurrent stochastically timed systems
in dtsiPBC.
Technical Report DIAB18051, 99 pages, Department of Computer Systems, High School of Computer
Science Engineering, University of Castilla  La Mancha, Albacete, Spain, May 2018. RSCI indexed.
Abstract: We propose an extension with immediate multiactions of discrete time stochastic Petri box calculus (dtsPBC), presented
by I.V. Tarasyuk. The resulting algebra dtsiPBC is a discrete time analogue of stochastic Petri box calculus (sPBC) with immediate
multiactions, proposed by H. Macia, V. Valero and others within a continuous time domain. In this version of dtsiPBC, we use positive
reals (instead of the previously used positive integers) as the weights of immediate multiactions to provide more flexibility in
specification. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational semantics is
defined on the basis of a subclass of labeled discrete time stochastic Petri nets with immediate transitions. The consistency of the both
semantics is demonstrated. In order to evaluate performance, the corresponding semiMarkov chains and (reduced) discrete time Markov chains
are analyzed. We define step stochastic bisimulation equivalence of expressions and prove that it can be applied to reduce their transition
systems and underlying semiMarkov chains while preserving the functionality and performance characteristics. We explain how this equivalence
may help to simplify performance analysis of the algebraic processes. In a case study, a method of modeling, performance evaluation and
behaviour preserving reduction of concurrent systems is outlined and applied to the shared memory system. We also determine the main
advantages of dtsiPBC by comparing it with other wellknown or similar SPAs.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, performance evaluation, stochastic
equivalence.
Spanish Government TIN201565845C0302, DFG BE 1267/141
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic equivalence for performance analysis of concurrent systems
in dtsiPBC.
Siberian Electronic Mathematical Reports 15, pages
17431812, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, December 2018 (ISSN 18133304). DOI:
10.33048/semi.2018.15.144. Web of Science, Scopus, Zentralblatt Math indexed. SJR
indicator (2018): 0.412 (Q2). RSCI indexed.
Abstract: We propose an extension with immediate multiactions of discrete time stochastic Petri Box Calculus (dtsPBC), presented by
I.V. Tarasyuk. The resulting algebra dtsiPBC is a discrete time analogue of stochastic Petri Box Calculus (sPBC) with immediate multiactions,
designed by H. Macia, V. Valero et al. within a continuous time domain. The step operational semantics is constructed via labeled probabilistic
transition systems. The denotational semantics is based on labeled discrete time stochastic Petri nets with immediate transitions. To evaluate
performance, the corresponding semiMarkov chains are analyzed. We define step stochastic bisimulation equivalence of expressions that is
applied to reduce their transition systems and underlying semiMarkov chains while preserving the functionality and performance characteristics.
We explain how this equivalence can be used to simplify performance analysis of the algebraic processes. In a case study, a method of modeling,
performance evaluation and behaviour reduction for concurrent systems is outlined and applied to the shared memory system.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, operational and denotational semantics,
semiMarkov chain, performance evaluation, stochastic equivalence, reduction.
Spanish Government TIN201565845C0302, DFG BE 1267/141
 2017
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC.
CoRR abs/1702.07478 (arXiv:1702.07478), 69 pages, Computing
Research Repository, Cornell University Library, Ithaca, NY, USA, February 2017. DBLP indexed. RSCI indexed.
Abstract: We propose an extension with immediate multiactions of discrete time stochastic Petri Box Calculus (dtsPBC), presented
by I.V. Tarasyuk. The resulting algebra dtsiPBC is a discrete time analogue of stochastic Petri Box Calculus (sPBC) with immediate
multiactions, designed by H. Macia, V. Valero et al. within a continuous time domain. The step operational semantics is constructed via
labeled probabilistic transition systems. The denotational semantics is based on labeled discrete time stochastic Petri nets with
immediate transitions. To evaluate performance, the corresponding semiMarkov chains are analyzed. We define step stochastic bisimulation
equivalence of expressions that is applied to reduce their transition systems and underlying semiMarkov chains while preserving the
functionality and performance characteristics. We explain how this equivalence can be used to simplify performance analysis of the
algebraic processes. In a case study, a method of modeling, performance evaluation and behaviour reduction for concurrent systems is
outlined and applied to the shared memory system.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, performance evaluation, stochastic
equivalence.
Spanish Government TIN201565845C0302, DFG BE 1267/141
 Tarasyuk I.V.,
Buchholz P.
Equivalences for fluid stochastic Petri nets.
Siberian Electronic Mathematical Reports 14,
pages 317366, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, April 2017 (ISSN 18133304). DOI:
10.17377/semi.2017.14.029. Web of Science, Scopus, Zentralblatt Math indexed.
SJR indicator (2017): 0.339 (Q3). RSCI indexed.
Abstract: We propose fluid equivalences to compare and reduce behaviour of labeled fluid stochastic Petri nets (LFSPNs) while
preserving their discrete and continuous properties. We define a lineartime relation of fluid trace equivalence and its branchingtime
counterpart, fluid bisimulation equivalence. Both fluid relations respect the essential features of the LFSPNs behaviour, such as
functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose continuous markings have no influence to the
discrete ones, i.e. every discrete marking determines completely both the set of enabled transitions, their firing rates and the fluid
flow rates of the incoming and outgoing arcs for each continuous place. We also require that the discrete part of the LFSPNs should be
continuous time stochastic Petri nets. The underlying stochastic model for the discrete part of the LFSPNs is continuous time Markov
chains (CTMCs). The performance analysis of the continuous part of LFSPNs is accomplished via the associated stochastic fluid models
(SFMs). We show that fluid trace equivalence preserves average potential fluid change volume for the transition sequences of every
certain length. We prove that fluid bisimulation equivalence preserves the following aggregated (by such a bisimulation) probability
functions: stationary probability mass for the underlying CTMC, as well as stationary fluid buffer empty probability, fluid density and
distribution for the associated SFM. Fluid bisimulation equivalence is then used to simplify the qualitative and quantitative analysis
of LFSPNs that is accomplished by means of quotienting (by the equivalence) the discrete reachability graph and underlying CTMC. The
application example of a document preparation system demonstrates the behavioural analysis via quotienting by fluid bisimulation
equivalence.
Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic
fluid model, transient and stationary behaviour, buffer empty probability, fluid density and distribution, performance analysis,
Markovian trace and bisimulation equivalences, fluid trace and bisimulation equivalences, quotient, application.
DFG BE 1267/141, RFBR 140191334
 Tarasyuk I.V.,
Buchholz P.
Behavioural equivalences for fluid stochastic Petri nets.
CoRR abs/1706.02641 (arXiv:1706.02641), 54 pages, Computing
Research Repository, Cornell University Library, Ithaca, NY, USA, June 2017. DBLP indexed. RSCI indexed.
Abstract: We propose fluid equivalences that allow one to compare and reduce behaviour of labeled fluid stochastic Petri nets (LFSPNs)
while preserving their discrete and continuous properties. We define a lineartime relation of fluid trace equivalence and its branchingtime
counterpart, fluid bisimulation equivalence. Both fluid relations take into account the essential features of the LFSPNs behaviour, such as
functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose continuous markings have no influence to the discrete
ones, i.e. every discrete marking determines completely both the set of enabled transitions, their firing rates and the fluid flow rates of
the incoming and outgoing arcs for each continuous place. Moreover, we require that the discrete part of the LFSPNs should be continuous time
stochastic Petri nets. The underlying stochastic model for the discrete part of the LFSPNs is continuous time Markov chains (CTMCs). The
performance analysis of the continuous part of LFSPNs is accomplished via the associated stochastic fluid models (SFMs). We show that fluid
trace equivalence preserves average potential fluid change volume for the transition sequences of every certain length. We prove that fluid
bisimulation equivalence preserves the following aggregated (by such a bisimulation) probability functions: stationary probability mass for
the underlying CTMC, as well as stationary fluid buffer empty probability, fluid density and distribution for the associated SFM. Hence, the
equivalence guarantees identity of a number of discrete and continuous performance measures. Fluid bisimulation equivalence is then used to
simplify the qualitative and quantitative analysis of LFSPNs that is accomplished by means of quotienting (by the equivalence) the discrete
reachability graph and underlying CTMC. To describe the quotient associated SFM, the quotients of the probability functions are defined. We
also characterize logically fluid trace and bisimulation equivalences with two novel fluid modal logics HML_flt and HML_flb, constructed on
the basis of the wellknown HennessyMilner Logic HML. These results can be seen as operational characterizations of the corresponding logical
equivalences. The application example of a document preparation system demonstrates the behavioural analysis via quotienting by fluid
bisimulation equivalence.
Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid model,
transient and stationary behaviour, probability mass, buffer empty probability, fluid density and distribution, performance analysis, Markovian
trace and bisimulation equivalences, fluid trace and bisimulation equivalences, quotient, fluid modal logic, logical and operational
characterizations, application example.
DFG BE 1267/141, RFBR 140191334
 Bause F.
Buchholz P.
Tarasyuk I.V.,
Telek M.
Equivalence and lumpability of FSPNs.
Proceedings of 24th International Conference on Analytical and Stochastic Modelling Techniques and Applications  17
(ASMTA'17) (N. Thomas, M. Forshaw, eds.), Newcastle upon Tyne, UK, July 1011, 2017,
Lecture Notes in Computer Science 10378, pages 1631, Springer, Germany, 2017 (ISSN 03029743, ISBN
9783319614281). DOI: 10.1007/9783319614281 2. Web of Science, Scopus,
Springer, DBLP indexed. SJR indicator (2017): 0.295 (Q3). RSCI indexed.
Abstract: We consider equivalence relations for Fluid Stochastic Petri Nets (FSPNs). Based on equivalence relations for Stochastic
Petri Nets (SPNs), which are derived from lumpability for Markov Chains, and from lumpability for certain classes of differential equations,
we define an equivalence relation for FSPNs. Lumpability for the differential equations is based on a finite discretization approach and
permutations of the fluid part of the FSPN. As for other modeling formalisms, the availability of an appropriate equivalence relation allows
one to aggregate sets of equivalent states into single states. This state space reduction can be exploited for a more efficient analysis of
FSPNs using a discretization approach. Lumpable equivalence relations can be computed from an appropriately discretized state space of the
stochastic process or directly from the FSPN.
Keywords: fluid stochastic Petri nets, lumpability, equivalence.
DFG BE 1267/141
 2016
 Macia S.H.,
Valero R.V.,
Cuartero G.F.,
Ruiz D.M.C.,
Tarasyuk I.V.
Modelling a video conference system with sPBC.
Applied Mathematics and Information Sciences
10(2), pages 475493, Natural Sciences Publishing, New York, NY, USA, March 2016 (ISSN 19350090). DOI:
10.18576/amis/100210. Web of Science, Scopus indexed. JCR impact factor (2013): 1.232.
SJR indicator (2016): 0.220 (Q3). RSCI indexed.
Abstract: Stochastic Petri Box Calculus (sPBC) with immediate multiactions is an algebraic model for the description of concurrent
systems, whose activities have a random time associated (governed by an exponential distribution) or they are immediate (no time is
required for their execution). One of the main features of sPBC, in contrast to other classical stochastic process algebras, is that it
considers multiactions instead of single actions. Furthermore, a description in this version of sPBC has a natural and easy translation
into Generalized Stochastic Petri Nets (GSPNs). In this paper we show how the calculus can be applied to information science phenomena,
specifically, to model and analyze a Video Conference System. We will see that this particular kind of system can be easily described
and analyzed within sPBC with immediate multiactions. This case study illustrates the power and flexibility of our stochastic process
algebra in the area of control and systems engineering.
Keywords: modelling, concurrent systems, Petri box calculus, stochastic process algebra, generalized stochastic Petri nets.
Spanish Government TIN201236812C0202, DFG BE 1267/141, RFBR 140191334
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Bisimulation equivalence and performance analysis of concurrent systems with discrete stochastic time in
dtsiPBC.
Technical Report DIAB16031, 92 pages, Department of Computer Systems, High School of Computer
Science Engineering, University of Castilla  La Mancha, Albacete, Spain, March 2016. RSCI indexed.
Abstract: We propose an extension with immediate multiactions of discrete time stochastic Petri box calculus (dtsPBC), presented by
I.V. Tarasyuk. The resulting algebra dtsiPBC is a discrete time analogue of stochastic Petri box calculus (sPBC) with immediate multiactions,
proposed by H. Macia, V. Valero and others within a continuous time domain. The step operational semantics is constructed via labeled
probabilistic transition systems. The denotational semantics is defined on the basis of a subclass of labeled discrete time stochastic Petri
nets with immediate transitions. The consistency of the both semantics is demonstrated. In order to evaluate performance, the corresponding
semiMarkov chains and (reduced) discrete time Markov chains are analyzed. We define step stochastic bisimulation equivalence of expressions
and prove that it can be applied to reduce their transition systems and underlying semiMarkov chains while preserving the functionality and
performance characteristics. We explain how this equivalence may help to simplify performance analysis of the algebraic processes. In a case
study, a method of modeling, performance evaluation and behaviour preserving reduction of concurrent systems is outlined and applied to the
shared memory system.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, performance evaluation, stochastic
equivalence.
Spanish Government TIN201236812C0202, DFG BE 1267/141, RFBR 140191334
 2015
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic process reduction for performance evaluation in
dtsiPBC.
Siberian Electronic Mathematical Reports 12,
pages 513551, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, September 2015 (ISSN 18133304). DOI:
10.17377/semi.2015.12.044. Scopus, Zentralblatt Math indexed. SJR indicator
(2015): 0.475 (Q2). RSCI indexed.
Abstract: Petri box calculus (PBC) is a wellknown algebra of concurrent processes with a Petri net semantics. In the paper, we
consider an extension of PBC with discrete stochastic time and immediate multiactions, which is referred to as discrete time stochastic
and immediate PBC (dtsiPBC). Performance analysis methods for concurrent and distributed systems with random time delays are
investigated in the framework of the new stochastic process algebra. It is demonstrated that the performance evaluation is possible not
only via the underlying semiMarkov chains of the algebraic process expressions but also by exploring the reduced discrete time Markov
chains, obtained from the semiMarkov chains by eliminating their states with zero residence time (called vanishing states). The latter
approach simplifies performance analysis of large systems due to abstraction from many instantaneous activities, such as those used to
specify logical conditions, probabilistic branching, as well as urgent or internal (unobservable) work.
Keywords: stochastic process algebras, stochastic Petri nets, Petri box calculus, discrete time, immediate multiactions,
operational semantics, transition systems, performance analysis, Markov chains, vanishing states, reduction.
Spanish Government TIN201236812C0202, DFG BE 1267/141, RFBR 140191334
 Tarasyuk I.V.,
Buchholz P.
Bisimulation for fluid stochastic Petri nets.
Bulletin of the Novosibirsk Computing Center, Series
Computer Science, IIS Special Issue 38, pages 121149, NCC Publisher, Novosibirsk, Russia, 2015 (ISSN 16806972). DOI:
10.31144/bncc.cs.25421972.2015.n38.p121150.
Zentralblatt Math indexed. RSCI indexed. RSCI impact factor (2014): 0.190.
Abstract: We propose a novel notion of fluid bisimulation equivalence that allows one to compare and reduce the behavior of labeled
fluid stochastic Petri nets (LFSPNs) while preserving their discrete and continuous properties. The underlying stochastic model for the
discrete part of the LFSPNs is a continuous time Markov chain (CTMC). The performance analysis of the continuous part of the LFSPNs is
accomplished via the associated stochastic fluid models. For the fluid bisimulation on the discrete markings of two LFSPNs, we require it
to be a (strong) Markovian bisimulation. On the continuous markings, for every pair of Markovian bisimilar discrete markings, the fluid
flow rates of the continuous places in the first LFSPN should coincide with those of the corresponding continuous places in the second LFSPN.
We prove that the resulting fluid bisimulation equivalence preserves fluid density and distribution, as well as discrete and continuous
performance measures.
Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid
model, fluid density and distribution, performance analysis, Markovian bisimulation, fluid bisimulation.
DFG BE 1267/141, RFBR 140191334
 2014
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic equivalence for performance evaluation of concurrent systems in dtsiPBC.
Technical Report DIAB14011, 75 pages, Department of Computer Systems, High
School of Computer Science Engineering, University of Castilla  La Mancha, Albacete, Spain, January 2014. RSCI indexed.
Abstract: We propose an extension with immediate multiactions of discrete time stochastic Petri box calculus (dtsPBC),
presented by I.V. Tarasyuk. The resulting algebra dtsiPBC is a discrete time analogue of stochastic Petri box calculus (sPBC)
with immediate multiactions, proposed by H. Macia, V. Valero and others within a continuous time domain. The step
operational semantics is constructed via labeled probabilistic transition systems. The denotational semantics is
defined on the basis of a subclass of labeled discrete time stochastic Petri nets with immediate transitions. A
consistency of the both semantics is demonstrated. In order to evaluate performance, the corresponding semiMarkov
chains and (reduced) discrete time Markov chains are analyzed. We define step stochastic bisimulation equivalence of
expressions and prove that it can be applied to reduce their transition systems and underlying semiMarkov chains while
preserving the functionality and performance characteristics. We explain how this equivalence may help to simplify
performance analysis of the algebraic processes. In a case study, a method of modeling, performance evaluation and
behaviour preserving reduction of concurrent systems is outlined and applied to the shared memory system.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, performance evaluation,
stochastic equivalence.
Highlights: Discrete time stochastic Petri box calculus is extended with immediate multiactions. dtsiPBC has a step
operational semantics and a Petri net denotational semantics. Performance is evaluated via semiMarkov or (reduced) discrete
time Markov chains. Stochastic bisimulation equivalence of expressions preserves performance measures. The equivalence simplifies
performance analysis, as demonstrated in the case study.
Spanish Government TIN201236812C0202
 Tarasyuk I.V.
Equivalence relations for modular performance evaluation
in dtsPBC.
Mathematical Structures in
Computer Science 24(1), pages 78154 (e240103), Cambridge University Press, Cambridge, UK, February 2014 (ISSN
09601295). Available on Cambridge Journals Online 2013, DOI:
10.1017/S0960129513000029. The copyright belongs to Cambridge
University Press. Web of Science, Scopus, DBLP indexed. JCR impact factor (2014): 0.449. SJR indicator (2014): 0.386 (Q3).
RSCI indexed.
Abstract: We define a number of stochastic equivalences in the dtsPBC framework, which is a discrete time stochastic
extension of finite Petri box calculus (PBC) enriched with iteration. These equivalences allow the identification of stochastic
processes that have similar behaviour but are differentiated by the semantics of the calculus. We explain how the equivalences
we propose can be used to reduce transition systems of expressions, and demonstrate how to apply the equivalences to compare the
stationary behaviour. The equivalences guarantee a coincidence of performance indices for stochastic systems, and can be used
for performance analysis simplification. We use a case study to outline a method of modelling, performance evaluation and
behaviour preserving reduction of concurrent computing systems, and apply it to the dining philosophers system.
Keywords: stochastic process algebra, Petri box calculus, iteration, discrete time, stochastic equivalence, reduction,
stationary behaviour, performance evaluation.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Performance analysis of concurrent systems in algebra
dtsiPBC.
Programming 40(5),
pages 327, MAIK Nauka/Interperiodica, Moscow, Russia, September 2014 (ISSN 01323474, in Russian). RSCI indexed. RSCI impact factor
(2013): 0.371.
Abstract: Petri box calculus PBC is a wellknown algebra of concurrent processes with a Petri net semantics. In the paper,
an extension of PBC with discrete stochastic time and immediate multiactions is considered, called discrete time stochastic and
immediate PBC (dtsiPBC). Performance analysis methods for concurrent and distributed systems with random time delays are
investigated in the framework of the new stochastic process algebra. It is demonstrated that the performance evaluation is
possible not only via the underlying semiMarkov chains of the dtsiPBC expressions, but also with the use of the underlying
discrete time Markov chains, and the latter analysis technique is more optimal.
Keywords: stochastic process algebras, stochastic Petri nets, Petri box calculus, discrete time, immediate multiactions,
semantics, transitions systems, dtsiboxes, performance analysis, Markov chains.
Spanish Government TIN201236812C0202, DFG BE 1267/141, RFBR 140191334
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Performance analysis of concurrent systems in algebra dtsiPBC.
Programming and Computer Software
40(5), pages 229249, Pleiades Publishing, Ltd., September 2014 (ISSN 03617688). DOI:
10.1134/S0361768814050089. Web of Science, Scopus, Springer, Zentralblatt
Math, DBLP indexed. JCR impact factor (2014): 0.191. SJR indicator (2014): 0.328 (Q3). RSCI indexed.
Abstract: Petri box calculus PBC is a wellknown algebra of concurrent processes with a Petri net semantics. In the paper,
an extension of PBC with discrete stochastic time and immediate multiactions is considered, called discrete time stochastic and
immediate PBC (dtsiPBC). Performance analysis methods for concurrent and distributed systems with random time delays are
investigated in the framework of the new stochastic process algebra. It is demonstrated that the performance evaluation is
possible not only via the underlying semiMarkov chains of the dtsiPBC expressions, but also with the use of the underlying
discrete time Markov chains, and the latter analysis technique is more optimal.
Keywords: stochastic process algebras, stochastic Petri nets, Petri box calculus, discrete time, immediate multiactions,
semantics, transitions systems, dtsiboxes, performance analysis, Markov chains.
Spanish Government TIN201236812C0202, DFG BE 1267/141, RFBR 140191334
 2013
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Discrete time stochastic Petri box calculus with immediate
multiactions dtsiPBC.
Proceedings of 6th International Workshop on Practical Applications of Stochastic Modelling  12
(PASM'12) and 11th International Workshop on Parallel
and Distributed Methods in Verification  12 (PDMC'12) (J. Bradley,
K. Heljanko, W. Knottenbelt, N. Thomas, eds.), London, UK, September 2012,
Electronic Notes in Theoretical Computer Science 296,
pages 229252, Elsevier, August 2013 (ISSN 15710661). DOI:
10.1016/j.entcs.2013.07.015. Scopus, DBLP indexed. SJR indicator
(2013): 0.334 (Q3). RSCI indexed.
Abstract: We propose discrete time stochastic Petri box calculus extended with immediate multiactions, called
dtsiPBC. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational
semantics is defined via labeled discrete time stochastic Petri nets with immediate transitions (LDTSIPNs). A
consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding semiMarkov chains
are analyzed. In a case study, performance of the shared memory system is evaluated.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, probabilistic
transition system, LDTSIPN, performance evaluation, shared memory system.
DFG 436 RUS 113/1002/01
 2012
 Tarasyuk I.V.
Behavioural equivalences of Petri nets with invisible
transitions.
Vestnik SibSUTI 3, pages 105135, Siberian State University of Telecommunications
and Information Sciences, Novosibirsk, Russia, 2012 (ISSN 19986920, in Russian). RSCI indexed. RSCI impact factor (2012):
0.101.
Abstract: We investigate behavioural equivalences of concurrent systems modeled by Petri nets with
invisible transitions labeled by silent actions. tauequivalences are relations which abstract from silent
actions corresponding to internal activity of the modeled system. The basic tauequivalences known from the
literature are supplemented by new notions. The interrelations of all the equivalences are determined on the
whole class of Petri nets as well as on two subclasses: Petri nets with visible transitions, where no
transitions are labeled by the invisible action, and sequential Petri nets, where no concurrent transition
firings exist. We present an example of equivalencepreserving reduction of a Petri net that models the
wellknown dining philosophers system. The decidability results for basic tauequivalences are outlined.
Keywords: Petri nets, invisible transitions, basic tauequivalences, Petri nets with visible transitions,
sequential Petri nets, reduction, decidability.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Discrete time stochastic Petri box calculus
with immediate multiactions.
Preproceedings of 6th International Workshop on Practical Applications of Stochastic Modelling
 12 (PASM'12) (J. Bradley, W. Knottenbelt,
N. Thomas, eds.), London, UK, September 17, 2012, 21 pages, Imperial College London, UK, 2012. RSCI indexed. See
slides.
Abstract: We propose discrete time stochastic Petri box calculus extended with immediate multiactions, called
dtsiPBC. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational
semantics is defined via labeled discrete time stochastic Petri nets with immediate transitions (LDTSIPNs). A
consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding semiMarkov chains
are analyzed. In a case study, performance of the shared memory system is evaluated.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, probabilistic
transition system, LDTSIPN, performance evaluation, shared memory system.
DFG 436 RUS 113/1002/01
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Applying stochastic equivalence to performance evaluation in dtsiPBC.
Technical Report DIAB12102, 62 pages, Department of Computer Systems, High
School of Computer Science Engineering, University of Castilla  La Mancha, Albacete, Spain, October 2012. RSCI indexed.
Abstract: We propose an extension of discrete time stochastic Petri box calculus (dtsPBC) presented by I.V.
Tarasyuk with immediate multiactions, called dtsiPBC. dtsiPBC is a discrete time analogue of stochastic Petri box
calculus (sPBC) with immediate multiactions proposed by H. Macia, V. Valero and others within a continuous time
domain. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational
semantics is defined on the basis of a subclass of labeled discrete time stochastic Petri nets with immediate
transitions. A consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding
semiMarkov chains are analyzed. We define step stochastic bisimulation equivalence of expressions and explain how it
can be used to reduce their transition systems and underlying semiMarkov chains, as well as to compare the stationary
behaviour. We prove that the introduced equivalence guarantees a coincidence of performance characteristics and can be
used for performance analysis simplification. In a case study, a method of modeling, performance evaluation and
behaviour preserving reduction of concurrent systems is outlined and applied to the shared memory system.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, discrete time, immediate
multiaction, operational semantics, denotational semantics, performance evaluation, stochastic equivalence.
DFG 436 RUS 113/1002/01
 2011
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic equivalence for modular performance evaluation in dtsiPBC.
Technical Report DIAB11062, 50 pages, Department of Computer Systems, High
School of Computer Science Engineering, University of Castilla  La Mancha, Albacete, Spain, June 2011. RSCI indexed.
Abstract: We propose the extension of discrete time stochastic Petri box calculus (dtsPBC) presented
by I.V. Tarasyuk with immediate multiactions. dtsPBC is a discrete time analog of stochastic Petri box
calculus (sPBC) with immediate multiactions proposed by H. Macia, V. Valero and others within a continuous
time domain. The step operational semantics is constructed via labeled probabilistic transition systems. The
denotational semantics is defined on the basis of a subclass of labeled discrete time stochastic Petri nets
with immediate transitions. A consistency of both semantics is demonstrated. In order to evaluate performance,
the corresponding semiMarkov chains are analyzed. We define step stochastic bisimulation equivalence of
expressions and explain how it can be used to reduce their transition systems and underlying semiMarkov chains
as well as to compare the stationary behaviour. We prove that the introduced equivalence guarantees a coincidence
of performance indices and can be used for performance analysis simplification. In a case study, a method of
modeling, performance evaluation and behaviour preserving reduction of concurrent systems is outlined and applied
to the shared memory system.
Keywords: stochastic Petri net, stochastic process algebra, Petri box calculus, discrete time, immediate
multiaction, transition system, operational semantics, immediate transition, dtsibox, denotational semantics,
Markov chain, performance evaluation, stochastic equivalence, reduction, shared memory system.
UCLM Invited Researchers, DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Performance analysis of the dining philosophers
system in dtsPBC.
Preproceedings of 8th Ershov Informatics Conference  11 (PSI'11)
(E. Clarke, I.B. Virbitskaite, A. Voronkov, eds.), Novosibirsk, Russia, June 27  July 1, 2011, pages 309321,
Novosibirsk, Russia, 2011 (UDK 519.6). RSCI indexed. See slides.
Abstract: Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC)
extended with iteration. In this paper, within dtsPBC, a method of modeling and performance evaluation
based on stationary behaviour analysis for concurrent computing systems is outlined applied to the dining
philosophers system.
Keywords: stochastic process algebra, Petri box calculus, discrete time, iteration, stationary
behaviour, performance evaluation, dining philosophers system.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Equivalences for modular
performance analysis in dtsPBC.
Berichte aus dem Department fuer Informatik
04/11, 41 pages, Carl von Ossietzky Universitaet Oldenburg, Germany, October 2011 (ISSN 18679218). RSCI indexed.
Abstract: In the framework of a discrete time stochastic extension dtsPBC of finite Petri box calculus (PBC)
enriched with iteration, we define a number of stochastic equivalences. They allow one to identify stochastic processes
with similar behaviour that are however differentiated by the semantics of the calculus. We explain in which way the
equivalences we propose can be used to reduce transition systems of expressions. It is demonstrated how to apply the
equivalences to compare the stationary behaviour. The equivalences guarantee a coincidence of performance indices for
stochastic systems and can be used for performance analysis simplification. In a case study, a method of modeling,
performance evaluation and behaviour preserving reduction of concurrent computing systems is outlined and applied to
the dining philosophers system.
Keywords: stochastic process algebra, Petri box calculus, iteration, discrete time, stochastic equivalence,
reduction, stationary behaviour, performance evaluation.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Performance evaluation of the generalized shared memory
system in dtsPBC.
Bulletin of the Novosibirsk Computing
Center, Series Computer Science, IIS Special Issue 32, pages 127155, NCC Publisher, Novosibirsk, Russia, 2011
(ISSN 16806972). Zentralblatt Math indexed. RSCI indexed. RSCI impact factor (2011): 0.051.
Abstract: Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC) enriched
with iteration. In this paper, a method of modeling and performance evaluation of concurrent systems in
dtsPBC is outlined based on stationary behaviour analysis. The method is then applied to the generalized
shared memory system with a variable probability of activities.
Keywords: stochastic process algebra, Petri box calculus, discrete time, iteration, stationary
behaviour, performance evaluation, shared memory system, variable probability.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Equivalences of Petri nets with invisible
transitions.
Proceedings of Russian Scientific Conference on Modeling of Informatics Systems  11
(MSI'11), Novosibirsk, Russia, November 811, 2011, 18 pages,
Siberian State University of Telecommunications and Information Sciences, Novosibirsk, Russia, 2011 (in Russian). RSCI indexed.
See slides (in Russian).
Abstract: We investigate behavioural equivalences of concurrent systems modeled by Petri nets with
invisible transitions labeled by silent actions. tauequivalences are relations which abstract from silent
actions corresponding to internal activity of the modeled system. The basic tauequivalences known from
the literature are supplemented by new notions. The interrelations of all the considered tauequivalences
are determined. We present an example of equivalencepreserving reduction of a Petri net that models the
wellknown dining philosophers system.
Keywords: Petri nets, invisible transitions, basic tauequivalences, reduction.
DFG 436 RUS 113/1002/01, RFBR 090191334
 2010
 Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Discrete time stochastic Petri box calculus with immediate multiactions.
Technical
Report DIAB10031, 25 pages, Department of Computer Systems, High School of Computer Science
Engineering, University of Castilla  La Mancha, Albacete, Spain, March 2010. RSCI indexed.
Abstract: Petri box calculus (PBC) is a flexible and expressive process algebra defined by E. Best,
R. Devillers and others in 1992. In this paper, we present the extension of discrete time stochastic Petri
box calculus (dtsPBC) presented by I.V. Tarasyuk in 2007 with immediate multiactions, which is a discrete
time analog of stochastic Petri box calculus (sPBC) with immediate multiactions proposed by H. Macia, V.
Valero and others in 2008 within a continuous time domain. The step operational semantics of the calculus
is constructed via labeled probabilistic transition systems. The denotational semantics is defined on the
basis of a subclass of labeled discrete time stochastic Petri nets with immediate transitions. A
consistency of both semantics is demonstrated. In order to evaluate performance, the corresponding
stochastic process is analyzed, which is the same for both semantics. A case study of the shared memory
system is presented as an example of specification, modeling, behaviour analysis and performance
evaluation for parallel systems.
Keywords: stochastic Petri net, stochastic process algebra, Petri box calculus, discrete time,
immediate multiaction, transition system, operational semantics, immediate transition, dtsibox,
denotational semantics, Markov chain, performance evaluation, shared memory system.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Equivalence
relations for behaviourpreserving reduction and modular performance evaluation in dtsPBC.
Berichte aus dem Department fuer Informatik
01/10, 75 pages, Carl von Ossietzky Universitaet Oldenburg, Germany, April 2010 (ISSN 18679218). RSCI indexed.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was
constructed to specify stochastic processes within the welldeveloped framework of algebraic calculi. In
2003, a continuous time stochastic extension sPBC of finite Petri box calculus (PBC) was enriched with
iteration operator by H. Macia, V. Valero, D. Cazorla and F. Cuartero. In 2006, the author added
iteration to the discrete time stochastic extension dtsPBC of finite PBC. In this paper, in the framework
of the dtsPBC with iteration, we define a variety of stochastic equivalences. They allow one to identify
stochastic processes with similar behaviour that are however differentiated by the standard semantic
equivalence of the calculus. The interrelations of all the introduced equivalences are investigated. It is
explained how the equivalences we propose can be used to reduce transition systems of expressions. A
logical characterization of the equivalences is presented via formulas of the new probabilistic modal
logics. We demonstrate how to apply the equivalences to compare stationary behaviour. A problem of
preservation of the equivalences by algebraic operations is discussed. As a result, we define an
equivalence that is a congruence relation. At last, two case studies of performance evaluation in the
algebra are presented.
Keywords: stochastic Petri net, stochastic process algebra, Petri box calculus, iteration, discrete
time, transition system, operational semantics, dtsbox, denotational semantics, empty loop, stochastic
equivalence, reduction, modal logic, stationary behaviour, congruence relation, performance evaluation.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Performance preserving equivalences for
dtsPBC.
Bulletin of the Novosibirsk
Computing Center, Series Computer Science, IIS Special Issue 31, pages 155178, NCC Publisher,
Novosibirsk, Russia, 2010 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed. RSCI impact factor (2010): 0.324.
Abstract: For a discrete time stochastic extension dtsPBC of finite Petri box calculus (PBC)
enriched with iteration, we define a number of stochastic equivalences. They allow one to identify
processes with similar behaviour which are differentiated by the too discriminate semantic equivalence of
the calculus. We investigate which is the weakest equivalence that guarantees a coincidence of performance
indices for stochastic systems and can be used to simplify their performance evaluation.
Keywords: stochastic process algebra, Petri box calculus, iteration, discrete time, stochastic
equivalence, stationary behaviour, performance evaluation.
DFG 436 RUS 113/1002/01, RFBR 090191334
 2009
 Tarasyuk I.V.
Performance evaluation in dtsPBC.
Proceedings of 18th Workshop on Concurrency, Specification and Programming  09
(CS&P'09) (L. Czaja, M. Szczuka, eds.), KrakowPrzegorzaly, Poland,
September 2830, 2009, Volume
2, pages 602615, Warsaw University, Poland, 2009. RSCI indexed. See
slides.
Abstract: Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC)
enriched with iteration. In this paper, within dtsPBC, a method of modeling and performance evaluation
based on stationary behaviour analysis for concurrent computing systems is outlined applied to the shared
memory system.
Keywords: stochastic process algebra, Petri box calculus, iteration, discrete time, stationary
behaviour, performance evaluation.
DFG 436 RUS 113/1002/01, RFBR 090191334
 Tarasyuk I.V.
Modeling and performance analysis of concurrent
processes in the algebra dtsPBC.
Vestnik, Quartal Journal of Novosibirsk State
University, Series: Mathematics, Mechanics, Informatics 9(4), pages 90117, Novosibirsk State
University, Novosibirsk, Russia, 2009 (ISSN 18187897, in Russian). RSCI indexed. RSCI impact factor (2009): 0.035.
Abstract: Petri box calculus PBC is a wellknown process algebra with Petri net semantics. The
author proposed discrete time stochastic extension of finite PBC called dtsPBC and enriched with iteration
operator later. In this paper, in the framework of the dtsPBC with iteration, a method of modeling,
performance analysis and behaviour preserving reduction of concurrent processes with stochastic time
delays is described applied to a shared memory system.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, iteration, discrete
time, transition system, operational semantics, dtsbox, denotational semantics, stochastic equivalence,
modeling, performance analysis, reduction.
DFG 436 RUS 113/1002/01, RFBR 090191334
 2008
 Tarasyuk I.V.
Investigating
equivalence relations in dtsPBC.
Berichte aus dem Department fuer Informatik
5/08, 57 pages, Carl von Ossietzky Universitaet Oldenburg, Germany, October 2008 (ISSN 18679218).
RSCI indexed.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was
constructed to specify stochastic processes within the welldeveloped framework of algebraic calculi. In
2003, a continuous time stochastic extension sPBC of finite Petri box calculus (PBC) was enriched with
iteration operator by H. Macia, V. Valero, D. Cazorla and F. Cuartero. In 2006, the author added
iteration to the discrete time stochastic extension dtsPBC of finite PBC. In this paper, in the framework
of the dtsPBC with iteration, we define a variety of stochastic equivalences. They allow one to identify
stochastic processes with similar behaviour that are differentiated by too strict notion of the semantic
equivalence. The interrelations of all the introduced equivalences are investigated. A logical
characterization of the equivalences is presented via formulas of the new probabilistic modal logics. We
demonstrate how to apply the equivalences to compare stationary behaviour. A problem of preservation of
the equivalences by algebraic operations is discussed. As a result, we define an equivalence that is a
congruence relation. At last, two case studies of performance evaluation in the algebra are presented.
Keywords: stochastic Petri net, stochastic process algebra, Petri box calculus, iteration, discrete
time, transition system, operational semantics, dtsbox, denotational semantics, empty loop, stochastic
equivalence, modal logic, stationary behaviour, congruence relation, performance evaluation.
DAAD A/08/08590
 Tarasyuk I.V.
A notion of congruence for dtsPBC.
Bulletin of the Novosibirsk
Computing Center, Series Computer Science, IIS Special Issue 28, pages 121141, NCC Publisher,
Novosibirsk, Russia, 2008 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed. RSCI impact factor (2008): 0.072.
Abstract: Algebra dtsPBC is a discrete time stochastic extension of finite Petri box calculus (PBC)
enriched with iteration. In this paper, we define a number of stochastic equivalences for dtsPBC which
allow one to identify finite and infinite stochastic processes with similar behaviour. A problem of
preservation of the equivalences by algebraic operations is discussed. As a result, we construct an
equivalence that is a congruence relation.
Keywords: stochastic process algebras, Petri box calculus, discrete time, operational semantics,
denotational semantics, empty loops, stochastic equivalences, congruence.
DAAD A/08/08590, DFG 436 RUS 113/1002/01, RFBR 090191334
 2007
 Tarasyuk I.V.
Stochastic Petri box calculus with discrete
time.
Fundamenta Informaticae
76(12), pages 189218,
IOS Press, Amsterdam, The Netherlands, February 2007 (ISSN 01692968).
Web of Science, Scopus, DBLP indexed. JCR impact factor (2007): 0.693. SJR indicator (2007): 0.540 (Q2).
RSCI indexed.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was
constructed to allow one for specification of stochastic processes within the welldeveloped
framework of algebraic calculi. In 2001, Macia S.H., Valero R.V. and de Frutos E.D. proposed a
continuous time stochastic extension of finite Petri box calculus (PBC) called sPBC. The algebra
sPBC has interleaving semantics due to the properties of continuous time distributions. At the same
time, PBC has step semantics, and it could be natural to propose its concurrent stochastic
enrichment. We construct a discrete time stochastic extension dtsPBC of finite PBC. A step
operational semantics is defined in terms of labeled transition systems based on action and inaction
rules. A denotational semantics is defined in terms of a subclass of labeled discrete time
stochastic Petri nets (LDTSPNs) called discrete time stochastic Petri boxes (dtsboxes). A
consistency of both semantics is demonstrated. In addition, we define a variety of probabilistic
equivalences that allow one to identify stochastic processes with similar behaviour which are
differentiated by too strict notion of the semantic equivalence. The interrelations of all the
introduced equivalences are investigated.
Keywords: stochastic Petri nets, stochastic process algebras, Petri box calculus, discrete
time, transition systems, operational semantics, dtsboxes, denotational semantics, empty loops,
probabilistic equivalences.
 Tarasyuk I.V.
Equivalences for behavioural analysis of
concurrent and distributed computing systems. 321 pages,
Academic Publisher "Geo", Novosibirsk, Russia, 2007 (ISBN 9785974700989,
in Russian). RSCI indexed.
Abstract: In the monograph, a wide range of behavioral equivalences has been proposed and
investigated on the wellknown models for concurrent systems specification and analysis such as Petri nets
and process algebras. The equivalence relations have been explored on subclasses and extensions of the
models: time and stochastic Petri nets and stochastic process algebras. On Petri nets both with and
without silent transitions and their subclasses a wide set of basic,
backforth and place behavioural equivalences were proposed and investigated in the semantics ranged from
interleaving to true concurrent as well as from linear to branching time ones. On time Petri nets both
with and without silent transitions and their subclasses a number of time, untime and regional
equivalences were proposed and investigated in interleaving and step semantics as well as in trace and
bisimulation ones. Semantic equivalences of standard and stochastic process algebras are investigated, and
a coherence between them and the net equivalence relations is clarified. An algorithm of automatic
formula comparison for the semantic equivalence is designed and implemented. For graduate and
postgraduate students and researchers interested in theoretical computer science, in
particular, formal modeling and analysis of behavioural properties of concurrent systems and processes.
Keywords: standard, time and stochastic Petri nets, subclasses, standard and stochastic process
algebras, invisible transitions and actions, behavioural and semantic equivalences, bisimulation, temporal
and probabilistic logics, reduction, refinement and composition, congruence, axiomatization, term rewrite
systems, implementation.
 2006
 Buchholz P.,
Tarasyuk I.V.
Equivalences for stochastic Petri nets and stochastic process algebras.
Vestnik, Quartal Journal of Novosibirsk State
University, Series: Mathematics, Mechanics, Informatics 6(1), pages 1442, Novosibirsk
State University, Novosibirsk, Russia, 2006 (ISSN 18187897, in Russian). RSCI indexed. RSCI impact factor (2008):
0.046.
Abstract: A new class of stochastic Petri nets (SPNs) is proposed that is a modification of
discrete time SPNs (DTSPNs) by transition labeling. The class is called labeled DTSPNs (LDTSPNs). The
observable behavior of a LDTSPN is described by labeling of transitions with actions that represent
elementary activities. The dynamic behavior of LDTSPNs is defined, and the corresponding discrete time
Markov chain (DTMC) is constructed. Behavioural equivalences of LDTSPNs are introduced as variants of
wellknown trace and bisimulation relations. Interrelations of all the mentioned equivalence relations
are investigated. A logical characterization of the equivalences is presented via formulas of
probabilistic modal logics. It is demonstrated how the equivalences can be used to compare stationary
behavior of LDTSPNs. A stochastic process algebra is proposed with formulas specifying a special subclass
of LDTSPNs.
Keywords: stochastic Petri nets, discrete time, labeling, equivalences, bisimulation, modal
logics, stationary behavior, stochastic process algebras.
 Tarasyuk I.V.
Iteration in discrete time stochastic Petri box calculus.
Bulletin of the
Novosibirsk Computing Center, Series Computer Science, IIS Special Issue 24, pages 129148,
NCC Publisher, Novosibirsk, Russia, 2006 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was
constructed to specify stochastic processes within the welldeveloped framework of algebraic
calculi. In 2001, Macia S.H., Valero R.V. and de Frutos E.D. proposed a continuous time stochastic
extension of finite Petri box calculus PBC called sPBC. The algebra sPBC has interleaving
semantics due to the properties of continuous time distributions. In 2004, the iteration operator
was added to sPBC by Macia S.H., Valero R.V., Cazorla L.D. and Cuartero G.F. to specify infinite
processes. Since PBC has step semantics, it could be more natural to propose its concurrent
stochastic enrichment based on discrete time distributions. In 2005, the author constructed a
discrete time stochastic extension dtsPBC of finite PBC. In this paper, we construct an enrichment
of dtsPBC with iteration. A step operational semantics is defined in terms of labeled transition
systems based on action and inaction rules. A denotational semantics is defined in terms of a
subclass of labeled discrete time stochastic Petri nets (LDTSPNs) called discrete time stochastic
Petri boxes (dtsboxes). Consistency of both semantics is demonstrated.
Keywords: stochastic Petri nets, stochastic process algebras, Petri box calculus, iteration,
discrete time, transition systems, operational semantics, dtsboxes, denotational semantics.
 2005
 Tarasyuk I.V.
Discrete time stochastic Petri box calculus.
Berichte aus dem Department fuer Informatik
3/05, 25 pages, Carl von Ossietzky Universitaet Oldenburg, Germany, November 2005 (ISSN 18679218).
RSCI indexed.
Abstract: Last decade, a number of stochastic enrichments of process algebras was
constructed to facilitate the specification of stochastic processes based on the the welldeveloped
framework of algebraic calculi. In 2001, Macia S.H., Valero R.V. and de Frutos E.D. proposed a
continuous time stochastic extension of finite PBC called sPBC. Algebra sPBC has interleaving
semantics due to the properties of continuous time distributions. At the same time, PBC has step
semantics, and it could be natural to propose its concurrent stochastic enrichment. We construct a
discrete time stochastic extension dtsPBC of finite PBC. Step operational semantics is defined in terms of
labeled transition systems based on action and inaction rules. Denotational semantics is defined in terms
of a subclass of labeled DTSPNs (LDTSPNs) called discrete time stochastic Petri boxes (dtsboxes). An
accordance of both the semantics is demonstrated. In addition, we define a variety of probabilistic
equivalences that allow one to identify stochastic processes with similar behaviour that are
differentiated by too strict notion of the semantic equivalence. The interrelations of all the introduced
equivalences are investigated. Some of the relations could be later considered as candidates for the role
of congruence.
Keywords: stochastic Petri nets, stochastic process algebras, Petri box calculus, discrete
time, transition systems, operational semantics, dtsboxes, denotational semantics, empty loops,
probabilistic equivalences.
DAAD A/05/05334
 2004
 Tarasyuk I.V.
Logical characterization of probabilistic taubisimulation equivalences.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 20,
pages 97111, Novosibirsk, Russia, 2004 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed.
Abstract: Stochastic Petri nets (SPNs) is a wellknown model for quantitative analysis. We consider the
class called DTWSPNs that is a modification of discrete time SPNs (DTSPNs) by transition labeling and weights.
Transitions of DTWSPNs are labeled by actions that represent elementary activities and can be visible or invisible
for an external observer. For DTWSPNs, interleaving and step probabilistic taubisimulation equivalences that
abstract from invisible actions are introduced. A logical characterization of the equivalences is
presented via formulas of the new probabilistic modal logics. This means that DTWSPNs are (interleaving
or step) probabilistic taubisimulation equivalent if they satisfy the same formulas of the corresponding
probabilistic modal logic. Thus, instead of comparing DTWSPNs operationally, one has to check the
corresponding satisfaction relation only. The new interleaving and step logics are modifications of the
probabilistic modal logic PML proposed by K.G. Larsen and A. Skou on probabilistic transition systems with
visible actions.
Keywords: stochastic Petri nets, invisible transitions, interleaving and step semantics,
equivalences, bisimulation, modal logics.
 Tarasyuk I.V.
Stochastic Petri nets: a formalism for
modeling and performance analysis of computing processes.
System Informatics 9, pages
135194, SB RAS Publisher, Novosibirsk, Russia, 2004 (ISSN 01323474, in Russian). RSCI indexed.
Abstract: Petri nets (PNs) are a wellknown formal model for qualitative analysis of discrete
dynamic systems. Stochastic Petri nets (SPNs) are an extension of PNs with an ability to calculate
performance of the systems i.e., with a feature of quantitative analysis. The behaviour analysis of a
modeled system consists in building a stochastic process based on the corresponding SPN, and in further
investigation of this process. At present, there are a lot of approaches to definition of SPNs. For
example, discrete and continuous time SPNs were proposed as well as those with different types of
transition delays, priorities and inhibitor arcs. In addition, other structural and behavioural
extensions of SPNs were introduced for more adequate treatment of particular problems of quantitative
simulation. In this paper we describe the most wellknown classes of SPNs and the related analysis
methods. We compare the presented SPN classes, give illustrative examples, describe application areas.
In addition, we discuss how to propose transition labeling for the SPN classes with a purpose to
compare SPNs by behavioural equivalences.
Keywords: standard, inhibitorpriority and stochastic Petri nets, probability distrubutions,
Markov processes and chains, transient and steady states, labelling, equivalence.
 2001
 Buchholz P.,
Tarasyuk I.V.
Net and algebraic approaches to probabilistic modeling.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 15,
pages 3164, Novosibirsk, Russia, 2001 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed.
Abstract: This paper presents a class of Stochastic Petri Nets with concurrent transition firings.
It is assumed that transitions occur in steps and for every step each enabled transition decides
probabilistically whether it wants to participate in the step or not. Among the transitions which want to
participate in a step, a maximal number is chosen to perform the firing step. The observable behavior of
a net is described by labels associated with transitions. For this class of nets the dynamic behavior is
defined and equivalence relations are introduced. These equivalences extend the wellknown trace and
bisimulation ones for systems with step semantics onto Stochastic Petri Nets with concurrent transition
firing. It is shown that the equivalence notions form a lattice of interrelations. We demonstrate how the
equivalences can be used to compare stationary behavior of nets. In addition, we propose a stochastic
process algebra that describes a subclass of the nets we introduced.
Keywords: stochastic Petri nets, step semantics, equivalence relations, bisimulation,
stationary behavior, stochastic process algebra.
GRP TUD DFG, RFBR 000100898, STYS RAS, SPYS RAS
 2000
 Tarasyuk I.V.
Tauequivalences and refinement for Petri nets based design.
Technische
Berichte TUDFI0011, 41 pages, Fakultaet Informatik, Technische Universitaet Dresden,
Germany, November 2000 (ISSN 1430211X). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioral equivalences of concurrent
systems modeled by Petri nets with silent transitions. Basic tauequivalences and backforth
taubisimulation equivalences known from the literature are supplemented by new ones, giving rise
to complete set of equivalence notions in interleaving / true concurrency and linear / branching
time semantics. Their interrelations are examined for the general class of nets as well as for
their subclasses of nets without silent transitions and sequential nets (nets without concurrent
transitions). In addition, the preservation of all the equivalence notions by refinements (allowing
one to consider the systems to be modeled on a lower abstraction levels) is investigated.
Keywords: Petri nets with and without silent transitions, sequential nets, basic and
backforth tauequivalences, refinement.
GRP TUD DFG, RFBR 000100898
 Tarasyuk I.V.
Tauequivalences and refinement for design of concurrent systems based on Petri
nets.
Papers of Young Scientists of SB RAS, 34 pages, Novosibirsk, Russia, 2000
(in Russian).
Abstract: The paper is devoted to the investigation of behavioural equivalences of
concurrent systems modeled
by Petri nets with silent transitions. Basic tauequivalences and backforth taubisimulation
equivalences known from the literature are supplemented by new ones. As a result, a complete enough
set of equivalence relations in interleaving / true concurrency and linear / branching time
semantics is obtained. The interrelations of all the mentioned equivalences are examined both on the
whole class of Petri nets and their subclasses: Petri nets without silent transitions and
sequential nets (Petri nets without concurrent transitions). In addition, the question of
preservation of the equivalences by refinement operation is investigated. Refinements allows one to
observe the modelled systems on a lower level of structural abstraction.
Keywords: Petri nets, silent transitions, sequential nets, basic and backforth equivalences,
refinement.
FPYS SB RAS
 Buchholz P.,
Tarasyuk I.V.
A class of stochastic Petri nets with step semantics and related equivalence
notions.
Technische
Berichte TUDFI0012, 18 pages, Fakultaet Informatik, Technische Universitaet Dresden,
Germany, November 2000 (ISSN 1430211X). RSCI indexed.
Abstract: This paper presents a class of Stochastic Petri Nets with concurrent transition
firings. It is assumed that transitions occur in steps and that for every step each enabled
transition decides probabilistically whether it wants to participate in the step or not. Among the
transitions which want to participate in a step, a maximal number is chosen to perform the firing
step. The observable behavior of a net is described by labels associated with transitions. For this
class of nets the dynamic behavior is defined and equivalence relations are introduced. The
equivalence relations extend the wellknown trace and bisimulation equivalences for systems with
step semantics to Stochastic Petri Nets with concurrent transition firing. It is shown that the
equivalence notions form a lattice of interrelations.
Keywords: stochastic Petri nets, step semantics, equivalence relations, bisimulation.
GRP TUD DFG, RFBR 000100898
 1999
 Tarasyuk I.V.
Tauequivalences for analysis of concurrent systems modeled by Petri nets with
silent transitions.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 12,
pages 4751, Novosibirsk, Russia, 1999 (ISSN 16806972). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural equivalences for Petri
nets with silent transitions (tauequivalences). Basic tauequivalences and backforth
taubisimulation equivalences are supplemented by new ones, giving rise to the complete set of
equivalence notions in interleaving / true concurrency and linear / branching time semantics. Their
interrelations are examined for the general Petri nets with silent transitions as well as for the
subclass of sequential nets. In addition, the preservation of all the equivalence notions by
refinements is investigated.
Keywords: Petri nets, silent transitions, basic tauequivalences, backforth
taubisimulation equivalences, sequential nets, refinement.
INTASRFBR 950378, FPYS SB RAS
 Tarasyuk I.V.
Equivalences for concurrent and distributed systems. A survey of
dissertation.
Berichte aus dem Fachbereich Informatik
9/99, 77 pages, Carl von Ossietzky Universitaet Oldenburg, Germany, September 1999 (ISSN 18679218).
DBLP indexed. RSCI indexed.
Abstract: The paper is a survey of the author's Ph.D. thesis defended at
IIS SB RAS in December 1997. On Petri nets both with and without silent
transitions a wide set of behavioral equivalences have been proposed and investigated, which provide one
with a possibility 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.
On time Petri nets both with and without 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. Semantic equivalences of algebraic calculi and their
extensions have been treated as well as their connections with net equivalence relations.
Keywords: Petri nets, time Petri nets, silent transitions, process algebras, behavioural equivalences.
DAAD A/98/38518
 1998
 Tarasyuk I.V.
Equivalence notions applied to designing concurrent systems
with the use of Petri nets.
Programming and Computer
Software 24(4), pages 162175, Pleiades Publishing, Ltd., July  August 1998 (ISSN 03617688).
Web of Science, Scopus, Springer, Zentralblatt Math, DBLP indexed. JCR impact factor (1999): 0.013. SJR indicator (1999):
0.117 (Q4). RSCI indexed.
Abstract: This paper is dedicated to the study of behavioral equivalences of concurrent systems modeled by Petri
nets. The main notions of equivalence known from the literature are complemented by new ones and analyzed on the whole
class of Petri nets and on the subclass of sequential nets (nets without concurrency). A complete description of
relationships between equivalences is obtained. Whether or not equivalence notions are preserved under the refinement
operation, which makes it possible to consider the behavior of nets at a lower abstraction level, is also analyzed.
Keywords: concurrent systems, Petri nets, behavioral equivalences, sequential nets, refinement.
VS I/70 564, INTASRFBR 950378, FPYS SB RAS
 Tarasyuk I.V.
Tauequivalences for analysis of concurrent systems modeled by Petri nets
with silent transitions.
Abstracts of 3rd Siberian Congress on Applied and Industrial Mathematics  98
(INPRIM'98), devoted to the memory
of S.L. Sobolev (O.L. Bandman, V.S. Belonosov, V.L. Vaskevich, I.A. Eganova, A.M. Matsokin, I.V.
Pottosin, V.P. Shapeev, A.A. Egorov, eds.), Novosibirsk, Russia, June 2227, 1998, pages 5656, S.L.
Sobolev Institute of Mathematics SB RAS, Novosibirsk, Russia, 1998 (ISBN 5861340501). RSCI indexed.
Abstract: Tauequivalences are relations which abstract from silent actions. In this paper,
on Petri nets with silent transitions (those labeled with silent actions), we consider basic
tauequivalences such as trace, bisimulation and conflict preserving ones. Moreover, we investigate a
set of backforth bisimulation relations which provide an operational characterization of equivalences
for temporal logics with past modalities. The diagram of interrelations for the equivalence notions is
presented. A preservation by refinement is treated for all the considered equivalences. We also compare
equivalences on a subclass of sequential nets with silent transitions.
Keywords: Petri nets, silent transitions, tauequivalences, refinement, sequential nets.
INTASRFBR 950378, FPYS SB RAS
 Tarasyuk I.V.
Place bisimulation equivalences for design of concurrent systems.
Preproceedings of 23rd International Symposium on Mathematical Foundations of Computer
Science  98 (MFCS'98), Workshop on Concurrency (P. Janchar,
M. Kretinsky, eds.), Brno, Czech Republic, August 2729, 1998,
FIMU Report Series FIMURS9806, pages 184198, Faculty of
Informatics, Masaryk University, Brno, Czech Republic, July 1998. RSCI indexed.
Abstract: In this paper, we supplement the set of basic and backforth behavioural equivalences
for Petri nets considered by the author earlier with place bisimulation ones. The relationships of all
the equivalence notions are examined, and their preservation by refinements is investigated to find out
which of these relations may be used in topdown design. It is demonstrated that the place bisimulation
equivalences may be used for the compositional and history preserving reduction of Petri nets.
Keywords: Petri nets, basic equivalences, backforth and place bisimulation equivalences,
refinement.
VS I/70 564, INTASRFBR 950378, FPYS SB RAS
 Tarasyuk I.V.
Place bisimulation equivalences for design of
concurrent and sequential systems. Proceedings of 23rd International Symposium
on Mathematical Foundations of Computer Science  98 (MFCS'98), Workshop
on Concurrency (P. Janchar, M. Kretinsky, eds.), Brno, Czech Republic, August 2729, 1998,
Electronic Notes in Theoretical Computer
Science 18, pages 191206, Elsevier, 1998 (ISSN 15710661). DOI:
10.1016/S15710661(05)802609. Scopus, DBLP indexed.
SJR indicator (1999): 0.333 (Q2). RSCI indexed.
Abstract: In this paper, we supplement the set of basic and backforth behavioural
equivalences for Petri nets considered by the author earlier by place bisimulation
ones. The relationships of all the equivalence notions are examined, and
their preservation by refinements is investigated to find out which of these
relations may be used in topdown design. It is demonstrated that the place
bisimulation equivalences may be used for the compositional and history
preserving reduction of Petri nets. In addition, we consider all the mentioned
equivalences on sequential nets which are a special subclass of general Petri
nets modelling sequential systems, where no two actions can happen
simultaneously. On this net subclass all pomset equivalences merge with the
corresponding interleaving ones, and it allows one to simplify their check.
Keywords: Petri nets, basic equivalences, backforth and place bisimulation equivalences,
refinement, sequential nets.
VS I/70 564, INTASRFBR 950378, FPYS SB RAS, DAAD A/98/38518
 Tarasyuk I.V.
Tauequivalences and refinement.
Proceedings of International Refinement Workshop and Formal Methods Pacific  98
(IRW/FMP'98), WorkinProgress Papers (J. Grundy, M. Schwenke, T.
Vickers, eds.), Canberra, Australia, September 29  October 2, 1998,
Joint Computer Science Technical Report Series TRCS9809, pages 110128,
The Australian National University, Canberra, Australia, September 1998. RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural equivalences for Petri
nets with silent transitions. Basic tauequivalences and backforth taubisimulation equivalences
are supplemented by new ones, giving rise to complete set of equivalence notions in interleaving /
true concurrency and linear / branching time semantics. Their interrelations are examined, and the
preservation of all the equivalence notions by refinements is investigated.
Keywords: Petri nets with silent transitions, basic tauequivalences, backforth
taubisimulation equivalences, refinement.
INTASRFBR 950378, FPYS SB RAS
 Tarasyuk I.V.
Notions of equivalence for development of concurrent systems with use of Petri nets.
Programming
4, pages 1939, MAIK Nauka/Interperiodica, Moscow, Russia, 1998 (ISSN 01323474, in Russian). RSCI indexed.
RSCI impact factor (2008): 0.406.
Abstract: This paper is dedicated to the study of behavioral equivalences of concurrent systems
modeled by Petri nets. The main notions of equivalence known from the literature are complemented by
new ones and analyzed on the whole class of Petri nets and on the subclass of sequential nets (nets
without concurrency). A complete description of relationships between equivalences is obtained. Whether
or not equivalence notions are preserved under the refinement operation, which makes it possible to
consider the behavior of nets at a lower abstraction level, is also analyzed.
Keywords: concurrent systems, Petri nets, behavioral equivalences, sequential nets,
refinement.
VS I/70 564, INTASRFBR 950378, FPYS SB RAS
 Tarasyuk I.V.
Equivalences of Petri nets for analysis of concurrent systems.
Papers of winners of the programm "Young Talents  97", 10 pages, Moscow, Russia, 1998
(in Russian).
Abstract: Last years, many equivalences notions were defined on Petri nets. In this paper,
a nubmer of new trace, bisimulation and multievent structure equivalences are proposed in addition
to the wellknown ones. The interrelations of all the relations are investigated both for Petri
nets and their subclass of sequential nets. The equivalences are treated for preservation by SMrefinements.
Keywords: Petri nets, sequential nets, equivalences, SMrefinement.
INTASRFBR 950378, YT 97
 Virbitskaite I.B.,
Tarasyuk I.V.
Equivalence notions and refinement for timed Petri nets.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 8, pages
5779, Novosibirsk, Russia, 1998 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed.
Abstract: The paper is contributed to develop a family of equivalence notions for realtime systems
represented by labelled Merlin's time Petri nets with zero length time intervals (i.e. with fixed time
delays). We call them "timed Petri nets". In particular, we introduce timed (timesensitive), untimed
(timeabstracting) and region (based on the notion of time region) equivalences in both the trace and
bisimulation semantics. The interrelations of all the equivalence notions are examined for a general class
of timed nets as well as for a subclass of untimed nets (timed nets with time delays equal to zero's).
Further we define a timed variant of statemachine refinement and investigate how the proposed equivalence
notions behave with respect to this class of refinements.
Keywords: timed and untimed Petri nets, timed, untimed and region equivalences, trace and
bisimulation semantics.
INTASRFBR 950378, ISSEP a97683, FPYS SB RAS
 1997
 Tarasyuk I.V.
Backforth equivalences for design of concurrent systems.
Proceedings of 4th International Symposium on Logical Foundations of Computer Science  97
(LFCS'97) (S. Adian, A. Nerode, eds.),
Yaroslavl, Russia, July 612, 1997, Lecture Notes in Computer Science 1234,
pages 374384, Springer, Germany, 1997 (ISSN 03029743, ISBN 9783540630456). DOI:
10.1007/3540630457_38. Scopus, Springer, DBLP indexed. SJR
indicator (1999): 0.299 (Q3). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural equivalences of concurrent systems modelled by
Petri nets. Backforth bisimulation equivalences known from the literature are supplemented by new ones, and their
relationship with basic behavioural equivalences is examined for the whole class of Petri nets as well as for their
subclass of sequential nets. In addition, the preservation of all the equivalence notions by refinements is examined.
Keywords: Petri nets, basic equivalences, backforth bisimulation equivalences, sequential nets, refinement.
VS I/70 564, RFBR 960101655
 Tarasyuk I.V.
An investigation of backforth and place bisimulation
equivalences.
Hildesheimer InformatikBerichte 8/97,
30 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, April 1997 (ISSN 09413014). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural
equivalences of concurrent systems modelled by Petri nets. Backforth and
place bisimulation equivalences known from the literature are supplemented by
new ones, and their relationship with basic behavioural equivalences is
examined for the general class of nets as well as for their subclass of
sequential nets (nets without concurrent transitions).
In addition, the preservation of all the equivalence notions by refinements
is investigated to find out which of these equivalences may be used for topdown design.
Keywords: Petri nets, sequential nets, basic equivalences, backforth bisimulations, place bisimulations,
refinement.
VS I/70 564, RFBR 960101655
 Tarasyuk I.V.
An investigation of tauequivalences.
Hildesheimer InformatikBerichte 9/97,
28 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, April 1997 (ISSN 09413014). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural
equivalences of concurrent systems modelled by Petri nets with silent transitions. Basic tauequivalences and
backforth taubisimulation equivalences known from the literature are supplemented by new ones, giving rise to
complete set of equivalence notions in interleaving / true concurrency and linear / branching time semantics.
Their interrelations are examined for the general class of nets as well as for their subclasses of nets without
silent transitions and sequential nets (nets without concurrent transitions). In addition, the preservation of all
the equivalence notions by refinements (allowing one to consider the systems to be modelled on a lower abstraction
levels) is investigated.
Keywords: Petri nets with silent transitions, sequential nets, basic tauequivalences, backforth
taubisimulation equivalences, refinement.
VS I/70 564, INTASRFBR 950378
 Tarasyuk I.V.
Equivalences for behavioural analysis of multilevel systems.
Joint Novosibirsk Computing
Center and Institute of Informatics Systems Bulletin, Series Computer Science 7, pages 5784,
Novosibirsk, Russia, 1997 (ISSN 16806972). Zentralblatt Math indexed. Zentralblatt Math indexed. RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural equivalences of concurrent
systems modelled by Petri nets. Backforth and place bisimulation equivalences known from the literature are
supplemented by new ones, and their relationship with relations is examined for the whole class of Petri nets
as well as for their subclass of sequential nets. In addition, the preservation of all the equivalence notions
by refinements is examined.
Keywords: Petri nets, basic equivalences, backforth bisimulation equivalences, place bisimulation
equivalences, sequential nets, refinement.
VS I/70 564, INTASRFBR 950378
 Tarasyuk I.V.
Equivalence notions for models of concurrent and distributed systems.
Abstract of Ph.D. thesis, 19 pages, Institute of Informatics Systems, Novosibirsk,
Russia, 1997 (in Russian). RSCI indexed.
Abstract: On Petri nets both with and without silent transitions a wide set of behavioral
equivalences have been proposed and investigated, which provide one with a possibility 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. On time
Petri nets both with and without 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. Semantic equivalences of algebraic calculi and their
extensions have been treated as well as their connections with net equivalence relations.
Keywords: Petri nets, time Petri nets, silent transitions, algebraic calculi, equivalences.
 Tarasyuk I.V.
Equivalence notions for models of concurrent and distributed systems.
Ph.D. thesis, 191 pages, Institute of Informatics Systems, Novosibirsk, Russia,
1997 (in Russian). RSCI indexed.
Abstract: On Petri nets both without and with silent transitions a wide set of behavioral
equivalences have been proposed and investigated, which provide one with a possibility 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. On time
Petri nets both with and without 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. Semantic equivalences of algebraic calculi and their
extensions have been treated as well as their connections with net equivalence relations.
Keywords: Petri nets, time Petri nets, silent transitions, algebraic calculi, equivalences.
 Virbitskaite I.B.,
Tarasyuk I.V.
Investigating equivalence notions for time Petri nets.
Abstracts of 4th Workshop on Logic, Languages, Information and Computation  97
(WoLLIC'97) (R.J.G.B. de Queiroz, M.
Pequeno, eds.), pages 8284, Fortaleza (Ceara), Brazil, August 1922, 1997, Grafica JB Ltda., Paraiba,
Brazil, 1997 (ISSN 13670751). RSCI indexed.
Abstract: In this paper, in the framework of time Petri nets with fixed time delays and silent
transitions we propose a number of timed, untimed and region equivalence notions in both trace and
bisimulation semantics. We also consider tauvariants of all these equivalences which abstract of silent
actions. Interrelations of all the equivalences are examined for general class of time nets as well as
for their subclass of untimed nets with instantaneous transition firings. Preservation of the equivalence
relations by new operation of time SMrefinement is investigated to have information which relations may
be used for topdown design.
Keywords: time and untime Petri nets, silent transitions, timed, untimed and region equivalences,
trace and bisimulation semantics.
VS I/70 564, ISSEP a97683, RFBR 960101655
 Virbitskaite I.B.,
Tarasyuk I.V.
Investigating equivalence notions for time Petri nets.
Logic Journal of the Interest Group in
Pure and Applied Logics 5(6), pages 921923, Oxford University Press, November 1997. Web of Science,
Scopus, DBLP indexed. JCR impact factor (2010): 0.458. SJR indicator (2006): 0.407 (Q1). RSCI indexed.
Abstract: In this paper we define equivalence notions for realtime systems represented by
labelled time Petri nets with fixed time delays called timed Petri nets. We introduce timed, untimed and
region equivalences in the trace and bisimulation semantics. The interrelations of all the equivalence
notions are examined for a general class of timed nets as well as for a subclass of untimed nets. Further
we define a timed SMrefinement and investigate how the proposed equivalence notions withstand
this class of refinements.
Keywords: time and untime Petri nets, timed, untimed and region equivalences, trace and bisimulation
semantics, timed SMrefinement.
VS I/70 564, ISSEP a97683, RFBR 960101655
 1996
 Tarasyuk I.V.
Equivalence notions for design of concurrent systems using Petri
nets.
Hildesheimer InformatikBerichte 4/96,
part 1, 19 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, January 1996 (ISSN 09413014).
RSCI indexed.
Abstract: The paper is devoted to the investigation of equivalence notions used to abstract
from concrete behavioural aspects of concurrent systems which are modelled by Petri nets. The basic
behavioural equivalences known from the literature are supplemented by new ones to obtain the
complete picture and examined for all class of nets as well as for some of their subclasses:
sequential nets (nets without concurrency) and strictly labelled nets (which are isomorphic to
nonlabelled nets). For topdown design of concurrent systems refinement is used which is the
inverse operator to abstraction of concrete structure of such systems. An important property of
equivalence notions is their preservation by refinements which guarantees equivalence of systems to
be modelled on different levels of abstraction. All of considered equivalence notions are checked
for preservation by refinements.
Keywords: Petri nets, sequential nets, strictly labelled nets, behavioural equivalences,
bisimulation, refinement.
VS I/70 564, RFBR 960101655
 Tarasyuk I.V.
Algebra AFLP_2: a calculus of labelled nondeterministic processes.
Hildesheimer InformatikBerichte 4/96,
part 2, 18 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, January 1996 (ISSN 09413014).
RSCI indexed.
Abstract: A new calculus of labelled nondeterministic processes AFLP_2 is proposed which is an
extension of the known calculus AFP_2 introduced by
Cherkasova L.A. with labelling function.
The denotational and operational semantics and complete axiomatization of the semantic equivalence are
presented. The interrelation of net equivalences investigated by the author earlier with equivalences
of the algebra (semantic and observational) is considered. Analogs of the net equivalences are defined
in AFLP_2, allowing one to consider the processes specified by formulas of the algebra at different
levels of abstraction.
Keywords: process algebras, labelling, denotational semantics, operational semantics, Petri
nets, Anets, behavioural equivalences, bisimulation, congruence.
VS I/70 564, RFBR 960101655
 Tarasyuk I.V.
Petri net equivalences for design of concurrent systems.
Proceedings of 5th Workshop on Concurrency, Specification and Programming  96
(CS&P'96) (L. Czaja, P. Starke,
H.D. Burkhard, M. Lenz, eds.), Berlin, Germany, September 2527, 1996,
InformatikBerichte 69, pages 190204, Institut fuer Informatik,
HumboldtUniversitaet zu Berlin, Berlin, Germany, 1996 (ISSN 0863095). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural
equivalences of concurrent systems modelled by Petri nets. The basic
equivalence notions known from the literature are supplemented by new ones
and examined for all class of nets as well as for their subclasses: sequential
nets (nets without concurrent transitions), strictly labelled nets (which
are isomorphic to unlabelled nets) and Tnets (nets without conflict
transitions). A complete diagram of interrelations of the considered
equivalences is obtained. In addition, the preservation of the equivalence notions by refinements is
investigated, which allows one to consider the behaviour of nets on a
lower abstraction level.
Keywords: concurrency, models, Petri nets, sequential nets, behavioural equivalences,
bisimulation, refinement.
VS I/70 564, RFBR 960101655
 Tarasyuk I.V.
An algebra of labelled nondeterministic processes.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 5,
pages 83100, Novosibirsk, Russia, 1996 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed.
Abstract: A new calculus of labelled nondeterministic processes AFLP_2
is proposed which is an extension of the known calculus AFP_2 proposed by
Cherkasova L.A. in 1989 by
labelling function. The denotational and operational semantics and complete
axiomatization of the semantic equivalence are presented. The interrelation
of net equivalences defined by the author earlier with equivalences of the
algebra (semantic and observational) is considered. Analogs of the net equivalences are defined in
AFLP_2, allowing one to consider the processes specified by formulas
of the algebra at different levels of abstraction.
Keywords: process algebras AFP_2 and AFLP_2, labelling, denotational semantics, operational
semantics, Petri nets, behavioural equivalences.
VS I/70 564, RFBR 960101655
 Virbitskaite I.B.,
Bozhenkova E.N., Votintseva A.V., Pokozy E.A., Tarasyuk I.V.
Development and investigation of semantic methods and tools of specification and
verification of concurrent systems and processes.
RFBR Information Bulletin
4(1), pages 682682, Russian Foundation for Basic Research, Nauchnyj Mir, Moscow, Russia, 1996
(ISBN 5891760010, in Russian). RSCI indexed.
RFBR 960101655
 1995
 Tarasyuk I.V.
An investigation of equivalence notions on some subclasses of Petri
nets.
Bulletin of the
Novosibirsk Computing Center, Series Computer Science 3, pages 89101, Computing
Center SB RAS, Novosibirsk, Russia, 1995 (ISSN 16806972). Zentralblatt Math indexed. RSCI indexed.
INTAS 1010CT930048
Abstract: In this paper, a variety of Petri net equivalences is examined. A correlation of
all the considered equivalences is established, and a lattice of implications is obtained. In
addition, the equivalences are treated for some subclasses of Petri nets: sequential nets, Tnets and
nets with strict labelling.
Keywords: Petri nets, behavioural equivalences, sequential nets, Tnets, strictly labelled nets.
 Tarasyuk I.V.
An investigation of net equivalences.
Proceedings of 4th International Conference on Applied Logics (AL'95)
(Yu.L. Ershov, S.S. Goncharov, A.V. Mantsivoda, eds.), June 1517, Irkutsk, Russia, 1995, pages 7475,
The State High Education Committee of Russian Federation, Irkutsk State University, Irkutsk, Russia,
1995 (UDK 518, in Russian). RSCI indexed.
Abstract: A number of Petri net equivalences is investigated. Interrelations of all the
considered equivalences are established, and a diagram of implications is obtained. Moreover,
the equivalences are treated for three subclasses of Petri nets: sequential nets, Tnets without
autoconcurrency and strictly labelled nets.
Keywords: Petri nets, equivalences, sequential nets, autoconcurrencyfree Tnets, strictly
labelled nets.
RFBR 930100986
 Tarasyuk I.V.
Algebra AFLP_2: a calculus of labelled nondeterministic concurrent
processes.
Problems of Specification and Verification of Concurrent Systems
(V.A. Nepomniaschy, ed.), pages 2249, Institute
of Informatics Systems, Novosibirsk, Russia, 1995 (ISBN 5762310698, in Russian). Zentralblatt
Math indexed. RSCI indexed.
Abstract: A calculus AFLP_2 is proposed as an extension of algebra AFP_2 by event labelling
function. Denotational and operational semantics are presented. The interrelations of a number of
behavioural net equivalences with semantic equivalences of the algebra are investigated. The
analogs of the net equivalences are defined on formulas of AFLP_2. The consistence of the formula
equivalences and their net prototypes is established. The semantic equivalence of AFLP_2 is proved
to be the only formula equivalence that is a congruence w.r.t. the algebraic operations.
Keywords: process algebras AFP_2 and AFLP_2, labelling, denotational semantics, operational
semantics, Petri nets, Anets, behavioural equivalences, bisimulation, congruence.
RFBR 930100986
 1994
 Tarasyuk I.V.
Equivalences on Petri nets.
Specification, Verification and Net Models of Concurrent Systems
(V.A. Nepomniaschy, ed.), pages 3557, Institute of
Informatics Systems, Novosibirsk, Russia, 1994 (ISBN 5762304108). RSCI indexed.
Abstract: In this paper, a set of Petri net equivalences is proposed. A correlation between all
introduced equivalences is established, and a lattice of implications is obtained. In addition, the
equivalences are examined on sequential nets. The process equivalences are demonstrated to be well
discerning on this net class.
Keywords: Petri nets, equivalences, sequential nets.
RFBR 930100986
 Tarasyuk I.V.
Equivalences on Petri nets.
Master's Thesis, Chair of Computing Systems, Department of Mathematics and
Mechanics, Novosibirsk State University, 71 pages, Novosibirsk, Russia, 1994 (in Russian).
Abstract: A wide range of semantic equivalences for Petri nets were proposed in the
literature. The relations can be classified both according to the detail of processes: sequential
(interleaving), step, partial word, pomset and process semantics and mutual simulation: standard
(trace), bisimulation, STbisimulation, history preserving bisimulation. In this thesis, a number
of new equivalences is defined which complete the variety of the known ones. Interrelarions of all
the considered equivalences are investigated, and the lattice of implications is obtained as a
result. In addition, the equivalences are treated for three subclasses of Petri nets: sequential
nets, Tnets and nets with strict labelling. It is demonstrated that the process equivalences are
well suited to discern sequential nets while the other relations merge on this net subclass.
The relationship equivalences on formulas of the calculus of finite nondeterministic processes
AFP_2 and the mentioned net equivalences is treated. Moreover, the way of automatization for
AFP_2formula comparison for semantic equivalence is presented.
Keywords: Petri nets, semantic equivalences, sequential nets, Tnets, strictly labelled
nets, process algebras, axiom system, canonical form, term rewrite system, implementation.
 1993
 Tarasyuk I.V.
Transformation formulas of algebra AFP_2 into canonical form.
Problems of Theoretical and Experimental Programming
(V.A. Nepomniaschy, ed.), pages 4759, Institute of
Informatics Systems, Novosibirsk, Russia, 1993 (ISBN 5762304108, in Russian). RSCI indexed.
Abstract: AFP_2 is a calculus of finite nondeterministic processes proposed by Kotov V.E. and
Cherkasova L.A.. Every formula of the
algebra can be transformed into a unique up to isomorphism canonical form with the axiom system for the
semantic equivalence. We construct a term rewrite system intended for automatic transformation every
formula of AFP_2 into canonical form. A computer program is designed that implements the rules of the
term rewrite system.
Keywords: calculus AFP_2, semantic equivalence, axiom system, canonical form, term rewrite
system, implementation.
 1992
 Tarasyuk I.V.
Transformation formulas of algebra AFP_2 into canonical form.
Bachelor's Thesis, Chair of Computing Systems, Department of Mathematics and
Mechanics, Novosibirsk State University, 47 pages, Novosibirsk, Russia, 1992 (in Russian).
Abstract: AFP_2 is a calculus of finite nondeterministic processes proposed by Kotov V.E. and
Cherkasova L.A.. Every formula of the
algebra can be transformed into a unique up to isomorphism canonical form with the axiom system for the
semantic equivalence. The canonical form is essentially a syntactic form of the set of partial orders
(posets) with actions, nonactions and deadlocked actions as elements. Every set of posets corresponds to
the nondeterministic process that the initial formula specifies. We construct a term rewrite system
intended for automatic transformation every formula of AFP_2 into canonical form. A computer program is
designed that implements the rules of the term rewrite system.
Keywords: calculus AFP_2, semantic equivalence, axiom system, canonical form, term rewrite
system, implementation.
