Discrete time stochastic and deterministic Petri box calculus

TL;DR

This paper introduces an extended Petri calculus with deterministic timing for multiactions, combining stochastic and deterministic models, and analyzes their semantics and performance through probabilistic and Markov chain methods.

Contribution

It extends discrete time stochastic Petri calculus with deterministic timing, providing new semantics and performance analysis tools.

Findings

Semantics are consistent between operational and denotational models.

Performance evaluation is achieved through semi-Markov and Markov chain analysis.

The extended calculus captures both stochastic and deterministic timing behaviors.

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

Tables

Table 1. Table 4: Comparison of inaction, action and empty move rules

Rules	State change	Time progress	Activities execution
Inaction rules	$-$	$-$	$-$
Action rules	$\pm$	$+$	$+$
(stochastic or waiting multiactions)
Action rules	$\pm$	$-$	$+$
(immediate multiactions)
Empty move rule	$-$	$+$	$-$

Equations

$$\gamma(x)=\left\{\begin{array}[]{ll}\alpha(x)+\beta(x)-1,&x=a\mbox{ or }x=\hat{a};\\ \alpha(x)+\beta(x),&\mbox{otherwise}.\end{array}\right.$$

$$E::=(\alpha ,\kappa )\mid (\alpha ,{♮}_l^{\theta }{)}^{\delta }\mid E;E\mid E[]E\mid E\Vert E\mid E[f]\mid E\mathsf{rs}a\mid E\mathsf{sy}a\mid [E\ast E\ast E].$$

$$\begin{array}[]{c}E::=\ (\alpha,\kappa)\mid(\alpha,\natural_{l}^{\theta})^{\delta}\mid E;E\mid E[]E\mid E\|E\mid E[f]\mid E\ {\sf rs}\ a\mid E\ {\sf sy}\ a\mid[E*D*E],\\ \mbox{where }D::=\ (\alpha,\kappa)\mid(\alpha,\natural_{l}^{\theta})^{\delta}\mid D;E\mid D[]D\mid D[f]\mid D\ {\sf rs}\ a\mid D\ {\sf sy}\ a\mid[D*D*E].\end{array}$$

$$G::=\overline{E}\mid \underline{E}\mid G;E\mid E;G\mid G[]E\mid E[]G\mid G\Vert G\mid G[f]\mid G\mathsf{rs}a\mid G\mathsf{sy}a\mid [G\ast E\ast E]\mid [E\ast G\ast E]\mid [E\ast E\ast G].$$

$$\begin{array}[]{ll}\overline{(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})}\Rightarrow\overline{(\{a\},\natural_{1}^{3})}[](\{b\},\frac{1}{3})\Rightarrow\overline{(\{a\},\natural_{1}^{3})^{3}}[](\{b\},\frac{1}{3}),&\overline{(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})}\Rightarrow(\{a\},\natural_{1}^{3})[]\overline{(\{b\},\frac{1}{3})}.\end{array}$$

$$\begin{array}[]{c}G=(\{a\},\natural_{1}^{3})[]\overline{(\{b\},\frac{1}{3})}\approx\overline{(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})}\approx\overline{(\{a\},\natural_{1}^{3})}[](\{b\},\frac{1}{3})\approx\overline{(\{a\},\natural_{1}^{3})^{3}}[](\{b\},\frac{1}{3})=H.\end{array}$$

$$\begin{array}[]{c}H=\overline{(\{a\},\natural_{1}^{3})^{3}}[](\{b\},\frac{1}{3})\approx\overline{(\{a\},\natural_{1}^{3})^{3}[](\{b\},\frac{1}{3})}\approx(\{a\},\natural_{1}^{3})^{3}[]\overline{(\{b\},\frac{1}{3})}=G_{1}=\widetilde{G}.\end{array}$$

$$\begin{array}[]{ll}\circlearrowleft\!(\overline{(\{a\},\natural_{1}^{3})^{3}}[](\{b\},\frac{1}{3}))=\overline{(\{a\},\natural_{1}^{3})^{2}}[](\{b\},\frac{1}{3}),&\circlearrowleft\!((\{a\},\natural_{1}^{3})^{3}[]\overline{(\{b\},\frac{1}{3})})=(\{a\},\natural_{1}^{3})^{2}[]\overline{(\{b\},\frac{1}{3})}.\end{array}$$

$$Cont(\iota)=\left\{\begin{array}[]{ll}\{\iota\},&\iota\in I\!\!N;\\ Cont(\iota_{1})\cup Cont(\iota_{2}),&\iota=(\iota_{1})(\iota_{2}).\end{array}\right.$$

$$Now(G)=\left\{\begin{array}[]{ll}Can(G)\cap I\!\!N_{fin}^{\cal IL},&Can(G)\cap I\!\!N_{fin}^{\cal IL}\neq\emptyset;\\ \{W\in Can(G)\cap I\!\!N_{fin}^{\cal WL}\mid\forall V\in Can(G)\cap I\!\!N_{fin}^{\cal WL}\ W\subseteq V\ \Rightarrow\ V\!=\!W\},&(Can(G)\cap I\!\!N_{fin}^{\cal IL}=\emptyset)\wedge\\ &(Can(G)\cap I\!\!N_{fin}^{\cal WL}\neq\emptyset);\\ Can(G),&\mbox{otherwise}.\end{array}\right.$$

$$PF(\Upsilon,s)=\left\{\begin{array}[]{ll}\prod_{(\alpha,\rho)\in\Upsilon}\rho\cdot\prod_{\{\{(\beta,\chi)\}\in Exec(s)\mid(\beta,\chi)\not\in\Upsilon\}}(1-\chi),&s\in DR_{ST}(G);\\ \sum_{(\alpha,\natural_{l}^{\theta})\in\Upsilon}l,&s\in DR_{WT}(G)\cup DR_{V}(G).\end{array}\right.$$

$$PF(\emptyset,s)=\left\{\begin{array}[]{ll}\prod_{\{(\beta,\chi)\}\in Exec(s)}(1-\chi),&Exec(s)\neq\{\emptyset\};\\ 1,&Exec(s)=\{\emptyset\}.\end{array}\right.$$

$$PT({\rm Y},s)=\frac{PF({\rm Y},s)}{{\sum }_{\Xi \in Exec(s)}PF(\Xi ,s)}.$$

$$PM(s,\tilde{s})=\sum _{\{{\rm Y}\mid \exists H\in s\exists \tilde{H}\in \tilde{s}H\stackrel{{\rm Y}}{\to }\tilde{H}\}}PT({\rm Y},s).$$

$$\begin{array}[]{l}\overline{(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})}\approx\overline{(\{a\},\natural_{1}^{3})^{3}}[](\{b\},\frac{1}{3})\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}\overline{(\{a\},\natural_{1}^{3})^{2}}[](\{b\},\frac{1}{3}),\\[2.84526pt] \overline{(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})}\approx(\{a\},\natural_{1}^{3})^{3}[]\overline{(\{b\},\frac{1}{3})}\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}(\{a\},\natural_{1}^{3})^{2}[]\overline{(\{b\},\frac{1}{3})}.\end{array}$$

$$\begin{array}[]{ll}s_{1}=[\overline{(\{a\},\natural_{1}^{2})^{2}}[](\{b\},\natural_{2}^{3})^{3}]_{\approx}\!=\![(\{a\},\natural_{1}^{2})^{2}[]\overline{(\{b\},\natural_{2}^{3})^{3}}]_{\approx},&s_{2}=[\overline{(\{a\},\natural_{1}^{2})^{1}}[](\{b\},\natural_{2}^{3})^{2}]_{\approx}\!=\![(\{a\},\natural_{1}^{2})^{1}[]\overline{(\{b\},\natural_{2}^{3})^{2}}]_{\approx},\\[2.84526pt] s_{3}=[\underline{(\{a\},\natural_{1}^{2})[](\{b\},\natural_{2}^{3})}]_{\approx}.&\end{array}$$

$$\begin{array}[]{ll}s_{1}=[\overline{(\{a\},\natural_{1}^{3})^{3}}[](\{b\},\frac{1}{3})]_{\approx}=[(\{a\},\natural_{1}^{3})^{3}[]\overline{(\{b\},\frac{1}{3})}]_{\approx},&s_{2}=[\overline{(\{a\},\natural_{1}^{3})^{2}}[](\{b\},\frac{1}{3})]_{\approx}=[(\{a\},\natural_{1}^{3})^{2}[]\overline{(\{b\},\frac{1}{3})}]_{\approx},\\[2.84526pt] s_{3}=[\overline{(\{a\},\natural_{1}^{3})^{1}}[](\{b\},\frac{1}{3})]_{\approx}=[(\{a\},\natural_{1}^{3})^{1}[]\overline{(\{b\},\frac{1}{3})}]_{\approx},&s_{4}=[\underline{(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})}]_{\approx}.\end{array}$$

$$\begin{array}[]{l}s_{1}=[[\overline{(\{a\},\frac{1}{2})}*(\{b\},\natural_{1}^{3})*(\{c\},\frac{1}{3})]]_{\approx},\\[4.2679pt] s_{2}=[[(\{a\},\frac{1}{2})*\overline{(\{b\},\natural_{1}^{3})^{3}}*(\{c\},\frac{1}{3})]]_{\approx}=[[(\{a\},\frac{1}{2})*(\{b\},\natural_{1}^{3})^{3}*\overline{(\{c\},\frac{1}{3})}]]_{\approx},\\[4.2679pt] s_{3}=[[(\{a\},\frac{1}{2})*\overline{(\{b\},\natural_{1}^{3})^{2}}*(\{c\},\frac{1}{3})]]_{\approx}=[[(\{a\},\frac{1}{2})*(\{b\},\natural_{1}^{3})^{2}*\overline{(\{c\},\frac{1}{3})}]]_{\approx},\\[4.2679pt] s_{4}=[[(\{a\},\frac{1}{2})*\overline{(\{b\},\natural_{1}^{3})^{1}}*(\{c\},\frac{1}{3})]]_{\approx}=[[(\{a\},\frac{1}{2})*(\{b\},\natural_{1}^{3})^{1}*\overline{(\{c\},\frac{1}{3})}]]_{\approx},\\[4.2679pt] s_{5}=[\underline{[(\{a\},\frac{1}{2})*(\{b\},\natural_{1}^{3})*(\{c\},\frac{1}{3})]}]_{\approx}.\end{array}$$

$$\begin{array}[]{ll}s_{1}=[\overline{(\{a\},\natural_{1}^{0})}\|\overline{(\{b\},\natural_{2}^{2})^{2}}\|\overline{(\{c\},\natural_{3}^{3})^{3}}]_{\approx},&s_{2}=[\underline{(\{a\},\natural_{1}^{0})}\|\overline{(\{b\},\natural_{2}^{2})^{2}}\|\overline{(\{c\},\natural_{3}^{3})^{3}}]_{\approx},\\[4.2679pt] s_{3}=[\underline{(\{a\},\natural_{1}^{0})}\|\overline{(\{b\},\natural_{2}^{2})^{1}}\|\overline{(\{c\},\natural_{3}^{3})^{2}}]_{\approx},&s_{4}=[\underline{(\{a\},\natural_{1}^{0})}\|\underline{(\{b\},\natural_{2}^{2})}\|\overline{(\{c\},\natural_{3}^{3})^{1}}]_{\approx},\\[4.2679pt] s_{5}=[\underline{(\{a\},\natural_{1}^{0})\|(\{b\},\natural_{2}^{2})\|(\{c\},\natural_{3}^{3})}]_{\approx}.&\end{array}$$

$$\begin{array}[]{lll}s_{1}=[\overline{(\{a\},\natural_{1}^{3})^{3}}\|\overline{(\{b\},\frac{1}{3})}]_{\approx},&s_{2}=[\overline{(\{a\},\natural_{1}^{3})^{2}}\|\overline{(\{b\},\frac{1}{3})}]_{\approx},&s_{3}=[\overline{(\{a\},\natural_{1}^{3})^{2}}\|\underline{(\{b\},\frac{1}{3})}]_{\approx},\\[4.2679pt] s_{4}=[\overline{(\{a\},\natural_{1}^{3})^{1}}\|\overline{(\{b\},\frac{1}{3})}]_{\approx},&s_{5}=[\overline{(\{a\},\natural_{1}^{3})^{1}}\|\underline{(\{b\},\frac{1}{3})}]_{\approx},&s_{6}=[\underline{(\{a\},\natural_{1}^{3})}\|\overline{(\{b\},\frac{1}{3})}]_{\approx},\\[4.2679pt] s_{7}=[\underline{(\{a\},\natural_{1}^{3})\|(\{b\},\frac{1}{3})}]_{\approx}.&&\end{array}$$

$$\begin{array}[]{ll}s_{1}=[(\overline{(\{a\},\natural_{1}^{2})^{2}}\|\overline{(\{\hat{a}\},\natural_{2}^{2})^{2}})\ {\sf sy}\ a\ {\sf rs}\ a]_{\approx},&s_{2}=[(\overline{(\{a\},\natural_{1}^{2})^{1}}\|\overline{(\{\hat{a}\},\natural_{2}^{2})^{1}})\ {\sf sy}\ a\ {\sf rs}\ a]_{\approx},\\[2.84526pt] s_{3}=[\underline{((\{a\},\natural_{1}^{2})\|(\{\hat{a}\},\natural_{2}^{2}))\ {\sf sy}\ a\ {\sf rs}\ a}]_{\approx}.&\end{array}$$

$$\begin{array}[]{l}s_{1}=[((\overline{(\{a\},\natural_{1}^{1})^{1}};(\{b,\hat{x}\},\natural_{2}^{0}))\|((\{x\},\natural_{3}^{0})[]\overline{(\{c\},\natural_{4}^{1})^{1}}))\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[((\overline{(\{a\},\natural_{1}^{1})^{1}};(\{b,\hat{x}\},\natural_{2}^{0}))\|(\overline{(\{x\},\natural_{3}^{0})}[](\{c\},\natural_{4}^{1})^{1}))\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx},\\[2.84526pt] s_{2}=[(((\{a\},\natural_{1}^{1});\overline{(\{b,\hat{x}\},\natural_{2}^{0})})\|\underline{((\{x\},\natural_{3}^{0})[](\{c\},\natural_{4}^{1}))})\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx}.\end{array}$$

$$\begin{array}[]{l}s_{1}=[((\overline{(\{a\},\natural_{1}^{2})^{2}};(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})^{2}[]\overline{(\{c\},\natural_{4}^{2})^{2}}))\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[((\overline{(\{a\},\natural_{1}^{2})^{2}};(\{b,\hat{x}\},\natural_{2}^{2}))\|(\overline{(\{x\},\natural_{3}^{2})^{2}}[](\{c\},\natural_{4}^{2})^{2}))\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx},\\[2.84526pt] s_{2}=[((\overline{(\{a\},\natural_{1}^{2})^{1}};(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})^{1}[]\overline{(\{c\},\natural_{4}^{2})^{1}}))\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[((\overline{(\{a\},\natural_{1}^{2})^{1}};(\{b,\hat{x}\},\natural_{2}^{2}))\|(\overline{(\{x\},\natural_{3}^{2})^{1}}[](\{c\},\natural_{4}^{2})^{1}))\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx},\\[2.84526pt] s_{3}=[(((\{a\},\natural_{1}^{2});\overline{(\{b,\hat{x}\},\natural_{2}^{2})^{2}})\|\underline{((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2}))})\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx},\\[2.84526pt] s_{4}=[(((\{a\},\natural_{1}^{2});\overline{(\{b,\hat{x}\},\natural_{2}^{2})^{1}})\|\underline{((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2}))})\ {\sf sy}\ x\ {\sf rs}\ x]_{\approx}.\end{array}$$

$$\begin{array}[]{l}s_{1}=[((\overline{(\{a\},\natural_{1}^{2})^{2}};(\{b,\hat{x}\},\natural_{2}^{2}))\|(\overline{(\{x\},\natural_{3}^{2})^{2}}[](\{c\},\natural_{4}^{2})^{2}))\ {\sf sy}\ x]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[((\overline{(\{a\},\natural_{1}^{2})^{2}};(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})^{2}[]\overline{(\{c\},\natural_{4}^{2})^{2}}))\ {\sf sy}\ x]_{\approx},\\[2.84526pt] s_{2}=[((\overline{(\{a\},\natural_{1}^{2})^{1}};(\{b,\hat{x}\},\natural_{2}^{2}))\|(\overline{(\{x\},\natural_{3}^{2})^{1}}[](\{c\},\natural_{4}^{2})^{1}))\ {\sf sy}\ x]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[((\overline{(\{a\},\natural_{1}^{2})^{1}};(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})^{1}[]\overline{(\{c\},\natural_{4}^{2})^{1}}))\ {\sf sy}\ x]_{\approx},\\[2.84526pt] s_{3}=[(((\{a\},\natural_{1}^{2});\overline{(\{b,\hat{x}\},\natural_{2}^{2})^{2}})\|\underline{((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2}))})\ {\sf sy}\ x]_{\approx},\\[2.84526pt] s_{4}=[(((\{a\},\natural_{1}^{2});\overline{(\{b,\hat{x}\},\natural_{2}^{2})^{1}})\|\underline{((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2}))})\ {\sf sy}\ x]_{\approx},\\[2.84526pt] s_{5}=[\underline{(((\{a\},\natural_{1}^{2});(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2})))\ {\sf sy}\ x}]_{\approx}.\end{array}$$

$$\begin{array}[]{l}s_{1}=[[\overline{(\{a\},\frac{1}{2})}*((\{b\},\natural_{1}^{1})[]((\{c\},\natural_{2}^{1});(\{d\},\frac{1}{3})))*{\sf Stop}]]_{\approx},\\[2.84526pt] s_{2}=[[(\{a\},\frac{1}{2})*(\overline{(\{b\},\natural_{1}^{1})^{1}}[]((\{c\},\natural_{2}^{1})^{1};(\{d\},\frac{1}{3})))*{\sf Stop}]]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[[(\{a\},\frac{1}{2})*((\{b\},\natural_{1}^{1})^{1}[](\overline{(\{c\},\natural_{2}^{1})^{1}};(\{d\},\frac{1}{3})))*{\sf Stop}]]_{\approx},\\[2.84526pt] s_{3}=[[(\{a\},\frac{1}{2})*((\{b\},\natural_{1}^{1})[]((\{c\},\natural_{2}^{1});\overline{(\{d\},\frac{1}{3})}))*{\sf Stop}]]_{\approx}.\end{array}$$

$$\begin{array}[]{l}s_{1}=[[\overline{(\{a\},\rho)}*((\{b\},\natural_{k}^{1});(((\{c\},\natural_{l}^{0});(\{d\},\theta))[]((\{e\},\natural_{m}^{0});(\{f\},\phi))))*{\sf Stop}]]_{\approx},\\[2.84526pt] s_{2}=[[(\{a\},\rho)*(\overline{(\{b\},\natural_{k}^{1})^{1}};(((\{c\},\natural_{l}^{0});(\{d\},\theta))[]((\{e\},\natural_{m}^{0});(\{f\},\phi))))*{\sf Stop}]]_{\approx},\\[2.84526pt] s_{3}=[[(\{a\},\rho)*((\{b\},\natural_{k}^{1});((\overline{(\{c\},\natural_{l}^{0})};(\{d\},\theta))[]((\{e\},\natural_{m}^{0});(\{f\},\phi))))*{\sf Stop}]]_{\approx}=\\[2.84526pt] \hskip 22.76219pt[[(\{a\},\rho)*((\{b\},\natural_{k}^{1});(((\{c\},\natural_{l}^{0});(\{d\},\theta))[](\overline{(\{e\},\natural_{m}^{0})};(\{f\},\phi))))*{\sf Stop}]]_{\approx},\\[2.84526pt] s_{4}=[[(\{a\},\rho)*((\{b\},\natural_{k}^{1});(((\{c\},\natural_{l}^{0});\overline{(\{d\},\theta))}[]((\{e\},\natural_{m}^{0});(\{f\},\phi))))*{\sf Stop}]]_{\approx},\\[2.84526pt] s_{5}=[[(\{a\},\rho)*((\{b\},\natural_{k}^{1});(((\{c\},\natural_{l}^{0});(\{d\},\theta))[]((\{e\},\natural_{m}^{0});\overline{(\{f\},\phi))}))*{\sf Stop}]]_{\approx}.\end{array}$$

$$PF(U,Q)=\left\{\begin{array}[]{ll}\prod_{t\in U}\Omega_{N}(t)\cdot\prod_{\{u\in Fire(Q)\mid u\not\in U\}}(1-\Omega_{N}(u)),&stang(Q);\\ \sum_{t\in U}\Omega_{N}(t),&wtang(Q)\vee vanish(Q).\end{array}\right.$$

$$PF(\emptyset,Q)=\left\{\begin{array}[]{ll}\prod_{u\in Fire(Q)}(1-\Omega_{N}(u)),&Fire(Q)\neq\emptyset;\\ 1,&Fire(Q)=\emptyset.\end{array}\right.$$

$$PT(U,Q)=\frac{PF(U,Q)}{{\sum }_{V\in Fire(Q)}PF(V,Q)}.$$

$$PM(Q,\tilde{Q})=\sum _{\{U\mid Q\stackrel{U}{\to }\tilde{Q}\}}PT(U,Q).$$

Full text

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.

1 Introduction

Algebraic process calculi like CSP [26], ACP [5] and CCS [43] are well-known formal models for specification of computing systems and analysis of their behaviour. In such process algebras (PAs), systems and processes are specified by formulas, and verification of their properties is accomplished at a syntactic level via equivalences, axioms and inference rules. In recent decades, stochastic extensions of PAs were proposed, such as MTIPP [23], PEPA [25] and EMPA [7]. Unlike standard PAs, stochastic process algebras (SPAs) do not just specify actions which can occur (qualitative features), but they associate with the actions the distribution parameters of their random time delays (quantitative characteristics).

1.1 Petri box calculus

PAs specify concurrent systems in a compositional way via an expressive formal syntax. On the other hand, Petri nets (PNs) provide a graphical representation of such systems and capture explicit asynchrony in their behaviour. To combine the advantages of both models, a semantics of algebraic formulas via PNs was defined.

Petri box calculus (PBC) [8, 10, 9] is a flexible and expressive process algebra developed as a tool for specification of the PNs structure and their interrelations. Its goal was also to propose a compositional semantics for high level constructs of concurrent programming languages in terms of elementary PNs. Formulas of PBC are combined not from single (visible or invisible) actions and variables, like in CCS, but from multisets of elementary actions and their conjugates, called multiactions (basic formulas). The empty multiset of actions is interpreted as the silent multiaction specifying some invisible activity. In contrast to CCS, synchronization is separated from parallelism (concurrent constructs). Synchronization is a unary multi-way stepwise operation, based on communication of actions and their conjugates. This extends the CCS approach with conjugate matching labels. Synchronization in PBC is asynchronous, unlike that in Synchronous CCS (SCCS) [43]. Other operations are sequence and choice (sequential constructs). The calculus includes also restriction and relabeling (abstraction constructs). To specify infinite processes, refinement, recursion and iteration operations were added (hierarchical constructs). Thus, unlike CCS, PBC has an additional iteration operation to specify infinite behaviour when the semantic interpretation in finite PNs is possible. PBC has a step operational semantics in terms of labeled transition systems, based on the rules of structural operational semantics (SOS). The operational semantics of PBC is of step type, since its SOS rules have transitions with (multi)sets of activities, corresponding to simultaneous executions of activities (steps). A denotational semantics of PBC was proposed via a subclass of PNs equipped with an interface and considered up to isomorphism, called Petri boxes. For more detailed comparison of PBC with other process algebras and the reasoning about importance of non-interleaving semantics see [8, 9].

The extensions of PBC with a deterministic, a nondeterministic or a stochastic model of time were presented.

1.2 Time extensions of Petri box calculus

To specify systems with time constraints, deterministic (fixed) or nondeterministic (interval) delays are used.

A time extension of PBC with a nondeterministic time model, called time Petri box calculus (tPBC), was proposed in [28]. In tPBC, timing information is added by associating time intervals (the earliest and the latest firing time) with instantaneous actions. Its denotational semantics was defined in terms of a subclass of labeled time Petri nets (LtPNs), based on tPNs [42] and called time Petri boxes (ct-boxes). tPBC has a step time operational semantics in terms of labeled transition systems.

Another time enrichment of PBC, called Timed Petri box calculus (TPBC), was defined in [38, 39], it accommodates a deterministic model of time. In contrast to tPBC, multiactions of TPBC are not instantaneous, but have time durations. Additionally, in TPBC there exist no “illegal” multiaction occurrences, unlike tPBC. The complexity of “illegal” occurrences mechanism was one of the main intentions to construct TPBC though this calculus appeared to be more complicated than tPBC. The denotational semantics of TPBC was defined in terms of a subclass of labeled Timed Petri nets (LTPNs), based on TPNs [49] and called Timed Petri boxes (T-boxes). TPBC has a step timed operational semantics in terms of labeled transition systems. tPBC and TPBC differ in ways they capture time information, and they are not in competition but complement each other.

The third time extension of PBC, called arc time Petri box calculus (atPBC), was constructed in [47, 48], and it implements a nondeterministic time. In atPBC, multiactions are associated with time delay intervals. Its denotational semantics was defined on a subclass of labeled arc time Petri nets (atPNs), based of those from [11, 21], where time restrictions are associated with the arcs, called arc time Petri boxes (at-boxes). atPBC possesses a step time operational semantics in terms of labeled transition systems.

tPBC, TPBC and atPBC, all adopt the discrete time approach, but TPBC has no immediate (multi)actions.

1.3 Stochastic extensions of Petri box calculus

The set of states for the systems with deterministic or nondeterministic delays often differs drastically from that for the timeless systems, hence, the analysis results for untimed systems may be not valid for the time ones. To solve this problem, stochastic delays are considered, which are the random variables with a (discrete or continuous) probability distribution. If the random variables governing delays have an infinite support then the corresponding SPA can exhibit all the same behaviour as its underlying untimed PA.

A stochastic extension of PBC, called stochastic Petri box calculus (sPBC), was proposed in [33, 30]. In sPBC, multiactions have stochastic delays that follow (negative) exponential distribution. Each multiaction is equipped with a rate that is a parameter of the corresponding exponential distribution. The instantaneous execution of a stochastic multiaction is possible only after the corresponding stochastic time delay. The calculus has an interleaving operational semantics defined via transition systems labeled with multiactions and their rates. Its denotational semantics was defined in terms of a subclass of labeled continuous time stochastic PNs, based on CTSPNs [40, 2] and called stochastic Petri boxes (s-boxes). In sPBC, performance of the processes is evaluated by analyzing their underlying continuous time Markov chains (CTMCs). In [31], a number of new equivalence relations were proposed for regular terms of sPBC to choose later a suitable candidate for a congruence. sPBC was enriched with immediate multiactions having zero delay in [32]. We call such an sPBC extension generalized sPBC or gsPBC. An interleaving operational semantics of gsPBC was constructed via transition systems labeled with stochastic or immediate multiactions together with their rates or probabilities. A denotational semantics of gsPBC was defined via a subclass of labeled generalized stochastic PNs, based on GSPNs [40, 2, 3] and called generalized stochastic Petri boxes (gs-boxes). The performance analysis in gsPBC is based on the semi-Markov chains (SMCs).

PBC has a step operational semantics, whereas sPBC has an interleaving one. In step semantics, parallel executions of activities (steps) are permitted while in interleaving semantics, we can execute only single activities. Hence, a stochastic extension of PBC with a step semantics was needed to keep the concurrency degree of behavioural analysis at the same level as in PBC. As mentioned in [44, 45], in contrast to continuous time approach (used in sPBC), discrete time approach allows for constructing models of common clock systems and clocked devices. In such models, multiple transition firings (or executions of multiple activities) at time moments (ticks of the central clock) are possible, resulting in a step semantics. Moreover, employment of discrete stochastic time fills the gap between the models with deterministic (fixed) time delays and those with continuous stochastic time delays. As argued in [1], arbitrary delay distributions are much easier to handle in a discrete time domain. In [36, 37, 34], discrete stochastic time was preferred to enable simultaneous expiration of multiple delays.

In [51, 52, 53, 54], a discrete time stochastic extension dtsPBC of finite PBC was presented. In dtsPBC, the residence time in the process states is geometrically distributed. A step operational semantics of dtsPBC was constructed via labeled probabilistic transition systems. Its denotational semantics was defined in terms of a subclass of labeled discrete time stochastic PNs (LDTSPNs), based on DTSPNs [44, 45] and called discrete time stochastic Petri boxes (dts-boxes). The performance evaluation in dtsPBC is accomplished via the underlying discrete time Markov chains (DTMCs) of the algebraic processes. Since dtsPBC has a discrete time semantics and geometrically distributed sojourn time in the process states, unlike sPBC with continuous time semantics and exponentially distributed delays, the calculi apply two different approaches to the stochastic extension of PBC, in spite of some similarity of their syntax and semantics inherited from PBC. The main advantage of dtsPBC is that concurrency is treated like in PBC having step semantics, whereas in sPBC parallelism is simulated by interleaving, obliging one to collect the information on causal independence of activities before constructing the semantics.

In [55, 56, 57, 58, 59], we presented an enhanced calculus dtsiPBC, an extension with immediate multiactions of dtsPBC. Immediate multiactions increase the specification capability: they can model logical conditions, probabilistic branching, instantaneous probabilistic choices and activities whose durations are negligible in comparison with those of others. They are also used to specify urgent activities and the ones that are not relevant for performance evaluation. Thus, immediate multiactions can be considered as a kind of instantaneous dynamic state adjustment and, in many cases, they result in a simpler and more clear system representation.

1.4 Our contributions

In this paper, we present dtsiPBC, extended with deterministic multiactions, called discrete time stochastic and deterministic Petri box calculus (dtsdPBC). In dtsdPBC, besides the probabilities from the real-valued interval $(0;1)$ that are used to calculate discrete-time delays of stochastic multiactions, also non-negative integers are used to specify fixed time delays of deterministic multiactions (including zero delay, which is the case of immediate multiactions). To resolve conflicts among deterministic multiactions, they are additionally equipped with positive real-valued weights. As argued in [61, 62], a combination of deterministic and stochastic delays fits well to model technical systems with constant (fixed) durations of the regular non-random activities and probabilistically distributed (stochastic) durations of the randomly occurring activities. The step operational semantics of dtsdPBC is constructed with the use of labeled probabilistic transition systems. The denotational semantics of dtsdPBC is defined in terms of a subclass of labeled discrete time stochastic and deterministic Petri nets (LDTSPNs with deterministic transitions, LDTSDPNs), based on the extension of DTSPNs with transition labeling and deterministic transitions, called dtsd-boxes. The consistency of both semantics is demonstrated. The corresponding stochastic process, which is a semi-Markov chain (SMC), is constructed and investigated, with the purpose of performance evaluation, which is the same for both semantics. In addition, the alternative solution methods are developed, based on the underlying discrete time Markov chain (DTMC) and its reduction (RDTMC) by eliminating vanishing states with zero sojourn (residence) times. The theory developed is illustrated with a series of the interesting and non-trivial examples that include the travel system case study, used to demonstrate application of the performance analysis methods within dtsdPBC.

Thus, the main contributions of the paper are the following.

• •

New powerful and expressive discrete time SPA with deterministic activities called dtsdPBC.

• •

Step operational semantics of dtsdPBC in terms of labeled probabilistic transition systems.

• •

Petri net denotational semantics of dtsdPBC via discrete time stochastic and deterministic Petri nets.

• •

Performance analysis via underlying semi-Markov chains and (reduced) discrete time Markov chains.

1.5 Structure of the paper

The paper is organized as follows. In Section 2, the syntax of the extended calculus dtsdPBC is presented. In Section 3, we construct the operational semantics of the algebra in terms of labeled probabilistic transition systems. In Section 4, we propose the denotational semantics based on a subclass of LDTSDPNs. In Section 5, the corresponding stochastic process is defined and analyzed. Finally, Section 6 summarizes the results obtained and outlines research perspectives in this area.

2 Syntax

In this section, we propose the syntax of dtsdPBC. First, we recall a definition of multiset that is an extension of the set notion by allowing several identical elements.

Definition 2.1

Let $X$ be a set. A finite multiset (bag) $M$ over $X$ is a mapping $M:X\rightarrow I\!\!N$ such that $|\{x\in X\mid M(x)>0\}|<\infty$, i.e. it can contain a finite number of elements only.

We denote the set of all finite multisets over a set $X$ by $I\!\!N_{fin}^{X}$. Let $M,M^{\prime}\in I\!\!N_{fin}^{X}$. The cardinality of $M$ is defined as $|M|=\sum_{x\in X}M(x)$. We write $x\in M$ if $M(x)>0$ and $M\subseteq M^{\prime}$ if $\forall x\in X\ M(x)\leq M^{\prime}(x)$. We define $(M+M^{\prime})(x)=M(x)+M^{\prime}(x)$ and $(M-M^{\prime})(x)=\max\{0,M(x)-M^{\prime}(x)\}$. When $\forall x\in X,\ M(x)\leq 1,\ M$ can be interpreted as a proper set and denoted by $M\subseteq X$. The set of all subsets (powerset) of $X$ is denoted by $2^{X}$.

Let $Act=\{a,b,\ldots\}$ be the set of elementary actions. Then $\widehat{Act}=\{\hat{a},\hat{b},\ldots\}$ is the set of conjugated actions (conjugates) such that $\hat{a}\neq a$ and $\hat{\hat{a}}=a$. Let ${\cal A}=Act\cup\widehat{Act}$ be the set of all actions, and ${\cal L}=I\!\!N_{fin}^{\cal A}$ be the set of all multiactions. Note that $\emptyset\in{\cal L}$, this corresponds to an internal move, i.e. the execution of a multiaction that contains no visible action names. The alphabet of $\alpha\in{\cal L}$ is defined as ${\cal A}(\alpha)=\{x\in{\cal A}\mid\alpha(x)>0\}$.

A stochastic multiaction is a pair $(\alpha,\rho)$, where $\alpha\in{\cal L}$ and $\rho\in(0;1)$ is the probability of the multiaction $\alpha$. This probability is interpreted as that of independent execution of the stochastic multiaction at the next discrete time moment. Such probabilities are used to calculate those to execute (possibly empty) sets of stochastic multiactions after one time unit delay. The probabilities of stochastic multiactions are required not to be equal to $1$ to avoid extra model complexity, since in this case one should assign with them weights, needed to make a choice when several stochastic multiactions with probability $1$ can be executed from a state. The difficulty is that when the stochastic multiactions with probability $1$ occur in a step (parallel execution), all other with the less probabilities do not. In this case, the conflicts resolving requires a special attention, as discussed in [44, 45] within SPNs. This decision also allows us to avoid technical difficulties related to conditioning events with probability [math]. The probability $1$ is left for (implicitly assigned to) waiting multiactions (positively delayed deterministic multiactions, to be defined later), which are delayed for at least one time unit before their execution and have weights to resolve conflicts with other waiting multiactions. On the other hand, there is no sense to allow probability [math] of stochastic multiactions, since they would never be performed in this case. Let ${\cal SL}$ be the set of all stochastic multiactions.

A deterministic multiaction is a pair $(\alpha,\natural_{l}^{\theta})$, where $\alpha\in{\cal L},\ \theta\in I\!\!N$ is the non-negative integer-valued (fixed) delay and $l\in I\!\!R_{>0}=(0;+\infty)$ is the positive real-valued weight of the multiaction $\alpha$. This weight is interpreted as a measure of importance (urgency, interest) or a bonus reward associated with execution of the deterministic multiaction at the current discrete time moment. Such weights are used to calculate the probabilities to execute sets of deterministic multiactions at the same moment of time. An immediate multiaction is a deterministic multiaction with the delay [math] while a waiting multiaction is a deterministic multiaction with a positive delay. In case of no conflicts among waiting multiactions, whose remaining times to execute (RTEs, to be explained later in more detail) are equal to one time unit, they are executed with probability $1$ at the next time moment. Deterministic multiactions have a priority over stochastic ones, and there is also difference in priorities between immediate and waiting multiactions. One can assume that all immediate multiactions have (the highest) priority $2$ and all waiting multiactions have (the intermediate) priority $1$, whereas all stochastic multiactions have (the lowest) priority [math]. This means that in a state where all kinds of multiactions can occur, immediate multiactions always occur before waiting ones that, in turn, are always executed before stochastic ones. Different types of multiactions cannot participate together in some step (parallel execution), i.e. just the steps consisting only of immediate multiactions or waiting ones, or those including only stochastic multiactions, are allowed. Let ${\cal DL}$ be the set of all deterministic multiactions, ${\cal IL}$ be the set of all immediate multiactions and ${\cal WL}$ be the set of all waiting multiactions. Obviously, we have ${\cal DL}={\cal IL}\cup{\cal WL}$.

Let us note that the same multiaction $\alpha\in{\cal L}$ may have different probabilities, (fixed) delays and weights in the same specification. An activity is a stochastic or a deterministic multiaction. Let ${\cal SDL}={\cal SL}\cup{\cal DL}={\cal SL}\cup{\cal IL}\cup{\cal WL}$ be the set of all activities. The alphabet of an activity $(\alpha,\kappa)\in{\cal SDL}$ is defined as ${\cal A}(\alpha,\kappa)={\cal A}(\alpha)$. The alphabet of a multiset of activities $\Upsilon\in I\!\!N_{fin}^{\cal SDL}$ is defined as ${\cal A}(\Upsilon)=\cup_{(\alpha,\kappa)\in\Upsilon}{\cal A}(\alpha)$. For an activity $(\alpha,\kappa)\in{\cal SDL}$, we define its multiaction part as ${\cal L}(\alpha,\kappa)=\alpha$ and its probability or weight part as $\Omega(\alpha,\kappa)=\kappa$ if $\kappa\in(0;1)$; or $\Omega(\alpha,\kappa)=l$ if $\kappa=\natural_{l}^{\theta},\ \theta\in I\!\!N,\ l\in I\!\!R_{>0}$. The multiaction part of a multiset of activities $\Upsilon\in I\!\!N_{fin}^{\cal SIL}$ is defined as ${\cal L}(\Upsilon)=\sum_{(\alpha,\kappa)\in\Upsilon}\alpha$.

Activities are combined into formulas (process expressions) by the following operations: sequential execution ;, choice $[]$, parallelism $\|$, relabeling $[f]$ of actions, restriction $\!\!\ {\sf rs}\ \!\!$ over a single action, synchronization $\!\!\ {\sf sy}\ \!\!$ on an action and its conjugate, and iteration $[\,*\,*\,]$ with three arguments: initialization, body and termination.

Sequential execution and choice have a standard interpretation, like in other process algebras, but parallelism does not include synchronization, unlike the corresponding operation in CCS [43].

Relabeling functions $f:{\cal A}\rightarrow{\cal A}$ are bijections preserving conjugates, i.e. $\forall x\in{\cal A}\ f(\hat{x})=\widehat{f(x)}$. Relabeling is extended to multiactions in the usual way: for $\alpha\in{\cal L}$ we define $f(\alpha)=\sum_{x\in\alpha}f(x)$. Relabeling is extended to activities: for $(\alpha,\kappa)\in{\cal SDL}$, we define $f(\alpha,\kappa)=(f(\alpha),\kappa)$. Relabeling is extended to the multisets of activities as follows: for $\Upsilon\in I\!\!N_{fin}^{\cal SDL}$ we define $f(\Upsilon)=\sum_{(\alpha,\kappa)\in\Upsilon}(f(\alpha),\kappa)$.

Restriction over an elementary action $a\in Act$ means that, for a given expression, any process behaviour containing $a$ or its conjugate $\hat{a}$ is not allowed.

Let $\alpha,\beta\in{\cal L}$ be two multiactions such that for some elementary action $a\in Act$ we have $a\in\alpha$ and $\hat{a}\in\beta$, or $\hat{a}\in\alpha$ and $a\in\beta$. Then, synchronization of $\alpha$ and $\beta$ by $a$ is defined as $\alpha\oplus_{a}\beta=\gamma$, where

[TABLE]

In other words, we require that $\alpha\oplus_{a}\beta=\alpha+\beta-\{a,\hat{a}\}$, i.e. we remove one exemplar of $a$ and one exemplar of $\hat{a}$ from the multiset sum $\alpha+\beta$, since the synchronization of $a$ and $\hat{a}$ produces $\emptyset$. Activities are synchronized with the use of their multiaction parts, i.e. the synchronization by $a$ of two activities, whose multiaction parts $\alpha$ and $\beta$ possess the properties mentioned above, results in the activity with the multiaction part $\alpha\oplus_{a}\beta$. We may synchronize activities of the same type only: either both stochastic multiactions or both immediate ones, since immediate multiactions have a priority over stochastic ones, hence, stochastic and immediate multiactions cannot be executed together (note also that the execution of immediate multiactions takes no time, unlike that of stochastic ones). Synchronization by $a$ means that, for a given expression with a process behaviour containing two concurrent activities that can be synchronized by $a$, there exists also the process behaviour that differs from the former only in that the two activities are replaced by the result of their synchronization.

In the iteration, the initialization subprocess is executed first, then the body is performed zero or more times, and finally, the termination subprocess is executed.

Static expressions specify the structure of processes. As we shall see, the expressions correspond to unmarked LDTSDPNs (LDTSDPNs are marked by definition). Remember that a marking is the allocation of tokens in the places of a PN and markings are used to describe dynamic behaviour of PNs in terms of transition firings.

We assume that every waiting multiaction has a countdown timer associated, whose value is the discrete time amount left till the moment when the waiting multiaction can be executed. Therefore, besides standard (unstamped) waiting multiactions in the form of $(\alpha,\natural_{l}^{\theta})\in{\cal WL}$, a special case of the stamped waiting multiactions should be considered in the definition of static expressions. Each (time) stamped waiting multiaction in the form of $(\alpha,\natural_{l}^{\theta})^{\delta}$ has an extra superscript $\delta\in\{1,\ldots,\theta\}$ assigned that specifies a time stamp indicating the latest value of the countdown timer associated with that multiaction. The standard waiting multiactions have no time stamps, to demonstrate irrelevance of the timer values for them (for example, their timers have not yet started or have already finished their operation). The notions of the alphabet, multiaction part, weight part for (the multisets of) stamped waiting multiactions are defined, respectively, like those for (the multisets of) unstamped waiting multiactions.

By reasons of simplicity, we do not assign the timer value superscripts $\delta$ to immediate multiactions, which are a special case of deterministic multiactions $(\alpha,\natural_{l}^{\theta})$ with the delay $\theta=0$ in the form of $(\alpha,\natural_{l}^{0})$, since their timer values can only be equal to [math]. Analogously, the superscript $\delta$ might be omitted for the waiting multiactions $(\alpha,\natural_{l}^{\theta})$ with the delay $\theta=1$ in the form of $(\alpha,\natural_{l}^{1})$, since the corresponding timer can only have a single value $1$. Nevertheless, to maintain syntactic uniformity among waiting multiactions, we leave the timer value superscripts for those that are $1$-delayed.

Definition 2.2

Let $(\alpha,\kappa)\in{\cal SDL},\ (\alpha,\natural_{l}^{\theta})\in{\cal WL},\ \delta\in\{1,\ldots,\theta\}$ and $a\in Act$. A static expression of dtsdPBC is defined as

[TABLE]

Let $StatExpr$ denote the set of all static expressions of dtsdPBC.

To make the grammar above unambiguous, one can add parentheses in the productions with binary operations: $(E;E),\ (E[]E),\ (E\|E)$. However, here and further we prefer the PBC approach and add them to resolve ambiguities only.

To avoid technical difficulties with the iteration operator, we should not allow any concurrency at the highest level of the second argument of iteration. This is not a severe restriction though, since we can always prefix parallel expressions by an activity with the empty multiaction part. Later on, in Example 4.3, we shall demonstrate that relaxing the restriction can result in nets which are not safe. Alternatively, we can use a different, safe, version of the iteration operator, but its net translation has six arguments. See also [9] for discussion on this subject. Remember that a PN is $n$-bounded ($n\in I\!\!N$) if for all its reachable (from the initial marking by the sequences of transition firings) markings there are at most $n$ tokens in every place, and a PN is safe if it is $1$-bounded.

Definition 2.3

Let $(\alpha,\kappa)\in{\cal SDL},\ (\alpha,\natural_{l}^{\theta})\in{\cal WL},\ \delta\in\{1,\ldots,\theta\}$ and $a\in Act$. A regular static expression of dtsdPBC is defined as

[TABLE]

Let $RegStatExpr$ denote the set of all regular static expressions of dtsdPBC.

Let $E$ be a regular static expression. The underlying timer-free regular static expression $\downharpoonleft\!\!E$ of $E$ is obtained by removing from it all timer value superscripts.

Further, the set of all stochastic multiactions (from the syntax) of $E$ is ${\cal SL}(E)=\{(\alpha,\rho)\mid(\alpha,\rho)\mbox{ is a}\\ \mbox{subexpression of }E\}$. The set of all immediate multiactions (from the syntax) of $E$ is ${\cal IL}(E)=\{(\alpha,\natural_{l}^{0})\mid(\alpha,\natural_{l}^{0})\mbox{ is a subexpression of }E\}$. The set of all waiting multiactions (from the syntax) of $E$ is ${\cal WL}(E)=\{(\alpha,\natural_{l}^{\theta})\mid(\alpha,\natural_{l}^{\theta})\mbox{ or }(\alpha,\natural_{l}^{\theta})^{\delta}\mbox{ is a}\mbox{subexpression of }E\mbox{ for }\delta\in\{1,\ldots,\theta\}\}$. Thus, the set of all deterministic multiactions (from the syntax) of $E$ is ${\cal DL}(E)={\cal IL}(E)\cup{\cal WL}(E)$ and the set of all activities (from the syntax) of $E$ is ${\cal SDL}(E)={\cal SL}(E)\cup{\cal DL}(E)={\cal SL}(E)\cup{\cal IL}(E)\cup{\cal WL}(E)$.

Dynamic expressions specify the states of processes. As we shall see, the expressions correspond to LDTSDPNs (which are marked by default). Dynamic expressions are obtained from static ones, by annotating them with upper or lower bars which specify the active components of the system at the current moment of time. The dynamic expression with upper bar (the overlined one) $\overline{E}$ denotes the initial, and that with lower bar (the underlined one) $\underline{E}$ denotes the final state of the process specified by a static expression $E$.

For every overlined stamped waiting multiaction in the form of $\overline{(\alpha,\natural_{l}^{\theta})^{\delta}}$, the superscript $\delta\in\{1,\ldots,\theta\}$ specifies the current value of the running countdown timer associated with the waiting multiaction. That decreasing discrete timer is started with the initial value $\theta$ (equal to the delay of the waiting multiaction) at the moment when the waiting multiaction becomes overlined. Then such a newly overlined stamped waiting multiaction $\overline{(\alpha,\natural_{l}^{\theta})^{\theta}}$ may be seen similar to the freshly overlined unstamped waiting multiaction $\overline{(\alpha,\natural_{l}^{\theta})}$. Such similarity will be captured by the structural equivalence, to be defined later.

While the stamped waiting multiaction stays overlined with the specified process execution, the timer decrements by one discrete time unit with each global time tick until the timer value becomes $1$. This fact indicates that one unit of time remains till execution of that multiaction (the remaining time to execute, RTE, equals one) that should follow in the next moment with probability $1$, in case the stamped waiting multiaction is still overlined and there are no conflicting with it waiting multiactions, whose RTEs equal to one.

Definition 2.4

Let $E\in StatExpr$ and $a\in Act$. A dynamic expression of dtsdPBC is defined as

[TABLE]

Let $DynExpr$ denote the set of all dynamic expressions of dtsdPBC.

Let $G$ be a dynamic expression. The underlying static (line-free) expression $\lfloor G\rfloor$ of $G$ is obtained by removing from it all upper and lower bars. Note that if the underlying static expression of a dynamic one is not regular, the corresponding LDTSDPN can be non-safe (though, it is $2$-bounded in the worst case [9]).

Definition 2.5

A dynamic expression $G$ is regular if its underlying static expression $\lfloor G\rfloor$ is regular.

Let $RegDynExpr$ denote the set of all regular dynamic expressions of dtsdPBC.

Let $G$ be a regular dynamic expression. The underlying timer-free regular dynamic expression $\downharpoonleft\!\!G$ of $G$ is obtained by removing from it all timer value superscripts.

Further, the set of all stochastic multiactions (from the syntax) of $G$ is ${\cal SL}(G)={\cal SL}(\lfloor G\rfloor)$. The set of all immediate multiactions (from the syntax) of $G$ is ${\cal IL}(G)={\cal IL}(\lfloor G\rfloor)$. The set of all waiting multiactions (from the syntax) of $G$ is ${\cal WL}(G)={\cal WL}(\lfloor G\rfloor)$. Thus, the set of all deterministic multiactions (from the syntax) of $G$ is ${\cal DL}(G)={\cal IL}(G)\cup{\cal WL}(G)$ and the set of all activities (from the syntax) of $G$ is ${\cal SDL}(G)={\cal SL}(G)\cup{\cal DL}(G)={\cal SL}(G)\cup{\cal IL}(G)\cup{\cal WL}(G)$.

3 Operational semantics

In this section, we define the step operational semantics in terms of labeled transition systems.

3.1 Inaction rules

The inaction rules for dynamic expressions describe their structural transformations in the form of $G\Rightarrow\widetilde{G}$ which do not change the states of the specified processes. The goal of those syntactic transformations is to obtain the well-structured resulting expressions called operative ones to which no inaction rules can be further applied. As we shall see, the application of an inaction rule to a dynamic expression does not lead to any discrete time tick or any transition firing in the corresponding LDTSDPN, hence, its current marking stays unchanged.

Thus, an application of every inaction rule does not require any discrete time delay, i.e. the dynamic expression transformation described by the rule is accomplished instantly.

In Table 1, we define inaction rules for regular dynamic expressions being overlined and underlined static ones. In this table, $(\alpha,\natural_{l}^{\theta})\in{\cal WL},\ \delta\in\{1,\ldots,\theta\},\ E,F,K\in RegStatExpr$ and $a\in Act$. The first inaction rule suggests that the timer value of each newly overlined waiting multiaction is set to the delay of that waiting multiaction.

In Table 2, we introduce inaction rules for regular dynamic expressions in the arbitrary form. In this table, $E,F\in RegStatExpr,\ G,H,\widetilde{G},\widetilde{H}\in RegDynExpr$ and $a\in Act$. By reason of brevity, two distinct inaction rules with the same premises are collated in some cases, resulting in the inaction rules with double conclusion.

Example 3.1

Let $E=(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})$. The following inferences by the inaction rules are possible from $\overline{E}$:

[TABLE]

Definition 3.1

A regular dynamic expression $G$ is operative if no inaction rule can be applied to it.

Let $OpRegDynExpr$ denote the set of all operative regular dynamic expressions of dtsdPBC.

Note that any dynamic expression can be always transformed into a (not necessarily unique) operative one by using the inaction rules.

In the following, we consider regular expressions only and omit the word “regular”.

Definition 3.2

The relation $\approx\ =(\Rightarrow\cup\Leftarrow)^{*}$ is a structural equivalence of dynamic expressions in dtsdPBC. Thus, two dynamic expressions $G$ and $G^{\prime}$ are structurally equivalent, denoted by $G\approx G^{\prime}$, if they can be reached from each other by applying the inaction rules in a forward or a backward direction.

Let $X$ be some set. We denote the Cartesian product $X\times X$ by $X^{2}$. Let ${\cal E}\subseteq X^{2}$ be an equivalence relation on $X$. Then the equivalence class (with respect to ${\cal E}$) of an element $x\in X$ is defined by $[x]_{\cal E}=\{y\in X\mid(x,y)\in{\cal E}\}$. The equivalence ${\cal E}$ partitions $X$ into the set of equivalence classes $X/_{\cal E}=\{[x]_{\cal E}\mid x\in X\}$.

Let $G$ be a dynamic expression. Then $[G]_{\approx}=\{H\mid G\approx H\}$ is the equivalence class of $G$ with respect to the structural equivalence, called the (corresponding) state. Next, $G$ is an initial dynamic expression, denoted by $init(G)$, if $\exists E\in RegStatExpr\ G\in[\overline{E}]_{\approx}$. Further, $G$ is a final dynamic expression, denoted by $final(G)$, if $\exists E\in RegStatExpr\ G\in[\underline{E}]_{\approx}$.

Let $G$ be a dynamic expression and $s=[G]_{\approx}$. The set of all enabled stochastic multiactions of $s$ is $EnaSto(s)=\{(\alpha,\rho)\in{\cal SL}\mid\exists H\in s\cap OpRegDynExpr\ \overline{(\alpha,\rho)}\mbox{ is a subexpression of }H\}$, i.e. it consists of all stochastic multiactions that, being overlined, are the subexpressions of some operative dynamic expression from the state $s$. Analogously, the set of all enabled immediate multiactions of $s$ is $EnaImm(s)=\{(\alpha,\natural_{l}^{0})\in{\cal IL}\mid\exists H\in s\cap OpRegDynExpr\ \overline{(\alpha,\natural_{l}^{0})}\mbox{ is a subexpression of }H\}$. The set of all enabled waiting multiactions of $s$ is $EnaWait(s)=\{(\alpha,\natural_{l}^{\theta})\in{\cal WL}\mid\exists H\in s\cap OpRegDynExpr\ \overline{(\alpha,\natural_{l}^{\theta})^{\delta}},\ \delta\in\{1,\ldots,\theta\},\mbox{ is a subexpression of }H\}$, i.e. it consists of all waiting multiactions that, being superscribed with the values of their timers and overlined, are the subexpressions of some operative dynamic expression from the state $s$. The set of all newly enabled waiting multiactions of $s$ is $EnaWaitNew(s)=\{(\alpha,\natural_{l}^{\theta})\in{\cal WL}\mid\exists H\in s\cap OpRegDynExpr\ \overline{(\alpha,\natural_{l}^{\theta})^{\theta}}\mbox{ is a }\\ \mbox{subexpression of }H\}$, i.e. it consists of all waiting multiactions that, being superscribed with the initial values of their timers (delays of those waiting multiactions) and overlined, are the subexpressions of some operative dynamic expression from the state $s$.

Thus, the set of all enabled deterministic multiactions of $s$ is $EnaDet(s)=EnaImm(s)\cup EnaWait(s)$ and the set of all enabled activities of $s$ is defined as $Ena(s)=EnaSto(s)\cup EnaDet(s)=EnaSto(s)\cup EnaImm(s)\cup EnaWait(s)$. As we shall see, $Ena(s)=Ena([G]_{\approx})$ is an algebraic analogue of the set of all transitions enabled at the initial marking of the LDTSDPN corresponding to $G$. Note that the activities, resulted from synchronization, are not present explicitly in the syntax of the dynamic expressions. Nevertheless, their enabledness status can be recovered by observing that of the pair of synchronized activities from the syntax (they both should be enabled for enabling their synchronized product), even if they are affected by restriction after the synchronization. An activity is said to be affected by restriction, if it is within the scope of a restriction operation with the argument action, such that it or its conjugate is contained in the multiaction part of that activity.

Definition 3.3

An operative dynamic expression $G$ is saturated (with the values of timers), if each enabled waiting multiaction of $[G]_{\approx}$, being (certainly) superscribed with the value of its timer and possibly overlined, is the subexpression of $G$.

Let $SaOpRegDynExpr$ denote the set of all saturated operative dynamic expressions of dtsdPBC.

Proposition 3.1

Any operative dynamic expression can be always transformed into the saturated one by using the inaction rules.

Proof. Let $G$ be a dynamic expression, $(\alpha,\natural_{l}^{\theta})\in EnaWait([G]_{\approx})$ and there exists $H\in[G]_{\approx}\cap OpRegDynExpr$ that contains a subexpression $\overline{(\alpha,\natural_{l}^{\theta})^{\delta}},\ \delta\in\{1,\ldots,\theta-1\}$. Then all operative dynamic expressions from $[G]_{\approx}\cap OpRegDynExpr$ contain a subexpression $\overline{(\alpha,\natural_{l}^{\theta})^{\delta}}$ or $(\alpha,\natural_{l}^{\theta})^{\delta}$, i.e. the (possibly overlined) enabled waiting multiaction $(\alpha,\natural_{l}^{\theta})$ with the (non-initial) timer value superscript $\delta\leq\theta-1$. Note that the timer value superscript $\delta$ is the same for all such structurally equivalent operative dynamic expressions. Indeed, all inaction rules, besides the first one, do not change the values of timers, but those rules just modify the overlines and underlines of dynamic expressions. The first inaction rule just sets up the timer of each overlined waiting multiaction $\overline{(\alpha,\natural_{l}^{\theta})}$ with the initial value $\delta=\theta$, equal to the delay of that waiting multiaction, as follows: $\overline{(\alpha,\natural_{l}^{\theta})^{\theta}}$. Then the remaining inaction rules can shift out the overline of that enabled waiting multiaction before setting up its timer, which results in a non-overlined enabled waiting multiaction without timer value superscript $(\alpha,\natural_{l}^{\theta})$. Thus, for $(\alpha,\natural_{l}^{\theta})\in EnaWait([G]_{\approx})$, it can happen that $\overline{(\alpha,\natural_{l}^{\theta})^{\theta}}$ a subexpression of some $H\in[G]_{\approx}\cap OpRegDynExpr$ and $(\alpha,\natural_{l}^{\theta})$ is a subexpression of a different $H^{\prime}\in[G]_{\approx}\cap OpRegDynExpr$.

Let now $G$ be an operative dynamic expression that is not saturated. By the arguments above, the saturation can be violated only if $G$ contains as a subexpression at least one newly enabled waiting multiaction $(\alpha,\natural_{l}^{\theta})$ of $[G]_{\approx}$ that is not superscribed with the timer value. By the definition of the new-enabling, there exists $H\in[G]_{\approx}\cap OpRegDynExpr$ such that $\overline{(\alpha,\natural_{l}^{\theta})^{\theta}}$ is a subexpression of $H$. Since $G\approx H$, there is a sequence of the inaction rules applications (in a forward or a backward direction) that transforms $G$ into $H$. Then the reverse sequence transforms $H$ into $G$. Let us remove from that reverse sequence the following backward application of the first inaction rule: $\overline{(\alpha,\natural_{l}^{\theta})}\Leftarrow\overline{(\alpha,\natural_{l}^{\theta})^{\theta}}$. Then such a reduced reverse sequence will turn $H$ into $G_{1}\in[G]_{\approx}\cap OpRegDynExpr$, obtained from $G$ by replacing $(\alpha,\natural_{l}^{\theta})$ with $(\alpha,\natural_{l}^{\theta})^{\theta}$.

Let us start from $G_{1}$ and apply the above procedure to the remaining not superscribed with the timer values newly enabled waiting multiactions of $[G]_{\approx}$ (which are also those of such kind of $[G_{1}]_{\approx}$). After repeated application of the mentioned procedure for all $n\geq 1$ non-superscribed newly enabled waiting multiactions of $G$, we shall get from it the saturated operative dynamic expression $G_{n}=\widetilde{G}\in[G]_{\approx}\cap OpRegDynExpr$. Note that the presented transformation of $G$ into $\widetilde{G}$ does not change the enabling, since it does not change any overlines or underlines in the syntax of the traversed operative dynamic expressions, but only iteratively assigns the timer value superscripts to all newly enabled waiting multiactions of $G$. Hence, $EnaWait([G]_{\approx})=EnaWait([G_{1}]_{\approx})=\cdots=EnaWait([G_{n}]_{\approx})=EnaWait([\widetilde{G}]_{\approx})$. $\sqcap\!\!\!\!\sqcup$

Thus, any dynamic expression can be always transformed into a (not necessarily unique) saturated operative one by using the inaction rules.

Example 3.2

Let $E$ be from Example 3.1. Consider the sequence of inaction rules, applied (in a forward or a backward direction) in the following transformation of a non-saturated $G\in[\overline{E}]_{\approx}\cap OpRegDynExpr$ with the non-superscribed with the timer value (unstamped) enabled waiting multiaction $(\{a\},\natural_{1}^{3})$ into (a saturated) $H\in[\overline{E}]_{\approx}\cap OpRegDynExpr$, in which $(\{a\},\natural_{1}^{3})$ is stamped:

[TABLE]

The reduced reverse sequence of inaction rules induces the following transformations of $H$ that result in a saturated $G_{1}=\widetilde{G}\in[\overline{E}]_{\approx}\cap OpRegDynExpr$, in which $(\{a\},\natural_{1}^{3})$ is stamped:

[TABLE]

Let $G$ be a saturated operative dynamic expression. Then $\circlearrowleft\!G$ is written for the timer decrement operator $\circlearrowleft$, applied to $G$. It denotes a saturated operative dynamic expression, obtained from $G$ via decrementing by one time unit all greater than $1$ values of the timers associated with all (if any) stamped waiting multiactions from the syntax of $G$. Thus, each such stamped waiting multiaction changes its timer value from $\delta$ in $G$ to $\max\{1,\delta-1\}$ in $\circlearrowleft\!G$, where $\delta\in I\!\!N_{\geq 1}$. More formally, the timer decrement operator affects the (possibly overlined) stamped waiting multiactions being the subexpressions of $G$ as follows. The overlined stamped waiting multiaction $\overline{(\alpha,\natural_{l}^{\theta})^{\delta}}$ is replaced with $\overline{(\alpha,\natural_{l}^{\theta})^{\max\{1,\delta-1\}}}$ while the stamped waiting multiaction without overline or underline $(\alpha,\natural_{l}^{\theta})^{\delta}$ is replaced with $(\alpha,\natural_{l}^{\theta})^{\max\{1,\delta-1\}}$.

Note that when $\delta=1$, we have $\max\{1,\delta-1\}=\max\{1,0\}=1$, hence, the timer value $\delta=1$ may remain unchanged for a stamped waiting multiaction that is not executed by some reason at the next time moment, but stays stamped. For example, that stamped waiting multiaction may be affected by restriction. If the timer values cannot be decremented with a time tick for all stamped waiting multiactions (if any) from $G$ then $\circlearrowleft\!G=G$ and we obtain so-called empty loop transition that will be formally defined later.

Observe that the timer decrement operator keeps stamping of the waiting multiactions, since it does not change any overlines or underlines, but it may only decrease their timer values, so that the stamped enabled waiting multiactions stay stamped (with their timer values, possibly decremented by one).

Example 3.3

Let $E$ be from Example 3.1. We have $Ena([\overline{E}]_{\approx})=\{(\{a\},\natural_{1}^{3}),(\{b\},\frac{1}{3})\}$ and $Ena([\overline{E}]_{\approx})\cap{\cal WL}=\{(\{a\},\natural_{1}^{3})\}$. The following one time unit timer decrements are possible from the saturated operative dynamic expressions belonging to $[\overline{E}]_{\approx}$:

[TABLE]

Note that, similar in [28], we are mainly interested in the dynamic expressions, derived from the overlined static expressions, such that no stamped waiting multiaction is a subexpression of them, to ensure that time proceeds uniformly. Therefore, we consider a dynamic expression $G=\overline{(\{a\},\natural_{1}^{2})^{1}}[](\{b\},\natural_{2}^{3})^{1}$ as “illegal” and that $H=\overline{(\{a\},\natural_{1}^{2})^{1}}[](\{b\},\natural_{2}^{3})^{2}$ as “legal”, since the latter is obtained from the overlined static expression without timer value superscripts $\overline{E}=\overline{(\{a\},\natural_{1}^{2})[](\{b\},\natural_{2}^{3})}$ after one time tick. On the other hand, $G$ is “illegal” only when it is intended to specify a complete process, but it may become “legal” as a part of such complete specification, like $G\ {\sf rs}\ a$, since after two time ticks from $\overline{E\ {\sf rs}\ a}$, the timer values cannot be decreased further when approaching the value $1$. Thus, we should allow the dynamic expressions like $G$, by assuming that they are incomplete specifications, to be further composed.

Let $G$ be a dynamic expression. Then $I_{G}:{\cal WL}(G)\rightarrow I\!\!N_{\geq 1}$ is the timer valuation function of the waiting multiactions of $G$, defined as follows. For $(\alpha,\natural_{l}^{\theta})\in{\cal WL}(G)$, let $I_{G}((\alpha,\natural_{l}^{\theta}))=\delta\in\{1,\ldots\theta\}$, if $(\alpha,\natural_{l}^{\theta})\in EnaWait([G]_{\approx})$ and $\exists H\in[G]_{\approx}\cap SatOpRegDynExpr\ \overline{(\alpha,\natural_{l}^{\theta})^{\delta}}$ or $(\alpha,\natural_{l}^{\theta})^{\delta}$ is a subexpression of $H$. We let $I_{G}(t)=*$, if $(\alpha,\natural_{l}^{\theta})\not\in EnaWait([G]_{\approx})$, where ‘$*$’ denotes the undefined value. The definition is correct by the argumentation from the proof of Proposition 3.1. Indeed, for each waiting multiaction of $G$, its timer value superscript (if any) is the same for every $H\in[G]_{\approx}\cap SatOpRegDynExpr$, in which that waiting multiaction, possibly being superscribed with the value of its timer and overlined or underlined, is a subexpression.

Let $G\in SatOpRegDynExpr$. Then for all $(\alpha,\natural_{l}^{\theta})\in{\cal WL}(G)$, we have $V_{\circlearrowleft\!G}((\alpha,\natural_{l}^{\theta}))=\max\{1,I_{G}((\alpha,\natural_{l}^{\theta}))-1\}$.

3.2 Action and empty move rules

The action rules are applied when some activities are executed. With these rules we capture the prioritization among different types of multiactions. We also have the empty move rule which is used to capture a delay of one discrete time unit when no immediate or waiting multiactions are executable. In this case, the empty multiset of activities is executed. The action and empty move rules will be used later to determine all multisets of activities which can be executed from the structural equivalence class of every dynamic expression (i.e. from the state of the corresponding process). This information together with that about probabilities or delays and weights of the activities to be executed from the current process state will be used to calculate the probabilities of such executions.

The action rules with stochastic (immediate or waiting, respectively) multiactions describe dynamic expression transformations in the form of $G\stackrel{{\scriptstyle\Gamma}}{{\rightarrow}}\widetilde{G}$ ($G\stackrel{{\scriptstyle I}}{{\rightarrow}}\widetilde{G}$ or $G\stackrel{{\scriptstyle W}}{{\rightarrow}}\widetilde{G}$, respectively) due to execution of non-empty multisets $\Gamma$ of stochastic ($I$ of immediate or $W$ of waiting, respectively) multiactions. The rules represent possible state changes of the specified processes when some non-empty multisets of stochastic (immediate or waiting, respectively) multiactions are executed. As we shall see, the application of an action rule with stochastic (immediate or waiting, respectively) multiactions to a dynamic expression leads in the corresponding LDTSDPN to a discrete time tick at which some stochastic or waiting transitions fire (or to the instantaneous firing of some immediate transitions) and possible change of the current marking. The current marking stays unchanged only if there is a self-loop produced by the iterative execution of a non-empty multiset, which must be one-element, i.e. a single stochastic (immediate or waiting, respectively) multiaction. The reason is the regularity requirement that allows no concurrency at the highest level of the second argument of iteration.

The empty move rule (applicable only when no immediate or waiting multiactions can be executed from the current state) describes dynamic expression transformations in the form of $G\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}\circlearrowleft\!G$, called the empty moves, due to execution of the empty multiset of activities at a discrete time tick. When no timer values are decremented within $G$ with the empty multiset execution at the next moment (for example, if $G$ contains no enabled waiting multiactions), we have $\circlearrowleft\!G=G$. In such a case, the empty move from $G$ is in the form of $G\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}G$, called the empty loop. As we shall see, the application of the empty move rule to a dynamic expression leads to a discrete time tick in the corresponding LDTSDPN at which no transitions fire and the current marking is not changed, but the timer values of the waiting transitions enabled at the marking (if any) are decremented by one. This is a new rule that has no prototype among inaction rules of PBC, since it represents a time delay, but no notion of time exists in PBC. The PBC rule $G\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}G$ from [10, 9] in our setting would correspond to the rule $G\Rightarrow G$ that describes staying in the current state when no time elapses. Since we do not need the latter rule to transform dynamic expressions into operative ones and it can even destroy the definition of operative expressions, we do not introduce it in dtsdPBC.

