Dr. Igor Valerievich Tarasyuk

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
1. 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.
2023
1. 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.
2. Tarasyuk I.V. Performance analysis of the shared memory system in stochastic process algebra dtsdPBC. ResearchGate Preprint 370215221, 60 pages, April 2023.
  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.
3. 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. 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
1. 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.
2. Tarasyuk I.V. Performance preserving equivalence for stochastic process algebra dtsdPBC. ResearchGate Preprint 362034663, 62 pages, July 2022.
  Abstract: Petri box calculus (PBC) of E. Best, R. Devillers, J.G. Hall and M. Koutny is a 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
1. Tarasyuk I.V. Performance evaluation in stochastic process algebra dtsdPBC. ResearchGate Preprint 352878216, 47 pages, July 2021.
  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.
2. 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.
3. 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
1. 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.
2. 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
1. 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
2. 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
1. 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
2. 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
1. 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
2. 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
3. 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
4. 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
1. 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
2. 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
1. 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
2. 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
1. 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
2. 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
3. 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
4. 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
1. 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
1. 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
2. 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
3. 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
1. 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
2. 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
3. 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
4. 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
5. 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
1. 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
2. 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
3. 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
1. 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
2. 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
1. 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
2. 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
1. 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.
2. 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
1. 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.
2. 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
1. 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
1. 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.
2. 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
1. 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
1. 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
2. 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
3. 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
1. 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
2. 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
1. 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
2. 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
3. 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
4. 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
5. 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
6. 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
7. 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
8. 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
1. 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
2. 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
3. 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
4. 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
5. 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.
6. 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.
7. 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
8. 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
1. 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
2. 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
3. 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
4. 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
5. 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
1. 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.
2. 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
3. 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
1. 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
2. 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
1. 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
1. 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.