Importance Sampling for Stochastic Timed Automata

Abstract

We present an importance sampling framework that combines symbolic analysis and simulation to estimate the probability of rare reachability properties in stochastic timed automata. By means of symbolic exploration, our framework first identifies states that cannot reach the goal. A state-wise change of measure is then applied on-the-fly during simulations, ensuring that dead ends are never reached. The change of measure is guaranteed by construction to reduce the variance of the estimator with respect to crude Monte Carlo, while experimental results demonstrate that we can achieve substantial computational gains.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Stochastic Timed Automata [7] extend Timed Automata [1] to reason on the stochastic performance of real time systems. Non-deterministic time delays are refined by stochastic choices and discrete non-deterministic choices are refined by probabilistic choices. The semantics of stochastic timed automata is given in terms of nested integrals over products of uniform and exponential distributions. Abstracting from the stochasticity of the model, it is possible to find the symbolic paths reaching a set of goal states, but solving the integrals to calculate the probability of a property becomes rapidly intractable. Using a similar abstraction it is possible to bound the maximum and minimum probabilities of a property, but this can lead to results such as the system could work or fail with high probability. Our goal is to quantify the expectation of rare behaviour with specific distributions.

A series of works [3–5, 7] has developed methods for analysing Stochastic Timed Automata using Statistical Model Checking (SMC) [18]. SMC includes a collection of Monte Carlo techniques that use simulation to avoid “state space explosion” and other intractabilities encountered by model checking. It is typically easy to generate sample executions of a system, while the confidence of estimates increases with the number of independently generated samples. Properties with low probability (rare properties) nevertheless pose a challenge for SMC because the relative error of estimates scales inversely with rarity. A number of standard variance reduction techniques to address this have been known since the early days of simulation [11]. The approach we present here makes use of importance sampling [11, 15], which works by performing Monte Carlo simulations under a probabilistic measure that makes the rare event more likely to occur. An unbiased estimate is achieved by compensating for the change of measure during simulation.

Fig. 1.

A due to timing constraints.

Our model may include rarity arising from explicit Markovian transitions, but our main contribution is addressing the more challenging rarity that results from the intersection of timing constraints and continuous distributions of time. To gain an intuition of the problem, consider the example in Fig. 1. The automaton first chooses a delay uniformly at random in $[0,10^6]$ and then selects to either go to or . Since the edge to is only enabled in the interval $[10^6-1,10^6]$, reaching constitutes a rare event with probability $\int _{10^6-1}^{10^6} 10^{-6}\cdot \frac{1}{2} \mathop {}\!\mathrm {d} t = \frac{1}{2}\cdot 10^{-6}$.

The probability theory relating to our model has been considered in the framework of generalised semi Markov processes, with related work done in the context of queueing networks. Theory can only provide tractable analytical solutions for special cases, however. Of particular relevance to our model, [17] proposes the use of state classes to model stochastic distributions over dense time, but calculations for the closely related Duration Probabilistic Automata [14] do not scale well [12]. Monte Carlo approaches provide an approximative alternative to analysis, but incur the problem of rare events. Researchers have thus turned to importance sampling. In [19] the authors consider rare event verification of a model of stochastic hybrid automata that shares a number of features in common with our own model. They suggest using the cross-entropy method [16] to refine a parametrised change of measure for importance sampling, but do not provide a means by which this can be applied to arbitrary hybrid systems.

Our contribution is an automated importance sampling framework that is integrated into Uppaal SMC and applicable to arbitrary time-divergent priced timed automata [7]. By means of symbolic analysis we first construct an exhaustive zone-based reachability graph of the model and property, thus identifying all “dead end” states that cannot reach a satisfying state. Using this graph we generate simulation traces that always avoid dead ends and satisfy the property, applying importance sampling to compensate estimates for the loss of the dead ends. In each concrete state we integrate over the feasible times of enabled actions to calculate their total probabilities, which we then use to choose an action at random. We then choose a new concrete vector of clock values at random from the feasible times of the chosen action, using the appropriately composed distribution. All simulated traces reach satisfying states, while our change of measure is guaranteed by construction to reduce the variance of estimates with respect to crude Monte Carlo. Our experimental results demonstrate substantial reductions of variance and overall computational effort.

The remainder of the paper is as follows. Sections 2 and 3 provide background: Sect. 2 recalls the basic notions of importance sampling and Sect. 3 describes Stochastic Timed Automata in terms of Stochastic Timed Transition Systems. We explain the basis of our importance sampling technique in Sect. 4 and describe how we realise it for Stochastic Timed Automata in Sect. 5. In Sect. 6 we present experimental results using our prototype implementation in Uppaal SMC and then briefly summarise our achievements and future work in Sect. 7.

2 Variance Reduction

Let F be a probability measure over the measurable set of all possible executions $\omega \in \varOmega$. The expected probability $p_{\varphi }$ of property $\varphi$ is defined by

$$\begin{aligned} p_{\varphi }=\int _{\varOmega }\mathbf {1}_{\varphi }\,\mathrm {d}F, \end{aligned}$$

(1)

where the indicator function $\mathbf {1}_{\varphi }:\varOmega \rightarrow \{0,1\}$ returns 1 iff $\omega$ satisfies $\varphi$. This leads to the standard (“crude”) unbiased Monte Carlo estimator used by SMC:

$$\begin{aligned} p_{\varphi }\approx \frac{1}{N}\sum _{i=1}^{N}\mathbf {1}_\varphi (\omega _i), \end{aligned}$$

(2)

where each $\omega _i\in \varOmega$ is selected at random and distributed according to F, denoted $\omega _i\sim F$. The variance of the random variable sampled in (2) is given by

$$\begin{aligned} \sigma ^2_{ crude }=\int _{\varOmega }(\mathbf {1}_{\varphi }-p_{\varphi })^2\,\mathrm {d}F =\int _{\varOmega }\mathbf {1}_{\varphi }\,\mathrm {d}F-(p_{\varphi })^2 \end{aligned}$$

(3)

The variance of an N-sample average of i.i.d. samples is the variance of a single sample divided by N. Hence the variance of the crude Monte Carlo estimator (2) is $\sigma ^2_{ crude }/N$ and it is possible to obtain more confident estimates of $p_{\varphi }$ by increasing N. However, when $p_{\varphi }\approx 0$, i.e., $\varphi$ is a rare property, standard concentration inequalities require infeasibly large numbers of samples to bound the relative error.

In this work we use importance sampling to reduce the variance of the random variable from which we sample, which then reduces the number of simulations necessary to estimate the probability of rare properties. Referring to the same probability space and property used in (1), importance sampling is based on the integral

$$\begin{aligned} p_{\varphi }=\int _{\varOmega }\mathbf {1}_{\varphi }\frac{\mathrm {d}F}{\mathrm {d}G}\,\mathrm {d}G, \end{aligned}$$

(4)

where G is another probability measure over $\varOmega$ and $\mathrm {d}F/\mathrm {d}G$ is called the likelihood ratio, with $\mathbf {1}_{\varphi }F$ absolutely continuous with respect to G. Informally, this means that $\forall \omega \in \varOmega , \mathrm {d}G(\omega )=0\implies \mathbf {1}_{\varphi }\mathrm {d}F(\omega )=0$. Hence $\mathbf {1}_{\varphi }(\omega )\mathrm {d}F(\omega )/\mathrm {d}G(\omega )>0$ for all realisable paths under F that satisfy $\varphi$ and is equal to 0 otherwise.