Thus, an application of every action rule with stochastic or waiting multiactions or the empty move rule requires one discrete time unit delay, i.e. the execution of a (possibly empty) multiset of stochastic or (non-empty) multiset of waiting multiactions leading to the dynamic expression transformation described by the rule is accomplished instantly after one time unit. An application of every action rule with immediate multiactions does not take any time, i.e. the execution of a (non-empty) multiset of immediate multiactions is accomplished instantly at the current moment of time.

Note that expressions of dtsdPBC can contain identical activities. To avoid technical difficulties, such as the proper calculation of the state change probabilities for multiple transitions, we can always enumerate coinciding activities from left to right in the syntax of expressions. The new activities, resulted from synchronization will be annotated with concatenation of numberings of the activities they come from, hence, the numbering should have a tree structure to reflect the effect of multiple synchronizations. We now define the numbering which encodes a binary tree with the leaves labeled by natural numbers.

Definition 3.4

The numbering of expressions is defined as $\iota::=\ n\mid(\iota)(\iota)$, where $n\in I\!\!N$.

Let $Num$ denote the set of all numberings of expressions.

Example 3.4

The numbering $1$ encodes the binary tree depicted in Figure 1(a) with the root labeled by $1$. The numbering $(1)(2)$ corresponds to the binary tree depicted in Figure 1(b) without internal nodes and with two leaves labeled by $1$ and $2$. The numbering $(1)((2)(3))$ represents the binary tree depicted in Figure 1(c) with one internal node, which is the root for the subtree $(2)(3)$, and three leaves labeled by $1,2$ and $3$.

The new activities resulting from synchronizations in different orders should be considered up to permutation of their numbering. In this way, we shall recognize different instances of the same activity. If we compare the contents of different numberings, i.e. the sets of natural numbers in them, we shall be able to identify the mentioned instances.

The content of a numbering $\iota\in Num$ is

[TABLE]

After the enumeration, the multisets of activities from the expressions will become the proper sets. In the following, we suppose that the identical activities are enumerated when needed to avoid ambiguity. This enumeration is considered to be implicit.

Definition 3.5

Let $G\in OpRegDynExpr$. We now define the set of all non-empty multisets of activities which can be potentially executed from $G$, denoted by $Can(G)$. Let $(\alpha,\kappa)\in{\cal SDL},\ E,F\in RegStatExpr,\ H\in OpRegDynExpr$ and $a\in Act$.

If $final(G)$ then $Can(G)=\emptyset$. 2. 2.

If $G=\overline{(\alpha,\kappa)^{\delta}}$ and $\kappa=\natural_{l}^{\theta},\ \theta\in I\!\!N_{\geq 2},\ l\in I\!\!R_{>0},\ \delta\in\{2,\ldots,\theta\}$, then $Can(G)=\emptyset$. 3. 3.

If $G=\overline{(\alpha,\kappa)}$ and $\kappa\in(0;1)$ or $\kappa=\natural_{l}^{0},\ l\in I\!\!R_{>0}$, then $Can(G)=\{\{(\alpha,\kappa)\}\}$. 4. 4.

If $G=\overline{(\alpha,\kappa)^{1}}$ and $\kappa=\natural_{l}^{\theta},\ \theta\in I\!\!N_{\geq 1},\ l\in I\!\!R_{>0}$, then $Can(G)=\{\{(\alpha,\kappa)\}\}$. 5. 5.

If $\Upsilon\in Can(G)$ then $\Upsilon\in Can(G\circ E),\ \Upsilon\in Can(E\circ G)\ (\circ\in\{;,[]\}),\ \Upsilon\in Can(G\|H),\ \Upsilon\in Can(H\|G),\\ f(\Upsilon)\in Can(G[f]),\ \Upsilon\in Can(G\ {\sf rs}\ a)\ (\mbox{when }a,\hat{a}\not\in{\cal A}(\Upsilon)),\ \Upsilon\in Can(G\ {\sf sy}\ a),\ \Upsilon\in Can([G*E*F]),\\ \Upsilon\in Can([E*G*F]),\ \Upsilon\in Can([E*F*G])$. 6. 6.

If $\Upsilon\in Can(G)$ and $\Xi\in Can(H)$ then $\Upsilon+\Xi\in Can(G\|H)$. 7. 7.

If $\Upsilon\in Can(G\ {\sf sy}\ a)$ and $(\alpha,\kappa),(\beta,\lambda)\in\Upsilon$ are different activities such that $a\in\alpha,\ \hat{a}\in\beta$, then

1. (a)

$(\Upsilon+\{(\alpha\oplus_{a}\beta,\kappa\cdot\lambda)\})\setminus\{(\alpha,\kappa),(\beta,\lambda)\}\in Can(G\ {\sf sy}\ a)$* if $\kappa,\lambda\in(0;1)$;* 2. (b)

$(\Upsilon+\{(\alpha\oplus_{a}\beta,\natural_{l+m}^{\theta})\})\setminus\{(\alpha,\kappa),(\beta,\lambda)\}\in Can(G\ {\sf sy}\ a)$* if $\kappa=\natural_{l}^{\theta},\ \lambda=\natural_{m}^{\theta},\ \theta\in I\!\!N,\ l,m\in I\!\!R_{>0}$.*

When we synchronize the same multiset of activities in different orders, we obtain several activities with the same multiaction and probability or delay and weight parts, but with different numberings having the same content. Then we only consider a single one of the resulting activities to avoid introducing redundant ones.

For example, the synchronization of stochastic multiactions $(\alpha,\rho)_{1}$ and $(\beta,\chi)_{2}$ in different orders generates the activities $(\alpha\oplus_{a}\beta,\rho\cdot\chi)_{(1)(2)}$ and $(\beta\oplus_{a}\alpha,\chi\cdot\rho)_{(2)(1)}$. Similarly, the synchronization of deterministic multiactions $(\alpha,\natural_{l}^{\theta})_{1}$ and $(\beta,\natural_{m}^{\theta})_{2}$ in different orders generates the activities $(\alpha\oplus_{a}\beta,\natural_{l+m}^{\theta})_{(1)(2)}$ and $(\beta\oplus_{a}\alpha,\natural_{m+l}^{\theta})_{(2)(1)}$. Since $Cont((1)(2))=\{1,2\}=Cont((2)(1))$, in both cases, only the first activity (or, symmetrically, the second one) resulting from synchronization will appear in a multiset from $Can(G\ {\sf sy}\ a)$.

Note that if $\Upsilon\in Can(G)$ then by definition of $Can(G),\ \forall\Xi\subseteq\Upsilon,\ \Xi\neq\emptyset$, we have $\Xi\in Can(G)$.

Let $G\in OpRegDynExpr$ and $Can(G)\neq\emptyset$. Obviously, if there are only stochastic (immediate or waiting, respectively) multiactions in the multisets from $Can(G)$ then these stochastic (immediate or waiting, respectively) multiactions can be executed from $G$. Otherwise, besides stochastic ones, there are also deterministic (immediate and/or waiting) multiactions in the multisets from $Can(G)$. By the note above, there are non-empty multisets of deterministic multiactions in $Can(G)$ as well, i.e. $\exists\Upsilon\in Can(G)\ \Upsilon\in I\!\!N_{fin}^{\cal DL}\setminus\{\emptyset\}$. In this case, no stochastic can be executed from $G$, even if $Can(G)$ contains non-empty multisets of stochastic multiactions, since deterministic multiactions have a priority over stochastic ones, and should be executed first. Further, if there are no stochastic, but both waiting and immediate multiactions in the multisets from $Can(G)$, then, analogously, no waiting multiactions can be executed from $G$, since immediate multiactions have a priority over waiting ones (besides that over stochastic ones).

When there are only waiting and, possibly, stochastic multiactions in the multisets from $Can(G)$ then, from above, only waiting ones can be executed from $G$. Then just maximal non-empty multisets of waiting multiactions can be executed from $G$, since all non-conflicting waiting multiactions cannot wait anymore and they should occur at the next time moment with probability $1$. The next definition formalizes these requirements.

Definition 3.6

Let $G\in OpRegDynExpr$. The set of all non-empty multisets of activities which can be executed from $G$ is

[TABLE]

Consider an operative dynamic expression $G\in OpRegDynExpr$. The expression $G$ is s-tangible (stochastically tangible), denoted by $stang(G)$, if $Now(G)\subseteq I\!\!N_{fin}^{\cal SL}\setminus\{\emptyset\}$. In particular, we have $stang(G)$, if $Now(G)=\emptyset$. The expression $G$ is w-tangible (waitingly tangible), denoted by $wtang(G)$, if $\emptyset\neq Now(G)\subseteq I\!\!N_{fin}^{\cal WL}\setminus\{\emptyset\}$. The expression $G$ is tangible, denoted by $tang(G)$, if $stang(G)$ or $wtang(G)$, i.e. $Now(G)\subseteq(I\!\!N_{fin}^{\cal SL}\cup I\!\!N_{fin}^{\cal WL})\setminus\{\emptyset\}$. Again, we particularly have $tang(G)$, if $Now(G)=\emptyset$. Otherwise, the expression $G$ is vanishing, denoted by $vanish(G)$, and in this case $\emptyset\neq Now(G)\subseteq I\!\!N_{fin}^{\cal IL}\setminus\{\emptyset\}$.

For a (possibly non-operative) dynamic expression $G\in RegDynExpr$, we write $stang(G)$ ($wtang(G)$ or $vanish(G)$, respectively), if $\forall H\in[G]_{\approx}\cap OpRegDynExpr$, we have $stang(H)$ ($wtang(H)$ or $vanish(H)$, respectively). We write $tang(G)$, if $stang(G)$ or $wtang(G)$. Note that the operative dynamic expressions from $[G]_{\approx}$ may have different types in general. The following example demonstrates two operative dynamic expressions $H$ and $H^{\prime}$ with $H\approx H^{\prime}$, such that $vanish(H)$, but $stang(H^{\prime})$.

Example 3.5

*Let $G=(\overline{(\{a\},\natural_{1}^{0})}[](\{b\},\natural_{2}^{0}))\|\overline{(\{c\},\frac{1}{2})}$ and $G^{\prime}=((\{a\},\natural_{1}^{0})[]\overline{(\{b\},\natural_{2}^{0})})\|\overline{(\{c\},\frac{1}{2})}$. Then $G\approx G^{\prime}$,

since $G\Leftarrow G^{\prime\prime}\Rightarrow G^{\prime}$ for $G^{\prime\prime}=\overline{((\{a\},\natural_{1}^{0})[](\{b\},\natural_{2}^{0}))}\|\overline{(\{c\},\frac{1}{2})}$, but $Can(G)=\{\{(\{a\},\natural_{1}^{0})\},\{(\{c\},\frac{1}{2})\},\{(\{a\},\natural_{1}^{0}),\\ (\{c\},\frac{1}{2})\}\},\ Can(G^{\prime})=\{\{(\{b\},\natural_{2}^{0})\},\{(\{c\},\frac{1}{2})\},\{(\{b\},\natural_{2}^{0}),(\{c\},\frac{1}{2})\}\}$ and $Now(G)=\{\{(\{a\},\natural_{1}^{0})\}\},\ Now(G^{\prime})=\{\{(\{b\},\natural_{2}^{0})\}\}$. Clearly, we have $vanish(G)$ and $vanish(G^{\prime})$. The executions like that of $\{(\{c\},\frac{1}{2})\}$ (and all multisets including it) from $G$ and $G^{\prime}$ must be disabled using preconditions in the action rules, since immediate multiactions have a priority over stochastic ones, hence, the former are always executed first.*

Let $H=\overline{(\{a\},\natural_{1}^{0})}[](\{b\},\frac{1}{2})$ and $H^{\prime}=(\{a\},\natural_{1}^{0})[]\overline{(\{b\},\frac{1}{2})}$. Then $H\approx H^{\prime}$, since $H\Leftarrow H^{\prime\prime}\Rightarrow H^{\prime}$ for $H^{\prime\prime}=\overline{(\{a\},\natural_{1}^{0})[](\{b\},\frac{1}{2})}$, but $Can(H)=Now(H)=\{\{(\{a\},\natural_{1}^{0})\}\}$ and $Can(H^{\prime})=Now(H^{\prime})=\{\{(\{b\},\frac{1}{2})\}\}$. We have $vanish(H)$, but $stang(H^{\prime})$. To make the action rules correct under structural equivalence, the executions like that of $\{(\{b\},\frac{1}{2})\}$ from $H^{\prime}$ must be disabled using preconditions in the action rules, since immediate multiactions have a priority over stochastic ones, hence, the choices between them are always resolved in favour of the former.

In Table 3, we define the action and empty move rules. In the table, $(\alpha,\rho),(\beta,\chi)\!\in{\cal SL},\ (\alpha,\natural_{l}^{0}),(\beta,\natural_{m}^{0})\in{\cal IL}$ and $(\alpha,\natural_{l}^{\theta}),(\beta,\natural_{m}^{\theta})\in{\cal WL}$ Further, $E,F,K\in RegStatExpr,\ G,H\in SatOpRegDynExpr,\ \widetilde{G},\widetilde{H}\!\in\!RegDynExpr$ and $a\in Act$. Moreover, $\Gamma,\Delta\in I\!\!N_{fin}^{\cal SL}\setminus\{\emptyset\},\ \Gamma^{\prime}\in I\!\!N_{fin}^{\cal SL},\ I,J\in I\!\!N_{fin}^{\cal IL}\setminus\{\emptyset\},\ I^{\prime}\in I\!\!N_{fin}^{\cal IL},\ V,W\in I\!\!N_{fin}^{\cal WL}\setminus\{\emptyset\},\ V^{\prime}\in I\!\!N_{fin}^{\cal WL}$ and $\Upsilon\in I\!\!N_{fin}^{\cal SDL}\setminus\{\emptyset\}$.

We use the following abbreviations in the names of the rules from the table: “E” for “Empty move”, “B” for “Basis case”, “S” for “Sequence”, “C” for “Choice”, “P” for “Parallel”, “L” for “reLabeling”, “R” for “Restriction”, “I” for “Iteraton” and “Sy” for “Synchronization”. The first rule in the table is the empty move rule E. The other rules are the action rules, describing transformations of dynamic expressions, which are built using particular algebraic operations. If we cannot merge the rules with stochastic, immediate ans waiting multiactions in one rule for some operation then we get the coupled action rules. In such cases, the names of the action rules with stochastic multiactions have a suffix ‘s’, those with immediate multiactions have a suffix ‘i’, and those with waiting multiactions have a suffix ‘w’. To make presentation more compact, the action rules with double conclusion are combined from two distinct action rules with the same premises.

Almost all the rules in Table 3 (excepting E, Bw, P2s, P2i, P2w, Sy2s, Sy2i and Sy2w) resemble those of gsPBC, but the former correspond to execution of multisets of activities, not of single activities, as in the latter, and our rules have simpler preconditions (if any), since all immediate multiactions in dtsdPBC have the same priority level, unlike those of gsPBC.

The preconditions in rules E, Cs, P1s, and I2s are needed to ensure that (possibly empty) multisets of stochastic multiactions are executed only from s-tangible saturated operative dynamic expressions, such that all dynamic expressions structurally equivalent to them are s-tangible as well. For example, if $init(G)$ in rule Cs then $G\approx\overline{F}$ for some static expression $F$ and $G[]E\approx\overline{F}[]E\approx\overline{F[]E}\approx F[]\overline{E}$. Hence, it should be guaranteed that $stang(F[]\overline{E})$, which holds iff $stang(\overline{E})$. The case $E[]G$ is treated similarly. In rule P1s, assuming that $stang(G)$, it should be guaranteed that $stang(G\|H)$ and $stang(H\|G)$, which holds iff $stang(H)$. The precondition in rule I2s is analogous to that in rule Cs.

Analogously, the preconditions in rules Cw, and I2w are needed to ensure that non-empty multisets of waiting multiactions are executed only from tangible saturated operative dynamic expressions, such that all dynamic expressions structurally equivalent to them are tangible as well. This requirement (about tangible expressions) means that only (possibly empty) multisets of stochastic multiactions or non-empty multisets of waiting multiactions, and no immediate multiactions, can be executed from the subprocess $H$ that is composed alternatively (in choice) with the subprocess $G$. Hence, the multiset $W$ of waiting multiactions, executed from $G$, can also be executed from the composition of $G$ and $H$, since immediate multiactions cannot occur from $H$. Otherwise, it would prevent the execution of $W$ from $G$ in the composite process, by disregarding the alternative choice of the branch specified by $H$, due to the zero delays and priority (captured by all action rules) of immediate multiactions over all other multiaction types.

The precondition in rule P1w is an exception from the above, and is needed to ensure that non-empty multisets of waiting multiactions are executed only from s-tangible saturated operative dynamic expressions, such that all dynamic expressions structurally equivalent to them are s-tangible as well. This stricter requirement (about s-tangible, instead of just tangible, expressions) means that only (possibly empty) multisets of stochastic multiactions, and no immediate or waiting multiactions, can be executed from the subprocess $H$ that is composed concurrently (in parallel) with the subprocess $G$. Hence, the multiset $W$ of waiting multiactions, executed from $G$, is also a maximal (by the inclusion relation) multiset that can be executed from the parallel composition of $G$ and $H$. The reason is that only the timers decrement by one time unit (by applying rule E) is actually possible in $H$ while executing $W$ from $G$, due to priority (captured by all action rules) of waiting multiactions over stochastic ones. Thus, taking the rule precondition $stang(H)$ instead of $tang(H)$ preserves maximality of the steps consisting of waiting multiactions while applying parallel composition.

In rules P1s and P1w, the timer value decrementing by one $\circlearrowleft\!H$, applied to the s-tangible saturated operative dynamic expression $H$ that is composed in parallel with $G$, from which stochastic multiactions are executed at the next time tick, is used to maintain the time progress uniformity in the composite expression. Although rules P1s and P1w can be merged, we have not done it, aiming to emphasize the exceptional precondition in rule P1w.

In rules Cs, Ci and Cw, the timer values discarding $\downharpoonleft\!\!E$, applied to the static expression $E$ that is composed in choice with $G$, from which activities are executed, signifies that the timer values of the non-chosen subexpression (branch) become irrelevant in the composite expression and thus may be removed. Analogously, in rules I2s, I2i and I2w, the timer values discarding $\downharpoonleft\!\!F$ is applied to the static expression $F$ that is an alternative to $G$, from which activities are executed, since the choice is always made between the body and termination subexpressions of the composite iteration expression (between the second and third arguments of iteration).

Rule E corresponds to one discrete time unit delay (passage of one unit of time) while executing no activities and therefore it has no analogues among the rules of gsPBC that adopts the continuous time model. Rule E is a global one, i.e. it is applied only to the whole (topmost level of) expressions, rather than to their parts. The reason is that all other action rules describe dynamic expressions transformations due to execution of non-empty multisets of activities. Hence, the actionless time move described by rule E cannot “penetrate” with action rules through the expressions structure. This guarantees that time progresses uniformly in all their subexpressions.

Rule Bw differs from the more standard ones Bs and Bi that both resemble rule B in gsPBC. The reason is that in Bw, the overlined waiting multiaction has an extra superscript ‘$1$’, indicating that one time unit is remained until the multiaction’s execution (RTE equals one) that should follow in the next moment.

Rules P2s, P2i and P2w have no similar rules in gsPBC, since interleaving semantics of the algebra allows no simultaneous execution of activities. On the other hand, P2s, P2i and P2w have in PBC the analogous rule PAR that is used to construct step semantics of the calculus, but the former two rules correspond to execution of multisets of activities, unlike that of multisets of multiactions in the latter rule. Rules P2s, P2i and P2w cannot be merged, since otherwise simultaneous execution of different types of multiactions would be allowed.

Rules Sy2s, Sy2i and Sy2w differ from the corresponding synchronization rules in gsPBC, since the probability or the weight of synchronization in the former rules and the rate or the weight of synchronization in the latter rules are calculated in two distinct ways. Rules Sy2i and Sy2w cannot be merged, since otherwise synchronous execution of immediate and waiting multiactions would be allowed.

