Geodesic
Performance preserving equivalence for stochastic process algebra dtsdPBC
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 20 (2023) no. 2, pp. 646-699

Voir la notice de l'article provenant de la source Math-Net.Ru

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, performance, stochastic bisimulation
Mots-clés : Markov chain, quotient. 
@article{SEMR_2023_20_2_a53,
     author = {I. V. Tarasyuk},
     title = {Performance preserving equivalence for stochastic process algebra {dtsdPBC}},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {646--699},
     publisher = {mathdoc},
     volume = {20},
     number = {2},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2023_20_2_a53/}
}
TY  - JOUR
AU  - I. V. Tarasyuk
TI  - Performance preserving equivalence for stochastic process algebra dtsdPBC
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2023
SP  - 646
EP  - 699
VL  - 20
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2023_20_2_a53/
LA  - en
ID  - SEMR_2023_20_2_a53
ER  - 
%0 Journal Article
%A I. V. Tarasyuk
%T Performance preserving equivalence for stochastic process algebra dtsdPBC
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2023
%P 646-699
%V 20
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2023_20_2_a53/
%G en
%F SEMR_2023_20_2_a53
I. V. Tarasyuk. Performance preserving equivalence for stochastic process algebra dtsdPBC. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 20 (2023) no. 2, pp. 646-699. http://geodesic.mathdoc.fr/item/SEMR_2023_20_2_a53/