Sibirskie Èlektronnye Matematicheskie Izvestiya [Siberian Electronic Mathematical Reports]
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Sib. Èlektron. Mat. Izv.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Sibirskie Èlektronnye Matematicheskie Izvestiya [Siberian Electronic Mathematical Reports], 2023, Volume 20, Issue 2, Pages 646–699
DOI: https://doi.org/10.33048/semi.2023.20.039
(Mi semr1602)
 

Computational mathematics

Performance preserving equivalence for stochastic process algebra dtsdPBC

I. V. Tarasyuk

A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences, Acad. Lavrentiev pr. 6, 630090 Novosibirsk, Russian Federation
References:
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.
Received May 16, 2022, published July 31, 2023
Document Type: Article
UDC: 004.423.4, 519.217.2,519.681
Language: English
Citation: I. V. Tarasyuk, “Performance preserving equivalence for stochastic process algebra dtsdPBC”, Sib. Èlektron. Mat. Izv., 20:2 (2023), 646–699
Citation in format AMSBIB
\Bibitem{Tar23}
\by I.~V.~Tarasyuk
\paper Performance preserving equivalence for stochastic process algebra dtsdPBC
\jour Sib. \`Elektron. Mat. Izv.
\yr 2023
\vol 20
\issue 2
\pages 646--699
\mathnet{http://mi.mathnet.ru/semr1602}
\crossref{https://doi.org/10.33048/semi.2023.20.039}
Linking options:
  • https://www.mathnet.ru/eng/semr1602
  • https://www.mathnet.ru/eng/semr/v20/i2/p646
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Statistics & downloads:
    Abstract page:216
    Full-text PDF :8
    References:10
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024