Rule Sy2s establishes that the synchronization of two stochastic multiactions is made by taking the product of their probabilities, since we are considering that both must occur for the synchronization to happen, so this corresponds, in some sense, to the probability of the independent event intersection, but the real situation is more complex, since these stochastic multiactions can also be executed in parallel. Nevertheless, when scoping (the combined operation consisting of synchronization followed by restriction over the same action [9]) is applied over a parallel execution, we get as final result just the simple product of the probabilities, since no normalization is needed there. Multiplication is an associative and commutative binary operation that is distributive over addition, i.e. it fulfills all practical conditions imposed on the synchronization operator in [24]. Further, if both arguments of multiplication are from $(0;1)$ then the result belongs to the same interval, hence, multiplication naturally maintains probabilistic compositionality in our model. Our approach is similar to the multiplication of rates of the synchronized actions in MTIPP [23] in the case when the rates are less than $1$. Moreover, for the probabilities $\rho$ and $\chi$ of two stochastic multiactions to be synchronized we have $\rho\cdot\chi<\min\{\rho,\chi\}$, i.e. multiplication meets the performance requirement stating that the probability of the resulting synchronized stochastic multiaction should be less than the probabilities of the two ones to be synchronized. While performance evaluation, it is usually supposed that the execution of two components together require more system resources and time than the execution of each single one. This resembles the bounded capacity assumption from [24]. Thus, multiplication is easy to handle with and it satisfies the algebraic, probabilistic, time and performance requirements. Therefore, we have chosen the product of the probabilities for the synchronization. See also [13, 12] for a discussion about binary operations producing the rates of synchronization in the continuous time setting.

In rules Sy2i and Sy2w, we sum the weights of two synchronized immediate (waiting, respectively) multiactions, since the weights can be interpreted as the rewards [50], thus, we collect the rewards. Moreover, we express that the synchronized execution of immediate (waiting) multiactions has more importance than that of every single one. The weights of immediate and waiting (i.e. deterministic) multiactions can also be seen as bonus rewards associated with transitions [6]. The rewards are summed during synchronized execution of immediate (waiting) multiactions, since in that case all the synchronized activities can be seen as participated in the execution. We prefer to collect more rewards, thus, the transitions providing greater rewards will have a preference and they will be executed with a greater probability. In particular, since execution of immediate multiactions takes no time, we prefer to collect in a step (parallel execution) as many synchronized immediate multiactions as possible to get more significant progress in behaviour. Under behavioural progress we understand an advance in executing activities, which does not always imply a progress in time, as in the case when the activities are immediate multiactions. This aspect will be used later, while evaluating performance via analysis of the embedded discrete time Markov chains (EDTMCs) of expressions. Since every state change in EDTMC takes one unit of (its local) time, greater advance in operation of the EDTMC allows one to calculate quicker many performance indices. As for waiting multiactions, only the maximal multisets of them, executable from a state, occur with a time tick. The reason is that each waiting multiaction has a probability $1$ to occur in the next moment, when the remaining time of its timer (RTE) equals one and there exist no conflicting waiting multiactions. Hence, all waiting multiactions with the RTE being one that are executable together from a state must participate in a step from that state. Since there may exist different such maximal multisets of waiting multiactions, a probabilistic choice among all possible steps is made, imposed by the weights of those multiactions. Thus, the steps of waiting multiactions always produce maximal overall weights, but they are mainly used to calculate the probabilities of alternative maximal steps rather than the cumulative bonus rewards.

We do not have self-synchronization, i.e. synchronization of an activity with itself, since all the (enumerated) activities executed together are considered to be different. This allows us to avoid rather cumbersome and unexpected behaviour, as well as many technical difficulties [9].

Notice that the timers of all waiting multiactions that lose their overlines when a state change occurs become inactive (turned off) and their values become irrelevant while the timers of all those preserving their overlines continue running with their stored values. Hence, we adopt the enabling memory memory policy [41, 1, 2, 3] when the process states are changed and the overlining of deterministic multiactions is possibly modified (remember that immediate multiactions may be seen as those with the timers displaying a single value [math], so we do not need to store their values). Then the timer values of waiting multiactions are taken as the enabling memory variables.

In Table 4, inaction rules, action rules (with stochastic or immediate, or waiting multiactions) and empty move rule are compared according to the three questions about their application: whether it changes the current state, whether it leads to a time progress, and whether it results in execution of some activities. Positive answers to the questions are denoted by the plus sign while negative ones are specified by the minus sign. If both positive and negative answers can be given to some of the questions in different cases then the plus-minus sign is written. Notice that the process states are considered up to structural equivalence of the corresponding expressions, and time progress is not regarded as a state change.

3.3 Transition systems

We now construct labeled probabilistic transition systems associated with dynamic expressions. The transition systems are used to define the operational semantics of dynamic expressions.

Let $G$ be a dynamic expression and $s=[G]_{\approx}$. The set of all multisets of activities executable in $s$ is defined as $Exec(s)=\{\Upsilon\mid\exists H\in s\ \exists\widetilde{H}\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}$. Here $H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}$ is an inference by the rules from Table 3.

It can be proved by induction on the structure of expressions that $\Upsilon\in Exec(s)\setminus\{\emptyset\}$ implies $\exists H\in s\ \Upsilon\in Now(H)$. The reverse statement does not hold in general, as the next example shows.

Example 3.6

Let $H,H^{\prime}$ be from Example 3.5 and $s=[H]_{\approx}=[H^{\prime}]_{\approx}$. We have $Now(H)=\{\{(\{a\},\natural_{1}^{0})\}\}$ and $Now(H^{\prime})=\{\{(\{b\},\frac{1}{2})\}\}$. Since only rules Ci and Bi can be applied to $H$ while no action rule can be applied to $H^{\prime}$, we get $Exec(s)=\{\{(\{a\},\natural_{1}^{0})\}\}$. Then, for $H^{\prime}\in s$ and $\Upsilon=\{(\{b\},\frac{1}{2})\}\in Now(H^{\prime})$, we obtain $\Upsilon\not\in Exec(s)$.

The state $s$ is s-tangible (stochastically tangible) if $Exec(s)\subseteq I\!\!N_{fin}^{\cal SL}$. For an s-tangible state $s$ we always have $\emptyset\in Exec(s)$ by rule E, hence, we may have $Exec(s)=\{\emptyset\}$. The state $s$ is w-tangible (waitingly tangible) if $Exec(s)\subseteq I\!\!N_{fin}^{\cal WL}\setminus\{\emptyset\}$. The state $s$ is tangible if it is s-tangible or w-tangible, i.e. $Exec(s)\subseteq I\!\!N_{fin}^{\cal SL}\cup I\!\!N_{fin}^{\cal WL}$. Again, for tangible states we may have $\emptyset\in Exec(s)$ and $Exec(s)=\{\emptyset\}$. Otherwise, the state $s$ is vanishing, and in this case $Exec(s)\subseteq I\!\!N_{fin}^{\cal IL}\setminus\{\emptyset\}$.

Note that if $\Upsilon\in Exec(s)$ and $\Upsilon\in I\!\!N_{fin}^{\cal SL}\cup I\!\!N_{fin}^{\cal IL}$ then by rules P2s, P2i, Sy2s, Sy2i and definition of $Exec(s)\ \forall\Xi\subseteq\Upsilon,\ \Xi\neq\emptyset$, we have $\Xi\in Exec(s)$.

Since the inaction rules only distribute and move upper and lower bars along the syntax of dynamic expressions, all $H\in s$ have the same underlying static expression $F$. Process expressions always have a finite length, hence, the number of all (enumerated) activities and the number of all operations in the syntax of $F$ are finite as well. The action rules Sy2s, Sy2i and Sy2w are the only ones that generate new activities. They result from the handshake synchronization of actions and their conjugates belonging to the multiaction parts of the first and second constituent activity, respectively. Since we have a finite number of operators \ {\sf sy}\ in $F$ and all the multiaction parts of the activities are finite multisets, the number of the new synchronized activities is also finite. The action rules contribute to $Exec(s)$ (in addition to the empty set, if rule E is applicable) only the sets consisting both of activities from $F$ and the new activities, produced by Sy2s, Sy2i and Sy2w. Since we have a finite number $n$ of all such activities, we get $|Exec(s)|\leq 2^{n}<\infty$. Thus, summation and multiplication by elements from the finite set $Exec(s)$ are well-defined. Similar reasoning can be used to demonstrate that for all dynamic expressions $H$ (not just for those from $s$), $Now(H)$ is a finite set.

Definition 3.7

The derivation set of a dynamic expression $G$, denoted by $DR(G)$, is the minimal set such that

• •

$[G]_{\approx}\in DR(G)$;

• •

if $[H]_{\approx}\in DR(G)$ and $\exists\Upsilon\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}$ then $[\widetilde{H}]_{\approx}\in DR(G)$.

The set of all s-tangible states from $DR(G)$ is denoted by $DR_{ST}(G)$, and the set of all w-tangible states from $DR(G)$ is denoted by $DR_{WT}(G)$. The set of all tangible states from $DR(G)$ is denoted by $DR_{T}(G)=DR_{ST}(G)\cup DR_{WT}(G)$. The set of all vanishing states from $DR(G)$ is denoted by $DR_{V}(G)$. Obviously, $DR(G)=DR_{T}(G)\uplus DR_{V}(G)=DR_{ST}(G)\uplus DR_{WT}(G)\uplus DR_{V}(G)$, where $\uplus$ denotes disjoint union.

Let now $G$ be a dynamic expression and $s,\tilde{s}\in DR(G)$.

Let $\Upsilon\in Exec(s)\setminus\{\emptyset\}$. The probability that the multiset of stochastic multiactions $\Upsilon$ is ready for execution in $s$ or the weight of the multiset of deterministic multiactions $\Upsilon$ which is ready for execution in $s$ is

[TABLE]

In the case $\Upsilon=\emptyset$ and $s\in DR_{ST}(G)$ we define

[TABLE]

If $s\in DR_{ST}(G)$ and $Exec(s)\neq\{\emptyset\}$ then $PF(\Upsilon,s)$ can be interpreted as a joint probability of independent events (in a probability sense, i.e. the probability of intersection of these events is equal to the product of their probabilities). Each such an event consists in the positive or the negative decision to be executed of a particular stochastic multiaction. Every executable stochastic multiaction decides probabilistically (using its probabilistic part) and independently (from others), if it wants to be executed in $s$. If $\Upsilon$ is a multiset of all executable stochastic multiactions which have decided to be executed in $s$ and $\Upsilon\in Exec(s)$ then $\Upsilon$ is ready for execution in $s$. The multiplication in the definition is used because it reflects the probability of the independent event intersection. Alternatively, when $\Upsilon\neq\emptyset,\ PF(\Upsilon,s)$ can be interpreted as the probability to execute exclusively the multiset of stochastic multiactions $\Upsilon$ in $s$, i.e. the probability of intersection of two events calculated using the conditional probability formula in the form of ${\sf P}(X\cap Y)={\sf P}(X|Y){\sf P}(Y)$. The event $X$ consists in the execution of $\Upsilon$ in $s$. The event $Y$ consists in the non-execution in $s$ of all the executable stochastic multiactions not belonging to $\Upsilon$. Since the mentioned non-executions are obviously independent events, the probability of $Y$ is a product of the probabilities of the non-executions: ${\sf P}(Y)=\prod_{\{\{(\beta,\chi)\}\in Exec(s)\mid(\beta,\chi)\not\in\Upsilon\}}(1-\chi)$. The conditioning of $X$ by $Y$ makes the executions of the stochastic multiactions from $\Upsilon$ independent, since all of them can be executed in parallel in $s$ by definition of $Exec(s)$. Hence, the probability to execute $\Upsilon$ under condition that no executable stochastic multiactions not belonging to $\Upsilon$ are executed in $s$ is a product of probabilities of these stochastic multiactions: ${\sf P}(X|Y)=\prod_{(\alpha,\rho)\in\Upsilon}\rho$. Thus, the probability that $\Upsilon$ is executed and no executable stochastic multiactions not belonging to $\Upsilon$ are executed in $s$ is the probability of $X$ conditioned by $Y$ multiplied by the probability of $Y$: ${\sf P}(X\cap Y)={\sf P}(X|Y){\sf P}(Y)=\prod_{(\alpha,\rho)\in\Upsilon}\rho\cdot\prod_{\{\{(\beta,\chi)\}\in Exec(s)\mid(\beta,\chi)\not\in\Upsilon\}}(1-\chi)$. When $\Upsilon=\emptyset,\ PF(\Upsilon,s)$ can be interpreted as the probability not to execute in $s$ any executable stochastic multiactions, thus, $PF(\emptyset,s)=\prod_{\{(\beta,\chi)\}\in Exec(s)}(1-\chi)$. When only the empty multiset of activities can be executed in $s$, i.e. $Exec(s)=\{\emptyset\}$, we take $PF(\emptyset,s)=1$, since we stay in $s$ in this case. Note that for $s\in DR_{T}(G)$ we have $PF(\emptyset,s)\in(0;1]$, hence, we can stay in $s$ at the next time moment with a certain positive probability.

If $s\in DR_{WT}(G)\cup DR_{V}(G)$ then $PF(\Upsilon,s)$ could be interpreted as the overall (cumulative) weight of the deterministic multiactions from $\Upsilon$, i.e. the sum of all their weights. The summation here is used since the weights can be seen as the rewards which are collected [50]. This means that concurrent execution of the deterministic multiactions has more importance than that of every single one. The weights of deterministic multiactions can also be interpreted as bonus rewards of transitions [6]. The rewards are summed when deterministic multiactions are executed in parallel, because all of them participated in the execution. In particular, since execution of immediate multiactions takes no time, we prefer to collect in a step (parallel execution of activities) as many parallel immediate multiactions as possible to get more progress in behaviour. This aspect will be used later, while while evaluating performance on the basis of the EDTMCs of expressions. Concerning waiting multiactions, only the maximal multisets of them executable from a state occur in the next moment. Therefore, the steps of waiting multiactions produce maximal overall weights, which are used to calculate probabilities of alternative maximal steps rather than the cumulative bonuses. Note that this reasoning is the same as that used to define the weight of synchronized immediate (waiting, respectively) multiactions in the rules Sy2i and Sy2w.

Note that the definition of $PF(\Upsilon,s)$ (as well as the definitions of other probability functions which we shall present) is based on the enumeration of activities which is considered implicit.

Let $\Upsilon\in Exec(s)$. Besides $\Upsilon$, some other multisets of activities may be ready for execution in $s$, hence, a kind of conditioning or normalization is needed to calculate the execution probability. The probability to execute the multiset of activities $\Upsilon$ in $s$ is

[TABLE]

If $s\in DR_{ST}(G)$ then $PT(\Upsilon,s)$ can be interpreted as the conditional probability to execute $\Upsilon$ in $s$ calculated using the conditional probability formula in the form of ${\sf P}(Z|W)=\frac{{\sf P}(Z\cap W)}{{\sf P}(W)}$. The event $Z$ consists in the exclusive execution of $\Upsilon$ in $s$, hence, ${\sf P}(Z)=PF(\Upsilon,s)$. The event $W$ consists in the exclusive execution of any set (including the empty one) $\Xi\in Exec(s)$ in $s$. Thus, $W=\cup_{j}Z_{j}$, where $\forall j,\ Z_{j}$ are mutually exclusive events (in a probability sense, i.e. intersection of these events is the empty event) and $\exists i,\ Z=Z_{i}$. We have ${\sf P}(W)=\sum_{j}{\sf P}(Z_{j})=\sum_{\Xi\in Exec(s)}PF(\Xi,s)$, because summation reflects the probability of the mutually exclusive event union. Since $Z\cap W=Z_{i}\cap(\cup_{j}Z_{j})=Z_{i}=Z$, we have ${\sf P}(Z|W)=\frac{{\sf P}(Z)}{{\sf P}(W)}=\frac{PF(\Upsilon,s)}{\sum_{\Xi\in Exec(s)}PF(\Xi,s)}$. $PF(\Upsilon,s)$ can also be seen as the potential probability to execute $\Upsilon$ in $s$, since we have $PF(\Upsilon,s)=PT(\Upsilon,s)$ only when all sets (including the empty one) consisting of the executable stochastic multiactions can be executed in $s$. In this case, all the mentioned stochastic multiactions can be executed in parallel in $s$ and we have $\sum_{\Xi\in Exec(s)}PF(\Xi,s)=1$, since this sum collects the products of all combinations of the probability parts of the stochastic multiactions and the negations of these parts. But in general, for example, for two stochastic multiactions $(\alpha,\rho)$ and $(\beta,\chi)$ executable in $s$, it may happen that they cannot be executed in $s$ together, in parallel, i.e. $\emptyset,\{(\alpha,\rho)\},\{(\beta,\chi)\}\in Exec(s)$, but $\{(\alpha,\rho),(\beta,\chi)\}\not\in Exec(s)$. Note that for $s\in DR_{T}(G)$ we have $PT(\emptyset,s)\in(0;1]$, hence, there is a non-zero probability to stay in the state $s$ at the next time moment, and the residence time in $s$ is at least $1$ discrete time unit.

If $s\in DR_{WT}(G)\cup DR_{V}(G)$ then $PT(\Upsilon,s)$ can be interpreted as the weight of the set of deterministic multiactions $\Upsilon$ which is ready for execution in $s$ normalized by the weights of all the sets executable in $s$. This approach is analogous to that used in the EMPA definition of the probabilities of immediate actions executable from the same process state [7] (inspired by way in which the probabilities of conflicting immediate transitions in GSPNs are calculated [3]). The only difference is that we have a step semantics and, for every set of deterministic multiactions executed in parallel, we should use its cumulative weight. To get the analogy with EMPA possessing interleaving semantics, we should interpret the weights of immediate actions of EMPA as the cumulative weights of the sets of deterministic multiactions of dtsdPBC.

The advantage of our two-stage approach to definition of the probability to execute a set of activities is that the resulting probability formula $PT(\Upsilon,s)$ is valid both for (sets of) stochastic and deterministic multiactions. It allows one to unify the notation used later while constructing the operational semantics and analyzing performance.

Note that the sum of outgoing probabilities for the expressions belonging to the derivations of $G$ is equal to $1$. More formally, $\forall s\in DR(G)\ \sum_{\Upsilon\in Exec(s)}PT(\Upsilon,s)=1$. This, obviously, follows from the definition of $PT(\Upsilon,s)$, and guarantees that it defines a probability distribution.

The probability to move from $s$ to $\tilde{s}$ by executing any multiset of activities is

[TABLE]

The summation in the definition above reflects the probability of the mutually exclusive event union, since $\sum_{\{\Upsilon\mid\exists H\in s,\ \exists\widetilde{H}\in\tilde{s},\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}}PT(\Upsilon,s)=\frac{1}{\sum_{\Xi\in Exec(s)}PF(\Xi,s)}\cdot\sum_{\{\Upsilon\mid\exists H\in s,\ \exists\widetilde{H}\in\tilde{s},\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}}PF(\Upsilon,s)$, where for each $\Upsilon,\ PF(\Upsilon,s)$ is the probability of the exclusive execution of $\Upsilon$ in $s$. Note that $\forall s\in DR(G)\\ \sum_{\{\tilde{s}\mid\exists H\in s\ \exists\widetilde{H}\in\tilde{s}\ \exists\Upsilon\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}}PM(s,\tilde{s})=\sum_{\{\tilde{s}\mid\exists H\in s\ \exists\widetilde{H}\in\tilde{s}\ \exists\Upsilon\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}}\sum_{\{\Upsilon\mid\exists H\in s\ \exists\widetilde{H}\in\tilde{s}\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}}PT(\Upsilon,s)=\\ \sum_{\Upsilon\in Exec(s)}PT(\Upsilon,s)=1$.

Example 3.7

Let $E=(\{a\},\rho)[](\{a\},\chi)$, where $\rho,\chi\in(0;1)$. $DR(\overline{E})$ consists of the equivalence classes $s_{1}=[\overline{E}]_{\approx}$ and $s_{2}=[\underline{E}]_{\approx}$. We have $DR_{T}(\overline{E})=\{s_{1},s_{2}\}$. The execution probabilities are calculated as follows. Since $Exec(s_{1})=\{\emptyset,\{(\{a\},\rho)\},\{(\{a\},\chi)\}\}$, we get $PF(\{(\{a\},\rho)\},s_{1})=\rho(1-\chi),\ PF(\{(\{a\},\chi)\},s_{1})=\chi(1-\rho)$ and $PF(\emptyset,s_{1})=(1-\rho)(1-\chi)$. Then $\sum_{\Xi\in Exec(s_{1})}PF(\Xi,s_{1})=\rho(1-\chi)+\chi(1-\rho)+(1-\rho)(1-\chi)=1-\rho\chi$. Thus, $PT(\{(\{a\},\rho)\},s_{1})=\frac{\rho(1-\chi)}{1-\rho\chi},\ PT(\{(\{a\},\chi)\},s_{1})=\frac{\chi(1-\rho)}{1-\rho\chi}$ and $PT(\emptyset,s_{1})=PM(s_{1},s_{1})=\frac{(1-\rho)(1-\chi)}{1-\rho\chi}$. Further, $Exec(s_{2})=\{\emptyset\}$, hence, $\sum_{\Xi\in Exec(s_{2})}PF(\Xi,s_{2})=PF(\emptyset,s_{2})=1$ and $PT(\emptyset,s_{2})=PM(s_{2},s_{2})=\frac{1}{1}=1$. Finally, $PM(s_{1},s_{2})=PT(\{(\{a\},\rho)\},s_{1})+PT(\{(\{a\},\chi)\},s_{1})=\frac{\rho(1-\chi)}{1-\rho\chi}+\frac{\chi(1-\rho)}{1-\rho\chi}=\frac{\rho+\chi-2\rho\chi}{1-\rho\chi}$.

Let $E^{\prime}=(\{a\},\natural_{l}^{0})[](\{a\},\natural_{m}^{0})$, where $l,m\in I\!\!R_{>0}$. $DR(\overline{E^{\prime}})$ consists of the equivalence classes $s_{1}^{\prime}=[\overline{E^{\prime}}]_{\approx}$ and $s_{2}^{\prime}=[\underline{E^{\prime}}]_{\approx}$. We have $DR_{T}(\overline{E^{\prime}})=\{s_{2}^{\prime}\}$ and $DR_{V}(\overline{E^{\prime}})=\{s_{1}^{\prime}\}$. The execution probabilities are calculated as follows. Since $Exec(s_{1}^{\prime})=\{\{(\{a\},\natural_{l}^{0})\},\{(\{a\},\natural_{m}^{0})\}\}$, we get $PF(\{(\{a\},\natural_{l}^{0})\},s_{1}^{\prime})=l$ and $PF(\{(\{a\},\natural_{m}^{0})\},s_{1}^{\prime})=m$. Then $\sum_{\Xi\in Exec(s_{1}^{\prime})}PF(\Xi,s_{1}^{\prime})=l+m$. Thus, $PT(\{(\{a\},\natural_{l}^{0})\},s_{1}^{\prime})=\frac{l}{l+m}$ and $PT(\{(\{a\},\natural_{m}^{0})\},s_{1}^{\prime})=\frac{m}{l+m}$. Further, $Exec(s_{2}^{\prime})=\{\emptyset\}$, hence, $\sum_{\Xi\in Exec(s_{2}^{\prime})}PF(\Xi,s_{2}^{\prime})=PF(\emptyset,s_{2}^{\prime})=1$ and $PT(\emptyset,s_{2}^{\prime})=PM(s_{2}^{\prime},s_{2}^{\prime})=\frac{1}{1}=1$. Finally, $PM(s_{1}^{\prime},s_{2}^{\prime})=PT(\{(\{a\},\natural_{l}^{0})\},s_{1}^{\prime})+PT(\{(\{a\},\natural_{m}^{0})\},s_{1}^{\prime})=\frac{l}{l+m}+\frac{m}{l+m}=1$.

Definition 3.8

Let $G$ be a dynamic expression. The (labeled probabilistic) transition system of $G$ is a quadruple $TS(G)=(S_{G},L_{G},{\cal T}_{G},s_{G})$, where

• •

the set of states is $S_{G}=DR(G)$;

• •

the set of labels is $L_{G}=I\!\!N_{fin}^{\cal SDL}\times(0;1]$;

• •

the set of transitions is ${\cal T}_{G}=\{(s,(\Upsilon,PT(\Upsilon,s)),\tilde{s})\mid s,\tilde{s}\in DR(G),\ \exists H\in s\ \exists\widetilde{H}\in\tilde{s}\ H\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\widetilde{H}\}$;

• •

the initial state is $s_{G}=[G]_{\approx}$.

Example 3.8

Let $E$ be from Example 3.1. The next inferences by rule E are possible from the elements of $[\overline{E}]_{\approx}$:

[TABLE]

The first and second inferences suggest the empty move transition $[\overline{E}]_{\approx}\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}[\overline{(\{a\},\natural_{1}^{3})^{2}[](\{b\},\frac{1}{3})}]_{\approx}\neq[\overline{E}]_{\approx}$. The intuition is that the timer of the enabled waiting multiaction $(\{a\},\natural_{1}^{3})$ is decremented by one time unit in the both cases, whenever it is overlined or not. Later we shall see that in the both cases, the respective waiting transition of the LDTSDPN corresponding to $\overline{E}$ will be enabled at a “common” marking (that also enables a stochastic transition, matched up to $(\{b\},\frac{1}{3})$), so its timer should be decreased by one with a time tick while staying at the same marking, and such a time move will lead to a different state of the LDTSDPN.

The definition of $TS(G)$ is correct, i.e. for every state, the sum of the probabilities of all the transitions starting from it is $1$. This is guaranteed by the note after the definition of $PT(\Upsilon,s)$. Thus, we have defined a generative model of probabilistic processes, according to the classification from [20]. The reason is that the sum of the probabilities of the transitions with all possible labels should be equal to $1$, not only of those with the same labels (up to enumeration of activities they include) as in the reactive models, and we do not have a nested probabilistic choice as in the stratified models.

The transition system $TS(G)$ associated with a dynamic expression $G$ describes all the steps (parallel executions) that occur at discrete time moments with some (one-step) probability and consist of multisets of activities. Every step consisting of stochastic (waiting, respectively) multiactions or the empty step (i.e. that consisting of the empty multiset of activities) occurs instantly after one discrete time unit delay. Each step consisting of immediate multiactions occurs instantly without any delay. The step can change the current state to a different one. The states are the structural equivalence classes of dynamic expressions obtained by application of action rules starting from the expressions belonging to $[G]_{\approx}$. A transition $(s,(\Upsilon,{\cal P}),\tilde{s})\in{\cal T}_{G}$ will be written as $s\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}_{\cal P}\tilde{s}$. It is interpreted as follows: the probability to change the state $s$ to $\tilde{s}$ as a result of executing $\Upsilon$ is ${\cal P}$.

Note that from every s-tangible state the empty multiset of activities can always be executed by rule E. Hence, for s-tangible states, $\Upsilon$ may be the empty multiset, and its execution only decrements by one the timer values (if any) of the current state (i.e. the equivalence class). Then we may have a transition $s\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}_{\cal P}\circlearrowleft\!s$ from an s-tangible state $s$ to the tangible (i.e. s-tangible or w-tangible) state $\circlearrowleft\!s=\bigcup\{[\circlearrowleft\!H]_{\approx}\mid H\in s\cap SatOpRegDynExpr\}$. Thus, $\circlearrowleft\!s$ is the union of the structural equivalence classes of all saturated operative dynamic expressions from $s$, whose timer values have been decremented by one, prior to combining them into the equivalence classes. This corresponds to applying the empty move rule to all saturated operative dynamic expressions from $s$, followed by unifying the structural equivalence classes of all the resulting expressions. We have to keep track of such executions, called the empty moves, because they affect the timers and have non-zero probabilities. The latter follows from the definition of $PF(\emptyset,s)$ and the fact that the probabilities of stochastic multiactions cannot be equal to $1$ as they belong to the interval $(0;1)$. When it holds $\forall H\in s\cap SatOpRegDynExpr\ \circlearrowleft\!H=H$, we obtain $\circlearrowleft\!s=s$ by definition of $\circlearrowleft\!s$. Then the empty move from $s$ is in the form of $s\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}_{\cal P}s$, called the empty loop. For w-tangible and vanishing states $\Upsilon$ cannot be the empty multiset, since we must execute some immediate (waiting, respectively) multiactions from them at the current (next, respectively) time moment.

The step probabilities belong to the interval $(0;1]$, being $1$ in the case when we cannot leave an s-tangible state $s$ and the only transition leaving it is the empty move one $s\stackrel{{\scriptstyle\emptyset}}{{\rightarrow}}_{1}\circlearrowleft\!s$, or if there is just a single transition from a w-tangible or a vanishing state to any other one.

We write $s\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\tilde{s}$ if $\exists{\cal P}\ s\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}_{\cal P}\tilde{s}$ and $s\rightarrow\tilde{s}$ if $\exists\Upsilon\ s\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}\tilde{s}$.

The first equivalence we are going to introduce is isomorphism which is a coincidence of systems up to renaming of their components or states.

Definition 3.9

Let $G,G^{\prime}$ be dynamic expressions and $TS(G)\!=\!(S_{G},L_{G},{\cal T}_{G},s_{G}),TS(G^{\prime})\!=\!(S_{G^{\prime}},L_{G^{\prime}},{\cal T}_{G^{\prime}},s_{G^{\prime}})$ be their transition systems. A mapping $\beta:S_{G}\rightarrow S_{G^{\prime}}$ is an isomorphism between $TS(G)$ and $TS(G^{\prime})$, denoted by $\beta:TS(G)\simeq TS(G^{\prime})$, if

$\beta$* is a bijection such that $\beta(s_{G})=s_{G^{\prime}}$;* 2. 2.

$\forall s,\tilde{s}\in S_{G}\ \forall\Upsilon\ s\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}_{\cal P}\tilde{s}\ \Leftrightarrow\ \beta(s)\stackrel{{\scriptstyle\Upsilon}}{{\rightarrow}}_{\cal P}\beta(\tilde{s})$.

Two transition systems $TS(G)$ and $TS(G^{\prime})$ are isomorphic, denoted by $TS(G)\simeq TS(G^{\prime})$, if $\exists\beta:TS(G)\simeq TS(G^{\prime})$.

Transition systems of static expressions can be defined as well. For $E\in RegStatExpr$, let $TS(E)=TS(\overline{E})$.

Definition 3.10

