# Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC

## TL;DR

This paper introduces an extension of discrete time stochastic Petri calculus with immediate multiactions, enabling simplified performance analysis of concurrent systems through bisimulation equivalence and case studies.

## Contribution

It presents a novel algebra dtsiPBC combining immediate multiactions with discrete time stochastic Petri nets, along with a bisimulation method for performance-preserving reduction.

## Key findings

- Bisimulation equivalence effectively reduces transition systems.
- The approach simplifies performance evaluation of concurrent systems.
- Case study demonstrates practical application to shared memory systems.

## 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. Maci\`a, 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.