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
Math-Net.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.
- 2024
- Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives hal-02573419v5
(version 5), 157 pages, France, January 2024.
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, non-negative 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 dtsd-boxes, 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 semi-Markov 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 well-known 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, dtsd-box, denotational semantics, Markov
chain, performance evaluation, reduction, stochastic bisimulation, quotient, shared memory system.
- Tarasyuk I.V.
Comparing dtsdPBC with other stochastic process algebras.
ResearchGate
Preprint 380669323, 70 pages, May 2024. DOI:
10.13140/RG.2.2.19344.21769. The formerly prepared
journal version.
Abstract: Petri box calculus (PBC) is a well-known algebra of parallel processes with a Petri net semantics. Discrete time stochastic and
deterministic PBC (dtsdPBC) 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 dtsd-boxes, a subclass of labeled discrete time stochastic and deterministic
Petri nets. To evaluate performance in dtsdPBC, the underlying semi-Markov chains (SMCs) and (reduced) discrete time Markov chains (DTMCs and RDTMCs) of
the process expressions are analyzed. We determine the main positive features of dtsdPBC by comparing it with well-known or similar stochastic process
algebras. We classify them by the time model (continuous of discrete) and concept (integrated or orthogonal), probability distribution of stochastic
delays, deterministic (including immediate) (multi)actions and semantic parallelism. The detected strong points of dtsdPBC are discrete stochastic time,
deterministic multiactions and step semantics. We also discuss the analytical solution, concurrency interpretation, application area and general
advantages of dtsdPBC.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, discrete time, stochastic delay, deterministic delay, transition
system, operational semantics, time aspect, probability distribution, determinism, parallelism, comparison, classification.
- Tarasyuk I.V.
Combining embedding and elimination for performance analysis in stochastic process algebra dtsdPBC.
ResearchGate Preprint 381435160, 42 pages, June 2024. DOI:
10.13140/RG.2.2.12633.33122/3.
Abstract: Petri box calculus (PBC) is a well-known algebra of parallel processes with a Petri net semantics. Discrete time stochastic and deterministic
PBC (dtsdPBC) 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 dtsd-boxes, a subclass of labeled discrete time stochastic and deterministic Petri nets. To analyze performance
in dtsdPBC, the underlying semi-Markov chains (SMCs) and (reduced) discrete time Markov chains (DTMCs and RDTMCs) of the process expressions are built. The
underlying SMCs are extracted from the transition systems with the embedding method that constructs the embedded DTMCs (EDTMCs) and calculates the sojourn time
distributions in the states. The reductions (RDTMCs) of the DTMCs are obtained with the elimination method that removes the states with zero sojourn time
(vanishing states) and recalculates the probabilities to change the (remaining) states with positive sojourn time (tangible states). We prove that the reduced
SMC (RSMC) coincides with the RDTMC, by demonstrating that an additional embedding (into RSMC) of the reduced EDTMC is needed to coincide with the embedded RDTMC,
and by comparing the respective sojourn times.
Keywords: stochastic process algebra, Petri box calculus, discrete time, stochastic delay, deterministic delay, transition system, operational semantics,
Markov chain, performance analysis, embedding, elimination.
- Tarasyuk I.V.
Embedding and elimination for performance analysis in stochastic process algebra dtsdPBC.
International Journal of Parallel, Emergent and Distributed Systems 39(6), pages 619-652, Tailor and Francis Group, Informa UK
Public Limited Company (PLC), London, UK, December 2024 (ISSN 1744-5779).
DOI: 10.1080/17445760.2024.2417873. Web of Science, Scopus, Zentralblatt Math, DBLP indexed. JCR impact
factor (2023): 0.600 (Q4). SJR indicator (2023): 0.286 (Q3).
Abstract: dtsdPBC extends the well-known algebra of parallel processes, Petri box calculus (PBC), by incorporating discrete time stochastic and deterministic
delays. To analyze performance in this extended calculus, the underlying semi-Markov chains, and the related (complete) and reduced discrete time Markov chains of the
process expressions are built. The semi-Markov chains are extracted using the embedding method, which constructs the embedded discrete time Markov chains and calculates
the sojourn time distributions in the states. The reductions of the discrete time Markov chains are obtained through the elimination method, which removes the vanishing
states (those with zero sojourn times) and recalculates the transition probabilities among the tangible states (those with positive sojourn times). We prove that the
reduced semi-Markov chain coincides with the reduced discrete time Markov chain, by demonstrating that an additional embedding into the reduced semi-Markov chain is
needed for the reduced embedded discrete time Markov chain to match the embedded reduced discrete time Markov chain, and by comparing the respective sojourn times.
Keywords: Petri box calculus, stochastic and deterministic delays, Markov chain, performance analysis, embedding, elimination.
- 2023
- Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives hal-02573419v4
(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, non-negative 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 dtsd-boxes, 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 semi-Markov 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 well-known 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, dtsd-box, denotational semantics, Markov
chain, performance evaluation, reduction, stochastic bisimulation, quotient, shared memory system.
- Tarasyuk I.V.
Performance analysis of the shared memory system in stochastic process algebra dtsdPBC.
ResearchGate
Preprint 370215221, 60 pages, April 2023. DOI:
10.13140/RG.2.2.29410.54722.
Abstract: Petri box calculus (PBC) is a well-known algebra of parallel processes with a Petri net semantics. Discrete time stochastic and
deterministic PBC (dtsdPBC) 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 dtsd-boxes, a subclass of labeled discrete time stochastic and
deterministic Petri nets. To evaluate performance in dtsdPBC, the underlying semi-Markov chains (SMCs) and (reduced) discrete time Markov chains
(DTMCs and RDTMCs) of the process expressions are analyzed. Step stochastic bisimulation equivalence that compares the qualitative and quantitative
behaviour is used for quotienting the transition systems, SMCs, DTMCs and RDTMCs of the process expressions while preserving their stationary
behaviour and residence time properties. We construct in dtsdPBC a case study that demonstrates how the method of modeling, performance analysis and
behaviour reduction by quotienting for concurrent systems with discrete fixed and stochastic delays is applied to the generalized shared memory system
with maintenance. Such a generalized system takes as variables the probabilities and weights from the standard one's specification. Then the variable
generalized probabilities of the reduced quotient DTMC are treated as parameters to be adjusted for the performance optimization of the modeled system.
Keywords: Petri box calculus, discrete time, stochastic and deterministic delays, transition system, operational semantics, dtsd-box, denotational
semantics, Markov chain, performance, stochastic bisimulation, quotient, shared memory system, maintenance, generalized probabilities and weights.
- Tarasyuk I.V.
Performance preserving equivalence for stochastic process algebra
dtsdPBC.
Siberian Electronic Mathematical Reports 20(2), pages
646-699, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, July 2023 (ISSN 1813-3304). DOI:
10.33048/semi.2023.20.039. Web of Science, Scopus, Zentralblatt Math indexed. JCR impact
factor (2023): 0.400 (Q4). SJR indicator (2023): 0.465 (Q2). RSCI indexed.
Abstract: Petri box calculus (PBC) of E. Best, R. Devillers, J.G. Hall and M. Koutny is a well-known 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 dtsd-boxes, a subclass of labeled discrete time stochastic and deterministic Petri nets (LDTSDPNs). To evaluate performance in dtsdPBC, the
underlying semi-Markov 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 dtsd-boxes 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, dtsd-box,
denotational semantics, Markov chain, performance, stochastic bisimulation, quotient.
- 2022
- Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives hal-02573419v3
(version 3), 132 pages, France, July 2022.
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, non-negative 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 dtsd-boxes, a subclass of labeled discrete time stochastic Petri nets with deterministic transitions. 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 equivalence is established. In order to
evaluate performance in dtsdPBC, the underlying semi-Markov chains and (reduced) discrete time Markov chains of the process-algebraic expressions are
analyzed. We explain how step stochastic bisimulation equivalence of the expressions can be used for quotienting their transition systems and
corresponding 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 well-known
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, dtsd-box, denotational semantics, Markov chain, performance
evaluation, reduction, stochastic bisimulation, quotient, shared memory system.
- Tarasyuk I.V.
Performance preserving equivalence for stochastic process algebra dtsdPBC.
ResearchGate
Preprint 362034663, 62 pages, July 2022. DOI:
10.13140/RG.2.2.36121.43367.
Abstract: Petri box calculus (PBC) of E. Best, R. Devillers, J.G. Hall and M. Koutny is a well-known 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 dtsd-boxes, a subclass of labeled discrete time stochastic and deterministic Petri nets (LDTSDPNs). To evaluate performance in dtsdPBC, the
underlying semi-Markov 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 dtsd-boxes 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, dtsd-box,
denotational semantics, Markov chain, performance, stochastic bisimulation, quotient.
- 2021
- Tarasyuk I.V.
Performance evaluation in stochastic process algebra dtsdPBC.
ResearchGate
Preprint 352878216, 47 pages, July 2021. DOI:
10.13140/RG.2.2.10536.17922.
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 well-known 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 non-negative 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 semi-Markov 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 non-stop 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.
- Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives hal-02573419v2
(version 2), 115 pages, France, September 2021.
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, non-negative 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. 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 equivalence is established. In order to evaluate performance in
dtsdPBC, the corresponding semi-Markov chains and (reduced) discrete time Markov chains of the process-algebraic expressions are analyzed. We explain
how step stochastic bisimulation equivalence of the expressions can be used to reduce their transition systems and underlying semi-Markov chains, as
well as to compare the stationary behaviour. 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.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, discrete time, stochastic multiaction, deterministic multiaction,
transition system, operational semantics, stochastic transition, deterministic transition, dtsd-box, denotational semantics, Markov chain, performance
evaluation, stochastic bisimulation, reduction, shared memory system.
- Tarasyuk I.V.
Performance evaluation in stochastic process algebra dtsdPBC.
Siberian Electronic Mathematical Reports 18(2), pages
1105-1145, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, October 2021 (ISSN 1813-3304). 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 well-known 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 non-negative 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 semi-Markov 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 non-stop 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.
Discrete time stochastic and deterministic Petri box calculus dtsdPBC.
ResearchGate
Preprint 341702320, 47 pages, March 2020. DOI:
10.13140/10.13140/RG.2.2.34024.28166/1.
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, non-negative integers are used to specify fixed (including zero) time delays of deterministic multiactions. The
step operational semantics is constructed via labeled probabilistic transition systems. A series of examples that construct the transition systems 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, Petri box calculus, discrete time, stochastic multiaction, deterministic multiaction, transition system, operational
semantics, semantic example.
- Tarasyuk I.V.
Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus
dtsdPBC.
HAL Open Archives
hal-02573419v1 (version 1), 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, non-negative 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 semi-Markov 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 semi-Markov 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, dtsd-box, 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
1598-1679, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, October 2020 (ISSN 1813-3304). 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, non-negative 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 dtsd-boxes, 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 dtsd-boxes 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, dtsd-box, 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, non-negative 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 semi-Markov 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, dtsd-box, denotational semantics, Markov chain, reduction, performance evaluation.
DFG BE 1267/14-1
- Tarasyuk I.V.,
Buchholz P.
Logical characterization of fluid equivalences.
Siberian Electronic Mathematical Reports 16, pages
826-862, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, June 2019 (ISSN 1813-3304). 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 linear-time relation of
fluid trace equivalence and its branching-time 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 well-known Hennessy-Milner 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/14-1
- 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 DIAB-18-05-1, 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 semi-Markov 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 semi-Markov 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 well-known or similar SPAs.
Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, performance evaluation, stochastic
equivalence.
Spanish Government TIN2015-65845-C03-02, DFG BE 1267/14-1
- 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
1743-1812, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, December 2018 (ISSN 1813-3304). 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 semi-Markov chains are analyzed. We define step stochastic bisimulation equivalence of expressions that is
applied to reduce their transition systems and underlying semi-Markov 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,
semi-Markov chain, performance evaluation, stochastic equivalence, reduction.
Spanish Government TIN2015-65845-C03-02, DFG BE 1267/14-1
- 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 semi-Markov chains are analyzed. We define step stochastic bisimulation
equivalence of expressions that is applied to reduce their transition systems and underlying semi-Markov 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 TIN2015-65845-C03-02, DFG BE 1267/14-1
- Tarasyuk I.V.,
Buchholz P.
Equivalences for fluid stochastic Petri nets.
Siberian Electronic Mathematical Reports 14,
pages 317-366, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, April 2017 (ISSN 1813-3304). 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 linear-time relation of fluid trace equivalence and its branching-time
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/14-1, RFBR 14-01-91334
- 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 linear-time relation of fluid trace equivalence and its branching-time
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 well-known Hennessy-Milner 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/14-1, RFBR 14-01-91334
- 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 10-11, 2017,
Lecture Notes in Computer Science 10378, pages 16-31, Springer, Germany, 2017 (ISSN 0302-9743, ISBN
978-3-319-61428-1). DOI: 10.1007/978-3-319-61428-1 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/14-1
- 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 475-493, Natural Sciences Publishing, New York, NY, USA, March 2016 (ISSN 1935-0090). 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 TIN2012-36812-C02-02, DFG BE 1267/14-1, RFBR 14-01-91334
- 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 DIAB-16-03-1, 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
semi-Markov 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 semi-Markov 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 TIN2012-36812-C02-02, DFG BE 1267/14-1, RFBR 14-01-91334
- 2015
- Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic process reduction for performance evaluation in
dtsiPBC.
Siberian Electronic Mathematical Reports 12,
pages 513-551, S.L. Sobolev Institute of Mathematics, Novosibirsk, Russia, September 2015 (ISSN 1813-3304). 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 well-known 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 semi-Markov chains of the algebraic process expressions but also by exploring the reduced discrete time Markov
chains, obtained from the semi-Markov 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 TIN2012-36812-C02-02, DFG BE 1267/14-1, RFBR 14-01-91334
- 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 121-149, NCC Publisher, Novosibirsk, Russia, 2015 (ISSN 1680-6972). DOI:
10.31144/bncc.cs.2542-1972.2015.n38.p121-150.
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/14-1, RFBR 14-01-91334
- 2014
- Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Stochastic equivalence for performance evaluation of concurrent systems in dtsiPBC.
Technical Report DIAB-14-01-1, 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 semi-Markov
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 semi-Markov 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 semi-Markov 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 TIN2012-36812-C02-02
- Tarasyuk I.V.
Equivalence relations for modular performance evaluation
in dtsPBC.
Mathematical Structures in
Computer Science 24(1), pages 78-154 (e240103), Cambridge University Press, Cambridge, UK, February 2014 (ISSN
0960-1295). 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 09-01-91334
- Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Performance analysis of concurrent systems in algebra
dtsiPBC.
Programming 40(5),
pages 3-27, MAIK Nauka/Interperiodica, Moscow, Russia, September 2014 (ISSN 0132-3474, in Russian). RSCI indexed. RSCI impact factor
(2013): 0.371.
Abstract: Petri box calculus PBC is a well-known 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 semi-Markov 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, dtsi-boxes, performance analysis, Markov chains.
Spanish Government TIN2012-36812-C02-02, DFG BE 1267/14-1, RFBR 14-01-91334
- Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Performance analysis of concurrent systems in algebra dtsiPBC.
Programming and Computer Software
40(5), pages 229-249, Pleiades Publishing, Ltd., September 2014 (ISSN 0361-7688). 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 well-known 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 semi-Markov 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, dtsi-boxes, performance analysis, Markov chains.
Spanish Government TIN2012-36812-C02-02, DFG BE 1267/14-1, RFBR 14-01-91334
- 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 229-252, Elsevier, August 2013 (ISSN 1571-0661). 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 semi-Markov 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 105-135, Siberian State University of Telecommunications
and Information Sciences, Novosibirsk, Russia, 2012 (ISSN 1998-6920, 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. tau-equivalences are relations which abstract from silent
actions corresponding to internal activity of the modeled system. The basic tau-equivalences 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 equivalence-preserving reduction of a Petri net that models the
well-known dining philosophers system. The decidability results for basic tau-equivalences are outlined.
Keywords: Petri nets, invisible transitions, basic tau-equivalences, Petri nets with visible transitions,
sequential Petri nets, reduction, decidability.
DFG 436 RUS 113/1002/01, RFBR 09-01-91334
- Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Discrete time stochastic Petri box calculus
with immediate multiactions.
Pre-proceedings 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 semi-Markov 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 DIAB-12-10-2, 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
semi-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 semi-Markov 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 DIAB-11-06-2, 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 semi-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 semi-Markov 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, dtsi-box, denotational semantics,
Markov chain, performance evaluation, stochastic equivalence, reduction, shared memory system.
UCLM Invited Researchers, DFG 436 RUS 113/1002/01, RFBR 09-01-91334
- Tarasyuk I.V.
Performance analysis of the dining philosophers
system in dtsPBC.
Pre-proceedings of 8th Ershov Informatics Conference - 11 (PSI'11)
(E. Clarke, I.B. Virbitskaite, A. Voronkov, eds.), Novosibirsk, Russia, June 27 - July 1, 2011, pages 309-321,
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 09-01-91334
- 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 1867-9218). 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 09-01-91334
- 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 127-155, NCC Publisher, Novosibirsk, Russia, 2011
(ISSN 1680-6972). 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 09-01-91334
- 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 8-11, 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. tau-equivalences are relations which abstract from silent
actions corresponding to internal activity of the modeled system. The basic tau-equivalences known from
the literature are supplemented by new notions. The interrelations of all the considered tau-equivalences
are determined. We present an example of equivalence-preserving reduction of a Petri net that models the
well-known dining philosophers system.
Keywords: Petri nets, invisible transitions, basic tau-equivalences, reduction.
DFG 436 RUS 113/1002/01, RFBR 09-01-91334
- 2010
- Tarasyuk I.V.,
Macia S.H.,
Valero R.V.
Discrete time stochastic Petri box calculus with immediate multiactions.
Technical
Report DIAB-10-03-1, 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, dtsi-box,
denotational semantics, Markov chain, performance evaluation, shared memory system.
DFG 436 RUS 113/1002/01, RFBR 09-01-91334
- Tarasyuk I.V.
Equivalence
relations for behaviour-preserving 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 1867-9218). RSCI indexed.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was
constructed to specify stochastic processes within the well-developed 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, dts-box, denotational semantics, empty loop, stochastic
equivalence, reduction, modal logic, stationary behaviour, congruence relation, performance evaluation.
DFG 436 RUS 113/1002/01, RFBR 09-01-91334
- Tarasyuk I.V.
Performance preserving equivalences for
dtsPBC.
Bulletin of the Novosibirsk
Computing Center, Series Computer Science, IIS Special Issue 31, pages 155-178, NCC Publisher,
Novosibirsk, Russia, 2010 (ISSN 1680-6972). 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 09-01-91334
- 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.), Krakow-Przegorzaly, Poland,
September 28-30, 2009, Volume
2, pages 602-615, 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 09-01-91334
- 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 90-117, Novosibirsk State
University, Novosibirsk, Russia, 2009 (ISSN 1818-7897, in Russian). RSCI indexed. RSCI impact factor (2009): 0.035.
Abstract: Petri box calculus PBC is a well-known 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, dts-box, denotational semantics, stochastic equivalence,
modeling, performance analysis, reduction.
DFG 436 RUS 113/1002/01, RFBR 09-01-91334
- 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 1867-9218).
RSCI indexed.
Abstract: In the last decades, a number of stochastic enrichments of process algebras was
constructed to specify stochastic processes within the well-developed 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, dts-box, 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 121-141, NCC Publisher,
Novosibirsk, Russia, 2008 (ISSN 1680-6972). 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 09-01-91334
- 2007
- Tarasyuk I.V.
Stochastic Petri box calculus with discrete
time.
Fundamenta Informaticae
76(1-2), pages 189-218,
IOS Press, Amsterdam, The Netherlands, February 2007 (ISSN 0169-2968).
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 well-developed
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 (dts-boxes). 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, dts-boxes, denotational semantics, empty loops,
probabilistic equivalences.
- Tarasyuk I.V.
Equivalences for behavioural analysis of
concurrent and distributed computing systems. 321 pages,
"Geo" Academic Publisher, Novosibirsk, Russia, 2007 (ISBN 978-5-9747-0098-9,
in Russian). RSCI indexed.
Abstract: In the monograph, a wide range of behavioral equivalences has been proposed and
investigated on the well-known 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,
back-forth 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
post-graduate 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 14-42, Novosibirsk
State University, Novosibirsk, Russia, 2006 (ISSN 1818-7897, 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
well-known 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 129-148,
NCC Publisher, Novosibirsk, Russia, 2006 (ISSN 1680-6972). 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 well-developed 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 (dts-boxes). Consistency of both semantics is demonstrated.
Keywords: stochastic Petri nets, stochastic process algebras, Petri box calculus, iteration,
discrete time, transition systems, operational semantics, dts-boxes, 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 1867-9218).
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 well-developed
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 (dts-boxes). 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, dts-boxes, denotational semantics, empty loops,
probabilistic equivalences.
DAAD A/05/05334
- 2004
- Tarasyuk I.V.
Logical characterization of probabilistic tau-bisimulation equivalences.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 20,
pages 97-111, Novosibirsk, Russia, 2004 (ISSN 1680-6972). Zentralblatt Math indexed. RSCI indexed.
Abstract: Stochastic Petri nets (SPNs) is a well-known 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 tau-bisimulation 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 tau-bisimulation 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
135-194, SB RAS Publisher, Novosibirsk, Russia, 2004 (ISSN 0132-3474, in Russian). RSCI indexed.
Abstract: Petri nets (PNs) are a well-known 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 well-known 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, inhibitor-priority 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 31-64, Novosibirsk, Russia, 2001 (ISSN 1680-6972). 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 well-known 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 00-01-00898, STYS RAS, SPYS RAS
- 2000
- Tarasyuk I.V.
Tau-equivalences and refinement for Petri nets based design.
Technische
Berichte TUD-FI00-11, 41 pages, Fakultaet Informatik, Technische Universitaet Dresden,
Germany, November 2000 (ISSN 1430-211X). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioral equivalences of concurrent
systems modeled by Petri nets with silent transitions. Basic tau-equivalences and back-forth
tau-bisimulation 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
back-forth tau-equivalences, refinement.
GRP TUD DFG, RFBR 00-01-00898
- Tarasyuk I.V.
Tau-equivalences 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 tau-equivalences and back-forth tau-bisimulation
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 back-forth 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 TUD-FI00-12, 18 pages, Fakultaet Informatik, Technische Universitaet Dresden,
Germany, November 2000 (ISSN 1430-211X). 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 well-known 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 00-01-00898
- 1999
- Tarasyuk I.V.
Tau-equivalences 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 47-51, Novosibirsk, Russia, 1999 (ISSN 1680-6972). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural equivalences for Petri
nets with silent transitions (tau-equivalences). Basic tau-equivalences and back-forth
tau-bisimulation 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 tau-equivalences, back-forth
tau-bisimulation equivalences, sequential nets, refinement.
INTAS-RFBR 95-0378, 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 1867-9218).
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 162-175, Pleiades Publishing, Ltd., July - August 1998 (ISSN 0361-7688).
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, INTAS-RFBR 95-0378, FPYS SB RAS
- Tarasyuk I.V.
Tau-equivalences 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 22-27, 1998, pages 56-56, S.L.
Sobolev Institute of Mathematics SB RAS, Novosibirsk, Russia, 1998 (ISBN 5-86134-050-1). RSCI indexed.
Abstract: Tau-equivalences are relations which abstract from silent actions. In this paper,
on Petri nets with silent transitions (those labeled with silent actions), we consider basic
tau-equivalences such as trace, bisimulation and conflict preserving ones. Moreover, we investigate a
set of back-forth 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, tau-equivalences, refinement, sequential nets.
INTAS-RFBR 95-0378, FPYS SB RAS
- Tarasyuk I.V.
Place bisimulation equivalences for design of concurrent systems.
Pre-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 27-29, 1998,
FIMU Report Series FIMU-RS-98-06, pages 184-198, Faculty of
Informatics, Masaryk University, Brno, Czech Republic, July 1998. RSCI indexed.
Abstract: In this paper, we supplement the set of basic and back-forth 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 top-down 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, back-forth and place bisimulation equivalences,
refinement.
VS I/70 564, INTAS-RFBR 95-0378, 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 27-29, 1998,
Electronic Notes in Theoretical Computer
Science 18, pages 191-206, Elsevier, 1998 (ISSN 1571-0661). DOI:
10.1016/S1571-0661(05)80260-9. Scopus, DBLP indexed.
SJR indicator (1999): 0.333 (Q2). RSCI indexed.
Abstract: In this paper, we supplement the set of basic and back-forth 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 top-down 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, back-forth and place bisimulation equivalences,
refinement, sequential nets.
VS I/70 564, INTAS-RFBR 95-0378, FPYS SB RAS, DAAD A/98/38518
- Tarasyuk I.V.
Tau-equivalences and refinement.
Proceedings of International Refinement Workshop and Formal Methods Pacific - 98
(IRW/FMP'98), Work-in-Progress Papers (J. Grundy, M. Schwenke, T.
Vickers, eds.), Canberra, Australia, September 29 - October 2, 1998,
Joint Computer Science Technical Report Series TR-CS-98-09, pages 110-128,
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 tau-equivalences and back-forth tau-bisimulation 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 tau-equivalences, back-forth
tau-bisimulation equivalences, refinement.
INTAS-RFBR 95-0378, FPYS SB RAS
- Tarasyuk I.V.
Notions of equivalence for development of concurrent systems with use of Petri nets.
Programming
4, pages 19-39, MAIK Nauka/Interperiodica, Moscow, Russia, 1998 (ISSN 0132-3474, 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, INTAS-RFBR 95-0378, 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 multi-event structure equivalences are proposed in addition
to the well-known 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 SM-refinements.
Keywords: Petri nets, sequential nets, equivalences, SM-refinement.
INTAS-RFBR 95-0378, 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
57-79, Novosibirsk, Russia, 1998 (ISSN 1680-6972). Zentralblatt Math indexed. RSCI indexed.
Abstract: The paper is contributed to develop a family of equivalence notions for real-time 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 (time-sensitive), untimed
(time-abstracting) 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 state-machine 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.
INTAS-RFBR 95-0378, ISSEP a97-683, FPYS SB RAS
- 1997
- Tarasyuk I.V.
Back-forth 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 6-12, 1997, Lecture Notes in Computer Science 1234,
pages 374-384, Springer, Germany, 1997 (ISSN 0302-9743, ISBN 978-3-540-63045-6). DOI:
10.1007/3-540-63045-7_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. Back-forth 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, back-forth bisimulation equivalences, sequential nets, refinement.
VS I/70 564, RFBR 96-01-01655
- Tarasyuk I.V.
An investigation of back-forth and place bisimulation
equivalences.
Hildesheimer Informatik-Berichte 8/97,
30 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, April 1997 (ISSN 0941-3014). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural equivalences of concurrent systems modelled by
Petri nets. Back-forth 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 top-down design.
Keywords: Petri nets, sequential nets, basic equivalences, back-forth bisimulations, place bisimulations,
refinement.
VS I/70 564, RFBR 96-01-01655
- Tarasyuk I.V.
An investigation of tau-equivalences.
Hildesheimer Informatik-Berichte 9/97,
28 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, April 1997 (ISSN 0941-3014). RSCI indexed.
Abstract: The paper is devoted to the investigation of behavioural
equivalences of concurrent systems modelled by Petri nets with silent transitions. Basic tau-equivalences and
back-forth tau-bisimulation 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 tau-equivalences, back-forth
tau-bisimulation equivalences, refinement.
VS I/70 564, INTAS-RFBR 95-0378
- 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 57-84,
Novosibirsk, Russia, 1997 (ISSN 1680-6972). 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. Back-forth 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, back-forth bisimulation equivalences, place bisimulation
equivalences, sequential nets, refinement.
VS I/70 564, INTAS-RFBR 95-0378
- 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 82-84, Fortaleza (Ceara), Brazil, August 19-22, 1997, Grafica JB Ltda., Paraiba,
Brazil, 1997 (ISSN 1367-0751). 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 tau-variants 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 SM-refinement is investigated to have information which relations may
be used for top-down design.
Keywords: time and untime Petri nets, silent transitions, timed, untimed and region equivalences,
trace and bisimulation semantics.
VS I/70 564, ISSEP a97-683, RFBR 96-01-01655
- 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 921-923, 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 real-time 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 SM-refinement 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 SM-refinement.
VS I/70 564, ISSEP a97-683, RFBR 96-01-01655
- 1996
- Tarasyuk I.V.
Equivalence notions for design of concurrent systems using Petri
nets.
Hildesheimer Informatik-Berichte 4/96,
part 1, 19 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, January 1996 (ISSN 0941-3014).
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 top-down 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 96-01-01655
- Tarasyuk I.V.
Algebra AFLP_2: a calculus of labelled nondeterministic processes.
Hildesheimer Informatik-Berichte 4/96,
part 2, 18 pages, Institut fuer Informatik, Universitaet Hildesheim, Germany, January 1996 (ISSN 0941-3014).
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, A-nets, behavioural equivalences, bisimulation, congruence.
VS I/70 564, RFBR 96-01-01655
- 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 25-27, 1996,
Informatik-Berichte 69, pages 190-204, Institut fuer Informatik,
Humboldt-Universitaet zu Berlin, Berlin, Germany, 1996 (ISSN 0863-095). 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
T-nets (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 96-01-01655
- Tarasyuk I.V.
An algebra of labelled nondeterministic processes.
Joint Novosibirsk
Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science 5,
pages 83-100, Novosibirsk, Russia, 1996 (ISSN 1680-6972). 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 96-01-01655
- 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 682-682, Russian Foundation for Basic Research, Nauchnyj Mir, Moscow, Russia, 1996
(ISBN 5-89176-001-0, in Russian). RSCI indexed.
RFBR 96-01-01655
- 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 89-101, Computing
Center SB RAS, Novosibirsk, Russia, 1995 (ISSN 1680-6972). Zentralblatt Math indexed. RSCI indexed.
INTAS 1010-CT93-0048
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, T-nets and nets with strict
labelling.
Keywords: Petri nets, behavioural equivalences, sequential nets, T-nets, 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 15-17, Irkutsk, Russia, 1995, pages 74-75,
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, T-nets without autoconcurrency and strictly
labelled nets.
Keywords: Petri nets, equivalences, sequential nets, autoconcurrency-free T-nets, strictly labelled
nets.
RFBR 93-01-00986
- 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 22-49, Institute
of Informatics Systems, Novosibirsk, Russia, 1995 (ISBN 5-7623-1069-8, 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, A-nets, behavioural equivalences, bisimulation, congruence.
RFBR 93-01-00986
- 1994
- Tarasyuk I.V.
Equivalences on Petri nets.
Specification, Verification and Net Models of Concurrent Systems
(V.A. Nepomniaschy, ed.), pages 35-57, Institute of
Informatics Systems, Novosibirsk, Russia, 1994 (ISBN 5-7623-0410-8). 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 93-01-00986
- 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, ST-bisimulation, 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, T-nets 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_2-formula comparison for semantic equivalence is presented.
Keywords: Petri nets, semantic equivalences, sequential nets, T-nets, 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 47-59, Institute of
Informatics Systems, Novosibirsk, Russia, 1993 (ISBN 5-7623-0410-8, 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, non-actions 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.
|