Two dynamic expressions $G$ and $G^{\prime}$ are equivalent with respect to transition systems, denoted by $G=_{ts}G^{\prime}$, if $TS(G)\simeq TS(G^{\prime})$.

Let us now present a series of examples that demonstrate how to construct the transition systems of the dynamic expressions that include various compositions of stochastic, waiting and immediate multiactions.

Example 3.9

This example demonstrates a choice between two waiting multiactions with different delays. It shows that the waiting multiaction $(\{a\},\natural_{1}^{2})$ with a less delay $2$ is always executed first, hence, the choice is resolved in favour of it in any case and an absorbing state is then reached, so that the waiting multiaction $(\{b\},\natural_{2}^{3})$ with a greater delay $3$ is never executed.

Let $E=(\{a\},\natural_{1}^{2})[](\{b\},\natural_{2}^{3})$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{3}\},\ DR_{WT}(\overline{E})=\{s_{2}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 2, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively. For simplicity of the graphical representation, the singleton multisets of activities are written without outer braces.

Example 3.10

This example demonstrates a choice between waiting and stochastic multiactions. It shows that the stochastic multiaction $(\{b\},\frac{1}{3})$ can be executed until the timer value of the waiting multiaction $(\{a\},\natural_{1}^{3})$ becomes $1$, after which only the waiting multiaction can be executed in the next moment, leading to an absorbing state. Thus, in our setting, a waiting multiaction that cannot be executed in the next time moment and whose timer is still running may be interrupted (preempted) by executing a stochastic multiaction.

Let $E=(\{a\},\natural_{1}^{3})[](\{b\},\frac{1}{3})$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{2},s_{4}\},\ DR_{WT}(\overline{E})=\{s_{3}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 3, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.11

This example demonstrates an iteration loop with a waiting multiaction. The iteration initiation is modeled by a (initiating) stochastic multiaction $(\{a\},\frac{1}{2})$. The iteration body that corresponds to the loop consists of a (looping) waiting multiaction $(\{b\},\natural_{1}^{3})$. The iteration termination is represented by a (terminating) stochastic multiaction $(\{c\},\frac{1}{3})$. The terminating stochastic multiaction can be executed until the timer value of the waiting multiaction becomes $1$, after which only the waiting multiaction can be executed in the next moment. Thus, the iteration termination can either complete the repeated execution of the iteration body or break its execution when the waiting multiaction timer shows some intermediate value (that is less than the initial value, being the multiaction delay, but greater than $1$). The execution of the waiting multiaction leads to the repeated start of the iteration body. The execution of the terminating stochastic multiaction brings to the final absorbing state of the iteration construction.

Let $E=[(\{a\},\frac{1}{2})*(\{b\},\natural_{1}^{3})*(\{c\},\frac{1}{3})]$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{2},s_{3},s_{5}\},\ DR_{WT}(\overline{E})=\{s_{4}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 4, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.12

This example demonstrates a parallel composition of an immediate and two waiting multiactions with different delays. It shows that the immediate multiaction $(\{a\},\natural_{1}^{0})$ is always executed before any parallel with it waiting multiaction. Further, from the two parallel waiting multiactions, that $(\{b\},\natural_{2}^{2})$ with a less delay $2$ executed first in any case. Finally, the execution of the waiting multiaction $(\{c\},\natural_{3}^{3})$ with a greater delay $3$ leads to an absorbing state. Thus, in spite of parallelism of those three deterministic multiactions, they are executed sequentially in fact, in the increasing order of their (different) delays. That sequence also includes the empty set, executed after the immediate multiaction, since the waiting multiaction with a less delay will then need a passage of one time unit (one time tick) for its timer value (RTE) become $1$ and it can be executed itself. Though the example is not complex, it shows a transition system with all types of states: s-tangible, w-tangible and vanishing.

Let $E=(\{a\},\natural_{1}^{0})\|(\{b\},\natural_{2}^{2})\|(\{c\},\natural_{3}^{3})$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{2},s_{5}\},\ DR_{WT}(\overline{E})=\{s_{3},s_{4}\}$ and $DR_{V}(\overline{E})=\{s_{1}\}$.

In Figure 5, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively, and the vanishing ones are depicted in boxes.

Example 3.13

This example demonstrates a parallel composition of waiting and stochastic multiactions. It shows that the stochastic multiaction $(\{b\},\frac{1}{3})$ can be executed until the timer value of the waiting multiaction $(\{a\},\natural_{1}^{3})$ becomes $1$, after which only the waiting multiaction can be executed in the next moment. The execution of the latter leads to an absorbing state either directly or indirectly, via executing a possible empty loop, followed (via sequential composition) by the stochastic multiaction that has not been executed in the preceding states.

Let $E=(\{a\},\natural_{1}^{3})\|(\{b\},\frac{1}{3})$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{2},s_{3},s_{6},s_{7}\},\ DR_{WT}(\overline{E})=\{s_{4},s_{5}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 6, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.14

This example demonstrates a parallel composition of two waiting multiactions $(\{a\},\natural_{1}^{2})$ and $(\{\hat{a}\},\natural_{2}^{2})$, whose multiaction parts are singleton multisets with an action $a$ and its conjugate $\hat{a}$, respectively. The resulting composition is synchronized and then restricted by that action, which (and its conjugate) therefore “disappears” from the composite process behaviour. From the initial state, only the empty multiset of activities is executed that decrements by one the values of the timers. That evolution follows by the execution of a new waiting multiaction $(\emptyset,\natural_{3}^{2})$ with the empty multiaction part, resulted from synchronization of the two waiting multiactions, which leads to an absorbing state.

*Note that the timer values of the two waiting multiactions and that of the new waiting multiaction (being their synchronous product) coincide until all of them remain enabled with the time progress. Thus, it is very useful that the expression syntax preserves such two enabled synchronized waiting multiactions, removed by restriction from the behaviour, since their timer values suggest that of their synchronous product, which is not explicit in the syntax. Thus, the timer values of those two “virtual” enabled waiting multiactions cannot just be marked as undefined in the syntax, provided that one keeps track of the timer value of their synchronous product being only implicit in the syntax. *

If both synchronized waiting multiactions lose their enabledness with the time progress then their synchronous product also loses its enabledness and all of them obviously loose their timer value annotations. It may happen that one of the synchronized waiting multiactions loses its enabledness (for example, when a conflicting waiting multiaction is executed) while the other one keeps its enabledness. Then their synchronous product also loses its enabledness, together with its timer value annotation. In such a case, the timer value of the enabled synchronized waiting multiaction does not suggest anymore that of the synchronous product. That “saved” timer value merely decrements with every time tick unless it becomes equal to $1$, after which either the enabled synchronized waiting multiaction is executed or it cannot be executed by some reason (for example, when affected by restriction) and then the timer value $1$ remains unchanged with the time progress. To verify this, recall the empty move rule E from Table 3 and the definition of $\circlearrowleft\!G$ with $\max\{1,\delta-1\}=\max\{1,0\}=1$ when $\delta=1$.

Let $E=((\{a\},\natural_{1}^{2})\|(\{\hat{a}\},\natural_{2}^{2}))\ {\sf sy}\ a\ {\sf rs}\ a$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{3}\},\ DR_{WT}(\overline{E})=\{s_{2}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 7, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.15

This example demonstrates a parallel composition of two subprocesses, synchronized and then restricted by an auxiliary action that (and its conjugate) hereupon “disappears” from the composite process behaviour. The first subprocess is a sequential composition of the waiting $(\{a\},\natural_{1}^{1})$ and immediate $(\{b,\hat{x}\},\natural_{2}^{0})$ multiactions. The second subprocess is a choice between the immediate $(\{x\},\natural_{3}^{0})$ and waiting $(\{c\},\natural_{4}^{1})$ multiactions. The immediate multiactions in the first and second subprocesses are synchronized via an auxiliary action $x$ that (and its conjugate) is then removed from the behaviour by the restriction operation. Since those immediate multiactions are within coverage of restriction by the auxiliary action, they cannot be executed. The new immediate multiaction $(\{b\},\natural_{5}^{0})$, resulted from that synchronization can only be executed if the waiting multiaction (preceding it via sequential composition) in the first subprocess has occurred and the waiting multiaction (conflicting with it via the choice composition) in the second subprocess has not occurred. Since only maximal multisets of parallel waiting multiactions may be executed, the waiting multiactions in both the subprocesses must occur, thus preventing execution of the new immediate multiaction, generated by synchronization.

Let $E=(((\{a\},\natural_{1}^{1});(\{b,\hat{x}\},\natural_{2}^{0}))\|((\{x\},\natural_{3}^{0})[](\{c\},\natural_{4}^{1})))\ {\sf sy}\ x\ {\sf rs}\ x$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{2}\},\ DR_{WT}(\overline{E})=\{s_{1}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 8, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.16

This example is a modification of the previous Example 3.15 by replacing all the immediate multiactions with the waiting ones and by setting to $2$ the delays of all the waiting multiactions from the syntax. Thus, we examine a compound process, constructed with parallelism, synchronization and restriction operations from the following two subprocesses. The first subprocess is a sequential composition of two waiting multiactions $(\{a\},\natural_{1}^{2})$ and $(\{b,\hat{x}\},\natural_{2}^{2})$. The second subprocess is a choice between other two waiting multiactions $(\{x\},\natural_{3}^{2})$ and $(\{c\},\natural_{4}^{2})$. The second waiting multiaction in the first subprocess and the first waiting multiaction in the second subprocess are synchronized via an auxiliary action $x$ that (and its conjugate) is then removed from the behaviour by the restriction operation. The new waiting multiaction $(\{b\},\natural_{5}^{2})$, resulted from that synchronization has the same delay $2$ as the two synchronized waiting multiactions. It can only be executed if the first waiting multiaction (preceding it via sequential composition) in the first subprocess has occurred and the second waiting multiaction (conflicting with it via the choice composition) in the second subprocess has not occurred. Since only maximal multisets of parallel waiting multiactions may be executed, the mentioned (“first in first” and “second in second”) waiting multiactions in both the subprocesses must occur, thus preventing execution of the new waiting multiaction, generated by synchronization.

Note that the overlined second waiting multiaction in the first subprocess is within coverage of restriction by the auxiliary action. Consider the state, reached from the initial state by execution of the empty multiset of activities, followed by the parallel execution of the mentioned (‘first in first” and “second in second”) waiting multiactions. After the empty multiset execution from the considered state, the associated timer value of that overlined waiting multiaction is decremented to $1$. Then an absorbing state is reached, from which only the empty loop is possible, which leaves that timer value $1$ unchanged though. To verify this, recall the empty move rule E from Table 3 and the definition of $\circlearrowleft\!G$ with $\max\{1,\delta-1\}=\max\{1,0\}=1$ when $\delta=1$.

Let $E=(((\{a\},\natural_{1}^{2});(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2})))\ {\sf sy}\ x\ {\sf rs}\ x$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{3},s_{4}\},\ DR_{WT}(\overline{E})=\{s_{2}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 9, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.17

This example is a modification of the previous Example 3.16 by removing restriction from the syntax. Thus, we examine a compound process, constructed with parallelism and synchronization operations from the two subprocesses being a sequential composition of two waiting multiactions $(\{a\},\natural_{1}^{2})$ and $(\{b,\hat{x}\},\natural_{2}^{2})$ and a choice between other two waiting multiactions $(\{x\},\natural_{3}^{2})$ and $(\{c\},\natural_{4}^{2})$, respectively. All the four waiting multiactions have the same delay $2$. The second waiting multiaction in the first subprocess and the first waiting multiaction in the second subprocess are synchronized via an auxiliary action $x$. The new waiting multiaction $(\{b\},\natural_{5}^{2})$, resulted from that synchronization has the same delay $2$ as the two synchronized waiting multiactions. It can only be executed if the first waiting multiaction (preceding it via sequential composition) in the first subprocess has occurred and the second waiting multiaction (conflicting with it via the choice composition) in the second subprocess has not occurred. Since only maximal multisets of parallel waiting multiactions may be executed, the mentioned (“first in first” and “second in second”) waiting multiactions in the subprocesses must occur, thus preventing execution of the new waiting multiaction, generated by synchronization. The alternative maximal multiset of parallel waiting multiactions that may be executed from the same state consists of the “first in first” and “first in second” waiting multiactions in the subprocesses, but the ‘first in second” waiting multiaction is the second of the two synchronized waiting multiactions, whose occurrence also prevents execution of their synchronization product.

Let $E=(((\{a\},\natural_{1}^{2});(\{b,\hat{x}\},\natural_{2}^{2}))\|((\{x\},\natural_{3}^{2})[](\{c\},\natural_{4}^{2})))\ {\sf sy}\ x$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{3},s_{5}\},\ DR_{WT}(\overline{E})=\{s_{2},s_{4}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 10, the transition system $TS(\overline{E})$ is shown. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively.

Example 3.18

Consider the expression ${\sf Stop}=(\{g\},\frac{1}{2})\ {\sf rs}\ g$ specifying the special process that is only able to perform empty loops with probability $1$ and never terminates. We could actually use any arbitrary action from ${\cal A}$ and any probability belonging to the interval $(0;1)$ in the definition of ${\sf Stop}$. Note that ${\sf Stop}$ is analogous to the one used in the examples within sPBC. The latter is a continuous time stochastic analogue of the stop process proposed in [9]. Stop is a discrete time stochastic analogue of the stop.

This example demonstrates an infinite iteration loop. The loop is preceded with the iteration initiation, modeled by a (first) stochastic multiaction $(\{a\},\frac{1}{2})$. The iteration body that corresponds to the loop consists of the choice between two conflicting waiting multiactions $(\{b\},\natural_{1}^{1})$ and $(\{c\},\natural_{2}^{1})$ with the same delay $1$, the second of them followed (via sequential composition) by a (second) stochastic multiaction $(\{d\},\frac{1}{3})$. Hence, the iteration loop actually consists of the two alternative subloops, such that the first one is a self-loop (one-state loop from a state to itself) with the first waiting multiaction, and the second one is a two-state loop with an intermediate state, reached after the second waiting multiaction has been executed, and from which the second stochastic multiaction is then started. Thus, the iteration generates the self-loop with probability less than one (since the two-state loop from the same state has a non-zero probability) from the states in which only waiting multiactions are executed. The iteration termination ${\sf Stop}$ demonstrates an empty behaviour, assuring that the iteration does not reach its final state after any number of repeated executions of its body.

Let $E=[(\{a\},\frac{1}{2})*((\{b\},\natural_{1}^{1})[]((\{c\},\natural_{2}^{1});(\{d\},\frac{1}{3})))*{\sf Stop}]$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{3}\},\ DR_{WT}(\overline{E})=\{s_{2}\}$ and $DR_{V}(\overline{E})=\emptyset$.

In Figure 11, the transition system $TS(\overline{E})$ is presented. The s-tangible states are depicted in ovals and the vanishing ones are depicted in boxes.

Example 3.19

This example demonstrates an infinite iteration loop. The loop is preceded with the iteration initiation, modeled by a stochastic multiaction $(\{a\},\rho)$. The iteration body that corresponds to the loop consists of a waiting multiaction $(\{b\},\natural_{k}^{1})$, followed (via sequential composition) by the probabilistic choice, modeled via two conflicting immediate multiactions $(\{c\},\natural_{l}^{0})$ and $(\{e\},\natural_{m}^{0})$, followed by different stochastic multiactions $(\{d\},\theta)$ and $(\{f\},\phi)$. The iteration termination ${\sf Stop}$ demonstrates an empty behaviour, assuring that the iteration does not reach its final state after any number of repeated executions of its body.

Let $E=[(\{a\},\rho)*((\{b\},\natural_{k}^{1});(((\{c\},\natural_{l}^{0});(\{d\},\theta))[]((\{e\},\natural_{m}^{0});(\{f\},\phi))))*{\sf Stop}]$, where $\rho,\theta,\phi\in(0;1)$ and $k,l,m\in I\!\!R_{>0}$. $DR(\overline{E})$ consists of the equivalence classes

[TABLE]

We have $DR_{ST}(\overline{E})=\{s_{1},s_{4},s_{5}\},\ DR_{WT}(\overline{E})=\{s_{2}\}$ and $DR_{V}(\overline{E})=\{s_{3}\}$.

In Figure 12, the transition system $TS(\overline{E})$ is presented. The s-tangible and w-tangible states are depicted in ordinary and double ovals, respectively, and the vanishing ones are depicted in boxes.

4 Denotational semantics

In this section, we construct the denotational semantics in terms of a subclass of labeled discrete time stochastic and deterministic PNs (LDTSDPNs), called discrete time stochastic and immediate Petri boxes (dtsd-boxes).

4.1 Labeled DTSDPNs

Let us introduce a class of labeled discrete time stochastic and deterministic PNs (LDTSDPNs), which are essentially a subclass of DTSPNs [44, 45] (since we do not allow the stochastic transition probabilities to be equal to $1$) extended with transition labeling and deterministic transitions. LDTSDPNs resemble in part discrete time deterministic and stochastic PNs (DTDSPNs) [61, 62, 64, 65], as well as discrete deterministic and stochastic PNs (DDSPNs) [63]. DTDSPNs and DDSPNs are the extensions of DTSPNs with deterministic transitions (having fixed delay that can be zero), inhibitor arcs, priorities and guards. In addition, while stochastic transitions of DTDSPNs, like those of DTSPNs, have geometrically distributed delays, stochastic transitions of DDSPNs have discrete time phase-type distributed delays. At the same time, LDTSDPNs are not subsumed by DTDSPNs or DDSPNs, by the following reasons. First, in DTDSPNs from [61, 62], both stochastic and deterministic (including immediate) transitions have probabilities and weights associated, but in LDTSDPNs only stochastic transitions have probabilities and only immediate ones have weights, hence, the state change probabilities of the underlying Markov chains for those PN classes are calculated in two different ways. Second, LDTSDPNs have a step semantics while DTDSPNs from [64, 65] and DDSPNs have interleaving one, since in in the first PN class simultaneous transition firings are possible while in the second and third PN classes only firings of single transitions are allowed. LDTSDPNs are somewhat similar to labeled weighted DTSPNs (LWDTSPNs) from [15], but in LWDTSPNs there are no deterministic transitions, all (stochastic) transitions have weights, the transition probabilities may be equal to $1$ and only maximal fireable subsets of the enabled transitions are fired.

Stochastic preemptive time PNs (spTPNs) [14] is a discrete time model with a maximal step semantics, where both time ticks and instantaneous parallel firings of maximal transition sets are possible, but the transition steps in LDTSDPNs are not obliged to be maximal (excepting the steps of waiting transitions). The transition delays in spTPNs are governed by static general discrete distributions, associated with the transitions, while the transitions of LDTSDPNs are only associated with probabilities, used later to calculate the step probabilities after one unit (from tangible markings) or zero (from vanishing markings) delay. Further, LDTSDPNs have just geometrically distributed or deterministic zero delays at the markings. Moreover, the discrete time tick and concurrent transition firing are treated in spTPNs as different events while firing every (possibly empty) set of stochastic or waiting transitions in LDTSDPNs requires one unit time delay. spTPNs are essentially a modification and extension of unlabeled LWDTSPNs with additional facilities, such as inhibitor arcs, priorities, resources, preemptions, schedulers etc. However, the price of such an expressiveness of spTPNs is that the model is rather intricate and difficult to analyze.

Note also that guards in DTDSPNs and DDSPNs, inhibitor arcs and priorities in DTDSPNs, DDSPNs and spTPNs, as well as the maximal step semantics of LWDTSPNs and spTPNs make all these models Turing powerful, resulting in undecidability of many important behavioural properties.

First, we present a formal definition (construction, syntax) of LDTSDPNs. The set of all row vectors of $n\in I\!\!N_{\geq 1}$ elements from a set $X$ is defined as $X^{n}=\{(x_{1},\ldots,x_{n})\mid x_{i}\in X\ (1\leq i\leq n)\}$.

Definition 4.1

*A labeled discrete time stochastic and deterministic PN (LDTSDPN) is a tuple

$N=(P_{N},T_{N},W_{N},D_{N},\Omega_{N},{\cal L}_{N},Q_{N})$, where*

• •

$P_{N}$* and $T_{N}=Ts_{N}\uplus Td_{N}$ are finite sets of places and stochastic and deterministic transitions, respectively, such that $P_{N}\cup T_{N}\neq\emptyset$ and $P_{N}\cap T_{N}=\emptyset$;*

• •

$W_{N}:(P_{N}\times T_{N})\cup(T_{N}\times P_{N})\rightarrow I\!\!N$* is a function providing the weights of arcs between places and transitions;*

• •

$D_{N}:Td_{N}\rightarrow I\!\!N$* is the transition delay function imposing delays to deterministic transitions;*

An immediate transition is a deterministic transition with the delay [math] while a waiting transition is that with a positive delay. Then $Td_{N}=Ti_{N}\uplus Tw_{N}$ consists of the sets of immediate and waiting transitions.

• •

$\Omega_{N}$* is the transition probability and weight function such that*

• –

$\Omega_{N}|_{Ts_{N}}:Ts_{N}\rightarrow(0;1)$* (it associates stochastic transitions with probabilities);*

• –

$\Omega_{N}|_{Td_{N}}:Td_{N}\rightarrow I\!\!R_{>0}$* (it associates deterministic transitions with weights);*

• •

${\cal L}_{N}:T_{N}\rightarrow{\cal L}$* is the transition labeling function assigning multiactions to transitions;*

• •

$Q_{N}=(M_{N},V_{N})$* is the initial state, where $M_{N}\in I\!\!N_{fin}^{P_{N}}$ is the initial marking (distribution of tokens in the places) and $V_{N}:Tw_{N}\rightarrow I\!\!N_{\geq 1}\cup\{*\}$ is the initial timer valuation function of the waiting transitions (in the vector notation, $V_{N}\in(I\!\!N_{\geq 1}\cup\{*\})^{|Tw_{N}|}$), where ‘$*$’ denotes the undefined value of inactive timers; we define $\forall t\in Tw_{N}\cap Ena(M_{N})\ V_{N}(t)=D_{N}(t)$ (each enabled waiting transition is initially valuated with its transition delay) and $\forall t\in Tw_{N}\setminus Ena(M_{N})\ V_{N}(t)=*$ (each non-enabled waiting transition is initially valuated with the undefined value), where $Ena(M)$ denotes the set of transitions enabled at the marking $M$, to be defined later.*

The graphical representation of LDTSDPNs is like that for standard labeled PNs, but with probabilities or delays and weights written near the corresponding transitions. Square boxes of normal thickness depict stochastic transitions, and those with thick borders represent deterministic transitions. In the case the probabilities or the delays and weights are not given in the picture, they are considered to be of no importance in the corresponding examples. The weights of arcs are depicted with them. The names of places and transitions are depicted near them when needed.

We now consider the semantics of LDTSDPNs.

Let $N$ be an LDTSDPN and $t\in T_{N},\ U\in I\!\!N_{fin}^{T_{N}}$. The precondition ${}^{\bullet}t$ and the postcondition $t^{\bullet}$ of $t$ are the multisets of places defined as $({{}^{\bullet}}t)(p)=W_{N}(p,t)$ and $(t^{\bullet})(p)=W_{N}(t,p)$. The precondition ${}^{\bullet}U$ and the postcondition $U^{\bullet}$ of $U$ are the multisets of places defined as ${{}^{\bullet}}U=\sum_{t\in U}{{}^{\bullet}}t$ and $U^{\bullet}=\sum_{t\in U}t^{\bullet}$. Note that for $U=\emptyset$ we have ${{}^{\bullet}}\emptyset=\emptyset=\emptyset^{\bullet}$.

Let $N$ be an LDTSDPN and $Q=(M,V),\widetilde{Q}=(\widetilde{M},\widetilde{V})\in I\!\!N_{fin}^{P_{N}}\times(I\!\!N_{\geq 1}\cup\{*\})^{|Tw_{N}|}$ be its states.

Deterministic transitions have a priority over stochastic ones, and there is also difference in priorities between immediate and waiting transitions. One can assume that all immediate transitions have (the highest) priority $2$ and all waiting transitions have (the intermediate) priority $1$, whereas all stochastic transitions have (the lowest) priority [math]. This means that at a marking where all kinds of transitions can occur, immediate transitions always occur before waiting ones that, in turn, are always executed before stochastic ones.

A transition $t\in T_{N}$ is enabled at a marking $M\in I\!\!N_{fin}^{P_{N}}$, if ${{}^{\bullet}}t\subseteq M$. In other words, a transition is enabled at a marking if it has enough tokens in its input places (i.e. in the places from its precondition) at the marking. Let $Ena(M)$ be the set of all transitions enabled at $M$.

Firings of transitions are atomic operations, and transitions can fire in parallel by taking part in steps. We assume that all transitions participating in a step should differ, hence, only the sets (not multisets) of transitions may fire. Thus, we do not allow self-concurrency, i.e. firing of transitions in parallel to themselves. This restriction is introduced to avoid some technical difficulties while calculating probabilities for multisets of transitions as we shall see after the following formal definitions. Moreover, we do not need to consider self-concurrency, since denotational semantics of expressions will be defined via dtsd-boxes which are safe LDTSDPNs (hence, no self-concurrency is possible).

The following definition of fireability respects the prioritization among different types of transitions. A set of transitions $U\subseteq Ena(M)$ is fireable in a state $Q=(M,V)$, if ${{}^{\bullet}}U\subseteq M$ (i.e. it has enough tokens in its input places at the substituent marking $M$), and one of the following holds:

$\emptyset\neq U\subseteq Ti_{N}$; or 2. 2.

$\emptyset\neq U\subseteq Tw_{N}$ and

• •

$\forall t\in U\ V(t)=1$,

• •

$Ena(M-{{}^{\bullet}}U)\cap\{u\in Tw_{N}\mid V(u)=1\}=\emptyset$,

• •

$Ena(M)\subseteq Tw_{N}\cup Ts_{N}$; or 3. 3.

$U\subseteq Ts_{N}$ and

• •

$Ena(M)\subseteq Ts_{N}$.

In other words, a set of transitions $U$ is fireable in a state, if has enough tokens in its input places at the substituent marking $M$ of the state and the following holds. If $U$ consists of immediate transitions then it is enabled, since no additional condition is needed for its fireability. If $U$ consists of waiting transitions then the countdown timer value (called remaining time to fire or RTF) of each transition from $U$ equals one, $U$ is a maximal (by the inclusion relation) set of the enabled at $M$ waiting transitions with the RTF equal to one and enough tokens in its input places at $M$, and there exist no immediate transitions enabled at $M$. If $U$ is empty or it consists of stochastic transitions then there exist no immediate or waiting transition enabled at $M$. Note that the second condition of item $2$ of the above definition means that no waiting transition (from $Ena(M)$) with the RTF being one can be added to $U$ so that the resulting transition set will still have enough tokens in its input places at $M$. This condition is equivalent to the following maximality requirement (informally mentioned above): $\forall T\subseteq Ena(M),\ (\forall u\in T\ V(u)=1)\wedge({{}^{\bullet}}T\subseteq M)\wedge(U\subseteq T)\ \Rightarrow\ T=U$. Let $Fire(Q)$ be the set of all transition sets fireable in $Q$.

By the fireability definition, it follows that $Fire(Q)\subseteq 2^{Ti_{N}}\setminus\{\emptyset\}$ or $Fire(Q)\subseteq 2^{Tw_{N}}\setminus\{\emptyset\}$, or $Fire(Q)\subseteq 2^{Ts_{N}}$ (to be convinced of it, check the definition’s items in the reverse order). The state $Q$ is s-tangible (stochastically tangible), denoted by $stang(Q)$, if $Fire(Q)\subseteq 2^{Ts_{N}}$, in particular, if $Fire(Q)=\{\emptyset\}$. The state $Q$ is w-tangible (waitingly tangible), denoted by $wtang(Q)$, if $Fire(Q)\subseteq 2^{Tw_{N}}\setminus\{\emptyset\}$. The state $Q$ is tangible, denoted by $tang(Q)$, if $stang(Q)$ or $wtang(Q)$, i.e. $Fire(Q)\subseteq 2^{Ts_{N}}\cup 2^{Tw_{N}}$, in particular, if $Fire(Q)=\{\emptyset\}$. Otherwise, the state $Q$ is vanishing, denoted by $vanish(Q)$, and in this case $Fire(Q)\subseteq 2^{Ti_{N}}\setminus\{\emptyset\}$. A transition $t\in Ena(M)$ is fireable in a state $Q$, denoted by $t\in Fire(Q)$, if $\{t\}\in Fire(Q)$. If $stang(Q)$ then a stochastic transition $t\in Fire(Q)$ fires with probability $\Omega_{N}(t)$ when no different stochastic transition in conflict with it is fireable. By definition if fireability, if $stang(Q)$ or $vanish(Q)$ then $\forall U\in Fire(Q)\ 2^{U}\subseteq Fire(Q)$.

Let $U\in Fire(Q)$ and $U\neq\emptyset$. The probability that the set of stochastic transitions $U$ is ready for firing in $Q$ or the weight of the set of deterministic transitions $U$ which is ready for firing in $Q$ is

[TABLE]

In the case $U=\emptyset$ and $stang(Q)$ we define

[TABLE]

Let $U\in Fire(Q)$ and $U\neq\emptyset$ or $U=\emptyset$ and $stang(Q)$. Besides $U$, some other sets of transitions may be ready for firing in $Q$, hence, a kind of conditioning or normalization is needed to calculate the firing probability. The parallel firing of the transitions from $U$ changes the state $Q=(M,V)$ to another state $\widetilde{Q}=(\widetilde{M},\widetilde{V})$, denoted by $Q\stackrel{{\scriptstyle U}}{{\rightarrow}}_{\cal P}\widetilde{Q}$, where

$\widetilde{M}=M-{{}^{\bullet}}U+U^{\bullet}$; 2. 2.

