DES - Definition of 'Stochastic Timed Automata with Poisson Clock Structure'

Stochastic Timed Automata with Poisson Clock Structure:

Given a stochastic timed automata we define it as having a Poisson clock structure if we have that all state holding times $\left\{V(x_1),V(x_2),V(x_3),\dots \right\}$ have a exponential distribution, so that:

$$V(x_i)\sim \mathrm{Exp}\left(\frac{1}{{\lambda }_i}\right)$$

Often you see $V(i)$ instead of $V(x_i)$, but they mean the same thing.

---

~Example: