DES - Theorem 'Distribution of the State Holding Time for a Poisson Clock Structure'

Summary:

We demonstrate that given a Timed Automata with Poisson Clock Structure the vector of all State Holding Time has an exponential distribution, with rate:

$$\sum _{e\in \Gamma (x)}{\lambda }_{e}p(x^{\prime }\mid x,e)\text{for}{x}^{\prime }\ne x$$

Where $p(x^{\prime }\mid x,e)$ is the probability of changing state from state $x$ when event $e$ occurs, and ${\lambda }_e$ is the rate of the exponential distribution that generated event $e$.

And the average state holding time is:

$$E\left[V(i)\right]=\frac{1}{\sum {\lambda }_{e}p(x^{\prime }\mid x,e)}$$

---

Theorem: Distribution of the State Holding Time for a Poisson Clock Structure

We want to compute the distribution of the State Holding Time $V(x)$ for a stochastic timed automaton with Poisson Clock Structure.

Preliminary result: Let $X_1,X_2,\dots ,X_n,X_{n+1}$ be independent, identically distributed random variables with $X_i\sim \mathrm{Exp}\left(\frac{1}{\lambda }\right)$ for all $i=1,2,\dots ,n+1$. Then, for $t>0$ :

$$P\left(X_1+\dots +X_n<t,X_1+\dots +X_n+X_{n+1}>t\right)=\frac{(\lambda t{)}^n}{n!}{e}^{-\lambda t}$$

The preliminary result can be found knowing the result from the Poisson Process and the memory-less property of the exponential distribution.

DES - Demonstration of the State Holding Time for a Poisson Clock Structure

---

~Example:

---