\forall u\in Tw_{N}\ \widetilde{V}(u)=\left\{\begin{array}[]{ll}*,&u\not\in Ena(\widetilde{M});\\ V_{N}(u),&u\in Ena(\widetilde{M})\setminus Ena(M-{{}^{\bullet}}U);\\ V(u),&(u\in Ena(M-{{}^{\bullet}}U))\wedge(U\subseteq Ti_{N});\\ V(u)-1,&\mbox{otherwise};\end{array}\right. 3. 3.

${\cal P}=PT(U,Q)$ is the probability that the set of transitions $U$ fires in $Q$ defined as

[TABLE]

Let us explain the definition above in more detail. The first case of the item $2$ demonstrates a waiting transition $u$ that is not enabled at the marking $\widetilde{M}$, regardless of whether it was enabled at the “intermediate” marking $M-{{}^{\bullet}}U$ (obtained by removing from $M$ the input places of all transitions belonging to $U$, and that should be examined, especially when $N$ has structural loops), and therefore the transition timer becomes inactive (turned off) and it is set to the undefined value $*$. The second case of the item $2$ describes a waiting transition $u$ that was not enabled at $M-{{}^{\bullet}}U$ and has first been enabled at $\widetilde{M}$, hence, its timer is restored to the initial value $V_{N}(u)$, which is the delay of that transition. The third case of the item $2$ explains a waiting transition $u$ that was enabled at $M-{{}^{\bullet}}U$ and, hence, still is enabled at $\widetilde{M}$, resulted in an firing of a set of immediate transitions $U$ instantly (in zero time), so the transition timer does not decrement and its value stays equal to $V(u)$. The fourth case of the item $2$ corresponds to the remaining option, i.e. a waiting transition $u$ that was enabled at $M-{{}^{\bullet}}U$ and, hence, still is enabled at $\widetilde{M}$, resulted in an firing of a set of stochastic (waiting) transitions $U$ at a time tick (in one time unit), so the transition timer decrements by one and its value becomes $V(u)-1$.

We do not have to worry that for $u\in Tw_{N}$, such that $u\in Ena(M-{{}^{\bullet}}U)$, where $U\subseteq Ts_{N}\cup Tw_{N}$, the value of $\widetilde{V}(u)=V(u)-1$ could become zero or negative, by the following reasons. Note that by the definition of fireability, we have $Ena(M)\subseteq Tw_{N}\cup Ts_{N}$. If $V(u)=1$ then $u$ must fire in the next time moment within some maximal (by the inclusion relation) set of the enabled at $M$ waiting transitions with the RTF equal to one and enough tokens in the set’s input places at $M$. Then we get $U\in Fire(Q)\subseteq 2^{Tw_{N}}\setminus\{\emptyset\}$, hence, $\emptyset\neq U\subseteq Tw_{N}$. Therefore, $\forall t\in U\ V(t)=1$ and $Ena(M-{{}^{\bullet}}U)\cap\{w\in Tw_{N}\mid V(w)=1\}=\emptyset$, which contradicts to $u\in Ena(M-{{}^{\bullet}}U)\cap\{w\in Tw_{N}\mid V(w)=1\}$. Thus, there exists no transition $u\in Tw_{N}$, such that $u\in Ena(M-{{}^{\bullet}}U)$ and $V(u)=1$. In regard to the transitions $t\in U\subseteq Tw_{N}$ with $V(t)=1$, we have $\widetilde{V}(t)=*$, if $t\not\in Ena(\widetilde{M})$, or $\widetilde{V}(t)=V_{N}(t)$, if $t\in Ena(\widetilde{M})\setminus Ena(M-{{}^{\bullet}}U)$.

Note that when $U=\emptyset$ and $stang(Q)$, we get $M=\widetilde{M}$ and \forall u\in Tw_{N}\ \widetilde{V}(u)=\left\{\begin{array}[]{ll}*,&u\not\in Ena(M);\\ V(u)-1,&u\in Ena(M).\end{array}\right.

Notice that the timers of all waiting transitions that are disabled when a marking change occurs become inactive (turned off) and their values become undefined while the timers of all those staying enabled continue running with their stored values. Hence, we adopt the enabling memory policy [41, 1, 2, 3] when the markings are changed and the enabling of deterministic transitions is possibly modified (remember that immediate transitions may be seen as those with the timers displaying a single value [math], so we do not need to store their values). Then the timer values of waiting transitions are taken as the enabling memory variables.

The advantage of our two-stage approach to definition of the probability that a set of transitions fires is that the resulting probability formula $PT(U,Q)$ is valid both for (sets of) stochastic and deterministic transitions. It allows one to unify the notation used later while constructing the denotational semantics and analyzing performance.

Note that for all states of an LDTSDPN $N$, the sum of outgoing probabilities is equal to $1$. More formally, $\forall Q=(M,V)\in I\!\!N_{fin}^{P_{N}}\times(I\!\!N_{\geq 1}\cup\{*\})^{|Tw_{N}|}\ \sum_{\{U\subseteq Ena(M)\mid{{}^{\bullet}}U\subseteq M\}}PT(U,Q)=1$. This obviously follows from the definition of $PT(U,Q)$ and guarantees that it defines a probability distribution.

We write $Q\stackrel{{\scriptstyle U}}{{\rightarrow}}\widetilde{Q}$ if $\exists{\cal P}\ Q\stackrel{{\scriptstyle U}}{{\rightarrow}}_{\cal P}\widetilde{Q}$ and $Q\rightarrow\widetilde{Q}$ if $\exists U\ Q\stackrel{{\scriptstyle U}}{{\rightarrow}}\widetilde{Q}$.

The probability to move from $Q$ to $\widetilde{Q}$ by firing any set of transitions is

[TABLE]

Since $PM(Q,\widetilde{Q})$ is the probability for any (including the empty one) transition set to change marking $Q$ to $\widetilde{Q}$, we use summation in the definition. Note that $\forall Q=(M,V)\in I\!\!N_{fin}^{P_{N}}\times(I\!\!N_{\geq 1}\cup\{*\})^{|Tw_{N}|}\ \sum_{\{\widetilde{Q}\mid Q\rightarrow\widetilde{Q}\}}PM(Q,\widetilde{Q})=\sum_{\{\widetilde{Q}\mid Q\rightarrow\widetilde{Q}\}}\sum_{\{U\mid Q\stackrel{{\scriptstyle U}}{{\rightarrow}}\widetilde{Q}\}}PT(U,Q)=\sum_{\{U\subseteq Ena(M)\mid{{}^{\bullet}}U\subseteq M\}}PT(U,Q)=1$.

Definition 4.2

Let $N$ be an LDTSDPN. The reachability set of $N$, denoted by $RS(N)$, is the minimal set of markings such that

• •

$Q_{N}\in RS(N)$;

• •

if $Q\in RS(N)$ and $Q\rightarrow\widetilde{Q}$ then $\widetilde{Q}\in RS(N)$.

Definition 4.3

Let $N$ be an LDTSDPN. The reachability graph of $N$ is a (labeled probabilistic) transition system $RG(N)=(S_{N},L_{N},{\cal T}_{N},s_{N})$, where

• •

the set of states is $S_{N}=RS(N)$;

• •

the set of labels is $L_{N}=2^{T_{N}}\times(0;1]$;

• •

the set of transitions is ${\cal T}_{N}=\{(Q,(U,{\cal P}),\widetilde{Q})\mid Q,\widetilde{Q}\in RS(N),\ Q\stackrel{{\scriptstyle U}}{{\rightarrow}}_{\cal P}\widetilde{Q}\}$;

• •

the initial state is $s_{N}=Q_{N}$.

The set of all s-tangible markings from $RS(N)$ is denoted by $RS_{ST}(N)$, and the set of all w-tangible markings from $RS(N)$ is denoted by $RS_{WT}(N)$. The set of all tangible markings from $RS(N)$ is denoted by $RS_{T}(N)=RS_{ST}(N)\cup RS_{WT}(N)$. The set of all vanishing markings from $RS(N)$ is denoted by $RS_{V}(N)$. Obviously, $RS(N)=RS_{T}(N)\uplus RS_{V}(N)=RS_{ST}(N)\uplus RS_{WT}(N)\uplus RS_{V}(N)$.

4.2 Algebra of dtsd-boxes

We now introduce discrete time stochastic and deterministic Petri boxes and the algebraic operations to define a net representation of dtsdPBC expressions.

Definition 4.4

*A discrete time stochastic and deterministic Petri box (dtsd-box) is a tuple

$N=(P_{N},T_{N},W_{N},\Lambda_{N})$, where*

• •

$P_{N}$* and $T_{N}$ are finite sets of places and transitions, respectively, such that $P_{N}\cup T_{N}\neq\emptyset$ and $P_{N}\cap T_{N}=\emptyset$;*

• •

$W_{N}:(P_{N}\times T_{N})\cup(T_{N}\times P_{N})\rightarrow I\!\!N$* is a function providing the weights of arcs between places and transitions;*

• •

$\Lambda_{N}$* is the place and transition labeling function such that*

• –

$\Lambda_{N}|_{P_{N}}:P_{N}\rightarrow\{{\sf e},{\sf i},{\sf x}\}$* (it specifies entry, internal and exit places, respectively);*

• –

$\Lambda_{N}|_{T_{N}}:T_{N}\rightarrow\{\varrho\mid\varrho\subseteq I\!\!N_{fin}^{\cal SDL}\times{\cal SDL}\}$* (it associates transitions with the relabeling relations on activities).*

Moreover, $\forall t\in T_{N}\ {{}^{\bullet}}t\neq\emptyset\neq t^{\bullet}$. In addition, for the set of entry places of $N$, defined as ${{}^{\circ}}N=\{p\in P_{N}\mid\Lambda_{N}(p)={\sf e}\}$, and for the set of exit places of $N$, defined as $N^{\circ}=\{p\in P_{N}\mid\Lambda_{N}(p)={\sf x}\}$, the following conditions hold: ${{}^{\circ}}N\neq\emptyset\neq N^{\circ}$ and ${{}^{\bullet}}({{}^{\circ}}N)=\emptyset=(N^{\circ})^{\bullet}$.

A dtsd-box is plain if $\forall t\in T_{N}\ \exists(\alpha,\kappa)\in{\cal SDL}\ \Lambda_{N}(t)=\varrho_{(\alpha,\kappa)}$, where $\varrho_{(\alpha,\kappa)}=\{(\emptyset,(\alpha,\kappa))\}$ is a constant relabeling that can be identified with the activity $(\alpha,\kappa)$. A (marked and timer-)clocked plain dtsd-box is a pair $(N,Q)$, where $N=(P_{N},T_{N},W_{N},\Lambda_{N})$ is a plain dtsd-box and $Q=(M,V)$ is its state. Here $M\in I\!\!N_{fin}^{P_{N}}$ is the marking of $N$ and $V:Tw_{N}\rightarrow I\!\!N_{\geq 1}\cup\{*\}$ is the timer valuation function of the waiting transitions of $N$. The set of waiting transitions of $N$ is defined as $Tw_{N}=\{t\in T_{N}\mid\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})},\ \theta\in I\!\!N_{\geq 1},\ l\in I\!\!R_{>0}\}$. A plain dtsd-box $N=(P_{N},T_{N},W_{N},\Lambda_{N})$ can be seen as a clocked plain dtsd-box $(N,Q^{*})$ with $Q^{*}=(\emptyset,V^{*})$, where for every waiting transition $t$ it holds $V^{*}(t)=*$, i.e. $V^{*}=*$.

We denote $\overline{N}=(N,Q_{\overline{N}})$, where $Q_{\overline{N}}=({{}^{\circ}}N,V_{\overline{N}})$ and $V_{\overline{N}}:Tw_{N}\rightarrow I\!\!N_{\geq 1}\cup\{*\}$ is such that $\forall t\in Tw_{N}\cap Ena({{}^{\circ}}N)\ V_{\overline{N}}(t)=\theta$ for $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$, whereas $\forall t\in Tw_{N}\setminus Ena({{}^{\circ}}N)\ V_{\overline{N}}(t)=*$. We also denote $\underline{N}=(N,Q_{\underline{N}})$, where $Q_{\underline{N}}=(N^{\circ},V^{*})$. We call ${{}^{\circ}}N$ and $N^{\circ}$ the entry and exit markings of $N$, respectively.

Note that a clocked plain dtsd-box $(P_{N},T_{N},W_{N},\Lambda_{N},Q_{N})$ can be interpreted as the LDTSDPN

$(P_{N},T_{N},W_{N},D_{N},\Omega_{N},{\cal L}_{N},Q_{N})$, where the functions $D_{N},\ \Omega_{N}$ and ${\cal L}_{N}$ are defined as follows: $\forall t\in T_{N}\ \Omega_{N}(t)=\kappa$ if $\kappa\in(0;1)$; or $D_{N}(t)=\theta,\ \Omega_{N}(t)=l$ if $\kappa=\natural_{l}^{\theta},\ \theta\in I\!\!N,\ l\in I\!\!R_{>0}$; and ${\cal L}_{N}(t)=\alpha$, where $\Lambda_{N}(t)=\varrho_{(\alpha,\kappa)}$ (we say that the transition $t$ corresponds to the activity $(\alpha,\kappa)$ in such a case). Behaviour of the clocked dtsd-boxes follows from the firing rule of LDTSDPNs. A plain dtsd-box $N$ is $n$-bounded ($n\in I\!\!N$) if $\overline{N}$ is so, i.e. $\forall Q=(M,V)\in RS(\overline{N})\ \forall p\in P_{N}\ M(p)\leq n$, and it is safe if it is $1$-bounded. A plain dtsd-box $N$ is clean if $\forall Q=(M,V)\in RS(\overline{N})\ {{}^{\circ}}N\subseteq M\ \Rightarrow\ M={{}^{\circ}}N$ and $N^{\circ}\subseteq M\ \Rightarrow\ M=N^{\circ}$, i.e. if there are tokens in all its entry (exit) places then no other places have tokens.

The structure of the plain dtsd-box corresponding to a static expression is constructed like in PBC [10, 9], i.e. we use simultaneous refinement and relabeling meta-operator (net refinement) in addition to the operator dtsd-boxes corresponding to the algebraic operations of dtsdPBC and featuring transformational transition relabelings. Operator dtsd-boxes specify $n$-ary functions from plain dtsd-boxes to plain dtsd-boxes (we have $1\leq n\leq 3$ in dtsdPBC). Thus, as we shall see in Theorem 4.1, the resulting plain dtsd-boxes are safe and clean. In the definition of the denotational semantics, we shall apply standard constructions used for PBC. Let $\Theta$ denote operator box and $u$ denote transition name from the PBC setting.

The relabeling relations $\varrho\subseteq I\!\!N_{fin}^{\cal SDL}\times{\cal SDL}$ are defined as follows:

• •

$\varrho_{id}=\{(\{(\alpha,\kappa)\},(\alpha,\kappa))\mid(\alpha,\kappa)\in{\cal SDL}\}$ is the identity relabeling keeping the interface as it is;

• •

$\varrho_{(\alpha,\kappa)}=\{(\emptyset,(\alpha,\kappa))\}$ is the constant relabeling that can be identified with $(\alpha,\kappa)\in{\cal SDL}$ itself;

• •

$\varrho_{[f]}=\{(\{(\alpha,\kappa)\},(f(\alpha),\kappa))\mid(\alpha,\kappa)\in{\cal SDL}\}$;

• •

$\varrho_{\!\!\ {\sf rs}\ a}=\{(\{(\alpha,\kappa)\},(\alpha,\kappa))\mid(\alpha,\kappa)\in{\cal SDL},\ a,\hat{a}\not\in\alpha\}$;

• •

$\varrho_{\!\!\ {\sf sy}\ a}$ is the least relabeling relation containing $\varrho_{id}$ such that if $(\Upsilon,(\alpha,\kappa)),(\Xi,(\beta,\lambda))\in\varrho_{\!\!\ {\sf sy}\ a}$ and

$a\in\alpha,\ \hat{a}\in\beta$ then

• –

$(\Upsilon+\Xi,(\alpha\oplus_{a}\beta,\kappa\cdot\lambda))\in\varrho_{\!\!\ {\sf sy}\ a}$ if $\kappa,\lambda\in(0;1)$;

• –

$(\Upsilon+\Xi,(\alpha\oplus_{a}\beta,\natural_{l+m}^{\theta}))\in\varrho_{\!\!\ {\sf sy}\ a}$ if $\kappa=\natural_{l}^{\theta},\ \lambda=\natural_{m}^{\theta},\ \theta\in I\!\!N,\ l,m\in I\!\!R_{>0}$.

The plain dtsd-boxes $N_{(\alpha,\rho)_{\iota}},\ N_{(\alpha,\natural_{l}^{\theta})_{\iota}}$, where $\rho\in(0;1),\ \theta\in I\!\!N,\ l\in I\!\!R_{>0}$, and operator dtsd-boxes are presented in Figure 13. Note that the label i of internal places is usually omitted.

In the case of the iteration, a decision that we must take is the selection of the operator box that we shall use for it, since we have two proposals in plain PBC for that purpose [9]. One of them provides us with a safe version with six transitions in the operator box, but there is also a simpler version, which has only three transitions. In general, in PBC, with the latter version we may generate $2$-bounded nets, which only occurs when a parallel behavior appears at the highest level of the body of the iteration. Nevertheless, in our case, and due to the syntactical restriction introduced for regular terms, this particular situation cannot occur, so that the net obtained will be always safe.

To define a semantic function that assigns a plain dtsd-box to every static expression of dtsdPBC, we introduce the enumeration function $Enu:T\rightarrow Num$, which associates the numberings with transitions of a plain dtsd-box $N=(P,T,W,\Lambda)$ in accordance with those of activities. In the case of synchronization, the function associates with the resulting new transition a concatenation of the parenthesized numberings of the transitions it comes from.

We now define the enumeration function $Enu$ for every operator of dtsdPBC. Let $N_{E}=Box_{dtsd}(E)=\\ (P_{E},T_{E},W_{E},\Lambda_{E})$ be the plain dtsd-box corresponding to a static expression $E$, and $Enu_{E}:T_{E}\rightarrow Num$ be the enumeration function for $N_{E}$. We shall use the analogous notation for static expressions $F$ and $K$.

• •

$Box_{\rm dtsi}((\alpha,\kappa)_{\iota})=N_{(\alpha,\kappa)_{\iota}}$. Since a single transition $t_{\iota}$ corresponds to the activity $(\alpha,\kappa)_{\iota}\in{\cal SDL}$, their numberings coincide:

[TABLE]

• •

$Box_{dtsd}(E\circ F)=\Theta_{\circ}(Box_{dtsd}(E),Box_{dtsd}(F)),\ \circ\in\{;,[],\|\}$. Since we do not introduce new transitions, we preserve the initial numbering:

[TABLE]

• •

$Box_{dtsd}(E[f])=\Theta_{[f]}(Box_{dtsd}(E))$. Since we only replace the labels of some multiactions by a bijection, we preserve the initial numbering:

[TABLE]

• •

$Box_{dtsd}(E\ {\sf rs}\ a)=\Theta_{\!\!\ {\sf rs}\ a}(Box_{dtsd}(E))$. Since we remove all transitions labeled with multiactions containing $a$ or $\hat{a}$, this does not change the numbering of the remaining transitions:

[TABLE]

• •

$Box_{dtsd}(E\ {\sf sy}\ a)=\Theta_{\!\!\ {\sf sy}\ a}(Box_{dtsd}(E))$. Note that $\forall v,w\in T_{E}$ such that $\Lambda_{E}(v)=\varrho_{(\alpha,\kappa)},\ \Lambda_{E}(w)=\varrho_{(\beta,\lambda)}$ and $a\in\alpha,\ \hat{a}\in\beta$, the new transition $t$ resulting from synchronization of $v$ and $w$ has the label $\Lambda(t)=\varrho_{(\alpha\oplus_{a}\beta,\kappa\cdot\lambda)}$ if $t$ is a stochastic transition ($\kappa,\lambda\in(0;1)$); or $\Lambda(t)=\varrho_{(\alpha\oplus_{a}\beta,\natural_{l+m}^{\theta})}$ if $t$ is a deterministic one ($\kappa=\natural_{l}^{\theta},\ \lambda=\natural_{m}^{\theta},\ \theta\in I\!\!N,\ l,m\in I\!\!R_{>0}$); and the numbering $Enu(t)=(Enu_{E}(v))(Enu_{E}(w))$.

Thus, the enumeration function is defined as

[TABLE]

According to the definition of $\varrho_{\!\!\ {\sf sy}\ a}$, the synchronization is only possible when all the transitions in the set are stochastic (immediate or waiting, respectively). If we synchronize the same set of transitions in different orders, we obtain several resulting transitions with the same label and probability or weight, but with the different numberings having the same content. Then, we only consider a single transition from the resulting ones in the plain dtsd-box to avoid introducing redundant transitions.

For example, if the transitions $t$ and $u$ are generated by synchronizing $v$ and $w$ in different orders, we have $\Lambda(t)=\varrho_{(\alpha\oplus_{a}\beta,\kappa\cdot\lambda)}=\Lambda(u)$ for stochastic transitions ($\kappa,\lambda\in(0;1)$) or $\Lambda(t)=\varrho_{(\alpha\oplus_{a}\beta,\natural_{l+m}^{\theta})}=\Lambda(u)$ for deterministic ones ($\kappa=\natural_{l}^{\theta},\ \lambda=\natural_{m}^{\theta},\ \theta\in I\!\!N,\ l,m\in I\!\!R_{>0}$), but $Enu(t)=(Enu_{E}(v))(Enu_{E}(w))\neq(Enu_{E}(w))(Enu_{E}(v))=Enu(u)$, whereas $Cont(Enu(t))=Cont(Enu(v))\cup Cont(Enu(w))=\\ Cont(Enu(u))$. Then only one transition $t$ (or $u$, symmetrically) will appear in $Box_{dtsd}(E\ {\sf sy}\ a)$.

• •

$Box_{dtsd}([E*F*K])=\Theta_{[\,*\,*\,]}(Box_{dtsd}(E),Box_{dtsd}(F),Box_{dtsd}(K))$. Since we do not introduce new transitions, we preserve the initial numbering:

[TABLE]

We now can formally define the denotational semantics as a homomorphism.

Definition 4.5

Let $(\alpha,\kappa)\in{\cal SDL},\ a\in Act$ and $E,F,K\in RegStatExpr$. The denotational semantics of dtsdPBC is a mapping $Box_{dtsd}$ from $RegStatExpr$ into the domain of plain dtsd-boxes defined as follows:

$Box_{dtsd}((\alpha,\kappa)_{\iota})=N_{(\alpha,\kappa)_{\iota}}$; 2. 2.

$Box_{dtsd}(E\circ F)=\Theta_{\circ}(Box_{dtsd}(E),Box_{dtsd}(F)),\ \circ\in\{;,[],\|\}$; 3. 3.

$Box_{dtsd}(E[f])=\Theta_{[f]}(Box_{dtsd}(E))$; 4. 4.

$Box_{dtsd}(E\circ a)=\Theta_{\circ a}(Box_{dtsd}(E)),\ \circ\in\{\!\!\ {\sf rs}\ \!\!,\!\!\ {\sf sy}\ \!\!\}$; 5. 5.

$Box_{dtsd}([E*F*K])=\Theta_{[\,*\,*\,]}(Box_{dtsd}(E),Box_{dtsd}(F),Box_{dtsd}(K))$.

The dtsd-boxes of dynamic expressions can be defined as well. For $E\in RegStatExpr$, let $Box_{dtsd}(\overline{E})=\overline{Box_{dtsd}(E)}$ and $Box_{dtsd}(\underline{E})=\underline{Box_{dtsd}(E)}$. Note that this definition is compositional in the sense that, for any arbitrary dynamic expression, we may decompose it in some inner dynamic and static expressions, for which we may apply the definition, thus obtaining the corresponding plain dtsd-boxes, which can be joined according to the term structure (by definition of $Box_{dtsd}$), the resulting plain box being marked in the places that were marked in the argument nets. Importantly, when composing dtsd-boxes of arbitrary dynamic expressions, we should guarantee that the operations correctly propagate the timer values from the clocked to non-clocked operands. For that, we have to respect the time spent in the entry markings.

Let $E,F\in RegStatExpr,\ G,H\in RegDynExpr$ and $a\in Act$. For $N_{E}=Box_{dtsd}(E)=(P_{E},T_{E},W_{E},\Lambda_{E})$, the clocked plain dtsd-box of $E$ is $(N_{E},(\emptyset,V^{*}))$, and analogously for $F$. Next, for $N_{G}=Box_{dtsd}(\lfloor G\rfloor)=(P_{G},T_{G},W_{G},\Lambda_{G})$, the clocked plain dtsd-box of $G$ is $Box_{dtsd}(G)=(N_{G},(M_{G},V_{G}))$ (defined by induction on the structure of $G$, as it will be descried below), and similarly for $H$.

Let $(P,T,W,\Lambda,(M,V))$ be a clocked plain dtsd-box, where $T=Ts\uplus Ti\uplus Tw$ consists of stochastic, immediate and waiting transitions. The marking age of the state $(M,V)$ is defined as $\Box(M,V)=\max\{\eta-V(u)\mid u\in Tw\cap Ena(M),\ \Lambda(u)=\varrho_{(\beta,\natural_{m}^{\eta})}\}$. The minimal delay of the waiting transitions from the set $U\subseteq Tw$ that are enabled at the marking $M$ is defined as $\theta(M,U)=\min\{\eta\mid u\in U\cap Ena(M),\ \Lambda(u)=\varrho_{(\beta,\natural_{m}^{\eta})}\}$. We now inductively define the dtsd-boxes of arbitrary dynamic expressions.

• •

$Box_{dtsd}(\overline{E})=\overline{Box_{dtsd}(E)}$ and $Box_{dtsd}(\underline{E})=\underline{Box_{dtsd}(E)}$.

• •