The integral (4) leads to the unbiased importance sampling estimator

$$\begin{aligned} p_{\varphi }\approx \frac{1}{N}\sum _{i=1}^{N}\mathbf {1}_\varphi (\omega _i)\frac{\mathrm {d}F(\omega _i)}{\mathrm {d}G(\omega _i)},\quad \omega _i\sim G. \end{aligned}$$

(5)

In practice, a simulation is performed under measure G and if the resulting trace satisfies $\varphi$, its contribution is compensated by the likelihood ratio, which is calculated on the fly. To reduce variance, the intuition is that G is constructed to make traces that satisfy $\varphi$ more likely to occur in simulations.

The variance $\sigma ^2_{ is }$ of the random variable sampled by the importance sampling estimator (4) is given by

$$\begin{aligned} \sigma ^2_ is =\int _\varOmega \left( \mathbf {1}_{\varphi }\frac{\mathrm {d}F}{\mathrm {d}G}-p_{\varphi }\right) ^2\mathrm {d}G =\int _\varOmega \mathbf {1}_{\varphi }\left( \frac{\mathrm {d}F}{\mathrm {d}G}\right) ^2\mathrm {d}G-(p_{\varphi })^2 \end{aligned}$$

(6)

If $F=G$, the likelihood ratio of realisable paths is uniformly equal to 1, (4) reduces to (1) and (6) reduces to (3). To ensure that the variance of (5) is less than the variance of (2) it is necessary to make $\sigma ^2_{ is }<\sigma ^2_{ crude }$, for which it is sufficient to make $\mathrm {d}F/\mathrm {d}G<1,\forall \omega \in \varOmega$.

Lemma 1

Let F, G be probability measures over the measurable space $\varOmega$, let $\mathbf {1}_\varphi : \varOmega \rightarrow \{0,1\}$ be an indicator function and let $\mathbf {1}_\varphi F$ be absolutely continuous with respect to G. If for all $\omega \in \varOmega$, $\mathbf {1}_\varphi (\omega )\cdot \frac{\mathop {}\!\mathrm {d} F(\omega )}{\mathop {}\!\mathrm {d} G(\omega )} \le 1$ then $\sigma _{is}^2 \le \sigma _{crude}^2$.

Proof

From the definitions of $\sigma ^2_{ crude }$ (3) and $\sigma ^2_ is$ (6), we have

$$ \sigma ^2_ is \le \sigma _{ crude }^2 \Longleftrightarrow \int _{\varOmega } \mathbf {1}_{\varphi }\left( \frac{\mathop {}\!\mathrm {d} F}{\mathop {}\!\mathrm {d} G}\right) ^2\mathop {}\!\mathrm {d} G - (p_\varphi )^2 \le \int _{\varOmega } \mathbf {1}_{\varphi }\mathop {}\!\mathrm {d} F - (p_\varphi )^2, $$

where $p_\varphi$ is the expectation of $\mathbf {1}_\varphi F$. Noting that $(p_\varphi )^2$ is outside the integrals and common to both sides of the inequality, we conclude

$$ \sigma ^2_{ is }\le \sigma _{ crude }^2 \Longleftrightarrow \int _{\varOmega }\mathbf {1}_{\varphi }\frac{\mathop {}\!\mathrm {d} F}{\mathop {}\!\mathrm {d} G} \mathop {}\!\mathrm {d} F \le \int _{\varOmega }\mathbf {1}_{\varphi }\mathop {}\!\mathrm {d} F. $$

Hence, given $\mathbf {1}_\varphi \in \{0,1\}$, to ensure $\sigma ^2_{ is }\le \sigma ^2_{ crude }$ it is sufficient that $\mathbf {1}_\varphi (\omega )\cdot \frac{\mathop {}\!\mathrm {d} F(\omega )}{\mathop {}\!\mathrm {d} G(\omega )}\le 1,\forall \omega \in \varOmega$.

3 Timed Systems

The modelling formalism we consider in this paper is a stochastic extension of Timed Automata [1] in which non-deterministic time delays are refined by stochastic choices and non-deterministic discrete choices are refined by probabilistic choices. Let $\varSigma _{}= \varSigma _{!}^{}\cup \varSigma _{?}^{}$ be a set of actions split into output ($\varSigma _{!}^{}$) and input ($\varSigma _{?}^{}$). As usual we assume there is a one-to-one-mapping between input actions and output actions. We adopt the scheme that $a!$ is an output action and $a?$ is the corresponding input action.

Definition 1 (Timed Transition System)

A timed transition system over actions $\varSigma _{}$ split into input actions $\varSigma _{?}^{}$ and output actions $\varSigma _{!}^{}$ is a tuple $\mathcal {L}_{}= (S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{})$ where 1) $S_{}$ is a set of states, 2) $s_{}^0$ is the initial state, 3) $\rightarrow \subseteq S_{}\times (\varSigma _{}\cup \mathbb {R}_{\ge 0})\times S_{}$ is the transition relation, 4) $\text {AP}_{}$ is a set of propositions and 5) $P_{} : S_{}\rightarrow 2^{\text {AP}_{}}$ maps states to propositions.    $\square$

For shorthand we write $s_{}\xrightarrow {a}s_{}'$ whenever $(s_{},a,s_{}')\in \rightarrow$. Following the compositional framework laid out by David et al. [6] we expect timed transition systems to be action-deterministic i.e. if $s_{}\xrightarrow {a}s_{}'$ and $s_{}\xrightarrow {a}s_{}''$ then $s_{}'=s_{}''$ and we expect them to be input-enabled meaning for all input actions $a?\in \varSigma _{?}^{}$ and all states $s_{}$ there exists $s_{}'$ such that $s_{}\xrightarrow {a?}s_{}'$. Let $s_{},s_{}'\in S_{}$ be two states then we write $s_{}\rightarrow ^*s_{}'$ if there exists a sequence of transitions such that $s_{}'$ is reachable and we write $s_{}\not \rightarrow ^*s_{}'$ if $s_{}'$ is not reachable from $s_{}$. Generalising this to a set of states $\mathtt {G}\subseteq S_{}$, we write $s_{}\rightarrow ^*\mathtt {G}$ if there exists $s_{}'\in \mathtt {G}$ such that $s_{}\rightarrow ^*s_{}'$ and $s_{}\not \rightarrow ^*\mathtt {G}$ if for all $s_{}'\in \mathtt {G}$, $s_{}\not \rightarrow ^*s_{}'$.

A run over a timed transition system $\mathcal {L}_{}= (S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{})$ is an alternating sequence of states, reals and output actions, $s_{0} d_0a_0! s_{1} d_1 a_1! \dots$ such that $s_{i}\xrightarrow {d_i}\xrightarrow {a_i!}s_{i+1}$. We denote by $\varOmega (\mathcal {L}_{})$ the entire set of runs over $\mathcal {L}_{}$. The set of propositional runs is the set $\varOmega ^{\text {AP}_{}}(\mathcal {L}_{}) = \{ P_{}(s_{0})d_0, \dots | s_{0}d_0a_0!\in \varOmega (\mathcal {L}_{})\}$.

Several Timed Transition Systems $\mathcal {L}_{1}\dots \mathcal {L}_{n}$, $\mathcal {L}_{i}= (S_{i},s_{i}^0,\rightarrow _{i},\text {AP}_{i},P_{i})$, may be composed in the usual manner. We denote this by $\mathcal {L}_{}= \mathcal {L}_{1}|\mathcal {L}_{2}|\dots |\mathcal {L}_{n}$ and for a state ${\varvec{s}}=(s_{1},s_{2},\dots ,s_{n})$ of $\mathcal {L}_{}$ we let ${\varvec{s}}[i] = s_{i}$.

Timed Automata. Let ${X}$ be a finite set of variables called clocks. A valuation over a set of clocks is a function $v: {X}\rightarrow \mathbb {R}_{\ge 0}$ assigning a value to each clock. We denote by $V({X})$ all valuations over ${X}$. Let $v\in V({X})$ and ${Y}\subseteq {X}$ then we denote by $v [{Y}]$ the valuation assigning 0 whenever $x\in {Y}$ and $v(x)$ whenever $x\notin {Y}$. For a value $d\in \mathbb {R}_{\ge 0}$ we let $(v+d)$ be the valuation assigning $v(x)+d$ for all $x\in {X}$. An upper bound (lower bound) over a set of clocks is an element $x\triangleleft n$ ($x\triangleright n$) where $x\in {X}$, $n\in \mathbb {N}$ and $\triangleleft \in \{<,\le \}$ ($\triangleright \in \{>,\ge \}$). We denote the set of finite conjunctions of upper bounds (lower bounds) over ${X}$ by $\mathcal {B}^{\triangleleft }({X})$ ($\mathcal {B}^{\triangleright }({X})$) and the set of finite conjunctions over upper and lower bounds by $\mathcal {B}({X})$. We write $v\,\models \,g$ whenever $v\in V({X})$ satisfies an element $g\in \mathcal {B}({X})$. We let $v_{0}\in V({X})$ be the valuation that assigns zero to all clocks.

Definition 2

A Timed Automaton over output actions $\varSigma _{!}^{}$ and input actions $\varSigma _{?}^{}$ is a tuple $({L},\ell _{0},{X},E,\text {Inv})$ where 1) ${L}$ is a set of control locations, 2) $\ell _{0}$ is the initial location, 3) ${X}$ is a finite set of clocks, 4) $E\subseteq {L}\times \mathcal {B}^{\triangleright }({X})\times (\varSigma _{!}^{}\cup \varSigma _{?}^{})\times 2^{X}\times {L}$ is a finite set of edges 5) $\text {Inv}: {L}\rightarrow \mathcal {B}^{\triangleleft }({X})$ assigns an invariant to locations.    $\square$

The semantics of a timed automaton $\mathcal {A}_{}= ({L},\ell _{0},{X},E,\text {Inv})$ is a timed transition system $\mathcal {L}_{}= (S_{},s_{}^0,\rightarrow _{},{L},P_{})$ where 1) $S_{}= {L}\times V({X})$, 2) $s_{}^0= (\ell _{0},v_{0})$, 3) $(\ell _{},v) \xrightarrow {d}(\ell _{},(v+d))$ if $(v+d)\,\models \,\text {Inv}(\ell _{})$, 4) $(\ell _{},v) \xrightarrow {a} (\ell _{}',v')$ if there exists $(\ell _{},g,a,r,\ell _{}')\in E$ such that $v\,\models \,g$, $v'=v [r]$ and $v'\,\models \,\text {Inv}(\ell _{}')$ and 5) $P_{} ((\ell _{},v)) = \{\ell _{}\}$.

3.1 Stochastic Timed Transition System

A stochastic timed transition system (STTS) is a pair $(\mathcal {L}_{},\nu _{})$ where $\mathcal {L}_{}$ is a timed transition system defining allowed behaviour and $\nu _{}$ gives for each state a density-function, that assigns densities to possible successors. Hereby some behaviours may, in theory, be possible for $\mathcal {L}_{}$ but rendered improbable by $\nu _{}$.

Definition 3 (Stochastic Timed Transition System)

Let $\mathcal {L}_{}\!=\! (S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{})$ be a timed transition system with output actions $\varSigma _{!}^{}$ and input actions $\varSigma _{?}^{}$. A stochastic timed transition system over $\mathcal {L}_{}$ is a tuple $(\mathcal {L}_{},\nu _{})$ where $\nu _{}: S_{}\rightarrow \mathbb {R}_{\ge 0}\times \varSigma _{!}^{}\rightarrow \mathbb {R}_{\ge 0}$ assigns a joint-delay-action density where for all states $s_{}\in S_{}$, (1) $\sum _{a!\in \varSigma _{!}^{}} (\int _{\mathbb {R}_{\ge 0}} \nu _{}(s_{})(t,a!)\mathop {}\!\mathrm {d} t )= 1$ and (2) $\nu _{}(s_{})(t,a!) \ne 0$ implies $s_{}\xrightarrow {t}\xrightarrow {a!}$.    $\square$

(1) captures that $\nu _{}$ is a probability density and (2) demands that if $\nu _{}$ assigns a non-zero density to a delay-action pair then the underlying timed transition system should be able to perform that pair. Note that (2) is not a bi-implication, reflecting that $\nu _{}$ is allowed to exclude possible successors of $\mathcal {L}_{}$.

Forming the core of a stochastic semantics for a stochastic timed transition system $\mathcal {T}_{}= ((S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{}),\nu _{})$, let $\pi = p_{0} I_0 p_{1} I_1 p_{2} \dots I_{n-1} p_{n}$ be a cylinder construction where for all i, $I_i$ is an interval with rational end points and $p_{i}\subseteq \text {AP}_{}$. For a finite run $\omega = p_{1}' d_1 p_{2}' \dots d_{n-1} p_{n}$ we write $\omega \,\models \,\pi$ if for all i, $d_i\in I_i$ and $p_{i}' = p_{i}$. The set of runs within $\pi$ is then $C(\pi ) = \{\omega \omega ' \in \varOmega ^{\text {AP}_{}}(\mathcal {T}_{}) \mid \omega \,\models \,\pi \}.$

Using the joint density, we define the measure of runs in $C(\pi )$ from $s_{}$ recursively:

$$ F_{s_{}}(\pi ) = (p_{0} = P_{}(s_{}))\cdot \int _{t\in I_0}\sum _{a!\in \varSigma _{!}^{}}\left( \nu _{}(s_{})(t,a!)\cdot F_{[[s_{}]^{d}]^{a!}}(\pi ^1)\right) \mathop {}\!\mathrm {d} t, $$

where $\pi ^1$ = $p_{1}I_1\dots p_{n-1}p_{n}$, base case $F_{s_{}}(p_{}) = (P_{\mathcal {T}_{}}(s_{})=(p_{}))$ and $[s_{}]^{a}$ is the uniquely defined $s_{}'$ such that $s_{}\xrightarrow {a}s_{}'$. With the cylinder construction above and the probability measure $F$, the set of runs reaching a certain proposition $p_{}$ within a time limit t, denoted as $\Diamond _{\le t}\,p_{}$, is measurable.

