arXiv subjects

Igor V. Tarasyuk

Publications and source records attributed to Igor V. Tarasyuk.

4 recordsLinked to original sources

arXiv2026

Discrete time phased Petri box calculus dtphPBC

We propose discrete time phased Petri box calculus (dtphPBC), an extension with phase type distributed multiaction delays of discrete time stochastic and deterministic Petri box calculus (dtsdPBC), previously presented by I.V. Tarasyuk. In dtphPBC, transition probability matrices (TPMs) of finite absorbing discrete time Markov chains (DTMCs) with a single absorbing state specify discrete phase type (DPH) distributed delays (including zero delay) of the phased multiactions that generalize stochastic and deterministic multiactions from dtsdPBC. The positively phased (timed) multiactions have positive DPH delays represented by the non-empty TPM matrices over transient states (transient TPMs). The zero phased (immediate) multiactions have zero DPH delay represented by the empty transient TPM. The step operational semantics of dtphPBC is constructed via labeled probabilistic transition systems. The transition systems incorporate the absorbing DTMCs of the DPH delays of the executed phased multiactions via the structural operational semantics (SOS) rules. The SOS rules define a labeling with the empty set on the transitions among transient states of the absorbing DTMC and on the self-loop in the absorbing state of it. The transitions going from the transient states (positive phases) to the absorbing state (zero phase) are labeled with the executions, being the positive phases-superscribed timed multiactions whose (positive) delays are defined by the absorbing DTMC. A series of examples demonstrates how to construct the transition systems of the dynamic expressions, combined from timed and immediate multiactions with different operations of the calculus.

cs.LO↗

arXiv2019

Discrete time stochastic and deterministic Petri box calculus

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. Macià 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.

cs.LO↗

arXiv2017

Behavioural equivalences for fluid stochastic Petri nets

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 take into account the essential features of the LFSPNs behaviour: functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose continuous markings have no influence to the discrete ones and whose discrete part is 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 aggregated 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 via quotienting the discrete reachability graph and underlying CTMC. To describe the quotient associated SFM, the quotients of the probability functions are defined. We characterize logically fluid trace and bisimulation equivalences with two novel fluid modal logics $HML_{flt}$ and $HML_{flb}$, based on the Hennessy-Milner Logic HML. The application example of a document preparation system demonstrates the behavioural analysis via quotienting by fluid bisimulation equivalence.

cs.LO↗

arXiv2017

Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC

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. Macià, 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.

cs.LO↗