$Box_{dtsd}(G;E)=(Box_{dtsd}(\lfloor G\rfloor;E),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

Thus, each waiting transition of $N_{E}$ enabled at the entry marking of it has set its timer to the transition delay $\theta$ (the initial valuation).

• •

$Box_{dtsd}(E;G)=(Box_{dtsd}(E;\lfloor G\rfloor),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

• •

$Box_{dtsd}(G[]E)=(Box_{dtsd}(\lfloor G\rfloor[]E),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

Thus, if $\zeta$ is the minimum of the time spent at the the marking $M=M_{G}$ of the state $(M_{G},V_{G})$ and the delays of the waiting transitions from $Tw_{E}$, enabled at that marking, then each waiting transition, enabled at $M$, has set its timer to $\theta-\zeta$, where $\theta$ is the delay of that transition. It is guaranteed that the new timer value is not less than $1$, since in case when $\Box(M_{G},V_{G})>\theta(M,Tw_{E})-1$ and $\theta=\theta(M,Tw_{E})$ we have $\theta-(\theta(M,Tw_{E})-1)=1$. In that case, the subnet $N_{G}$ should “wait” for the subnet $N_{E}$ by modifying appropriately (via increasing by the difference between the residence time at $M$ and minimal delay of transitions from $Tw_{E}\cap Ena(M)$ minus $1$) the timer values of its waiting transitions, enabled at $M$.

Note that $\Box(M_{G},V_{G})>\theta(M,Tw_{E})-1$ does not hold for any dynamic expression, obtained by applying action rules, starting from an overlined static expression without timer value superscripts. The reason is that all the action rules maintain the time progress uniformity, hence, $\zeta=\Box(M_{G},V_{G})$ in that case. Further, the inequality $\eta-V_{G}(u)<\Box(M_{G},V_{G})$ may only happen when the $(\beta,\natural_{m}^{\eta})\in{\cal WL}(G)$, corresponding to $u\in Tw_{G}\cap Ena(M_{G})$, is later affected by restriction, so that the timer of that waiting multiaction stops with the value $1$ while the waiting multiaction can never be executed. Thus, if we start from an overlined static expression without time stamps and the waiting multiaction corresponding to $t$ is not subsequently affected by restriction then $V(t)=\theta-\Box(M_{G},V_{G})=V_{G}(t)$ for $t\in Tw_{G}\cap Ena(M)$ and $V(t)=\theta-\Box(M_{G},V_{G})$ for $t\in Tw_{E}\cap Ena(M)$.

The definition of $Box_{dtsd}(E[]G)$ is similar.

• •

$Box_{dtsd}(G\|H)=(Box_{dtsd}(\lfloor G\rfloor\|\lfloor H\rfloor),(M,V))$, where $M=M_{G}\cup M_{H}$, and $\forall t\in Tw_{N}$ with

$\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

Thus, if $\zeta$ is the minimum of the times spent at the markings of the states $(M_{G},V_{G})$ and $(M_{H},V_{H})$ then each waiting transition, enabled at the marking $M$, has set its timer to $\theta-\zeta$, where $\theta$ is the delay of that transition. The idea is to ensure that the time progresses uniformly, for which the timer decrements of all waiting transitions, enabled at $M$, should be synchronized (equalized). Hence, the subnet with the more time spent in its local marking should “wait” for the other subnet by modifying appropriately (via increasing by the difference between residence times at $M_{G}$ and $M_{H}$) the timer values of its waiting transitions, enabled at $M$.

Note that $\Box(M_{G},V_{G})\neq\Box(M_{H},V_{H})$ cannot hold for any dynamic expression, obtained by applying action rules, starting from an overlined static expression without timer value superscripts. The reason is that all the action rules maintain the time progress uniformity, hence, $\zeta=\Box(M_{G},V_{G})=\Box(M_{H},V_{H})$ in that case. Further, the inequality $\eta-V_{G}(u)<\Box(M_{G},V_{G})$ may only happen when the $(\beta,\natural_{m}^{\eta})\in{\cal WL}(G)$, corresponding to $u\in Tw_{G}\cap Ena(M_{G})$, is later affected by restriction, so that the timer of that waiting multiaction stops with the value $1$ while the waiting multiaction can never be executed. The same holds for $\Box(M_{H},V_{H})$. Thus, if we start from an overlined static expression without time stamps and the waiting multiaction corresponding to $t$ is not subsequently affected by restriction then $V(t)=\theta-\Box(M_{G},V_{G})=V_{G}(t)$ for $t\in Tw_{G}\cap Ena(M)$ and $V(t)=\theta-\Box(M_{H},V_{H})=V_{H}(t)$ for $t\in Tw_{H}\cap Ena(M)$.

The definition of $Box_{dtsd}(H\|G)$ is similar.

• •

$Box_{dtsd}(G[f])=(Box_{dtsd}(\lfloor G\rfloor[f]),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

• •

$Box_{dtsd}(G\ {\sf rs}\ a)=(Box_{dtsd}(\lfloor G\rfloor\ {\sf rs}\ a),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

• •

$Box_{dtsd}(G\ {\sf sy}\ a)=(Box_{dtsd}(\lfloor G\rfloor\ {\sf sy}\ a),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

Thus, the timer of the synchronous product of the two waiting transitions $v$ and $w$ of $N_{G}$ is set to their timer values. Those values coincide, since only waiting transitions with the same delays are synchronized and the time progresses uniformly in every whole dynamic expression.

• •

$Box_{dtsd}([G*E*F])=(Box_{dtsd}(\lfloor G\rfloor*E*F),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with

$\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

Thus, each waiting transition of $N_{E}$, enabled at the entry marking of it, has set its timer to the transition delay $\theta$ (the initial valuation).

• •

$Box_{dtsd}([E*G*F])=(Box_{dtsd}(E*\lfloor G\rfloor*F),(M,V))$, where $M=M_{G}$, and $\forall t\in Tw_{N}$ with

$\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})}$:

[TABLE]

Thus, if $\zeta$ is the minimum of the time spent at the the marking $M=M_{G}$ of the state $(M_{G},V_{G})$ and the delays of the waiting transitions from $Tw_{F}$, enabled at that marking, then each waiting transition, enabled at $M$, has set its timer to $\theta-\zeta$, where $\theta$ is the delay of that transition. It is guaranteed that the new timer value is not less than $1$, since in case when $\Box(M_{G},V_{G})>\theta(M,Tw_{F})-1$ and $\theta=\theta(M,Tw_{F})$ we have $\theta-(\theta(M,Tw_{F})-1)=1$. In that case, the subnet $N_{G}$ should “wait” for the subnet $N_{F}$ by modifying appropriately (via increasing by the difference between the residence time at $M$ and minimal delay of transitions from $Tw_{F}\cap Ena(M)$ minus $1$) the timer values of its waiting transitions, enabled at $M$.

The definition of $Box_{dtsd}([E*F*G])$ is similar.

Theorem 4.1

For any static expression $E,\ Box_{dtsd}(\overline{E})$ is safe and clean.

Proof. The structure of the net is obtained as in PBC [10, 9], combining both refinement and relabeling. Consequently, the dtsd-boxes thus obtained will be safe and clean. $\sqcap\!\!\!\!\sqcup$

Let $\simeq$ denote isomorphism between transition systems and reachability graphs that binds their initial states. Note that the names of transitions of the dtsd-box corresponding to a static expression could be identified with the enumerated activities of the latter.

Theorem 4.2

For any static expression $E$,

[TABLE]

Proof. As for the qualitative (functional) behaviour, we have the same isomorphism as in PBC [10, 9].

The quantitative behaviour is the same by the following reasons. First, the activities of an expression have the probability or delay and weight parts coinciding with the probabilities or delays and weights of the transitions belonging to the corresponding dtsd-box. Second, we use analogous probability or delay and weight functions to construct the corresponding transition systems and reachability graphs.

In general, the proof goes along the same lines as that from [31]. For instance, observe the relationships between the process expressions and their Petri net counterparts in dtsdPBC. Let $E\in RegStatExpr$ and $\overline{N}=Box_{dtsd}(\overline{E})$. There is the following bijection between $DR(\overline{E})$ and $RS(\overline{N})$. For a process state $s=[G]_{\approx}\in DR(\overline{E})$, the corresponding net state is $Q=(M,V)\in RS(\overline{N})$ with the next properties. First, $M$ is the marking of the clocked dtsd-box $(N,(M,V))=Box_{dtsd}(G)$. Second, for each transition $t\in T_{N}$ with $\Lambda_{N}(t)=\varrho_{(\alpha,\natural_{l}^{\theta})},\ \theta\in I\!\!N_{\geq 1},\ l\in I\!\!R_{>0}$, we have $V(t)=I_{G}((\alpha,\natural_{l}^{\theta}))$. Note that each expression $H\in s\cap SatOpRegDynExpr$ can be seen as a “partial” representation of the net marking $M$ and state $Q$, since possibly not all enabled activities are overlined in $H$. The transition set $U\subseteq T_{N}$ corresponding to a (multi)set of activities $\Upsilon\in I\!\!N_{fin}^{\cal SDL}$ is such that $\forall t\in U\ \Lambda_{N}(t)=\varrho_{(\alpha,\kappa)}$, where $(\alpha,\kappa)\in\Upsilon$. Thus, here we also have a bijection. Notice that the marking $M$ is obtained from ${{}^{\circ}}N$ by firing the sequence of transition sets corresponding to the activities (multi)sets, whose execution from $[\overline{E}]_{\approx}$ has led to the state $s$. For the corresponding process and net states $s\in DR(\overline{E})$ and $Q=(M,V)\in RS(\overline{N})$, the sets of the enabled activities $Ena(s)$ and transitions $Ena(M)$ are constructed similarly. The sets of the executable activities (multi)sets $Exec(s)$ and fireable transitions sets $Fire(Q)$ are analogous as well. At last, the probability functions $PF(s,\Upsilon)$ and $PT(s,\Upsilon)$ are respectively defined in the same way as $PF(Q,U)$ and $PT(Q,U)$, for the corresponding (multi)set of activities $\Upsilon$ and transition set $U$. $\sqcap\!\!\!\!\sqcup$

Example 4.1

Let $E$ be from Examples 3.9–3.18. In Figures 14–23, the clocked dtsd-boxes $N=Box_{dtsd}(\overline{E})$ are presented. Due to the time constraints and since waiting multiactions may be preempted by stochastic ones, some dynamic expressions can have complex transition systems and simple clocked dtsd-boxes (Examples 3.9–3.13), or vice versa (Examples 3.14–3.18).

Example 4.2

Let $E$ be from Example 3.19. In Figure 24, the clocked dtsd-box $N=Box_{dtsd}(\overline{E})$ and its reachability graph $RG(N)$ are presented. Since $N$ has a single waiting transition $t_{2}$ that is enabled only at marking $M_{2}=(0,1,0,0,0,0)$ and whose delay is $1$, the timer valuation function is defined as follows: $V(t_{2})=1$ at $M_{2}$, and $V(t_{2})=*$ at each of the four different markings. It is easy to see that $TS(\overline{E})$ and $RG(N)$ are isomorphic.

The following example demonstrates that without the syntactic restriction on regularity of expressions the corresponding clocked dtsd-boxes may be not safe.

Example 4.3

Let $E=[((\{a\},\frac{1}{2})*((\{b\},\frac{1}{2})\|(\{c\},\frac{1}{2}))*(\{d\},\frac{1}{2})]$. In Figure 25, the clocked dtsd-box $N=Box_{dtsd}(\overline{E})$ and its reachability graph $RG(N)$ are presented. Since $N$ has no waiting transitions, we may consider the substituent markings as the whole states. At the marking $(0,1,1,2,0,0)$ there are $2$ tokens in the place $p_{4}$. Symmetrically, at the marking $(0,1,1,0,2,0)$ there are $2$ tokens in the place $p_{5}$. Thus, allowing concurrency in the second argument of iteration in the expression $\overline{E}$ can lead to non-safeness of the corresponding clocked dtsd-box $N$, though, it is $2$-bounded in the worst case [9]. The origin of the problem is that $N$ has as a self-loop with two subnets which can function independently. Therefore, we have decided to consider regular expressions only, since the alternative, which is a safe version of the iteration operator with six arguments in the corresponding dtsd-box, like that from [9], is rather cumbersome and has too intricate PN interpretation. Our motivation was to keep the algebraic and PN specifications as simple as possible.

5 Performance evaluation

In this section we demonstrate how Markov chains corresponding to the expressions and dtsd-boxes can be constructed and then used for performance evaluation.

5.1 Analysis of the underlying SMC

For a dynamic expression $G$, a discrete random variable $\xi(s)$ is associated with every tangible state $s\in DR_{T}(G)$. The variable captures the residence (sojourn) time in the state. One can interpret staying in a state at the next discrete time moment as a failure and leaving it as a success in some trial series. It is easy to see that $\xi(s)$ is geometrically distributed with the parameter $1-PM(s,s)$, since the probability to stay in $s$ for $k-1$ time moments and leave it at the moment $k\geq 1$, called the probability mass function (PMF) of the residence time in $s$, is $p_{\xi(s)}(k)={\sf P}(\xi(s)=k)=PM(s,s)^{k-1}(1-PM(s,s))\ (k\in I\!\!N_{\geq 1})$ (the residence time is $k$ in this case). Hence, the probability distribution function (PDF) of the residence time in $s$ is $F_{\xi(s)}(k)={\sf P}(\xi(s)<k)=1-PM(s,s)^{k-1}\ (k\in I\!\!N_{\geq 1})$ (the probability that the residence time in $s$ is less than $k$). The mean value formula for the geometrical distribution allows us to calculate the average sojourn time in $s$ as $SJ(s)=\frac{1}{1-PM(s,s)}$. The average sojourn time in each vanishing state $s\in DR_{V}(G)$ is $SJ(s)=0$. Let $s\in DR(G)$.

The average sojourn time in the state $s$ is

[TABLE]

The average sojourn time vector of $G$, denoted by $SJ$, has the elements $SJ(s),\ s\in DR(G)$.

The sojourn time variance in the state $s$ is

[TABLE]

The sojourn time variance vector of $G$, denoted by $VAR$, has the elements $VAR(s),\ s\in DR(G)$.

To evaluate performance of the system specified by a dynamic expression $G$, we should investigate the stochastic process associated with it. The process is the underlying semi-Markov chain (SMC) [50, 29], denoted by $SMC(G)$, which can be analyzed by extracting from it the embedded (absorbing) discrete time Markov chain (EDTMC) corresponding to $G$, denoted by $EDTMC(G)$. The construction of the latter is analogous to that applied in the context of generalized stochastic PNs (GSPNs) in [40, 2, 3], and also in the framework of discrete time deterministic and stochastic PNs (DTDSPNs) in [61, 62, 64, 65], as well as within discrete deterministic and stochastic PNs (DDSPNs) [63]. $EDTMC(G)$ only describes the state changes of $SMC(G)$ while ignoring its time characteristics. Thus, to construct the EDTMC, we should abstract from all time aspects of behaviour of the SMC, i.e. from the sojourn time in its states. The (local) sojourn time in every state of the EDTMC is deterministic and it is equal to one discrete time unit. It is well-known that every SMC is fully described by the EDTMC and the state sojourn time distributions (the latter can be specified by the vector of PDFs of residence time in the states) [22].

Let $G$ be a dynamic expression and $s,\tilde{s}\in DR(G)$. The transition system $TS(G)$ can have self-loops going from a state to itself which have a non-zero probability. Clearly, the current state remains unchanged in this case.

Let $s\rightarrow s$. The probability to stay in $s$ due to $k\ (k\geq 1)$ self-loops is

[TABLE]

Let $s\rightarrow\tilde{s}$ and $s\neq\tilde{s}$. The probability to move from $s$ to $\tilde{s}$ by executing any multiset of activities after possible self-loops is

[TABLE]

[TABLE]

Here $SL(s)$ is the self-loops abstraction factor in the state $s$. The self-loops abstraction vector of $G$, denoted by $SL$, has the elements $SL(s),\ s\in DR(G)$. The value $k=0$ in the summation above corresponds to the case when no self-loops occur.

Let $s\in DR_{T}(G)$. If there exist self-loops from $s$ (i.e. if $s\rightarrow s$) then $PM(s,s)>0$ and $SL(s)=\frac{1}{1-PM(s,s)}=SJ(s)$. Otherwise, if there exist no self-loops from $s$ then $PM(s,s)=0$ and $SL(s)=1=\frac{1}{1-PM(s,s)}=SJ(s)$. Thus, $\forall s\in DR_{T}(G)\ SL(s)=SJ(s)$, hence, $\forall s\in DR_{T}(G)\ PM^{*}(s,\tilde{s})=SJ(s)PM(s,\tilde{s})$. Note that the self-loops from tangible states are of the empty or non-empty type, the latter produced by iteration, since empty loops are not possible from w-tangible states, but they are possible from s-tangible states, while non-empty loops are possible from both s-tangible and w-tangible states.

Let $s\in DR_{V}(G)$. We have $\forall s\in DR_{V}(G)\ SL(s)\neq SJ(s)=0$ and $\forall s\in DR_{V}(G)\ PM^{*}(s,\tilde{s})=SL(s)PM(s,\tilde{s})$. If there exist self-loops from $s$ then $PM^{*}(s,\tilde{s})=\frac{PM(s,\tilde{s})}{1-PM(s,s)}$. Otherwise, if there exist no self-loops from $s$ then $PM^{*}(s,\tilde{s})=PM(s,\tilde{s})$. Note that the self-loops from vanishing states are always of the non-empty type, produced by iteration, since empty loops are not possible from vanishing states.

Note that after abstraction from the probabilities of transitions which do not change the states, the remaining transition probabilities are normalized. In order to calculate transition probabilities $PT(\Upsilon,s)$, we had to normalize $PF(\Upsilon,s)$. Then, to obtain transition probabilities of the state-changing steps $PM^{*}(s,\tilde{s})$, we now have to normalize $PM(s,\tilde{s})$. Thus, we have a two-stage normalization as a result.

Notice that $PM^{*}(s,\tilde{s})$ defines a probability distribution, since $\forall s\in DR(G)$ such that $s$ is not a terminal state, i.e. there are transitions to different states after possible self-loops from it, we have $\sum_{\{\tilde{s}\mid s\rightarrow\tilde{s},\ s\neq\tilde{s}\}}PM^{*}(s,\tilde{s})=\frac{1}{1-PM(s,s)}\sum_{\{\tilde{s}\mid s\rightarrow\tilde{s},\ s\neq\tilde{s}\}}PM(s,\tilde{s})=\frac{1}{1-PM(s,s)}(1-PM(s,s))=1$.

We decided to consider self-loops followed only by a state-changing step just for convenience. Alternatively, we could take a state-changing step followed by self-loops or a state-changing step preceded and followed by self-loops. In all these three cases our sequence begins or/and ends with the loops which do not change states. At the same time, the overall probabilities of the evolutions can differ, since self-loops have positive probabilities. To avoid inconsistency of definitions and too complex description, we consider sequences ending with a state-changing step. It resembles in some sense a construction of branching bisimulation [19] taking self-loops instead of silent transitions.

Definition 5.1

*Let $G$ be a dynamic expression. The embedded (absorbing) discrete time Markov chain

(EDTMC) of $G$, denoted by $EDTMC(G)$, has the state space $DR(G)$, the initial state $[G]_{\approx}$ and the transitions $s\rightarrow\!\!\!\!\!\rightarrow_{\cal P}\tilde{s}$, if $s\rightarrow\tilde{s}$ and $s\neq\tilde{s}$, where ${\cal P}=PM^{*}(s,\tilde{s})$.*

The underlying SMC of $G$, denoted by $SMC(G)$, has the EDTMC $EDTMC(G)$ and the sojourn time in every $s\in DR_{T}(G)$ is geometrically distributed with the parameter $1-PM(s,s)$ while the sojourn time in every $s\in DR_{V}(G)$ is equal to [math].

EDTMCs and underlying SMCs of static expressions can be defined as well. For $E\in RegStatExpr$, let $EDTMC(E)=EDTMC(\overline{E})$ and $SMC(E)=SMC(\overline{E})$.

Let $G$ be a dynamic expression. The elements ${\cal P}_{ij}^{*}\ (1\leq i,j\leq n=|DR(G)|)$ of the (one-step) transition probability matrix (TPM) ${\bf P}^{*}$ for $EDTMC(G)$ are defined as

[TABLE]

The transient ($k$-step, $k\in I\!\!N$) PMF $\psi^{*}[k]=(\psi^{*}[k](s_{1}),\ldots,\psi^{*}[k](s_{n}))$ for $EDTMC(G)$ is calculated as

[TABLE]

where $\psi^{*}[0]=(\psi^{*}[0](s_{1}),\ldots,\psi^{*}[0](s_{n}))$ is the initial PMF defined as

[TABLE]

Note also that $\psi^{*}[k+1]=\psi^{*}[k]{\bf P}^{*}\ (k\in I\!\!N)$.

The steady-state PMF $\psi^{*}=(\psi^{*}(s_{1}),\ldots,\psi^{*}(s_{n}))$ for $EDTMC(G)$ is a solution of the equation system

[TABLE]

where ${\bf I}$ is the identity matrix of order $n$ and ${\bf 0}$ is a row vector of $n$ values $0,\ {\bf 1}$ is that of $n$ values $1$.

Note that the vector $\psi^{*}$ exists and is unique if $EDTMC(G)$ is ergodic. Then $EDTMC(G)$ has a single steady state, and we have $\psi^{*}=\lim_{k\to\infty}\psi^{*}[k]$.

The steady-state PMF for the underlying semi-Markov chain $SMC(G)$ is calculated via multiplication of every $\psi^{*}(s_{i})\ (1\leq i\leq n)$ by the average sojourn time $SJ(s_{i})$ in the state $s_{i}$, after which we normalize the resulting values. Remember that for each w-tangible state $s\in DR_{WT}(G)$ we have $SJ(s)=1$, and for each vanishing state $s\in DR_{V}(G)$ we have $SJ(s)=0$.

Thus, the steady-state PMF $\varphi=(\varphi(s_{1}),\ldots,\varphi(s_{n}))$ for $SMC(G)$ is

[TABLE]

Thus, to calculate $\varphi$, we apply abstraction from self-loops to get ${\bf P}^{*}$ and then $\psi^{*}$, followed by weighting by $SJ$ and normalization. $EDTMC(G)$ has no self-loops, unlike $SMC(G)$, hence, the behaviour of $EDTMC(G)$ stabilizes quicker than that of $SMC(G)$ (if each of them has a single steady state), since ${\bf P}^{*}$ has only zero elements at the main diagonal.

Example 5.1

Let $E$ be from Example 3.19. In Figure 26, the underlying SMC $SMC(\overline{E})$ is presented. The average sojourn times in the states of the underlying SMC is written next to them in bold font.

The average sojourn time vector of $\overline{E}$ is

[TABLE]

The sojourn time variance vector of $\overline{E}$ is

[TABLE]

The TPM for $EDTMC(\overline{E})$ is

[TABLE]

The steady-state PMF for $EDTMC(\overline{E})$ is

[TABLE]

The steady-state PMF $\psi^{*}$ weighted by $SJ$ is

[TABLE]

It remains to normalize the steady-state weighted PMF by dividing it by the sum of its components

[TABLE]

Thus, the steady-state PMF for $SMC(\overline{E})$ is

[TABLE]

In the case $l=m$ and $\theta=\phi$ we have

[TABLE]

Let $G$ be a dynamic expression and $s,\tilde{s}\in DR(G),\ S,\widetilde{S}\subseteq DR(G)$. The following standard performance indices (measures) can be calculated based on the steady-state PMF $\varphi$ for $SMC(G)$ and the average sojourn time vector $SJ$ of $G$ [46, 27].

• •

The average recurrence (return) time in the state $s$ (i.e. the number of discrete time units or steps required for this) is $ReturnTime(s)=\frac{1}{\varphi(s)}$.

• •

The fraction of residence time in the state $s$ is $TimeFract(s)=\varphi(s)$.

• •

The fraction of residence time in the set of states $S$ or the probability of the event determined by a condition that is true for all states from $S$ is $TimeFract(S)=\sum_{s\in S}\varphi(s)$.

• •

The relative fraction of residence time in the set of states $S$ with respect to that in $\widetilde{S}$ is

$RltTimeFract(S,\widetilde{S})=\frac{\sum_{s\in S}\varphi(s)}{\sum_{\tilde{s}\in\widetilde{S}}\varphi(\tilde{s})}$.

• •

The exit/entrance frequency (rate of leaving/entering, average number of exits/entrances per unit of time) the state $s$ is $ExitFreq(s)=\frac{\varphi(s)}{SJ(s)}$.

• •

The steady-state probability to perform a step with a multiset of activities $\Xi$ is

$ActsProb(\Xi)=\sum_{s\in DR(G)}\varphi(s)\sum_{\{\Upsilon\mid\Xi\subseteq\Upsilon\}}PT(\Upsilon,s)$.

• •

The steady-state execution frequency (throughput) of the activity $(\alpha,\kappa)$ is

$ExecFreq((\alpha,\kappa))=\sum_{s\in DR(G)}\frac{\varphi(s)}{SJ(s)}\sum_{\{\Upsilon\mid(\alpha,\kappa)\in\Upsilon\}}PT(\Upsilon,s)$.

• •

The probability of the event determined by a reward function $r$ on the states is

$Prob(r)=\sum_{s\in DR(G)}\varphi(s)r(s)$, where $\forall s\in DR(G)\ 0\leq r(s)\leq 1$.

Example 5.2

Let us interpret $E$ be from Example 3.19 as a specification of the travel system. A tourist visits regularly new cities. After seeing the sights of the current city, he goes to the next city by the nearest train or bus available at the city station. Buses depart less frequently than trains, but the next city is quicker reached by bus than by train. We suppose that the stay duration in every city (being a constant), the departure numbers of trains and buses, as well as their speeds do not depend on a particular city, bus or train. The travel route has been planned so that the distances between successive cities coincide.

The meaning of actions from the syntax of $E$ is as follows. The action $a$ corresponds to the system activation (the travel route has been planned) that takes a time, geometrically distributed with the parameter $\rho$. The action $b$ represents the completion of looking round the current city and coming to the city station that takes a fixed time equal to $1$ (say, one hour) for every city. The actions $c$ and $e$ correspond to the urgent getting on bus and train, respectively, and thus model the choice between these two transport facilities. The weights of the two corresponding immediate multiactions suggest that every $l$ departures of buses take the same time as $m$ departures of trains ($l<m$), hence, a bus departs with the probability $\frac{l}{l+m}$ while a train departs with the probability $\frac{m}{l+m}$. The actions $c$ and $e$ correspond to the coming in a city by bus and train, respectively, that takes a time, geometrically distributed with the parameters $\theta$ and $\phi$, respectively ($\theta>\phi$).

The meaning of states from $DR(\overline{E})$ is the following. The s-tangible state $s_{1}$ corresponds to staying at home and planning the future travel. The w-tangible state $s_{2}$ means residence in a city for exactly one time unit (hour). The vanishing state $s_{3}$ with zero residence time represents instantaneous stay at the city station, signifying that the tourist does not wait there for departure of the transport. The s-tangible states $s_{4}$ and $s_{5}$ correspond to going by bus and train, respectively.

Using Example 5.1, we now calculate the performance indices, based on the steady-state PMF for $SMC(\overline{E})\\ \varphi=\frac{1}{\theta\phi(l+m)+\phi l+\theta m}(0,\theta\phi(l+m),0,\phi l,\theta m)$ and the average sojourn time vector of $\overline{E}\ SJ=\left(\frac{1}{\rho},1,0,\frac{1}{\theta},\frac{1}{\phi}\right)$.

• •

The average time between comings to the successive cities (mean sightseeing and travel time) is

$ReturnTime(s_{2})=\frac{1}{\varphi(s_{2})}=1+\frac{\phi l+\theta m}{\theta\phi(l+m)}$.

• •

The fraction of time spent in a city (sightseeing time fraction) is $TimeFract(s_{2})=\varphi(s_{2})=\\ \frac{\theta\phi(l+m)}{\theta\phi(l+m)+\phi l+\theta m}$.

• •

The fraction of time spent in a transport (travel time fraction) is $TimeFract(\{s_{4},s_{5}\})=\varphi(s_{4})+\varphi(s_{5})=\frac{\phi l+\theta m}{\theta\phi(l+m)+\phi l+\theta m}$.

• •

The relative fraction of time spent in a city with respect to that spent in transport (sightseeing relative to travel time fraction) is $RltTimeFract(\{s_{2}\},\{s_{4},s_{5}\})=\frac{\varphi(s_{2})}{\varphi(s_{4})+\varphi(s_{5})}=\frac{\theta\phi(l+m)}{\phi l+\theta m}$.

• •

The rate of leaving/entering a city (departure/arrival rate) is $ExitFreq(s_{2})=\frac{\varphi(s_{2})}{SJ(s_{2})}=\frac{\theta\phi(l+m)}{\theta\phi(l+m)+\phi l+\theta m}$.

Let $N=(P_{N},T_{N},W_{N},D_{N},\Omega_{N},{\cal L}_{N},Q_{N})$ be a LDTSDPN and $Q,\widetilde{Q}$ be its states. Then the average sojourn time $SJ(Q)$, the sojourn time variance $VAR(Q)$, the probabilities $PM^{*}(M,\widetilde{M})$, the transition relation $M\rightarrow\!\!\!\!\!\rightarrow_{\cal P}\widetilde{M}$, the EDTMC $EDTMC(N)$, the underlying SMC $SMC(N)$ and the steady-state PMF for it are defined like the corresponding notions for dynamic expressions.

As we have mentioned earlier, every clocked plain dtsd-box could be interpreted as the LDTSDPN. Therefore, we can evaluate performance with the LDTSDPNs corresponding to dtsd-boxes and then transfer the results to the latter.

Let $\simeq$ denote isomorphism between SMCs that binds their initial states, where two SMCs are isomorphic if their EDTMCs are so and the sojourn times in the isomorphic states of the EDTMCs are identically distributed.

Proposition 5.1

For any static expression $E$

[TABLE]

Proof. By Theorem 4.2 and definitions of underlying SMCs for dynamic expressions and LDTSDPNs taking into account the following. First, for the associated SMCs, the average sojourn time in the states is the same, since it is defined via the analogous probability functions. Second, the transition probabilities of the associated SMCs are the sums of those belonging to transition systems or reachability graphs.

Fore instance, observe that the probability functions $PM(s,\tilde{s})$ and $PM^{*}(s,\tilde{s})$ can be respectively defined in the same way as $PM(Q,\widetilde{Q})$ and $PM^{*}(Q,\widetilde{Q})$, for the corresponding $s$ and $Q$, as well as $\tilde{s}$ and $\widetilde{Q}$. $\sqcap\!\!\!\!\sqcup$

Example 5.3

Let $E$ be from Example 3.19. In Figure 27, the underlying SMC $SMC(N)$ is presented. It is easy to see that $SMC(\overline{E})$ and $SMC(N)$ are isomorphic. Thus, both the transient and steady-state PMFs for $SMC(N)$ and $SMC(\overline{E})$ coincide.

As mentioned in [61, 62], if is useful to consider performance measures over only the markings of DTDSPNs, instead of their whole states, whose second components are the remaining firing time vectors. In the context of dtsdPBC, such markings correspond to those of the dtsd-boxes of dynamic expressions, i.e. to the markings of the respective LDTSDPNs, obtained from their states by abstracting from the second components, which are the timer valuation functions.

Let $G$ be a dynamic expression. The underlying timer-free state of a state $s\in DR(G)$ is defined as $\downharpoonleft\!\!s=[\downharpoonleft\!\!H]_{\approx}$ for $H\in s$. Since structurally equivalent dynamic expressions obviously remain so after removing their timer value annotations, $\downharpoonleft\!\!s$ is unique for each $s$ and the previous definition is correct. The timer-free states (i.e. those from $\downharpoonleft\!\!DR(G)=\{\downharpoonleft\!\!s\mid s\in DR(G)\}$) correspond to the markings of the LDTSDPN $N=Box_{dtsd}(G)$. Let $s\in DR(G)$ and $\bar{s}=\downharpoonleft\!\!s$. The average sojourn time vector $SJ$, sojourn time variance vector $VAR$ and steady-state PMF for $SMC(G)$ over the timer-free states of $G$ are defined as follows: $SJ(\bar{s})=\sum_{\{s\in DR(G)\mid\downharpoonleft\!s=\bar{s}\}}SJ(s),\ VAR(\bar{s})=\sum_{\{s\in DR(G)\mid\downharpoonleft\!s=\bar{s}\}}VAR(s)$ and $\varphi(\bar{s})=\sum_{\{s\in DR(G)\mid\downharpoonleft\!s=\bar{s}\}}\varphi(s)$. Then $\varphi(\bar{s})$ and $SJ(\bar{s})$ can be used to calculate the standard performance indices over the timer-free states of $G$ (hence, over the markings of $N$), by analogy with the standard performance indices, defined over the arbitrary states of $G$. Then also the performance measures that are specific for LDTSDPNs can be derived, based on the numbers of tokens in the places of $N$.

5.2 Analysis of the DTMC

Let us consider an alternative solution method, studying the DTMCs of expressions based on the state change probabilities $PM(s,\tilde{s})$.

Definition 5.2

Let $G$ be a dynamic expression. The discrete time Markov chain (DTMC) of $G$, denoted by $DTMC(G)$, has the state space $DR(G)$, the initial state $[G]_{\approx}$ and the transitions $s\rightarrow_{\cal P}\tilde{s}$, where ${\cal P}=PM(s,\tilde{s})$.

DTMCs of static expressions can be defined as well. For $E\in RegStatExpr$, let $DTMC(E)=DTMC(\overline{E})$.

One can see that $EDTMC(G)$ is constructed from $DTMC(G)$ as follows. For each state of $DTMC(G)$, we remove a possible self-loop associated with it and then normalize the probabilities of the remaining transitions from the state. Thus, $EDTMC(G)$ and $DTMC(G)$ differ only by existence of self-loops and magnitudes of the probabilities of the remaining transitions. Hence, $EDTMC(G)$ and $DTMC(G)$ have the same communication classes of states and $EDTMC(G)$ is irreducible iff $DTMC(G)$ is so. Since both $EDTMC(G)$ and $DTMC(G)$ are finite, they are positive recurrent. Thus, in case of irreducibility, each of them has a single stationary PMF. Note that both $EDTMC(G)$ and $DTMC(G)$ or just one of them may be periodic, thus having a unique stationary distribution, but no steady-state (limiting) one. For example, it may happen that $EDTMC(G)$ is periodic while $DTMC(G)$ is aperiodic due to self-loops associated with some states of the latter. The states of $SMC(G)$ are classified using $EDTMC(G)$, hence, $SMC(G)$ is irreducible (positive recurrent, aperiodic) iff $EDTMC(G)$ is so.

Let $G$ be a dynamic expression. The elements ${\cal P}_{ij}\ (1\leq i,j\leq n=|DR(G)|)$ of (one-step) transition probability matrix (TPM) ${\bf P}$ for $DTMC(G)$ are defined as

[TABLE]

The steady-state PMF $\psi$ for $DTMC(G)$ is defined like the corresponding notion $\psi^{*}$ for $EDTMC(G)$.

Let us determine a relationship between steady-state PMFs for $DTMC(G)$ and $EDTMC(G)$. The following theorem proposes the equation that relates the mentioned steady-state PMFs.

First, we introduce some helpful notation. For a vector $v=(v_{1},\ldots,v_{n})$, let $Diag(v)$ be a diagonal matrix of order $n$ with the elements $Diag_{ij}(v)\ (1\leq i,j\leq n)$ defined as

[TABLE]

Theorem 5.1

Let $G$ be a dynamic expression and $SL$ be its self-loops abstraction vector. Then the steady-state PMFs $\psi$ for $DTMC(G)$ and $\psi^{*}$ for $EDTMC(G)$ are related as follows: $\forall s\in DR(G)$

[TABLE]

Proof. Let $PSL$ be a vector with the elements

[TABLE]

By definition of $PM^{*}(s,\tilde{s})$, we have ${\bf P}^{*}=Diag(SL)({\bf P}-Diag(PSL))$. Further,

[TABLE]

After replacement of ${\bf P}^{*}$ by $Diag(SL)({\bf P}-Diag(PSL))$ we obtain

[TABLE]

Note that $\forall s\in DR(G)$ we have

[TABLE]

Hence, $Diag(SL)Diag(PSL)+{\bf I}=Diag(SL)$. Thus,

[TABLE]

Then, for $v=\psi^{*}Diag(SL)$, we have

[TABLE]

In order to calculate $\psi$ on the basis of $v$, we must normalize it by dividing its elements by their sum, since we should have $\psi{\bf 1}^{T}=1$ as a result:

[TABLE]

Thus, the elements of $\psi$ are calculated as follows: $\forall s\in DR(G)$

[TABLE]

It is easy to check that $\psi$ is a solution of the equation system

[TABLE]

hence, it is indeed the steady-state PMF for $DTMC(G)$. $\sqcap\!\!\!\!\sqcup$

The following proposition relates the steady-state PMFs for $SMC(G)$ and $DTMC(G)$.

Proposition 5.2

Let $G$ be a dynamic expression, $\varphi$ be the steady-state PMF for $SMC(G)$ and $\psi$ be the steady-state PMF for $DTMC(G)$. Then $\forall s\in DR(G)$

[TABLE]

Proof. Let $s\in DR_{T}(G)$. Remember that $\forall s\in DR_{T}(G)\ SL(s)=SJ(s)$ and $\forall s\in DR_{V}(G)\ SJ(s)=0$.

Then, by Theorem 5.1, we have $\frac{\psi(s)}{\sum_{\tilde{s}\in DR_{T}(G)}\psi(\tilde{s})}=\frac{\frac{\psi^{*}(s)SL(s)}{\sum_{\tilde{s}\in DR(G)}\psi^{*}(\tilde{s})SL(\tilde{s})}}{\sum_{\tilde{s}\in DR_{T}(G)}\left(\frac{\psi^{*}(\tilde{s})SL(\tilde{s})}{\sum_{\breve{s}\in DR(G)}\psi^{*}(\breve{s})SL(\breve{s})}\right)}=\frac{\psi^{*}(s)SL(s)}{\sum_{\tilde{s}\in DR(G)}\psi^{*}(\tilde{s})SL(\tilde{s})}\cdot\\ \frac{\sum_{\breve{s}\in DR(G)}\psi^{*}(\breve{s})SL(\breve{s})}{\sum_{\tilde{s}\in DR_{T}(G)}\psi^{*}(\tilde{s})SL(\tilde{s})}=\frac{\psi^{*}(s)SL(s)}{\sum_{\tilde{s}\in DR_{T}(G)}\psi^{*}(\tilde{s})SL(\tilde{s})}=\frac{\psi^{*}(s)SJ(s)}{\sum_{\tilde{s}\in DR_{T}(G)}\psi^{*}(\tilde{s})SJ(\tilde{s})}=\frac{\psi^{*}(s)SJ(s)}{\sum_{\tilde{s}\in DR(G)}\psi^{*}(\tilde{s})SJ(\tilde{s})}=\varphi(s)$. $\sqcap\!\!\!\!\sqcup$

Thus, to calculate $\varphi$, one can only apply normalization to some elements of $\psi$ (corresponding to the tangible states), instead of abstracting from self-loops to get ${\bf P}^{*}$ and then $\psi^{*}$, followed by weighting by $SJ$ and normalization. Hence, using $DTMC(G)$ instead of $EDTMC(G)$ allows one to avoid multistage analysis, but the payment for it is more time-consuming numerical and more complex analytical calculation of $\psi$ with respect to $\psi^{*}$. The reason is that $DTMC(G)$ has self-loops, unlike $EDTMC(G)$, hence, the behaviour of $DTMC(G)$ stabilizes slower than that of $EDTMC(G)$ (if each of them has a single steady state) and ${\bf P}$ is more dense matrix than ${\bf P}^{*}$, since ${\bf P}$ may additionally have non-zero elements at the main diagonal. Nevertheless, Proposition 5.2 is very important, since the relationship between $\varphi$ and $\psi$ it discovers will be used in Proposition 5.3 to relate the steady-state PMFs for $SMC(G)$ and the reduced $DTMC(G)$.

Example 5.4

Let $E$ be from Example 3.19. In Figure 28, the DTMC $DTMC(\overline{E})$ is presented.

The TPM for $DTMC(\overline{E})$ is

[TABLE]

The steady-state PMF for $DTMC(\overline{E})$ is

[TABLE]

Remember that $DR_{T}(\overline{E})=DR_{ST}(\overline{E})\cup DR_{WT}(\overline{E})=\{s_{1},s_{2},s_{4},s_{5}\}$ and $DR_{V}(\overline{E})=\{s_{3}\}$. Hence,

[TABLE]

By Proposition 5.2, we have

[TABLE]

Thus, the steady-state PMF for $SMC(\overline{E})$ is

[TABLE]

This coincides with the result obtained in Example 5.1 with the use of $\psi^{*}$ and $SJ$.

5.3 Analysis of the reduced DTMC

Let us now consider the method from [18, 16, 17, 41, 2, 4, 3] that eliminates vanishing states from the EMC (EDTMC, in our terminology) corresponding to the underlying SMC of every GSPN $N$. The TPM for the resulting reduced EDTMC (REDTMC) has smaller size than that for the EDTMC. The method demonstrates that there exists a transformation of the underlying SMC of $N$ into a CTMC, whose states are the tangible markings of $N$. This CTMC, which is essentially the reduced underlying SMC (RSMC) of $N$, is constructed on the basis of the REDTMC. The CTMC can then be directly solved to get both the transient and the steady-state PMFs over the tangible markings of $N$. In [17], the program and computational complexities of such an elimination method, based on the REDTMC, were evaluated and compared with those of the preservation method that does not eliminate vanishing states and based on the EDTMC. The preservation method for GSPNs corresponds in dtsdPBC to the analysis of the underlying SMCs of expressions.

The elimination method for GSPNs can be easily transferred to dtsdPBC, hence, for every dynamic expression $G$, we can find a DTMC (since the sojourn time in the tangible states from $DR(G)$ is discrete and geometrically distributed) with the states from $DR_{T}(G)$, which can be directly solved to find the transient and the steady-state PMFs over the tangible states. We shall demonstrate that such a reduced DTMC (RDTMC) of $G$, denoted by $RDTMC(G)$, can be constructed from $DTMC(G)$, using the method analogous to that designed in [41, 2, 4, 3] in the framework of GSPNs to transform EDTMC into REDTMC. Since the sojourn time in the vanishing states is zero, the state changes of $RDTMC(G)$ occur in the moments of the global discrete time associated with $SMC(G)$, unlike those of $EDTMC(G)$, which happen only when the current state changes to some different one, irrespective of the global time. Therefore, in our case, we can skip the stages of constructing the REDTMC of $G$, denoted by $REDTMC(G)$, from $EDTMC(G)$, and recovering RSMC of $G$, denoted by $RSMC(G)$, (which is the sought-for DTMC) from $REDTMC(G)$, since we shall have $RSMC(G)=RDTMC(G)$.

Let $G$ be a dynamic expression and ${\bf P}$ be the TPM for $DTMC(G)$. We reorder the states from $DR(G)$ such that the first rows and columns of ${\bf P}$ will correspond to the states from $DR_{V}(G)$ and the last ones will correspond to the states from $DR_{T}(G)$. Let $|DR(G)|=n$ and $|DR_{T}(G)|=m$. The resulting matrix can be decomposed as follows:

[TABLE]

The elements of the $(n-m)\times(n-m)$ submatrix ${\bf C}$ are the probabilities to move from vanishing to vanishing states, and those of the $(n-m)\times m$ submatrix ${\bf D}$ are the probabilities to move from vanishing to tangible states. The elements of the $m\times(n-m)$ submatrix ${\bf E}$ are the probabilities to move from tangible to vanishing states, and those of the $m\times m$ submatrix ${\bf F}$ are the probabilities to move from tangible to tangible states.

The TPM ${\bf P}^{\diamond}$ for $RDTMC(G)$ is the $m\times m$ matrix, calculated as

[TABLE]

where the elements of the matrix ${\bf G}$ are the probabilities to move from vanishing to vanishing states in any number of state changes, without traversal of the tangible states.

If there are no loops among vanishing states then for any vanishing state there exists a value $l\in I\!\!N$ such that every sequence of state changes that starts in a vanishing state and is longer than $l$ should reach a tangible state. Thus, $\exists l\in I\!\!N\ \forall k>l\ {\bf C}^{k}={\bf 0}$ and $\sum_{k=0}^{\infty}{\bf C}^{k}=\sum_{k=0}^{l}{\bf C}^{k}$. If there are loops among vanishing states then all such loops are supposed to be of “transient” rather than “absorbing” type, since the latter is treated as a specification error to be corrected, like in [41, 3]. We have earlier required that $SMC(G)$ has a single closed communication (which is also ergodic) class of states. Remember that a communication class of states is their equivalence class w.r.t. communication relation, i.e. a maximal subset of communicating states. A communication class of states is closed if only the states belonging to it are accessible from every its state. The ergodic class cannot consist of vanishing states only to avoid “absorbing” loops among them, hence, it contains tangible states as well. Thus, any sequence of vanishing state changes that starts in the ergodic class will reach a tangible state at some time moment. All the states that do not belong to the ergodic class should be transient. Hence, any sequence of vanishing state changes that starts in a transient vanishing state will some time reach either a transient tangible state or a state from the ergodic class [29]. In the latter case, a tangible state will be reached as well, as argued above. Thus, every sequence of vanishing state changes in $SMC(G)$ that starts in a vanishing state will exit the set of all vanishing states in the future. This implies that the probabilities to move from vanishing to vanishing states in $k\in I\!\!N$ state changes, without traversal of tangible states, will lead to [math] when $k$ tends to $\infty$. Then we have $\lim_{k\to\infty}{\bf C}^{k}=\lim_{k\to\infty}({\bf I}-({\bf I}-{\bf C}))^{k}={\bf 0}$, hence, ${\bf I}-{\bf C}$ is a non-singular matrix, i.e. its determinant is not equal to zero. Thus, the inverse matrix of ${\bf I}-{\bf C}$ exists and may be expressed by a Neumann series as $\sum_{k=0}^{\infty}({\bf I}-({\bf I}-{\bf C}))^{k}=\sum_{k=0}^{\infty}{\bf C}^{k}=({\bf I}-{\bf C})^{-1}$. Therefore,

[TABLE]

where ${\bf 0}$ is the square matrix consisting only of zeros and ${\bf I}$ is the identity matrix, both of order $n-m$.

For $1\leq i,j\leq m$ and $1\leq k,l\leq n-m$, let ${\cal F}_{ij}$ be the elements of the matrix ${\bf F},\ {\cal E}_{ik}$ be those of ${\bf E},\ {\cal G}_{kl}$ be those of ${\bf G}$ and ${\cal D}_{lj}$ be those of ${\bf D}$. By definition, the elements ${\cal P}_{ij}^{\diamond}$ of the matrix ${\bf P}^{\diamond}$ are calculated as

[TABLE]

i.e. ${\cal P}_{ij}^{\diamond}\ (1\leq i,j\leq m)$ is the total probability to move from the tangible state $s_{i}$ to the tangible state $s_{j}$ in any number of steps, without traversal of tangible states, but possibly going through vanishing states.

Let $s,\tilde{s}\in DR_{T}(G)$ such that $s=s_{i},\ \tilde{s}=s_{j}$. The probability to move from $s$ to $\tilde{s}$ in any number of steps, without traversal of tangible states is

[TABLE]

Definition 5.3

Let $G$ be a dynamic expression and $[G]_{\approx}\in DR_{T}(G)$. The reduced discrete time Markov chain (RDTMC) of $G$, denoted by $RDTMC(G)$, has the state space $DR_{T}(G)$, the initial state $[G]_{\approx}$ and the transitions $s\hookrightarrow_{\cal P}\tilde{s}$, where ${\cal P}=PM^{\diamond}(s,\tilde{s})$.

RDTMCs of static expressions can be defined as well. For $E\in RegStatExpr$, let $RDTMC(E)=RDTMC(\overline{E})$.

Let us now try to define $RSMC(G)$ as a “restriction” of $SMC(G)$ to its tangible states. Since the sojourn time in the tangible states of $SMC(G)$ is discrete and geometrically distributed, we can see that $RSMC(G)$ is a DTMC with the state space $DR_{T}(G)$, the initial state $[G]_{\approx}$ and the transitions whose probabilities collect all those in $SMC(G)$ to move from the tangible to the tangible states, directly or indirectly, namely, by going through its vanishing states only. Thus, $RSMC(G)$ has the transitions $s\hookrightarrow_{\cal P}\tilde{s}$, where ${\cal P}=PM^{\diamond}(s,\tilde{s})$, hence, we get $RSMC(G)=RDTMC(G)$.

One can see that $RDTMC(G)$ is constructed from $DTMC(G)$ as follows. All vanishing states and all transitions to, from and between them are removed. All transitions between tangible states are preserved. The probabilities of transitions between tangible states may become greater and new transitions between tangible states may be added, both iff there exist moves between these tangible states in any number of steps, going through vanishing states only. Thus, for each sequence of transitions between two tangible states in $DTMC(G)$ there exists a (possibly shorter, since the eventual passed through vanishing states are removed) sequence between the same states in $RDTMC(G)$ and vice versa. If $DTMC(G)$ is irreducible then all its states (including tangible ones) communicate, hence, all states of $RDTMC(G)$ communicate as well and it is irreducible. Since both $DTMC(G)$ and $RDTMC(G)$ are finite, they are positive recurrent. Thus, in case of irreducibility of $DTMC(G)$, each of them has a single stationary PMF. Note that $DTMC(G)$ and/or $RDTMC(G)$ may be periodic, thus having a unique stationary distribution, but no steady-state (limiting) one. For example, it may happen that $DTMC(G)$ is aperiodic while $RDTMC(G)$ is periodic due to removing vanishing states from the former.

Let $DR_{T}(G)=\{s_{1},\ldots,s_{m}\}$ and $[G]_{\approx}\in DR_{T}(G)$. Then the transient ($k$-step, $k\in I\!\!N$) PMF $\psi^{\diamond}[k]=(\psi^{\diamond}[k](s_{1}),\ldots,\psi^{\diamond}[k](s_{m}))$ for $RDTMC(G)$ is calculated as

[TABLE]

where $\psi^{\diamond}[0]=(\psi^{\diamond}[0](s_{1}),\ldots,\psi^{\diamond}[0](s_{m}))$ is the initial PMF defined as

[TABLE]

Note also that $\psi^{\diamond}[k+1]=\psi^{\diamond}[k]{\bf P}^{\diamond}\ (k\in I\!\!N)$.

The steady-state PMF $\psi^{\diamond}=(\psi^{\diamond}(s_{1}),\ldots,\psi^{\diamond}(s_{m}))$ for $RDTMC(G)$ is a solution of the equation system

[TABLE]

where ${\bf I}$ is the identity matrix of order $m$ and ${\bf 0}$ is a row vector of $m$ values $0,\ {\bf 1}$ is that of $m$ values $1$.

Note that the vector $\psi^{\diamond}$ exists and is unique if $RDTMC(G)$ is ergodic. Then $RDTMC(G)$ has a single steady state, and we have $\psi^{\diamond}=\lim_{k\to\infty}\psi^{\diamond}[k]$.

The zero sojourn time in the vanishing states guarantees that the state changes of $RDTMC(G)$ occur in the moments of the global discrete time associated with $SMC(G)$, i.e. every such state change occurs after one time unit delay. Hence, the sojourn time in the tangible states is the same for $RDTMC(G)$ and $SMC(G)$. The state change probabilities of $RDTMC(G)$ are those to move from tangible to tangible states in any number of steps, without traversal of the tangible states. Therefore, $RDTMC(G)$ and $SMC(G)$ have the same transient behaviour over the tangible states, thus, the transient analysis of $SMC(G)$ is possible to accomplish using $RDTMC(G)$.

The following proposition relates the steady-state PMFs for $SMC(G)$ and $RDTMC(G)$. It proves that the steady-state probabilities of the tangible states coincide for them.

Proposition 5.3

Let $G$ be a dynamic expression, $\varphi$ be the steady-state PMF for $SMC(G)$ and $\psi^{\diamond}$ be the steady-state PMF for $RDTMC(G)$. Then $\forall s\in DR(G)$

[TABLE]

Proof. To make the proof more clear, we use the following unified notation. ${\bf I}$ denotes the identity matrices of any size. ${\bf 0}$ denotes square matrices and row vectors of any size and length of values [math]. ${\bf 1}$ denotes square matrices and row vectors of any size and length of values $1$.

Let ${\bf P}$ be the reordered TPM for $DTMC(G)$ and $\psi$ be the steady-state PMF for $DTMC(G)$, i.e. $\psi$ is a solution of the equation system

[TABLE]

Let $|DR(G)|=n$ and $|DR_{T}(G)|=m$. The decomposed ${\bf P},\ {\bf P}-{\bf I}$ and $\psi$ are

[TABLE]

where $\psi_{V}=(\psi_{1},\ldots,\psi_{n-m})$ is the subvector of $\psi$ with the steady-state probabilities of vanishing states and $\psi_{T}=(\psi_{n-m+1},\ldots,\psi_{n})$ is that with the steady-state probabilities of tangible states.

Then the equation system for $\psi$ is decomposed as follows:

[TABLE]

Further, let ${\bf P}^{\diamond}$ be the TPM for $RDTMC(G)$. Then $\psi^{\diamond}$ is a solution of the equation system

[TABLE]

We have

[TABLE]

where the matrix ${\bf G}$ can have two different forms, depending on whether the loops among vanishing states exist, hence, we consider the two following cases.

There exist no loops among vanishing states. We have $\exists l\in I\!\!N\ \forall k>l\ {\bf C}^{k}={\bf 0}$ and ${\bf G}=\sum_{k=0}^{l}{\bf C}^{k}$.

Let us right-multiply the first equation of the decomposed equation system for $\psi$ by ${\bf G}$:

[TABLE]

Taking into account that ${\bf G}=\sum_{k=0}^{l}{\bf C}^{k}$, we get

[TABLE]

Since ${\bf C}^{0}={\bf I}$ and ${\bf C}^{l+1}={\bf 0}$, we obtain

[TABLE]

Let us substitute $\psi_{V}$ with $\psi_{T}{\bf E}{\bf G}$ in the second equation of the decomposed equation system for $\psi$:

[TABLE]

Since ${\bf F}+{\bf E}{\bf G}{\bf D}={\bf P}^{\diamond}$, we have

[TABLE] 2. 2.

There exist loops among vanishing states. We have $\lim_{\to\infty}{\bf C}^{k}={\bf 0}$ and ${\bf G}=({\bf I}-{\bf C})^{-1}$.

Let us right-multiply the first equation of the decomposed equation system for $\psi$ by ${\bf G}$:

[TABLE]

Taking into account that ${\bf G}=({\bf I}-{\bf C})^{-1}$, we get

[TABLE]

Let us substitute $\psi_{V}$ with $\psi_{T}{\bf E}{\bf G}$ in the second equation of the decomposed equation system for $\psi$:

[TABLE]

Since ${\bf F}+{\bf E}{\bf G}{\bf D}={\bf P}^{\diamond}$, we have

[TABLE]

The third equation $\psi_{V}{\bf 1}^{T}+\psi_{T}{\bf 1}^{T}=1$ of the decomposed equation system for $\psi$ implies that if $\psi_{V}$ has nonzero elements then the sum of the elements of $\psi_{T}$ is less than one. We normalize $\psi_{T}$ by dividing its elements by their sum:

[TABLE]

It is easy to check that $v$ is a solution of the equation system

[TABLE]

hence, it is the steady-state PMF for $RDTMC(G)$ and we have

[TABLE]

Note that $\forall s\in DR_{T}(G)\ \psi_{T}(s)=\psi(s)$. Then the elements of $\psi^{\diamond}$ are calculated as follows: $\forall s\in DR_{T}(G)$

[TABLE]

By Proposition 5.2, $\forall s\in DR_{T}(G)\ \varphi(s)=\frac{\psi(s)}{\sum_{\tilde{s}\in DR_{T}(G)}\psi(\tilde{s})}$.

Therefore, $\forall s\in DR_{T}(G)$

[TABLE]

$\sqcap\!\!\!\!\sqcup$

Thus, to calculate $\varphi$, one can just take all the elements of $\psi^{\diamond}$ as the steady-state probabilities of the tangible states, instead of abstracting from self-loops to get ${\bf P}^{*}$ and then $\psi^{*}$, followed by weighting by $SJ$ and normalization. Hence, using $RDTMC(G)$ instead of $EDTMC(G)$ allows one to avoid such a multistage analysis, but constructing ${\bf P}^{\diamond}$ also requires some efforts, including calculating matrix powers or inverse matrices. Note that $RDTMC(G)$ has self-loops, unlike $EDTMC(G)$, hence, the behaviour of $RDTMC(G)$ may stabilize slower than that of $EDTMC(G)$ (if each of them has a single steady state). On the other hand, ${\bf P}^{\diamond}$ is smaller and denser matrix than ${\bf P}^{*}$, since ${\bf P}^{\diamond}$ has additional non-zero elements not only at the main diagonal, but also many of them outside it. Therefore, in most cases, we have less time-consuming numerical calculation of $\psi^{\diamond}$ with respect to $\psi^{*}$. At the same time, the complexity of the analytical calculation of $\psi^{\diamond}$ with respect to $\psi^{*}$ depends on the model structure, such as the number of vanishing states and loops among them, but usually it is lower, since the matrix size reduction plays an important role in many cases. Hence, for the system models with many immediate activities we normally have a significant simplification of the solution. At the abstraction level of SMCs, the elimination of vanishing states decreases their impact to the solution complexity while allowing immediate activities to specify a comprehensible logical structure of systems at the higher level of transition systems.

Example 5.5

Let $E$ be from Example 3.19. Remember that $DR_{T}(\overline{E})=DR_{ST}(\overline{E})\cup DR_{WT}(\overline{E})=\{s_{1},s_{2},s_{4},s_{5}\}$ and $DR_{V}(\overline{E})=\{s_{3}\}$. We reorder the states from $DR(\overline{E})$, by moving the vanishing states to the first positions, as follows: $s_{3},s_{1},s_{2},s_{4},s_{5}$.

The reordered TPM for $DTMC(\overline{E})$ is

[TABLE]

The result of the decomposing ${\bf P}_{r}$ are the matrices

[TABLE]

Since ${\bf C}^{1}={\bf 0}$, we have $\forall k>0\ {\bf C}^{k}={\bf 0}$, hence, $l=0$ and there are no loops among vanishing states. Then

[TABLE]

Further, the TPM for $RDTMC(\overline{E})$ is

[TABLE]

In Figure 29, the reduced DTMC $RDTMC(\overline{E})$ is presented. The steady-state PMF for $RDTMC(\overline{E})$ is

[TABLE]

Note that $\psi^{\diamond}=(\psi^{\diamond}(s_{1}),\psi^{\diamond}(s_{2}),\psi^{\diamond}(s_{4}),\psi^{\diamond}(s_{5}))$. By Proposition 5.3, we have

[TABLE]

Thus, the steady-state PMF for $SMC(\overline{E})$ is

[TABLE]

This coincides with the result obtained in Example 5.1 with the use of $\psi^{*}$ and $SJ$.

Example 5.6

In Figure 30, the reduced underlying SMC $RSMC(\overline{E})$ is depicted. The average sojourn times in the states of the reduced underlying SMC are written next to them in bold font. In spite of the equality $RSMC(\overline{E})=RDTMC(\overline{E})$, the graphical representation of $RSMC(\overline{E})$ differs from that of $RDTMC(\overline{E})$, since the former is based on the $REDTMC(\overline{E})$, where each state is decorated with the positive average sojourn time of $RSMC(\overline{E})$ in it. $REDTMC(\overline{E})$ is constructed from $EDTMC(\overline{E})$ in the similar way as $RDTMC(\overline{E})$ is obtained from $DTMC(\overline{E})$. By construction, the residence time in each state of $RSMC(\overline{E})$ is geometrically distributed. Hence, the associated parameter of geometrical distribution is uniquely recovered from the average sojourn time in the state.

Note that our reduction of the underlying SMC by eliminating its vanishing states, resulting in the reduced DTMC, resembles the reduction from [35] by removing instantaneous states of stochastically discontinuous Markov reward chains. The latter are “limits” of continuous time Markov chains with state rewards and fast transitions when the rates (speeds) of these transitions tend to infinity, making them immediate. By analogy with this work, we could consider DTMCs extended with instantaneous states instead of SMCs with geometrically distributed or zero sojourn time in the states. However, within $dtsdPBC$, we have decided to take SMCs as the underlying stochastic process to be able to consider not only geometrically distributed and zero residence time in the states, but arbitrary fixed discrete time delays as well.

6 Conclusion

In this paper, we have proposed a discrete time stochastic extension dtsdPBC of PBC, enriched with deterministic multiactions. The calculus has a parallel step operational semantics, based on labeled probabilistic transition systems and a denotational semantics in terms of a subclass of LDTSDPNs. A technique of performance evaluation in the framework of the calculus has been presented that explores the corresponding stochastic process, which is a semi-Markov chain (SMC). It has been proven that the underlying discrete time Markov chain (DTMC) or its reduction (RDTMC) by eliminating vanishing states may alternatively and suitably be studied for that purpose. The theory presented has been illustrated with an extensive series of examples, among which is the travel system application example demonstrating performance analysis within dtsdPBC.

The advantage of our framework is twofold. First, one can specify in it concurrent composition and synchronization of (multi)actions, whereas this is not possible in classical Markov chains. Second, algebraic formulas represent processes in a more compact way than PNs and allow one to apply syntactic transformations and comparisons. Process algebras are compositional by definition and their operations naturally correspond to operators of programming languages. Hence, it is much easier to construct a complex model in the algebraic setting than in PNs. The complexity of PNs generated for practical models in the literature demonstrates that it is not straightforward to construct such PNs directly from the system specifications. dtsdPBC is well suited for the discrete time applications, whose discrete states change with a global time tick, such as business processes, neural and transportation networks, computer and communication systems, timed web services [60], as well as for those, in which the distributed architecture or the concurrency level should be preserved while modeling and analysis (remember that, in step semantics, we have additional transitions due to concurrent executions). dtsdPBC is also capable to model and analyze parallel systems with fixed durations of the typical activities (loading, processing, transfer, repair) and stochastic durations of the randomly occurring activities (arrival, failure), including industrial, manufacturing, queueing, computing and network systems. The main advantages of dtsdPBC are the flexible multiaction labels, deterministic multiactions, powerful operations, as well as a step operational and a Petri net denotational semantics allowing for concurrent execution of activities (transitions), together with an ability for analytical and parametric performance evaluation.

Future work will consist in constructing a congruence relation for dtsdPBC, i.e. the equivalence that withstands application of all operations of the algebra. The first possible candidate is a stronger version of $\underline{\leftrightarrow}_{ss}$ defined via transition systems equipped with two extra transitions skip and redo, like those from sPBC. Moreover, recursion operation could be added to dtsdPBC to increase further specification power of the algebra.