Fig. 2.

Two stochastic timed automata.

Stochastic Timed Automata (STA). Following [7], we associate to each state, $s_{}$, of timed automaton $\mathcal {A}_{}= ({L},\ell _{0},{X},E,\text {Inv})$ a delay density $\delta _{}$ and a probability mass function $\gamma _{}$ that assigns a probability to output actions. The delay density is either a uniform distribution between the minimal delay ($d_{min}$) before a guard is satisfied and maximal delay ($d_{max}$) while the invariant is still satisfied, or an exponential distribution shifts $d_{min}$ time units in case no invariant exists. The $\gamma _{}$ function is a simple discrete uniform choice of all possible actions. Formally, let $d_{min}(s_{}) = \min \{d | s_{}\xrightarrow {d}\xrightarrow {a!} \text { for some } a! \}$ and $d_{max}(s_{}) = \sup \{d | s_{}\xrightarrow {d} \}$ then $\delta _{}(s_{})(t) = \frac{1}{d_{max}(s_{})-d_{min}(s_{})}$ if $d_{max}(s_{}) \ne \infty$ and $\delta _{}(s_{})(t) = \lambda \cdot e^{-\lambda (t-d_{min}(s_{})}$, for a user specified $\lambda$, if $d_{max}(s_{}) = \infty$. Regarding output actions, let $\mathtt {Act}(s_{}) = \{a! | s_{}\xrightarrow {a!}\}$, then $\gamma _{}(s_{})(a!) = \frac{1}{|\mathtt {Act}|}$ for $a!\in \mathtt {Act}$. With $\delta _{}$ and $\gamma _{}$ at hand we define the stochastic timed transition system for $\mathcal {A}_{}$ with underlying timed transition system $\mathcal {L}_{}$ as $\mathcal {T}_{}^{\mathcal {A}_{}}=(\mathcal {L}_{},\delta _{}\bullet \gamma _{})$, where $\delta _{}\bullet \gamma _{}$ is a composed joint-delay-density function and $(\delta _{}\bullet \gamma _{})(s_{})(t,a!) = \delta _{}(s_{})(t)\cdot \gamma _{}([s_{}]^{t})(a!)$. Notice that for any t, $\sum _{a!\in \varSigma _{!}^{}}\nu _{}(s_{})(t,a!) = \delta _{}(s_{})(t)$. In the remainder we will often write a stochastic timed transition as $(\mathcal {L}_{},\delta _{}\bullet \gamma _{})$. Also we will write $\gamma _{}(s_{})(t)(a!)$ in lieu of $\gamma _{}([s_{}]^{t})(a!)$.

Example 1

Consider Fig. 2 and the definition of and in the initial state . By definition we have for $t\in [90,100]$ and for $t\in [90,100]$. Similarly for the component in the state we have if $t\in [0,100]$ and zero otherwise and if $t\in [0,100]$ and zero otherwise.

3.2 Composition of Stochastic Timed Transitions Systems

Following [7], the semantics of STTS is race based, in the sense that each component first chooses a delay, then the component with the smallest delay wins the race and finally selects an output to perform. For the remainder we fix $\mathcal {T}_{i} = (\mathcal {L}_{i},\nu _{i})$ where $\mathcal {L}_{i} = (S_{i},s_{i}^0,\rightarrow _{i},\text {AP}_{i},P_{i})$ is over the output actions $\varSigma _{!}^{i}$ and the common input actions $\varSigma _{?}^{}$.

Definition 4

Let $\mathcal {T}_{1},\mathcal {T}_{2},\dots ,\mathcal {T}_{n}$ be stochastic timed transition systems with disjoint output actions. The composition of these is a stochastic timed transition system $\mathcal {J}= (\mathcal {L}_{1}|\mathcal {L}_{2}|\dots |\mathcal {L}_{n},\nu _{})$ where

$$\nu _{}({\varvec{s}})(t,a!) = \nu _{k}({\varvec{s}}[k])(t,a!)\cdot \prod _{j\ne k} \left( \int _{\tau >t}\sum _{b!\in \varSigma _{!}^{j}}\nu _{j}({\varvec{s}}[j])(\tau ,b!)\mathop {}\!\mathrm {d} \tau \right) \text { for } a!\in \varSigma _{!}^{k}. $$

The race based semantics is apparent from $\nu _{}$ in Definition 4, where the $k^{th}$ component chooses a delay t and action $a!$ and each of the other components independently select a $\tau > t$ and an output action $b!$. For a composition of Stochastic Timed Automata we abstract from the losing components’ output actions and just integrate over $\delta _{}$, as the following shows. Let $\mathcal {J}= (\mathcal {L}_{},\nu _{})$ be a composition of stochastic timed transition systems, $\mathcal {T}_{1},\mathcal {T}_{2},\dots ,\mathcal {T}_{n}$, and let for all i, $\mathcal {T}_{i} = (\mathcal {L}_{i},\delta _{i}\bullet \gamma _{i})$ originate from a timed automaton. Let $a!\in \varSigma _{!}^{k}$, then $\nu _{}({\varvec{s}})(t,a!)$ is given by

$$\begin{aligned}&\delta _{k}({\varvec{s}}[k])(t)\cdot \gamma _{k}(s_{k})(t)(a!)\cdot \prod _{j\ne k} \left( \int _{\tau>t}\sum _{b!\in \varSigma _{!}^{j}}\delta _{j}({\varvec{s}}[j])(\tau )\gamma _{j}({\varvec{s}}[j])(\tau )(b!)\mathop {}\!\mathrm {d} \tau \right) \\ =\,&\delta _{k}({\varvec{s}}[k])(t)\cdot \prod _{j\ne k} \left( \int _{\tau >t}\delta _{j}({\varvec{s}}[j])(\tau )\mathop {}\!\mathrm {d} \tau \right) \cdot \gamma _{k}({\varvec{s}}[k])(t)(a!). \end{aligned}$$

The term $\delta _{k}({\varvec{s}}[k])(t)\cdot \prod _{j\ne k} \left( \int _{\tau >t}\delta _{j}({\varvec{s}}[j])(\tau )\mathop {}\!\mathrm {d} \tau \right)$ is essentially the density of the $k^{th}$ component winning the race with a delay of t. In the sequel we let $\kappa ^{\delta _{}}_{k}(t) = \delta _{k}({\varvec{s}}[k])(t)\cdot \prod _{j\ne k} \left( \int _{\tau >t}\delta _{j}({\varvec{s}}[j])(\tau )\mathop {}\!\mathrm {d} \tau \right)$.

Example 2

Returning to our running example of Fig. 2, we consider the joint-delay density of the composition in the initial state , where and . Applying the definition of composition we see that

4 Variance Reduction for STTS

For a stochastic timed transition system $\mathcal {T}_{}= ((S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{\mathcal {L}_{}}),\nu _{})$ and a set of goal states $\mathtt {G}\subseteq S_{}$ we split the state space into dead ends ($\frown _{\mathtt {G}}$) and good ends ($\smile _{\mathtt {G}}$) i.e. states that can never reach $\mathtt {G}$ and those that can. Formally,

$$\frown _{\mathtt {G}} = \{s_{}\in S_{}\mid s_{}\not \rightarrow ^*\mathtt {G}\} \text { and } \smile _{\mathtt {G}} = \{s_{}\in S_{}\mid s_{}\rightarrow ^*\mathtt {G}\}.$$

For a state $s_{}$, let $\mathtt {Act}_{\mathtt {G},t}(s_{}) = \{ a! \mid [[s_{}]^{t}]^{a!} \in \smile _{\mathtt {G}}\}$ and $\mathtt {Del}_{F}(s_{}) = \{d \mid [s_{}]^{d}\in \smile _{\mathtt {G}} \wedge \mathtt {Act}_{\mathtt {G},d}(s_{}) \ne \emptyset \}$. Informally, $\mathtt {Act}_{\mathtt {G},t}(s_{})$ extracts all the output actions that after a delay of t will ensure having a chance to reach $\mathtt {G}$. Similarly, $\mathtt {Del}_{\mathtt {G}}(s_{})$ finds all the possible delays after which an action can be performed that ensures staying in good ends.

Definition 5 (Dead End Avoidance)

For a stochastic timed transition system $\mathcal {T}_{}= ((S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{}),\nu _{})$ and goal states $\mathtt {G}$, we define an alternative dead end-avoiding stochastic timed transition system as any stochastic timed transition system $\acute{\mathcal {T}}_{}= ((S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{}),{\acute{\nu _{}}})$ where if ${\acute{\nu _{}}} (s_{})(t,a!) \ne 0$ then $a!\in \mathtt {Act}_{\mathtt {G},t}(s_{})$.    $\square$

Recall from Lemma 1 in Sect. 2 that in order to guarantee a variance reduction, the likelihood ratio should be less than 1. Let $\mathcal {T}_{}= ((S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{\mathcal {L}_{}}),\nu _{})$ be a stochastic timed transition system, let $\mathtt {G}\subseteq S_{}$ be a set of goal states and let $\acute{\mathcal {T}}_{}= ((S_{},s_{}^0,\rightarrow ,\text {AP}_{},P_{\mathcal {L}_{}}),\acute{\nu _{}})$ be a dead end-avoiding alternative. Let $\omega = s_{0},d_0,a_0!s_{1},\dots d_{n-1}a_{n-1}!s_{n}$ be a time bounded run, then the likelihood ratio of $\omega$ sampled under $\acute{\mathcal {T}}_{}$ is

$$ \frac{\mathop {}\!\mathrm {d} \mathcal {T}_{}(\omega )}{\mathop {}\!\mathrm {d} \acute{\mathcal {T}}_{}(\omega )} = \frac{\nu _{}(s_{0})(d_0,a_0!)}{\acute{\nu _{}}(s_{0})(d_0,a_0!)}\cdot \frac{\nu _{}(s_{1})(d_1,a_1!)}{\acute{\nu _{}}(s_{1})(d_1,a_1!)}\dots \frac{\nu _{}(s_{n-1})(d_{n-1},a_{n-1}!)}{\acute{\nu _{}}(s_{n-1})(d_{n-1},a_{n-1}!)} $$

Clearly, if for all i, $\nu _{}(s_{i})(d_i,a_i!) \le \acute{\nu _{}}(s_{i})(d_i,a_i!)$ then $\frac{\mathop {}\!\mathrm {d} \mathcal {T}_{}(\omega )}{\mathop {}\!\mathrm {d} \acute{\mathcal {T}}_{}(\omega )}\le 1$. For a stochastic timed transition system $(\mathcal {L}_{},\nu _{}= \delta _{}\bullet \gamma _{})$ originating from a stochastic timed automaton we achieve this by proportionalising $\delta _{}$ and $\gamma _{}$ with respect to good ends, i.e. we use $\tilde{\upsilon }_{}= \tilde{\delta }_{}\bullet \tilde{\gamma }_{}$ where

$$ \tilde{\delta }_{}(s_{})(t) = \frac{\delta _{}(s_{})(t)}{\int _{\mathtt {Del}_{\mathtt {G}}(s_{})} \delta _{}(s_{})(\tau )\mathop {}\!\mathrm {d} \tau } \text{ and } \tilde{\gamma }_{}(s_{})(t)(a!) = \frac{\gamma _{}(s_{})(t)(a!)}{\sum _{b!\in \mathtt {Act}_{\mathtt {G},t}(s_{})} \gamma _{}(s_{})(t)(b!)}. $$

Lemma 2

Let $\mathcal {T}_{}= (\mathcal {L}_{},\nu _{}= \delta _{}\bullet \gamma _{})$ be a stochastic timed transition system from a stochastic timed automata, let $\mathtt {G}$ be a set of goal states and let $\tilde{\mathcal {T}_{}} = (\mathcal {L}_{},\tilde{\upsilon }_{})$ be a dead end avoiding alternative where $\tilde{\upsilon }_{}(s_{})(t,a!) = \tilde{\delta }_{}(s_{})(t) \bullet \tilde{\gamma }_{}(s_{})(t)(a!)$. Also, let $\mathbf {1}_\mathtt {G}$ be an indicator function for $\mathtt {G}$. Then for any finite $\omega \in \varOmega (\mathcal {T}_{})$, $\mathbf {1}_\mathtt {G}(\omega )\cdot \frac{\mathop {}\!\mathrm {d} \mathcal {T}_{}(\omega )}{\mathop {}\!\mathrm {d} \tilde{\mathcal {T}_{}}(\omega )} \le 1$    $\square$

For a composition, $\mathcal {J}= (\mathcal {L}_{},\nu _{})$ of stochastic timed transition systems $\mathcal {T}_{1},\mathcal {T}_{2},\dots ,\mathcal {T}_{n}$ where for all i, $\mathcal {T}_{i} = (\mathcal {L}_{i},\delta _{i}\bullet \gamma _{i})$, we define a dead end avoiding stochastic timed transition system for $\mathtt {G}$ as $\acute{\mathcal {T}}_{}= (\mathcal {L}_{},\tilde{\upsilon }^{*}_{})$ where

$$ \tilde{\upsilon }^{*}_{}({\varvec{s}})(t,a!) = {\left\{ \begin{array}{ll} 0 &{}\text { if } t\notin \mathtt {Del}_{\mathtt {G},k}({\varvec{s}}) \\ \frac{\kappa ^{\delta _{}}_{k}({\varvec{s}}[k])(t)}{\sum _{i=1}^n (\int _{t'\in \mathtt {Del}_{\mathtt {G},i}({\varvec{s}})}\kappa ^{\delta _{}}_{i}({\varvec{s}}[i])(t')\mathop {}\!\mathrm {d} t')} \cdot \kappa ^{\gamma _{}}_{k}({\varvec{s}}[k])(t,a!) &{} \text{ otherwise } \end{array}\right. } $$

where $\mathtt {Del}_{\mathtt {G},k}({\varvec{s}}) = \{ d \mid (\mathtt {Act}_{\mathtt {G},d}({\varvec{s}}))\cap \varSigma _{!}^{k} \ne \emptyset \}$ and

$$ \kappa ^{\gamma _{}}_{k}({\varvec{s}}[k])(t,a!) = {\left\{ \begin{array}{ll} \frac{\gamma _{k}({\varvec{s}}[k])(t)(a!)}{\sum _{b!\in (\mathtt {Act}_{\mathtt {G},t}({\varvec{s}})\cap \varSigma _{!}^{k})}\gamma _{k}({\varvec{s}}[k])(t)(b!)} &{} \text{ if } a! \in \mathtt {Act}_{\mathtt {G},t}({\varvec{s}})\cap \varSigma _{!}^{k} \\ 0 &{}\text { otherwise } \end{array}\right. } $$

First the density of the $k^{th}$ component winning ($\kappa ^{\delta _{}}_{k}$) is proportionalised with respect to all components winning delays. Afterwards, the probability mass of the actions leading to good ends for the $k^{th}$ component is proportionalised as well ($\kappa ^{\gamma _{}}_{k}$).

Lemma 3

Let $\mathcal {J}= (\mathcal {L}_{},\nu _{})$ be a stochastic timed transition system for a composition of stochastic timed transitions $\mathcal {T}_{1},\mathcal {T}_{2},\dots ,\mathcal {T}_{n}$, where for all i, $\mathcal {T}_{i} = (\mathcal {L}_{i},\delta _{i}\bullet \gamma _{i})$ originates from a stochastic timed automaton. Let $\mathtt {G}$ be a set of goal states and let $\acute{\mathcal {J}}= (\mathcal {L}_{},\tilde{\upsilon }^{*}_{})$, where $\tilde{\upsilon }^{*}_{}$ is defined as above. Also, let $\mathbf {1}_\mathtt {G}$ be an indicator function for $\mathtt {G}$. Then for any finite $\omega \in \varOmega (\mathcal {J})$, $\mathbf {1}_\mathtt {G}(\omega )\cdot \frac{\mathop {}\!\mathrm {d} \mathcal {J}(\omega )}{\mathop {}\!\mathrm {d} \acute{\mathcal {J}}(\omega )} \le 1$.    $\square$

Example 3

For our running example let us consider as defined above:

5 Realising Proportional Dead End Avoidance for STA

In this section we focus on how to obtain the modified stochastic timed transition $\acute{\mathcal {T}}_{}= (\mathcal {L}_{},\tilde{\upsilon }_{})$ for a stochastic timed transition system $\mathcal {T}_{}= (\mathcal {L}_{},\nu _{})$ originating from a stochastic timed automaton $\mathcal {A}_{}$ and how to realise $\acute{\mathcal {T}}_{}= (\mathcal {L}_{},\tilde{\upsilon }^{*}_{})$ for a composition of stochastic timed automata. In both cases the practical realisation consists of two steps: first the sets $\smile _{\mathtt {G}}$ and $\frown _{\mathtt {G}}$ are located by a modified algorithm of uppaal Tiga [2]. The result of running this algorithm is a reachability graph annotated with what actions to perform in certain states to ensure staying in good ends. On top of this reachability graph the sets $\mathtt {Del}_{\mathtt {G},k}(s_{})$ and $\mathtt {Act}_{\mathtt {G},k}(s_{})$ can be extracted.

5.1 Identifying Good Ends

Let ${X}$ be a set of clocks, a $zone$ is a convex subset of $V({X})$ described by a conjunction of integer bounds on individual clocks and clock differences. We let $\mathcal {Z}_{M}({X})$ denote all sets of zones, where the integers bounds do not exceed M.

For $\mathcal {A}_{}= ({L},\ell _{0},{X},E,\text {Inv})$ we call elements $(\ell _{},Z)$ of ${L}\times \mathcal {Z}_{M}({X})$, where M is the maximal integer occuring in $\mathcal {A}_{}$, for symbolic states and write $(\ell _{},v)\in (\ell _{},Z)$ if $v\in Z$. An element of $2^{\mathcal {Z}_M({X})}$ is called a federation of zones and we denote all federations by $\mathcal {F}_M({X})$. For a valuation $v$ and federation $F$ we write $v\in F$ if there exists a zone $Z\in F$ such that $v\in Z$.

Zones may be effectively represented using Difference Bound Matrices (DBM) [8]. Furthermore, DBMs allow for efficient symbolic exploration of the reachable state space of timed automata as implemented in the tool Uppaal [13]. In particular, a forward symbolic search will result in a finite set $\mathcal{R}$ of symbolic states:

$$\begin{aligned} \mathcal{R} = \{(\ell _{0},Z_0),\ldots ,(\ell _{n},Z_n)\} \end{aligned}$$

(7)

such that whenever $v_i\in Z_i$, then the state $(\ell _{i},v_i)$ is reachable from the initial state $(\ell _{i},v_0)$ (where $v_0(x)=0$ for all clocks x). Dually, for any reachable state $(\ell _{},v)$ there is a zone $Z$ such that $v\in Z$ and $(\ell _{},Z)\in \mathcal{R}$.

To capture the good ends, i.e. the subset of $\mathcal{R}$ which may actually reach a state in the goal-set $\mathtt {G}$, we have implemented a simplified version of the backwards propagation algorithm of uppaal Tiga [2] resulting in a strategy $\mathcal{S}$ “refining” $\mathcal{R}$:

$$\begin{aligned} \mathcal{S} = \{ (\ell _{0},Z_0,F_0,a_0!),\ldots ,(\ell _{k},Z_k,F_k,a_k!)\} \end{aligned}$$

(8)

where $F_i\subseteq Z_i$ and whenever $v_i\in F_i$ then $(\ell _{i},v_i)\xrightarrow {a_i!}\rightarrow ^*\mathtt {G}$. Also, $(\ell _{i},Z_i)\in \mathcal{R}$ whenever $(\ell _{i},Z_i,F_i,a_i!)\in \mathcal{S}$. Thus, the union of the symbolic states $(\ell _{i},F_i)$ appearing in quadruples of $\mathcal{S}$ ¹ identifies exactly the reachable states from which a discrete action $a_i!$ guarantees to enter a good end of the timed automaton (or network). Figure 3 depicts the reachability set $\mathcal{R}$ (grey area) and strategy set $\mathcal{S}$ (blue area) of our running example.

Given the strategy set $\mathcal{S}$ (8) and a state $s_{}=(\ell _{},v)$, the set of possible delays after which an output action $a!$ leads to a good end is given by

$$ \mathtt {Del}_{a!}(s_{}) = \{\,d \,\, |\,\, \exists (\ell _{i},Z_i,F_i,a!)\in \mathcal{S}\, \text { s.t. } [s_{}]^{d}\in F_i) \}. $$

Fig. 3.

Running example reachability set $\mathcal{R}$ (grey) and strategy set $\mathcal{S}$ (blue) for goal . (Color figure online)

For a single stochastic timed automaton $\mathtt {Del}_{\mathtt {G}}(s_{}) =\bigcup _{a!\in \varSigma _{!}^{}}\mathtt {Del}_{a!}(s_{})$ and for a network $\mathtt {Del}_{\mathtt {G},i}({\varvec{s}}) = \bigcup _{a!\in \varSigma _{!}^{i}}\mathtt {Del}_{a!}({\varvec{s}}) .$ Importantly, note that $\mathtt {Del}_{a!}((\ell _{},v))$ – and thus also $\mathtt {Del}_{\mathtt {G}}((\ell _{},v))$ – can be represented as a finite union of disjoint intervals. Given a closed zone $Z$ and a valuation $v$, the Uppaal DBM library² provides functions that return the minimal delay ($d_{min}$) for entering a zone as well as the maximal delay for leaving it again ($d_{max}$). Due to convexity of zones then $\{(v+d) \mid d_{min} \le d \le d_{max}\} \subseteq Z$ and thus the possible delays to stay in $Z$ from $v$ is equal to the interval $[d_{min},d_{max}]$. For the remainder of this paper we write $\{I_1,I_2\dots , I_n\} = \mathtt {Del}_{\mathtt {G}}(s_{})$ where $I_1,I_2\dots I_n$ are the intervals making up $\mathtt {Del}_{\mathtt {G}}(s_{})$.

Extracting the possible actions from a state $s_{}=(\ell _{i},v_i)$ after a delay of d is simply a matter of iterating over all elements $(\ell _{i},Z_i,F_i,a_i!)$ in $\mathcal{S}$ and checking whether $[s_{}]^{d}\in F_i$. Formally, given a state $s_{}=(\ell _{i},v_i)$, $\mathtt {Act}_{\mathtt {G},d}((s)) = \{ a_i!\in \varSigma _{!}^{}\mid \exists (\ell _{i},Z_i,F_i,a_i!)\in \mathcal{S}\,\,\, \text {s.t.}\, [s_{}]^{d}\in F_i \}$.

5.2 On-the-Fly State-Wise Change of Measure

Having found methods for extracting the sets $\mathtt {Act}_{\mathtt {G},d}(s_{})$ and $\mathtt {Del}_{\mathtt {G},k}(s_{})$, we focus on how to perform the state-wise change of measure.

Single Stochastic Timed Automaton. In the following let $\mathcal {A}_{}$ be a timed automaton, $\mathcal {T}_{\mathcal {A}_{}} = (\mathcal {L}_{},\delta _{\mathcal {A}_{}}\bullet \gamma _{\mathcal {A}_{}})$ be its stochastic timed transition system and let $\mathtt {G}$ be the goal states. For a fixed t obtaining samples $\tilde{\gamma }_{\mathcal {A}_{}} (s_{})(t)$ is a straightforward normalised weighted choice. Sampling delays from $\tilde{\delta }_{\mathcal {A}_{}}(s_{})$ requires a bit more work: let $\mathcal {I} = \{I_1,I_2,\dots I_n\}=\mathtt {Del}_{\mathtt {G}}(s_{})$ and let $t\in I_j$, for some j then

$$ \tilde{\delta }_{\mathcal {A}_{}}(s_{})(t) = \frac{\delta _{\mathcal {A}_{}}(s_{})(t)}{\int _{\tau \in \mathtt {Del}_{\mathtt {G}}(s_{})}\delta _{\mathcal {A}_{}}(s_{})(t)\mathop {}\!\mathrm {d} \tau } = \frac{\int _{\tau \in I_j}\delta _{\mathcal {A}_{}}(s_{})(t)\mathop {}\!\mathrm {d} \tau }{\sum _{I\in \mathcal {I}}\int _{\tau \in I}\delta _{\mathcal {A}_{}}(s_{})(\tau )\mathop {}\!\mathrm {d} \tau }\cdot \frac{\delta _{\mathcal {A}_{}}(s_{})(t)}{\int _{\tau \in I_j}\delta _{\mathcal {A}_{}}(s_{})(t)\mathop {}\!\mathrm {d} \tau } .$$

Thus, to sample a delay we first choose an interval–weighted by its probability–and then sample from the conditional probability distribution of being inside that interval. Since $\delta _{\mathcal {A}_{}}(s_{})$ is either an exponential distribution or uniform, integrating over it is easy and sampling from the conditional distribution is straightforward.

Network of Stochastic Timed Automata. In the following let $\mathcal {A}_{1},\mathcal {A}_{2},\dots ,\mathcal {A}_{n}$ be timed automata, $\mathcal {T}_{i} = (\mathcal {L}_{i},\delta _{i}\bullet \gamma _{i})$ be their stochastic timed transition systems and let $\mathcal {J}= (\mathcal {J},\nu _{})$ be their composition. Recall from previously we wish to obtain $\tilde{\upsilon }^{*}_{}({\varvec{s}})(t,a!) = \frac{\kappa ^{\delta _{}}_{k}({\varvec{s}}[k])(t)}{\sum _{i=1}^n (\int _{t'\in \mathtt {Del}_{\mathtt {G},i}({\varvec{s}})}\kappa ^{\delta _{}}_{i}({\varvec{s}}[i])(t')\mathop {}\!\mathrm {d} t')} \cdot \kappa ^{\gamma _{}}_{k}({\varvec{s}}[k])(t,a!)$ for $t\in \mathtt {Del}_{\mathtt {G},k}({\varvec{s}})$. Let $\mathcal {I}^i=\{I_1^i,I_2^i,\dots ,I_k^i\}=\mathtt {Del}_{\mathtt {G},i}({\varvec{s}})$ for all $1 \le i\le n$ and let $t\in I$ for some $I\in \mathcal {I}^w$ then

$$ \tilde{\upsilon }^{*}_{}({\varvec{s}})(t,a!) = \frac{\int _{I}\kappa ^{\delta _{}}_{w}({{\varvec{s}}[w]})(\tau )\mathop {}\!\mathrm {d} \tau }{\sum _{i=1}^n\sum _{I'\in \mathcal {I}^i}\int _{I'}\kappa ^{\delta _{}}_{i}({{\varvec{s}}[i]})(\tau )\mathop {}\!\mathrm {d} \tau }\frac{\kappa ^{\delta _{}}_{w}({\varvec{s}}[w])(t)}{\int _{I}\kappa ^{\delta _{}}_{w}({{\varvec{s}}[w]})(\tau )\mathop {}\!\mathrm {d} \tau } \cdot \kappa ^{\gamma _{}}_{w}({\varvec{s}}[w])(t,a!), $$

when $t\in I$ and thus sampling from $\tilde{\upsilon }^{*}_{}$ reduces to selecting an interval I and winner w, sample a delay t from $\frac{\kappa ^{\delta _{}}_{w}({\varvec{s}}[m])(t)}{\int _{I}\kappa ^{\delta _{}}_{w}({{\varvec{s}}[w]})(\tau )\mathop {}\!\mathrm {d} \tau }$ and finally sample an action $a!$ from $\kappa ^{\gamma _{}}_{w}({\varvec{s}}[w])(t,a!)$.

Algorithm 1 is our importance sampling algorithm for a composition of STA. In line 5 the delay densities of components according to standard semantics is extracted, and the win-densities ($\kappa ^{\delta _{}}_{i}$) of each component winning is defined in line 6. In line 7 the delay intervals we should alter the distributions of $\kappa ^{\delta _{}}_{i}$ into is found. Lines 8 and 9 find a winning component ,w, and an interval in which it won, and then lines 10 and 11 sample a delay from that interval according to $\kappa ^{\delta _{}}_{w}$. After sampling a delay, lines 13 and 14 sample an action. Afterwards the current state and likelihood ratio (L) is updated. The sampling in line 14 is a standard weighted choice, likewise is the sampling in line 9 - provided we have first calculated the integrals over $\kappa ^{\delta _{}}_{i}$ for all i. In line 11 the sampling from the conditional distribution is performed by Inverse Transform Sampling, requiring integration of $\kappa ^{\delta _{}}_{k}({\varvec{s}}[k])$.

A recurring requirement for the algorithm is thus that $\kappa ^{\delta _{}}_{k}({\varvec{s}}[k])$ is integrable: In the following we assume, without loss of generality, that ${\varvec{s}}$ is a state where there exists some k such that for all $i\le k$, $\delta _{i}({\varvec{s}}[i])$ is a uniform distribution between $a_i$ and $b_i$ and for all $i> k$ that $\delta _{i}({\varvec{s}}[i])(t) = \lambda _i e^{-\lambda _i(t-d_i)}$ for $t>d_i$ i.e. $\delta _{i}({\varvec{s}}[i])$ is a shifted exponential distribution. For any $i\le k$ we can now derive that $\kappa ^{\delta _{}}_{i} ({\varvec{s}}[i])(t) = \delta _{i}({\varvec{s}}[i])(t)\prod _{j\ne i}\left( \int _{\tau >t}\delta _{j}({\varvec{s}}[j])(\tau \mathop {}\!\mathrm {d} \tau )\right)$ is

$$\begin{aligned}&\frac{1}{b_i-a_i}\prod _{j\le k, j\ne i}\left( {\left\{ \begin{array}{ll} \frac{b_j -t}{b_j-a_j} &{} \text { if } a_j \le t \le b_j \\ 1 &{} \text { if } t< a_j\\ 0 &{} \text { if } b_j< t \text { or } t< a_i \\ &{}\text { or } t>a_i \end{array}\right. } \right) \cdot&\prod _{j>k}\left( {\left\{ \begin{array}{ll} e^{-\lambda _i(t-d_i)} &{} \text { if } t > d_i\\ 1 &{}\text { else } \end{array}\right. } \right) \end{aligned}$$

and in general it can be seen that $\kappa ^{\delta _{}}_{i}({\varvec{s}}[i])(t) = {\left\{ \begin{array}{ll} \mathcal {P}_{0}(t) \cdot \mathcal {E}_{0}(t)&{} \text{ if } t\in I_0 \\ \mathcal {P}_{1}(t) \cdot \mathcal {E}_{1}(t)&{} \text{ if } t\in I_1 \\ &{}\vdots \\ \mathcal {P}_{k}(t) \cdot \mathcal {E}_{k}(t) &{} \text{ if } t\in I_l \end{array}\right. }$

where $I_0,I_1\dots I_l$ are disjoint intervals covering $[a_i,b_i]$, and for all j, $\mathcal {P}_{j}(t)$ is a polynomial constructed by the multiplication of uniform distribution and $\mathcal {E}_{j}(t)$ is an exponential function of the form $e^{\alpha \cdot t+\beta }$ constructed by multiplying shifted exponential distributions. Notice that although we assumed $i\le k$, the above generalisation also holds for $i>k$. As a result we need to show for any polynomial, $\mathcal {P}_{}(t)$, that $\mathcal {P}_{}(t)\cdot e^{\alpha \cdot t+\beta }$ is integrable.

Lemma 4

( ³ ). Let $\mathcal {P}_{}(t) = \sum _{i=0}^n a_i t^i$ be a polynomial and let $\mathcal {E}_{0}(t) = e^{\alpha \cdot t+\beta }$ be an exponential function with $\alpha ,\beta \in \mathbb {R}_{\ge 0}$. Then $\int \mathcal {P}_{}(t)\cdot \mathcal {E}_{}(t) \mathop {}\!\mathrm {d} t = \hat{\mathcal {P}_{}(t)}\cdot \mathcal {E}_{}(t),$ with $\hat{\mathcal {P}_{}(t)} = \sum _{i=0}^{n+1} b_i t^i$, where $b_{n+1}=0$ and $b_i=\frac{a_i-b_{i+1}(i+1)}{\alpha }$.    $\square$

6 Experiments

In this section we compare the variance of our importance sampling (IS) estimator with that of standard SMC. We include a variety of scalable models, with both rare and not-so-rare properties to compare performance. Running is a parametrised version of our running example. Race is based on a simple race between automata. Both Running and Race are parametrised by , which affects the bounds in guards and invariants. Race considers the property of reaching goal location within a fixed time, denoted $\Diamond _{\le 1}$ . Running considers the property of reaching goal location within a time related to , denoted $\Diamond _{\le \mathsf {scale}\cdot 100}$ . The DPA (Duration Probabilistic Automata) are job-scheduling models [7] that have proven challenging to analyse in other contexts [12]. We consider the probability of all processes completing their tasks within parametrised time limit $\tau$. The property has the form , where are the goal states of the n components that comprise the model.

The variance of our IS estimator is typically lower than that of SMC, but SMC simulations are generally quicker. IS also incurs additional set-up and initial analysis with respect to SMC. To make a valid comparison we therefore consider the amount of variance reduction after a fixed amount of CPU time. For each approach and model instance we calculate results based on 30 CPU-time-bounded experiments, where individual experiments estimate the probability of the property and the variance of the estimator after 1 s. This time is sufficient to generate good estimates with IS, while SMC may produce no successful traces. Using an estimate of the expected number of SMC traces after 1 s, we are nevertheless able to make a valid comparison, as described below.

Table 1. Experimental results. $\mathbb {P}$ is exact probability, when available. SMC (IS) indicates crude Monte Carlo (importance sampling). $\widehat{\sigma ^{2}_{\mathrm {is}}}$ is empirical variance of likelihood ratio. Gain estimates true improvement of IS at 1 s CPU time. Mem. reports memory use. Model DPAxSy contains x processes and y tasks.

Our results are given in Table 1. The Gain column gives an estimate of the true performance improvement of IS by approximating the ratio (variance of SMC estimator)/(variance of IS estimator) after 1 s of CPU time. The variance of the IS estimator is estimated directly from the empirical distribution of all IS samples. The variance of the SMC estimator is estimated by $\hat{p}(1-\hat{p})/N_\mathrm {SMC}$, where $\hat{p}$ is our best estimate of the true probability (the true value itself or the mean of the IS estimates) and $N_\mathrm {SMC}$ is the mean number of standard SMC simulations observed after 1 s.

For each model type we see that computational gain increases with rarity and that real gains of several orders of magnitude are possible. We also include model instances where the gain is approximately 1, to give an idea of the largest probability where IS is worthwhile. Memory usage is approximately constant over all models for SMC and approximately constant within a model type for IS. The memory required for the reachability graph is a potential limiting factor of our IS approach, although this is not evident in our chosen examples.

7 Conclusion

Our approach is guaranteed to reduce estimator variance, but it incurs additional storage and simulation costs. We have nevertheless demonstrated that our framework can make substantial real reductions in computational effort when estimating the probability of rare properties of stochastic timed automata. Computational gain tends to increase with rarity, hence we observe marginal cases where the performance of IS and SMC are similar. We hypothesise that it may be possible to make further improvements in performance by applying cross-entropy optimisation to the discrete transitions of the reachability graph, along the lines of [9], making our techniques more efficient and useful for less-rare properties.

Importance splitting [11, 15] is an alternative variance reduction technique with potential advantages for SMC [10]. We therefore intend to compare our current framework with an implementation of importance splitting for stochastic timed automata, applying both to substantial case studies.