Model checking for probabilistic timed automata

Abstract

Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as “the maximum probability of the airbag failing to deploy within 0.02 seconds”, “the maximum expected time for the protocol to terminate” or “the minimum expected energy consumption required to complete all tasks”. We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem.

1 Introduction

Automated verification techniques, such as model checking, provide powerful methods for rigorously analysing the correctness of systems. Increasingly, this analysis must also take into account quantitative aspects of the systems being verified, including both real-time characteristics and probabilistic behaviour. Embedded systems, for example, whether in communication and multimedia devices or in automotive and avionic control systems, often operate under timing constraints. The need for automated formal verification techniques in this domain is clear, as evidenced by the take-up of timed automata verification tools such as UPPAAL [13]. On the other hand, many real-life systems also exhibit stochastic behaviour, due, for example, to component failures, unreliable communication media or the use of randomisation. Probabilistic verification tools such as PRISM [51] and MRMC [45] have been widely used to analyse many systems with stochastic behaviour. Another vital ingredient in system modelling is nondeterminism, which is often used to capture concurrency between parallel components and to under-specify or abstract certain aspects of a system.

Probabilistic timed automata (PTAs) [11, 35, 54] are a modelling formalism for systems that exhibit probabilistic, nondeterministic and real-time characteristics. In many application domains, all three aspects need to be modelled; these include wireless communication protocols such as Bluetooth or Zigbee, automotive network protocols such as FlexRay, randomised security protocols, e.g. for anonymity or non-interference, and many others. The interplay between these different aspects can be subtle, making automated verification techniques and tool support essential. Verification of PTAs permits analysis of a wide range of quantitative properties, from reliability to performance, e.g.:

• “the maximum probability of an airbag failing to deploy within 0.02 seconds”;

• “the minimum probability that a packet is correctly delivered with 1 second”;

• “the maximum expected time for the protocol to terminate”.

PTAs can also be augmented with additional quantitative information in the form of costs or rewards. The resulting model is sometimes referred to as priced probabilistic timed automata and allows reasoning about a wide range of additional properties, e.g.:

• “the maximum expected number of lost packets within the first hour”;

• “the minimum expected energy consumption for completion of all tasks”;

• “the maximum number of queued requests after 10 seconds of operation”.

This paper provides an introduction to PTAs and the techniques that have been developed to specify and verify properties such as those listed above.

Paper structure

This paper is organised as follows. After background material in Sect. 2, Sect. 3 introduces the model of PTAs and discusses various issues relating to their use and analysis. Then, Sect. 4 presents a probabilistic temporal logic to represent properties of PTAs and Sect. 5 surveys the various techniques that can be used to perform model checking of this logic. Section 6 describes two case studies illustrating the usage of PTAs and their associated model-checking algorithms: a probabilistic non-repudiation protocol and a task-graph scheduling problem. Throughout the paper we give pointers to the relevant literature on PTAs and describe related work.

2 Background

We use ℝ_≥0 to denote the set of non-negative real numbers, ℚ_≥0 for the set of non-negative rationals and ℕ for the set of natural numbers. A discrete probability distribution over a countable set Q is a function μ:Q→[0,1] such that ∑ _q∈Q μ(q)=1. For a function μ:Q→ℝ_≥0 we define Support(μ)={q∈Q∣μ(q)>0}. Then, for an arbitrary set Q, we define Dist(Q) to be the set of functions μ:Q→[0,1] such that Support(μ) is a countable set and μ restricted to Support(μ) is a distribution. For q∈Q, let μ _q be the point distribution at q which assigns probability 1 to q. Let AP be a set of atomic propositions, which we assume to be fixed throughout the paper.

Markov decision processes (MDPs) are a widely used formalism for modelling systems that exhibit both nondeterministic and probabilistic behaviour. In this paper, we will use timed probabilistic systems (TPSs) [52, 56], an extension of MDPs in which transitions are labelled with either an action or a time duration.

Definition 1

(TPS)

A timed probabilistic systems ${\sf T}$ is a tuple $(S , {\overline{s}}, \mathit {Act}, {\mathit {Steps}}_{{\sf T}}, {\mathit {lab}})$ where S is (possibly infinite) a set of states, ${\overline{s}}\in S$ an initial state, Act a (finite) set of actions, ${\mathit {Steps}}_{{\sf T}}: S \times (\mathit {Act}\cup {\mathbb {R}_{\geq 0}}) \rightarrow {\mathit {Dist}}(S)$ a (partial) probabilistic transition function and lab:S→2^AP a labelling function.

A TPS ${\sf T}$ starts in the initial state ${\overline{s}}$ and, when in state s∈S, there is a nondeterministic choice between one or more available actions or time durations a∈Act∪ℝ_≥0 (those for which ${\mathit {Steps}}_{{\sf T}}(s,a)$ is defined). After the choice of an available action or time duration a, a successor state s′ is selected at random according to the probability distribution ${\mathit {Steps}}_{{\sf T}}(s,a)$. We use the notation $\smash{s \xrightarrow{a,\mu} s'}$ for such a transition, i.e., to denote that ${\mathit {Steps}}_{{\sf T}}(s,a)$ is defined and equal to μ, and that s′∈Support(μ). We assume, for each state s∈S, there exists at least one available action or time duration. An MDP M is a special case of a TPS where time is omitted from the transition function, i.e., the probabilistic transition function takes the form Steps _M :S×Act→Dist(S).

A path of a TPS represents a particular resolution of both the nondeterminism and probability present in the system. Formally, a path is a finite or infinite sequence of probabilistic transitions alternating between time durations and actions, for example:

$$\omega = s_0 \xrightarrow{a_0,\mu_0} s_1 \xrightarrow{a_1,\mu_1} s_2 \xrightarrow{a_2,\mu_2} \cdots $$

where a _2i ∈ℝ_≥0 and a _2i+1∈Act for i∈ℕ. We denote by ω(i) the (i+1)th state s _i of ω and the accumulated duration up until this state ω(i) is defined by:

$$\mathit {dur}_{\omega}(i)\ {\,\stackrel {\mbox {\rm {\tiny def}}}{=}}\ \sum_{0 \leq j {<} i \wedge a_j \in {\mathbb {R}_{\geq 0}}} a_{j}. $$

A position of ω is a pair (i,t)∈ℕ×ℝ_≥0 such that t≤dur _ω (i+1)−dur _ω (i). We say that the position (j,t′) precedes the position (i,t), written (j,t′)≺(i,t), when j<i or j=i and t′<t.

To reason about the probabilistic behaviour of a TPS ${\sf T}$, we use the notion of an adversary, which is a possible resolution of nondeterminism only. Formally, an adversary is a function from finite paths with an even number of transitions to available time durations, and from finite paths with an odd number of transitions to available actions). For a fixed adversary σ and state s, we can define a probability measure ${\mathit {Pr}_{{\sf T},s}^{{\sigma }}}$ over the set ${\mathit {Path}}^{{\sigma }}_{{\sf T},s}$ of infinite paths starting in s corresponding to σ [47]. For a real-valued random variable f over ${\mathit {Path}}^{{\sigma }}_{{\sf T},s}$, we let $\mathbb {E}_{{\sf T},s}^{{\sigma }}(f)$ denote the expected value of f with respect to ${\mathit {Pr}_{{\sf T},s}^{{\sigma }}}$.

We restrict our attention to time-divergent (or non-Zeno) adversaries, i.e., we do not consider executions in which time does not advance beyond a certain point. These can be ignored on the grounds that they do not correspond to actual, realisable behaviour of the system being modelled [2, 40]. Formally, an adversary σ of a TPS ${\sf T}$ is time divergent if:

$${\mathit {Pr}_{{\sf T},s}^{{\sigma }}}\bigl(\bigl\{ \omega \in {\mathit {Path}}^{\sigma }_{{\sf T},s} \, | \, \forall c \in {\mathbb {N}}. \,\exists i \in {\mathbb {N}}. \, \mathit {dur}_{\omega}(i) {>} c \bigr\}\bigr) = 1 $$

for all states s of ${\sf T}$. We denote by ${\mathit {Adv}}_{{\sf T}}$ the set of all time-divergent adversaries of ${\sf T}$. This issue is discussed in more depth in Sect. 3.

We next introduce rewards (or, equivalently, costs or prices) for TPSs. These are used to represent additional information about the system that the TPS represents, e.g., the number of packets sent or requests lost, the time spent in a particular state or the energy consumed.

Definition 2

(Reward structure)

A reward structure for a TPS ${\sf T}= (S , {\overline{s}}, \mathit {Act}, {\mathit {Steps}}_{{\sf T}}, {\mathit {lab}})$ is a pair r=(r _S ,r _Act ) where r _S :S→ℝ_≥0 is a state reward function and r _Act :(S×Act)→ℝ_≥0 is an action reward function.

For a reward structure r=(r _S ,r _Act ) and state s, the value r _S (s) defines the rate (per time unit) at which reward is accumulated when in state s. On the other hand, for state s and action a, the value r _Act (s,a) defines the reward acquired when the action a is taken in state s. More formally, for any infinite path $\omega=s_{0} \xrightarrow{a_{0},\mu_{0}} s_{1} \xrightarrow{a_{1},\mu_{1}} \cdots$, the reward accumulated during the transition of ω from state s _i to s _i+1 is defined by:

$$\mathit {r}(\omega,i) {\,\stackrel {\mbox {\rm {\tiny def}}}{=}}\left \{ \begin{array}{l@{\quad}l} \mathit {r}_{S}(s_i) {\cdot} a_i & \mbox{if $a_{i} \in {\mathbb {R}_{\geq 0}}$ (or, equivalently, if $i\ \mathrm{mod}\ 2 = 0$)}, \\[3pt] \mathit {r}_{\mathit {Act}}(s_i,a_i) & \mbox{otherwise}. \end{array} \right . $$

Alternatively, we can also interpret state rewards as defining a reward at a particular time instant. An example of this usage would be a reward structure that represents the number of messages stored in a queue at a particular time instant. When using this interpretation, action reward values are not considered.

3 Probabilistic timed automata

Probabilistic timed automata (PTAs) [11, 42, 54] model real-time behaviour in the same fashion as classical timed automata [4], using clocks. Clocks are variables whose values range over the non-negative reals and which increase at the same rate as time. Throughout this paper, we assume a finite set of clocks $\mathcal {X}$. A function $v: \mathcal {X}\rightarrow {\mathbb {R}_{\geq 0}}$ is referred to as a clock valuation and the set of all clock valuations is denoted by ${\mathbb {R}}_{\geq 0}^{\mathcal {X}}$. For any $v \in {\mathbb {R}}_{\geq 0}^{\mathcal {X}}$, t∈ℝ_≥0 and $X\subseteq \mathcal {X}$, we use v+t to denote the clock valuation which increments all clock values in v by t and v[X:=0] for the clock valuation in which clocks in X are reset to 0. We use ${\bf 0}$ to denote the clock valuation that assigns 0 to all clocks in $\mathcal {X}$.

The set of clock constraints over $\mathcal {X}$, denoted $\mathit {CC}({\mathcal {X}})$, is defined by the syntax:

$$\chi :: = \mathtt {true}\, | \, x \leq d \, | \, c \leq x \, | \, x+ c \leq y+ d \, | \, \neg \chi \, | \, \chi \wedge \chi $$

where $x,y \in \mathcal {X}$ and c,d∈ℕ. A clock valuation v satisfies a clock constraint χ, denoted by v⊨χ, if χ resolves to true when substituting each occurrence of clock x with v(x). The set of valuations satisfying a clock constraint is called a zone. Clock constraints will be used in the syntactic definition of PTAs and for the specification of properties.

Definition 3

(PTA syntax)

A probabilistic timed automaton (PTA) is defined by a tuple $\mathsf {P}= ( L, \overline {l}, \mathcal {X}, \mathit {Act}, \mathit {inv}, \mathit {enab}, \mathit {prob}, \mathcal {L})$ where:

• L is a finite set of locations and $\overline {l}\in L$ is an initial location;

• $\mathcal {X}$ is a finite set of clocks;

• Act is a finite set of actions;

• $\mathit {inv}: L\rightarrow \mathit {CC}({\mathcal {X}})$ is an invariant condition;

• $\mathit {enab}: L\times \mathit {Act}\rightarrow \mathit {CC}({\mathcal {X}})$ is an enabling condition;

• $\mathit {prob}: L\times \mathit {Act}\rightarrow {\mathit {Dist}}(2^{\mathcal {X}} \times L)$ is a (partial) probabilistic transition function;

• $\mathcal {L}: L \rightarrow 2^{{\mathit{AP}}}$ is a labelling function mapping each location to a set of atomic propositions.

A state of a PTA is a pair $(l,v) \in L\times {\mathbb {R}}_{\geq 0}^{\mathcal {X}}$ such that v⊨inv(l). In any state (l,v), either a certain amount of time t∈ℝ_≥0 elapses, or an action a∈Act is performed. If time elapses, then the choice of t requires that the invariant inv(l) remains continuously satisfied while time passes. The resulting state after this transition is (l,v+t) and, to ease notation, we denote this state by (l,v)+t. In the case where an action is performed, an action a can only be chosen if it is enabled, i.e., if the clock constraint enab(l,a) is satisfied by v. Once an enabled action a is chosen, a set of clocks to reset and a successor location are selected at random, according to the distribution prob(l,a). We call each element $(X,l') \in 2^{\mathcal {X}}\times L$ in the support of prob(l,a) an edge and use edges(l,a) to denote the set of such edges.

We assume that PTAs are well-formed, meaning that, for each state (l,v) and action a such that v satisfies enab(l,a), every edge (X,l′)∈edges(l,a) results in a transition to a valid state, i.e., we have v[X:=0]⊨inv(l′). A PTA can be transformed into one that is well-formed by incorporating the invariant associated with the target location into the enabling condition of each location-action pair (see [56]).

Definition 4

(PTA semantics)

Let $\mathsf {P}=( L, \overline {l}, \mathcal {X}, \mathit {Act}, \mathit {inv}, \mathit {enab}, \mathit {prob}, \mathcal {L})$ be a PTA. The semantics of P is defined as the (infinite-state) TPS $[ \! [ {\mathsf {P}} ] \! ]=(S,{\overline{s}},\mathit {Act},{\mathit {Steps}}_{\mathsf {P}},{\mathit {lab}})$ where:

• $S = \{ (l,v) \in L\times {\mathbb {R}}_{\geq 0}^{\mathcal {X}}\ | \ v \models \mathit {inv}(l)\}$ and ${\overline{s}}= (\overline {l},\mathbf{0})$;

• for any (l,v)∈S and a∈Act∪ℝ_≥0, we have Steps _P ((l,v),a)=λ if and only if either:

  • time transitions: a∈ℝ_≥0, v+t′⊨inv(l) for all 0≤t′≤a, and λ=μ _(l,v+a),

  • action transitions: a∈Act, v⊨enab(l,a) and for each (l′,v′)∈S:

    $$\lambda\bigl(l',v'\bigr) = \sum \bigl\{ \big| \mathit {prob}(l,a) \bigl(X,l'\bigr) \, | \, X \in 2^\mathcal {X}\wedge v' = v[X{:=}0] \big| \bigr\} ; $$

• for any (l,v)∈S we have ${\mathit {lab}}(l,v) = \mathcal {L}(l)$.

Example of a PTA

In Fig. 1, we present a PTA modelling a simple communication protocol. We adopt the standard conventions for the graphical representation of timed automata. Distributions are represented by an arc connecting edges at their source and by probability labels attached to edges (omitted for edges taken with probability 1). The PTA has two clocks x and y, which start with the value 0. In the location init, the system waits for at least 1 time unit (represented by the enabling condition x≥1 on the outgoing distribution of action send) and at most 2 time units (represented by conjunct x≤2 of the invariant condition), before sending a message. With probability 0.9 the message is received correctly (edge to done); otherwise, with probability 0.1, the message is lost (edge to lost). In the latter case, once clock x reaches 8, the PTA returns to init where another attempt to send the message can be made. If, in total, at least 20 and at most 25 time units have elapsed since the start of system execution, the PTA performs a timeout and moves to location fail.

Fig. 1

Example of a PTA

Rewards for PTAs

We can also define rewards for a PTA. Often, these model usage of some resource and are equivalently referred to as costs or prices. A reward structure at the level of a PTA P is defined using a pair r=(r _L ,r _Act ), where r _L :L→ℝ_≥0 is a function assigning to each location the rate at which rewards are accumulated as time passes in that location and r _Act :L×Act→ℝ_≥0 is a function assigning the reward of executing each action in each location. The corresponding reward structure of the TPS [[P]] is given by r=(r _S ,r _Act ) where r _S (l,v)=r _L (l) and r _Act ((l,v),a)=r _Act (l,a) for $(l,v) \in L \times {\mathbb {R}}_{\geq 0}^{\mathcal {X}}$ and a∈Act. PTAs equipped with reward structures are a probabilistic extension of linearly-priced timed automata (also known as weighted timed automata) [5, 14].

Modelling with PTAs

We now summarise a variety of extensions to the standard definition of PTAs that facilitate high-level modelling using this formalism.

Parallel composition. It is often useful to define complex systems as the parallel composition of several interacting components. The definition of the parallel composition operator ∥ for PTAs [55] uses ideas from (untimed) probabilistic automata [62] and classical timed automata [4]. Let $\mathsf {P}_{i} = ( L_{i}, \overline {l}_{i}, \mathit {Act}_{i} , \mathcal {X}_{i}, \mathit {inv}_{i} , \mathit {enab}_{i}, \mathit {prob}_{i}, \mathcal {L}_{i} \ )$ for i∈{1,2} and assume that $\mathcal {X}_{1} \cap \mathcal {X}_{2}= \emptyset$. Given $\mu_{1} \in {\mathit {Dist}}(2^{\mathcal {X}_{1}} \times L_{1})$ and $\mu_{2} \in {\mathit {Dist}}(2^{\mathcal {X}_{2}} \times L_{2})$, we let $\mu_{1} {\otimes} \mu_{2} \in {\mathit {Dist}}(2^{\mathcal {X}_{1} \cup \mathcal {X}_{2}} \times (L_{1} \times L_{2}))$ be such that μ ₁⊗μ ₂(X ₁∪X ₂,(l ₁,l ₂))=μ ₁(X ₁,l ₁)⋅μ ₂(X ₂,l ₂) for $X_{i} \subseteq \mathcal {X}_{i}$, l _i ∈L _i and i∈{1,2}. The parallel composition of PTAs P ₁ and P ₂ is the PTA:

$$\mathsf {P}_1 \| \mathsf {P}_2 = \bigl(L_1 \times L_2 , (\overline {l}_1,\overline {l}_2), \mathcal {X}_1 \cup \mathcal {X}_2, \mathit {Act}_1 \cup \mathit {Act}_2, \mathit {inv}, \mathit {enab}, \mathit {prob}, \mathcal {L}\bigr) $$

such that, for each location pair (l ₁,l ₂)∈L ₁×L ₂ and action a∈Act ₁∪Act ₂:

• the invariant condition is given by inv(l ₁,l ₂)=inv ₁(l ₁)∧inv ₂(l ₂);

• the enabling condition is given by:

  $$\mathit {enab}\bigl((l_1,l_2),a\bigr) = \left \{ \begin{array}{l@{\quad}l} \mathit {enab}_1(l_1,a) \wedge \mathit {enab}_2(l_2,a) & \text{if $a \in \mathit {Act}_{1} \cap \mathit {Act}_{2}$},\\[3pt] \mathit {enab}_1(l_1,a) & \text{if $a \in \mathit {Act}_{1} \setminus \mathit {Act}_{2}$},\\[3pt] \mathit {enab}_2(l_2,a) & \text{if $a \in \mathit {Act}_{2} \setminus \mathit {Act}_{1}$;} \end{array} \right . $$

• the probabilistic transition function is given by:

  $$\mathit {prob}\bigl((l_1,l_2),a\bigr) = \left \{ \begin{array}{l@{\quad}l} \mathit {prob}_1(l_1,a) \; {\otimes} \; \mathit {prob}_2(l_2,a) & \text{if $a \in \mathit {Act}_{1} \cap \mathit {Act}_{2}$},\\[3pt] \mathit {prob}_1(l_1,a) \; {\otimes} \; \mu _{(\emptyset,l_2)} & \text{if $a \in \mathit {Act}_{1} \setminus \mathit {Act}_{2}$},\\[3pt] \mu _{(\emptyset,l_1)} \; {\otimes} \; \mathit {prob}_2(l_2,a) & \text{if $a \in \mathit {Act}_{2} \setminus \mathit {Act}_{1}$;} \end{array} \right . $$

• the labelling function is given by $\mathcal {L}(l_{1},l_{2}) = \mathcal {L}_{1}(l_{1}) \cup \mathcal {L}_{2}(l_{2})$.

If PTA P _i has associated reward structure $(\mathbf {r}_{L}^{i},\mathbf {r}_{\mathit {Act}}^{i})$, then the reward structure r=(r _L ,r _Act ) for P ₁∥P ₂ is such that, for (l ₁,l ₂)∈L ₁×L ₂ and a∈Act ₁∪Act ₂, we have $\mathbf {r}_{L}(l_{1},l_{2}) = \mathbf {r}_{L}^{1}(l_{1}) + \mathbf {r}_{L}^{2}(l_{2})$, $\mathbf {r}_{\mathit {Act}}((l_{1},l_{2}),a) = \mathbf {r}_{\mathit {Act}}^{1}(l_{1},a) + \mathbf {r}_{\mathit {Act}}^{2}(l_{2},a)$ if a∈Act ₁∩Act ₂, $\mathbf {r}_{\mathit {Act}}((l_{1},l_{2}),a) = \mathbf {r}_{\mathit {Act}}^{1}(l_{1},a)$ if a∈Act ₁∖Act ₂ and $\mathbf {r}_{\mathit {Act}}((l_{1},l_{2}),a) = \mathbf {r}_{\mathit {Act}}^{2}(l_{2},a)$ if a∈Act ₂∖Act ₁.

Discrete variables. When modelling systems with (probabilistic) timed automata, it is often convenient to augment the model with discrete variables [13, 65]. We restrict ourselves to the case in which a finite number of variables, each with a finite domain, are added to the PTA framework; enabling conditions can then refer to the current value of the variables, and the probabilistic transition relation is extended to allow updating variable values. Such an extended PTA model can be represented in the standard PTA framework presented above in the following way. Let L be the set of locations of the extended PTA, and suppose the extended PTA has n bounded integer variables. The locations of the standard PTA are tuples comprising n+1 elements: the first element is a location from L, while the remaining n elements are values of the bounded integer variables. Enabling conditions are obtained by resolving partially the enabling conditions of the extended PTA, using the variable values corresponding to the locations and the probabilistic transition function is obtained by encoding variable updates into target locations of edges.

Urgency. When modelling real-time systems, it is often necessary to express the fact that a particular action should be taken immediately, without letting time pass. In this way, we can model, for example, an instantaneous system event comprising several atomic actions. A number of mechanisms for modelling such situations have been introduced for timed automata, for example in the system-description language of the UPPAAL model checker [13]; here, we describe how they are adapted to PTAs.

Firstly, an urgent location of a PTA is a location in which no time can pass. Urgent locations can be represented in the PTA framework by introducing an additional clock, which is reset on entry to an urgent location, and by including a conjunct in the invariant condition of the location to specify that the value of the clock should be equal to 0 in the location.

Secondly, a committed location of a PTA is, like an urgent location, a location in which no time can pass, but also must be left before any other system component makes a transition. We adapt to PTAs the method of [65] for encoding committed locations in the standard timed automata framework. First a global Boolean variable atom is added to the PTA. Now, consider a PTA which is to be composed in parallel with other PTAs. A committed location of the PTA is subject to the constructs added in the case of urgent locations and, in addition, atom is set to true on entry to the committed location, is set to false on exiting the committed location, and all enabling conditions of the PTA except those corresponding to committed locations have the conjunct requiring that atom is false.

Finally we mention urgent actions [13, 30]. Informally, an action is urgent if it must be chosen as soon as it is enabled. Urgent actions can be introduced to the PTA syntax simply by identifying the subset Act _u of actions which are interpreted as urgent. The presence of urgent actions necessitates the following modifications to the semantics of a PTA. For PTA $\mathsf {P}=( L, \overline {l}, \mathit {Act}, \mathcal {X}, \mathit {inv}, \mathit {enab}, \mathit {prob}, \mathcal {L})$ with urgent actions Act _u , [[P]] is the TPS $(S,{\overline{s}},\mathit {Act},{\mathit {Steps}}_{\mathsf {P}},{\mathit {lab}})$ where S, ${\overline{s}}$, lab and Steps _P ((l,v),a) for (l,v)∈S and a∈Act are as in Definition 4, while for (l,v)∈L, t∈ℝ_≥0, we have Steps _P ((l,v),t)=μ _(l,v+t′) if and only if:

• v+t′⊨inv(l) for all 0≤t′≤t;

• for all 0≤t′<t and a′∈Act, if v+t′⊨enab(l,a′) then $a' \not\in \mathit {Act}_{u}$.

Non-standard clock resets. In the PTA framework, as in the standard definition of timed automata, clocks can only be reset to value 0 when taking a probabilistic transition. It may be useful, though, to also allow clocks to be reset to any non-negative integer value. If ℕ_⊥=ℕ∪{⊥}, v is a clock valuation and $\theta : \mathcal {X}{\rightarrow } {\mathbb {N}}_{\bot}$, then define the clock valuation v[θ] such that v[θ](x)=v(x) if θ(x)=⊥ and v[θ](x)=θ(x) otherwise. Then, a PTA with extended resets is defined as a PTA in Definition 3, except that the probabilistic transition function is now defined as $\mathit {prob}: L\times \mathit {Act}\rightarrow {\mathit {Dist}}( (\mathcal {X}{\rightarrow } {\mathbb {N}}_{\bot}) \times L)$. The semantics of a PTA with extended resets P is defined as in Definition 4, except that for (l,v)∈S and a∈Act, we have Steps _P ((l,v),a)=λ if and only if v⊨enab(l,a) and, for each (l′,v′)∈S:

$$\lambda\bigl(l',v'\bigr) = \sum \bigl\{\big| \mathit {prob}(l,a) \bigl(\theta ,l'\bigr) \, | \, \theta \in \mathcal {X}{\rightarrow } {\mathbb {N}}_\bot \wedge v' = v\bigl[\theta \bigr] \big| \bigr\}. $$

A PTA with extended resets can be translated into a PTA with the standard restriction of clock resets to 0, by adapting an analogous construction for (non-probabilistic) timed automata [26]. However, this construction can give an exponential blow-up in the size of the model, which is unavoidable [25]. Instead, model-checking algorithms for PTAs can be developed which incorporate the extended definition of resets directly.

Channels. The definitions of actions and parallel composition presented here can be extended to allow for channels and the sending and receiving (to either single or multiple recipients) of messages along them, as in UPPAAL [13]. Such behaviour can be encoded in the action names of a standard PTA.

Time divergence

An important issue with regard to the verification of models of real-time systems is that of time divergence. As explained in Sect. 2, such behaviour does not correspond to that of the real system, and hence the verification technique used must be able to disregard such behaviour during analysis. We use the notion of time divergence of Sect. 2, i.e., we restrict our attention to the adversaries Adv _[[P]] (those adversaries for which the probability of time passing beyond any bound is 1).

Note that a PTA may feature states from which time cannot diverge for any adversary; such states correspond to a probabilistic generalisation of timelocks in the timed automata setting [40], and are considered to indicate modelling errors. The set of timelock states can be identified using (extensions of) the analysis methods that we present in Sect. 5, and removed from the model by modifying the invariant and enabling conditions.

For some PTAs, all adversaries will be time-divergent by construction. We give a syntactic and compositional condition, derived from analogous results on timed automata [66, 67], which guarantees that all adversaries are time-divergent: a PTA is structurally divergent if, for every sequence (l ₀,a ₀),(X ₀,l ₁),…,(l _n ,a _n ),(X _n ,l _n+1) such that (X _i ,l _i+1)∈edges(l _i ,a _i ) for 0≤i<n and l _n+1=l ₀, there exists $x \in \mathcal {X}$ and 0≤i,j≤n such that x∈X _i and enab(l _j ,a _j )⇒(x≥1) (i.e. enab(l _j ,a _j ) contains a conjunct of the form x≥c for c≥1). If a PTA is not structurally divergent, verification algorithms can be adjusted to disregard non-divergent adversaries, as we will describe in Sect. 5.

Finally we note that a more restrictive notion of divergent adversary of a PTA, namely that of a strictly divergent adversary, has been presented in [63]. An adversary is strictly divergent if all of its paths entail time passing beyond any bound. In many contexts, strictly divergent adversaries are more realistic than divergent adversaries, e.g., if we regard the edge traversals of a PTA as corresponding to the change in a physical state of the system.

Alternative models

We conclude this section with a brief discussion of some alternative probabilistic models that also incorporate nondeterministic, probabilistic and timed aspects. One example, which has recently attracted increased interest in the context of probabilistic verification, is continuous-time Markov decision processes, along with closely related models such as interactive Markov chains [41] and Markov automata [31]. These extend classical (discrete-time) Markov decision processes with real-time delays modelled by exponential distributions. Thus, such models can alternatively be viewed as extensions of continuous-time Markov chains, which also model probabilistic real-time systems using exponentially-distributed delays, but which do not exhibit nondeterministic behaviour. Other proposed models in the literature include [1], which is based on generalised semi-Markov processes, and [53], which defines PTAs with continuously distributed random delays.

4 Property specification for PTAs

In this section, we present a temporal logic for the formal specification of quantitative properties of PTAs. The basis for this is the temporal logic PCTL [20, 37], a probabilistic extension of the logic CTL [29] which has been proposed for specifying properties of both MDPs [20] and discrete-time Markov chains [37]. We augment the logic with operators to reason about rewards (or costs or prices), in the style of the logic in [32] for MDPs (and as used in the probabilistic model checker PRISM [51]). We also discuss extensions to more expressive logics such as PTCTL and PCTL*. In the next section, we will survey the available techniques for model checking of PTAs against properties specified in our logic.

Definition 5

(Syntax)

The syntax of our logic is given by the following grammar:

$$\begin{array}{rcl} \phi & ::= & \mathtt {true}\ |\ \mathsf {a}\ |\ \chi \ |\ \phi\wedge\phi\ |\ \neg\phi\ |\ {\mathtt{P}}_{\bowtie\,p}[\psi] \ |\ {\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q} [ \rho ], \\[3pt] \psi & ::= & \phi {\ {\mathtt{U}}^{\leq k}\ }\phi\ |\ \phi {\ {\mathtt{U}}\ }\phi, \\[3pt] \rho & ::= & \mathtt {I}^{=k} \ |\ \mathtt {C}^{\le k}\ |\ \mathtt {F}\ {\phi} \end{array} $$

where a∈AP is an atomic proposition, $\chi \in \mathit {CC}({\mathcal {X}})$ is a clock constraint, ⋈∈{≤,<,≥,>}, p∈ℚ∩[0,1], q∈ℚ_≥0, r is a reward structure and k∈ℕ.

This logic extends propositional logic with a probabilistic operator (P) and a reward operator (R). Informally, a property of the form P _⋈ p [ψ] states that the probability of path formula ψ being true always satisfies the bound ⋈p. A property of the form ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ means that the expected value of reward function ρ on reward structure r meets the bound ⋈q.

Formulae in the logic are always state formulae, i.e., those formed by the production ϕ in the grammar above. These are evaluated over the states of a PTA P (or, more precisely, over the states of the TPS [[P]] representing its semantics). For state s and formula ϕ, we write s ⊨ ϕ to denote that ϕ is satisfied in s. The syntax also includes path formulae (ψ) and reward operators (ρ), which appear only as subformulae of the P and R operators.

We include two types of path formulae: time-bounded until (ϕ ₁ U ^≤k ϕ ₂) and (unbounded) until (ϕ ₁ U ϕ ₂). Formula ϕ ₁ U ϕ ₂ means that a state satisfying ϕ ₂ is eventually reached and that, at every time-instant prior to that, ϕ ₁ is satisfied. The time-bounded variant has the same meaning, with the additional constraint that the occurrence of ϕ ₂ must occur within time k. We can derive several useful operators, such as F ϕ≡true U ϕ, which means that ϕ is eventually satisfied, and F ^≤k ϕ≡true U ^≤k ϕ, which means that ϕ is satisfied within time k. We also have G ϕ≡¬(F ¬ϕ), which means that ϕ is always satisfied, and G ^≤k ϕ≡¬(F ^≤k ¬ϕ) which means that ϕ is continuously satisfied for time k. Although the G and G ^≤k operators cannot be derived from the basic syntax of the logic since there is no negation of path formulae, it can be shown that P _≤p [¬ψ]≡P _≥1−p [ψ], P _<p [¬ψ]≡P _>1−p [ψ], P _≥p [¬ψ]≡P _≤1−p [ψ] and P _>p [¬ψ]≡P _<1−p [ψ]. PCTL-style logics often include a next (X ) operator but this is of less use in timed models and omitted.

The reward operator I ^=k refers to the reward of the current state at time instant k, C ^≤k to the total reward accumulated up until time point k, and F ϕ to the total reward accumulated until a state satisfying ϕ is reached. Formally, we define the semantics of the logic as follows.

Definition 6

(Semantics)

Let P be a PTA, $[ \! [ {\mathsf {P}} ] \! ] = (S , {\overline{s}}, \mathit {Act}, {\mathbb {T}}, {\mathit {Steps}}_{\mathsf {P}}, {\mathit {lab}})$ be its semantics, and let r denote the reward structure over [[P]] corresponding to a reward structure r over P. For state s=(l,v)∈S, the satisfaction relation  ⊨  is defined inductively by:

$$\begin{array}{lll} s {\,\models\,}\mathtt {true}& & \mbox{always} \\[3pt] s {\,\models\,}\mathsf {a}& \iff\ & \mathsf {a}\in {\mathit {lab}}(s) \\[3pt] s {\,\models\,}\chi & \iff & v \models \chi \\[3pt] s {\,\models\,}\phi_1\wedge\phi_2 & \iff & s {\,\models\,}\phi_1 \wedge s {\,\models\,}\phi_2 \\[3pt] s {\,\models\,}\neg\phi & \iff & s {\,\not\models\,}\phi \\ s {\,\models\,}{\mathtt{P}}_{\bowtie\,p}[\psi] & \iff & {\mathit {Pr}_{ [ \! [ {\mathsf {P}} ] \! ],s}^{{\sigma }}}(\{\omega \in {\mathit {Path}}^{\sigma }_{ [ \! [ {\mathsf {P}} ] \! ],s}\ |\ \omega {\,\models\,}\psi\}) \bowtie p \mbox{ for all } {\sigma }\in {\mathit {Adv}}_{ [ \! [ {\mathsf {P}} ] \! ]} \\[3pt] s {\,\models\,}{\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q} [ \rho ] & \iff & \mathbb {E}_{ [ \! [ {\mathsf {P}} ] \! ],s}^{{\sigma }}(\mathit {rew}(\mathit {r},\rho))\bowtie q \text{ for all } {\sigma }\in {\mathit {Adv}}_{ [ \! [ {\mathsf {P}} ] \! ]} \end{array} $$

where, for any infinite path ω of [[P]]:

$$\begin{array}{lll} \omega {\,\models\,}\phi_1{\ {\mathtt{U}}^{\leq k}\ }\phi_2 & \Longleftrightarrow & \mbox{there exists a position $(i,t)$ of $\omega$ such that $\omega(i)+ t {\,\models\,}\phi_{2}$} \\[3pt] && \mbox{and $\mathit {dur}_{\omega}(i)+ t \leq k$ and $\omega(j)+ t' {\,\models\,}\phi_{1} {\vee} \phi_{2}$ for all positions}\\[3pt] &&\mbox{$(j,t') {\prec} (i,t)$ of $\omega$}, \\[3pt] \omega {\,\models\,}\phi_1{\ {\mathtt{U}}\ }\phi_2 & \Longleftrightarrow & \mbox{there exists a position $(i,t)$ of $\omega$ such that $\omega(i)+ t {\,\models\,}\phi_{2}$} \\ && \mbox{and $\omega(j)+ t' {\,\models\,}\phi_{1} {\vee} \phi_{2}$ for all positions $(j,t') {\prec} (i,t)$ of $\omega$} \end{array} $$

and, for reward structure r=(r _S ,r _Act ) over [[P]], the random variable rew(r,ρ) over infinite paths of [[P]] is defined as follows:

where j ₀=0, j _k =max{i | dur _ω (i)<k} for k>0 and, when it exists, (j _ϕ ,t _ϕ ) is the minimum position under the ordering ≺ such that ω(j _ϕ )+t _ϕ  ⊨ ϕ.

In addition to the basic syntax of Definition 6, we allow, in the style of the PRISM model checker, quantitative (numerical) queries yielding the minimum or maximum probability or expected reward value from a state s. We use ${\mathtt{P}}_{\mathtt{min=?}}[\psi]$, ${\mathtt{P}}_{\mathtt{max=?}}[\psi]$, ${\mathtt{R}}^{\mathbf {r}}_{\mathtt{min=?}}[\rho]$ and ${\mathtt{R}}^{\mathbf {r}}_{\mathtt{max=?}}[\rho]$, which give, respectively:

Some typical examples of PTA properties, specified in this logic are:

• P _≥0.8[F ^≤k ack _n ]—“the probability that the sender has received n acknowledgements within k clock-ticks is at least 0.8”;

• trigger→P _<0.0001[G ^≤20 ¬deploy]—“the probability of the airbag failing to deploy within 20 milliseconds of being triggered is strictly less than 0.0001”;

• ${\mathtt{P}}_{\mathtt{max=?}} [ \neg\mathsf{sent}{\ {\mathtt{U}}\ }\mathsf{fail} ]$—“what is the maximum probability of a failure occurring before message transmission is complete?”;

• ${\mathtt{R}}^{\mathbf{time}}_{\mathtt{max=?}}\vadjust{\vspace*{1.5pt}} [ {{\mathtt{F}}\ }\mathsf{end} ]$—“what is the maximum expected time for the protocol to terminate?”;

• ${\mathtt{R}}^{\mathbf{pwr}}_{<q} [ \mathtt {C}^{\le 60} ]$ – “the expected energy consumption during the first 60 seconds is <q”.

Property reductions

We now describe how model checking for several of the operators included in our logic can be reduced to checking satisfaction of a simpler formula on a modified PTA. Consider first a time-bounded until property P _⋈ p [ϕ ₁ U ^≤k ϕ ₂] on a PTA P. If we augment P with an additional clock z, then it follows that a state (l,v) of P satisfies the formula P _⋈ p [ϕ ₁ U ^≤k ϕ ₂] if and only if the state (l,v′) of the augmented PTA where v′(x)=v(x) for all clocks x of P and v′(z)=0 satisfies P _⋈ p [ϕ ₁ U (ϕ ₂∧(z≤k))] (see [56]). Second, given an until property P _⋈ p [ϕ ₁ U ϕ ₂], if we modify the PTA such that, upon reaching a state not satisfying ϕ ₁, only a transition to a sink state is possible, then a state of the PTA satisfies P _⋈ p [ϕ ₁ U ϕ ₂] if and only if a state of the modified PTA satisfies P _⋈ p [F ϕ ₂].

Next, we show how to reduce checking a property of the form P _≥p [F ^≤k ϕ], to a formula of the form P _≤1−p [F a _exc ] (the former requires computation of minimum probabilities, whereas the latter needs maximum probabilities, which are sometimes easier to compute). The reduction is correct only for states satisfying P _≥1[F ϕ], i.e. ϕ is always reachable with probability 1. We augment P with an extra clock z and then modify it such that states satisfying ϕ are forced to make a transition to a sink-location and, in all other states, we add a transition to a different, sink-location exceeded, enabled when z>k. Then P _≥p [F ^≤k ϕ] is true in a state of the original model if and only if the corresponding state of the modified PTA with z=0 satisfies P _≤1−p [F a _exc ], where a _exc is true only in location exceeded (see [55]).

Finally, we show how to reduce properties of the form ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {C}^{\le k}]$ or ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {I}^{=k}]$ to ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {F}\ {\phi}]$. In both cases, we add an extra clock z to P. For ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {C}^{\le k}]$, it suffices to check ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {F}\ {(z=k)}]$ on the augmented PTA. For ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {I}^{=k}]$, we add the conjunct z≤k to all invariants and a transition to a new sink location done (labelled a _done ) with enabling condition z=k to all locations, while changing the enabling conditions of all other transitions so that they are not enabled when z=k. It then suffices to check ${\mathtt{R}}^{\mathit {r}}_{\,\bowtie \,q}[\mathtt {F}\ { \mathsf {a}_{\mathsf{done}}}]$, where the only non-zero rewards are action rewards on the new transitions, set to the location reward of the source location.

More expressive logics

The next section of this paper will discuss techniques for model checking the properties expressible in the logic given above. A variety of more expressive logics have also been considered for PTAs. PTCTL [54] is a probabilistic extension of the timed temporal logic TCTL. In particular, it includes a freeze quantifier (or reset quantifier) z.ϕ, which introduces a formula clock z, reset to zero, that can be referred to in the subformula ϕ. Although not considered further in this paper, PTCTL can be model checked using the region graph construction and backwards reachability method discussed in Sect. 5. Formulae of the logics LTL and PCTL*, originally proposed for discrete-time probabilistic systems, can be verified on PTAs using a Rabin automaton product construction and the model checking algorithm of [64].

5 Model checking for PTAs

We now consider the problem of model checking a PTA P with respect to a property ϕ of the logic presented in Sect. 4, i.e., determining ${\mathit{Sat}}(\phi) {\,\stackrel {\mbox {\rm {\tiny def}}}{=}}\{s \in S\,|\,s\models\phi\}$, where S is the set of states of [[P]]. We will survey the various PTA model checking techniques that have been proposed in the literature, which support different fragments of the logic. We will cover:

• the region graph construction [54];

• the boundary region graph [43];

• the digital clocks method [52];

• backwards reachability [56];

• abstraction refinement with stochastic games [50].

The first two approaches, which are based on the concept of the region graph [2, 4], are used primarily to establish the decidability and complexity of model checking, rather than for practical implementations. The others provide efficient methods for model checking particular fragments of the logic. Table 1 provides a summary of the methods and their applicability. We omit the forwards reachability algorithm described in [54] since it only computes bounds on probabilities of system behaviour, rather than the exact values.

Table 1 Summary of PTA model checking techniques and their applicability

Unless otherwise stated, we also assume that P has no timelocks and is structurally divergent (structurally non-Zeno). In Sect. 5.1, we do explain how to treat PTAs that are not structurally divergent. Similar adaptations can also be applied to the other methods that we discuss in this section.

5.1 The region graph

We first discuss the region graph construction for a PTA [54], which is based on the classic construction for timed automata [2, 4]. This approach provides a way to model check the fragment of the logic from Sect. 4 that excludes ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ formulae (in the next section, we will relax this restriction). The region graph of a PTA P and formula ϕ takes the form of a finite-state MDP whose states are regions of the form (l,α), where l is a location and α is an equivalence class of clock valuations according to the equivalence defined below. Let c be the maximal constant to which any clock is compared in the clock constraints of P and ϕ. Then clock valuations ν and ν′ are equivalent if and only if they satisfy the following conditions:

• for any $x \in \mathcal {X}$, either ν(x)>c and ν′(x)>c, or ν(x) and ν′(x) agree on their integer parts;

• for any $x,x' \in \mathcal {X}$, either ν(x)−ν(x′)>c and ν′(x)−ν′(x′)>c, or ν(x)−ν(x′) and ν′(x)−ν′(x′) agree on their integer parts,

where two values q,q′∈ℝ_≥0 agree on their integer parts when ⌊q⌋=⌊q′⌋ and ⌊q⌋−q=0 if and only if ⌊q′⌋−q′=0. Figure 2 shows the set of possible equivalence classes of clock valuations for clocks x,y when c=2. Note that equivalent clock valuations satisfy the same clock constraints of the PTA. The set of regions needed for the region graph, denoted R, is the set of regions (l,α) such that there exists v∈α such that v⊨inv(l). The size of R is bounded by $|L| \cdot (2c+2)^{(|\mathcal {X}|+1)^{2}}$ (see [23]).

Fig. 2

Clock equivalence classes for two clocks x and y (c=2)

A region (l,α)∈R may have a time-successor, defined as follows. If v+t∈α for all v∈α and t∈ℝ_≥0, then the time-successor of (l,α) is (l,α) itself. Otherwise, there exists the unique region (l,β)≠(l,α) for which there are v∈α and t∈ℝ_≥0 such that v+t∈β and v+t′∈α∪β for all 0≤t′≤t. If additionally we have v+t′⊨inv(l) for all 0≤t′≤t, then (l,β) is the time-successor of (l,α), otherwise (l,α) has no time-successor.

The region graph for P and ϕ is the finite-state MDP $\mathsf {Reg}[{\mathsf {P},\phi}] = (R, (\overline {l},{[{\mathbf{0}}]}), \mathit {Act}\cup \{ \tau \}, {\mathit {Steps}}, {\mathit {lab}})$, where for each (l,α)∈R and a∈Act∪{τ}, we have Steps((l,α),a)=λ if and only if either:

• time transitions: a=τ, λ=μ _(l,β) and (l,β) is the time-successor of (l,α);

• action transitions: a∈Act, there is a ν∈α with ν⊨enab(l,a) and, for each (l′,β)∈R

  $$\lambda\bigl(l',\beta \bigr) = \mbox{$\sum$} \bigl\{ \big| \, \mathit {prob}(l,a) \bigl(X,l'\bigr) \, \big| \, X \in 2^\mathcal {X}\wedge \beta = \alpha [X{:=}0] \big|\bigr\} ; $$

and ${\mathit {lab}}(l,\alpha ) = \mathcal {L}(l)$ for all (l,α)∈R.

We now consider how Reg[P,ϕ] can be used to verify P against ϕ (recall that we consider the fragment of the logic without the ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\cdot]$ operator). For simplicity, we first assume that P is structurally divergent. Model checking proceeds in standard fashion (for a branching-time logic), recursing over subformulae ϕ′ of ϕ and computing Sat(ϕ′). Identifying states that satisfy atomic propositions, clock constraints or Boolean connectives is straightforward and time-bounded properties are dealt with using the reduction given in Sect. 4. Hence, we focus on formulae of the form P _⋈ p [ϕ ₁ U ϕ ₂]. If the state sets satisfying ϕ ₁ and ϕ ₂ have already been computed and the regions of Reg[P,ϕ] corresponding to these sets are labelled a ₁ and a ₂, respectively, then the states in [[P]] satisfying P _⋈ p [ϕ ₁ U ϕ ₂] are simply those in the regions corresponding to states in the MDP Reg[P,ϕ] that satisfy P _⋈ p [a ₁ U a ₂].

Thus, the region graph yields an algorithm for model checking structurally divergent PTAs against properties of the logic without the ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\cdot]$ operator. The algorithm runs in exponential time, because verifying properties of the form P _⋈ p [a ₁ U a ₂] on MDPs can be done in polynomial time [10, 20], and the size of the region graph Reg[P,ϕ] is exponential in the size of P (the size of P is the sum of the number of locations and clocks, the size of the binary encoding of the constants used in invariant and enabling conditions, and the size of the encoding of its transition probabilities, which are expressed as a ratio between two natural numbers, each in binary). The problem is EXPTIME-complete, where an EXPTIME lower bound can be obtained even for the restricted case in which the PTA has only two clocks (for PTAs with one clock, the model-checking problem for certain restricted classes of properties, such as PCTL properties or time-bounded until properties with probability thresholds 0 or 1 only, is PTIME-complete) [44].

We now consider the case where P is not structurally divergent. For P _≤p [ϕ ₁ U ϕ ₂] or P _<p [ϕ ₁ U ϕ ₂] (i.e., where maximum probabilities are needed), the method given above can be applied without further modification [63]. The case of P _≥p [ϕ ₁ U ϕ ₂] or P _>p [ϕ ₁ U ϕ ₂] (which needs minimum probabilities) is more involved. Intuitively, adversaries which can avoid reaching states satisfying ϕ ₂ only because they perform some non-divergent behaviour can result in the minimum probability of satisfying ϕ ₁ U ϕ ₂ computed over all adversaries being lower than the probability computed over divergent adversaries only. An algorithm that resolves this problem, based on the computation of the maximum probability of satisfying the dual path property ¬(ϕ ₁ U ϕ ₂), is presented in [63]. The model-checking problem remains EXPTIME-complete in this case. Details on model-checking algorithms for the strictly divergent adversaries described in Sect. 3 are also given in [63].

Finally, we note that region equivalence is an example of a time-abstracting bisimulation, a relation which combines time-abstracting bisimulation [3, 59] and (probabilistic) bisimulation [58, 62]. As with region equivalence, time-abstracting bisimilar PTA states satisfy the same formulae (without ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ formulae). An algorithm for computing a time-abstracting equivalence relation of a PTA, which may be coarser than region equivalence, has been presented in [28]. This approach is described as being applicable to formulae of the logic without ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ or P _⋈ p [ϕ ₁ U ^≤k ϕ ₂]; however, as explained in Sect. 4, time-bounded until properties can be reduced to unbounded until properties on a modified PTA.

5.2 The boundary region graph

The region graph construction presented above is not sufficient for verifying reward properties. In particular, we note that, for a particular region (l,α), the values $\smash{ \mathbb {E}_{\mathsf {P},s}^{\mathbf {r},\min }(\rho)}$ and $\smash{ \mathbb {E}_{\mathsf {P},s}^{\mathbf {r},\max }(\rho)}$ will generally not be uniform on states s∈(l,α). We now briefly describe a generalisation of the region graph, called the boundary region graph [43], which is a finite MDP equipped with a reward structure on which we can decide whether a particular state s of a PTA satisfies an $\smash{{\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {F}\ {\phi}]}$ property, under the restriction that there is no nesting of the $\smash{{\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\cdot]}$ operator and the bound ⋈ is non-strict. For $\smash{{\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {C}^{\le k}]}$ and $\smash{{\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {I}^{=k}]}$ properties, the reduction given in Sect. 4 can be used under the same restrictions.

The boundary region graph construction is an extension of the corner point abstraction for timed automata [24]. The underlying idea is that optimal behaviour (resulting in minimum or maximum expected rewards) corresponds to the case in which edge transitions of the PTA are taken either in a clock equivalence class in which the value of at least one clock equals an integer, or close to a boundary of a clock equivalence class in which the fractional parts of all clocks are positive: in this case, for computing the accumulation of rewards over time, it is necessary to distinguish which of the class’s boundaries is considered. Furthermore, the exact position on the clock equivalence boundaries is determined by the values of the clocks in the state s, and must also be encoded in the boundary region graph. The reward structure for the boundary region graph is derived directly from that of the PTA. From the boundary region graph (a finite-state MDP), we can compute the minimum or maximum expected accumulated reward to a target set (see, e..g [32]). We can then obtain either $\mathbb {E}_{\mathsf {P},s}^{\mathbf {r},\min }(\mathtt {F}\ {\phi})$ or $\mathbb {E}_{\mathsf {P},s}^{\mathbf {r},\max }(\mathtt {F}\ {\phi})$ and hence decide whether s satisfies ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {F}\ {\phi}]$.

5.3 Digital clocks

Region graph-based approaches are not usually practically applicable since the region graphs are generally of a prohibitive size. Thus, various other PTA model checking approaches have been developed. We first describe the digital clocks method [52], which restricts the standard continuous-time semantics of a PTA so that only time transitions of duration 1 occur. This means that clocks take only integer, rather than real, values. Using this fact, and knowing there is a maximal constant c _x to which each clock x is compared in PTA P and property ϕ, we can again build and analyse a finite-state MDP. This approach builds on the use of digital clocks for (non-probabilistic) timed automata verification [8, 19, 39].

The digital clocks method is applicable to properties of the form P _⋈ p [ψ] and ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ without nesting of further P _⋈ p [⋅] and ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\cdot]$ operators within the subformulae ψ and ρ (see [52] for an explanation as to this limitation). It can only be used to determine satisfaction in states where all clocks take natural-numbered values, and we will restrict our attention to checking satisfaction in the initial state. The correctness of the digital clocks method also relies on the assumption that P and ϕ are closed, meaning that all clock constraints of the form x≤d or d≤x are contained within an even number of negations. Furthermore, all invariant and enabling conditions of P are assumed to be diagonal-free , meaning that constraints of the form x+c≤y+d are not permitted. Any PTA can be transformed into one containing only diagonal-free constraints by applying the construction of [15] (the construction is presented for timed automata, and requires minor modifications for PTAs).

For a digital clock valuation $v \in {\mathbb {N}}^{\mathcal {X}}$, let v⊕1 be the clock valuation such that (v⊕1)(x)=min{v(x)+1,c _x +1} for all $x \in \mathcal {X}$. The digital clock semantics of P and ϕ is defined as for the standard semantics, except that the rule for time transitions restricts durations to 1, and each clock x can increase to at most c _x +1. Formally, the digital clock semantics of a closed PTA P is defined as the finite-state MDP $\mathsf {Dgt}({\mathsf {P},\phi})=(S,(\overline {l},\mathbf{0}),\mathit {Act}\cup \{ 1 \},{\mathit {Steps}},{\mathit {lab}})$ where:

• $S = \{ (l,v) \in L\times {\mathbb {N}}^{\mathcal {X}} \, | \, v \models \mathit {inv}(l) \wedge (\forall x \in \mathcal {X}. \, v(x) \leq c_{x} + 1) \}$;

• Steps((l,v),a)=λ if and only if either:

  • time transitions: a=1, v⊕1⊨inv(l) and λ=μ _(l,v⊕1);

  • action transitions: a∈Act, v⊨enab(l,a), and, for any (l′,v′)∈S:

    $$\lambda\bigl(l',v'\bigr) = \sum \bigl\{ \big|\mathit {prob}(l,a) \bigl(X,l'\bigr) \, | \, X \in 2^\mathcal {X}\wedge v' = v[X{:=}0] \big| \bigr\} ; $$

• ${\mathit {lab}}(l,v) = \mathcal {L}(l)$ for each (l,v)∈S.

The number of states of the digital clock semantics of P is bounded by $|L| \cdot \prod_{x \in \mathcal {X}} (c_{x}+ 1)$.

Model checking for formulae of the form P _⋈ p [ψ] and ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ without nesting can then be carried out directly on the finite MDP from the digital clock semantics. For P _⋈ p [ψ] formulae, we proceed as in the case of the region graph in Sect. 5.1. For a formula ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\mathtt {F}\ {\phi}]$ formulae and PTA reward structure r=(r _Act ,r _L ), we proceed as follows. We construct the reward structure r=(r _S ,r _Act ) where r _S (l,v)=0, r _Act ((l,v),1)=r _L (l) and r _Act ((l,v),a)=r _Act (l,a) for all (l,v)∈S and a∈Act. We then use standard algorithms for MDPs to compute the minimum or maximum expected reward to reach the set of states Sat(ϕ). The cases for ρ=C ^≤k and ρ=I ^=k use the reductions presented in Sect. 4.

5.4 Backwards reachability

The next method we consider is backwards reachability [56], which provides model checking for properties without ${\mathtt{R}}^{\mathbf {r}}_{\,\bowtie \,q}[\rho]$ operators. This is based on the repeated application of a predecessor operation that, given a set of states S′, returns the set of states that can reach S′ by performing an action and then letting time pass. Sets of states are represented by symbolic states, pairs z=(l,ζ) comprising a location l and a clock constraint ζ over $\mathcal {X}$, representing the set of states {(l,v) | v⊨ζ}.

This approach is an adaptation of the algorithm in [40] for model checking timed automata. Whereas the latter just requires iteration of a generic predecessor operation, for PTAs it is necessary to retain information about the probabilities of the PTA edges used along paths. First, the predecessor operation is parameterised by actions and edges of the PTA. Then, as the predecessor iteration proceeds, a graph is constructed, where the nodes are the generated symbolic states, and an edge is added from symbolic state z to symbolic state z′ if z was generated from z′ by a predecessor operation. The edge (z,z′) is labelled by the corresponding action and PTA edge. The symbolic states generated in this manner do not form a partition of the state space of the PTA, unlike the region graph or time-abstracting bisimulation approaches described in Sect. 5.1.

After the iteration of predecessor operations terminates (which is guaranteed because a symbolic state corresponds to a union of regions), the obtained graph can then be used as a basis for the construction of a finite MDP. To build the probabilistic transition function, information has to be combined from different symbolic states in order to obtain the exact combination of PTA edges (corresponding to a particular action) available in states of the PTA. This is done by computing the conjunctions of symbolic states which have at least one outgoing edge labelled with the same action, and adding the corresponding graph edges to the newly generated symbolic states. For more information, see [56].

The approach outlined above only applies to P _⋈p [ψ] operators where ⋈ ∈{≤,<}, i.e. it computes only maximum probabilities for the PTA. For the case ⋈ ∈{≥,>}, which needs minimum probabilities, the method needs to be adapted [56]. Like the reduction described in Sect. 5.1 for the region graph approach on non-structurally-divergent PTAs, the solution taken in [56] works by considering the dual formula.

5.5 Abstraction refinement using stochastic games

The final model checking technique we discuss for PTAs is abstraction refinement using stochastic games, which can verify P _⋈ p [ψ] properties via computation of reachability probabilities. This approach uses the game-based notion of abstraction put forward for MDPs in [49] and the corresponding refinement techniques proposed in [46]. The method can be applied to PTAs containing diagonal-free constraints only, because one of its procedures is a (forwards) reachability exploration and, by the results of Bouyer [22], such a procedure is only correct if the considered PTA is diagonal-free.

The idea of [49] is to build an abstraction of a large or infinite-state MDP based on a finite partition of its state space. Abstractions take the form of stochastic two-player games, a generalisation of MDPs in which there are two distinct types of nondeterminism, each controlled by a separate player. In this case, player 1 controls nondeterminism introduced by the abstraction, and player 2 controls nondeterminism from the original MDP. An analysis of the optimal probabilities in the stochastic game (e.g. the maximum probability that player 1 can achieve for some objective, assuming that player 2 aims to minimise it) yields lower and upper bounds on reachability probabilities for the original MDP.

The abstraction-refinement framework of [46] provides a way to automatically construct stochastic game abstractions, by iteratively refining abstractions until the difference between the lower and upper bounds produced is below some desired level of precision ε. In [50], this technique is adapted to an algorithm to compute exact (minimum or maximum) reachability probabilities for PTAs. First, a reachability graph is constructed, based on a successor operation that returns the set of states that can be reached by performing an action and then letting time pass. This works in a similar style to the classic approach to verifying (non-probabilistic) timed automata. From this, a stochastic game abstraction is created, over symbolic states of the same form as in Sect. 5.4. The abstraction is repeatedly analysed and refined until the exact required probabilities are obtained (i.e. ε=0). The iterative refinement process is guaranteed to terminate thanks to the fact that there is an underlying finite time-abstracting bisimulation quotient, namely the region graph.

5.6 A comparison of the methods

We briefly summarise the relative merits of the three practical approaches to PTA model checking discussed above. In terms of applicability, digital clocks is currently the only method for computing expected rewards, but handles only closed (non-strict) and diagonal-free clock constraints. The other limitations of the remaining two methods are that abstraction refinement only applies to PTAs with diagonal-free clock constraints, and backwards reachability requires (non-trivial) adaptation to compute minimum probabilities.

In terms of efficiency and scalability, the digital clocks approach has proved to work well in practice, but performance suffers for large numbers of clocks or when large constants appear in the clock constraints; in these cases, the other two methods described have been shown to work better. The techniques based on parameter synthesis of [7] can be used to reduce the size of the constants of clock constraints for subclasses of PTAs and for probabilistic properties without time bounds. Another good approach to improving performance is the use of symbolic (binary decision diagram based) implementations. The original implementation of backward reachability [56] showed that it yielded relatively small MDPs, but that the algorithm can be expensive to implement. Experimental results for abstraction refinement [50] later demonstrated better performance in all cases. However, subsequent optimisations presented for backwards reachability [18] have led to much better performance, improving on abstraction refinement in many cases.

5.7 Implementations and tool support

Thanks to increasing interest in the verification of probabilistic real-time systems, a variety of related software tools have recently been developed. The probabilistic model checker PRISM [51], for example, which provides verification of Markov chains and MDPs, now also supports PTAs, via the digital clocks, backwards reachability and abstraction-refinement methods. A second tool is mcpta [38], which applies the digital clocks method to translate a subset of the modelling language Modest [21] directly into the PRISM modelling language.

Fortuna [18] is a tool that focuses on PTAs augmented with prices (called rewards in this paper). In particular, it implements the semi-algorithm of [17] for computing the maximum probability of reaching a target while accumulating a reward below a given threshold (this problem is shown to be undecidable in [16]). Since this algorithm generalises the backwards reachability method of [56], computation of (maximum) reachability probabilities is also supported. Several optimisations of the basic algorithm are also implemented. Finally, UPPAAL PRO [68] is an extension of the popular timed automaton verifier UPPAAL. It computes the maximum probability of reaching a set of target states of a PTA, by progressively partitioning the state space, constructing and solving a finite MDP at each step.

6 Case studies

PTAs have been used for the modelling and analysis of a wide variety of systems, including communication protocols [33, 55], aviation security systems [34], streaming download protocols [69] and service level agreements [48]. In this section, we give an illustration of the PTA model checking techniques described in this paper by presenting two case studies: a non-repudiation protocol and a task-graph scheduling problem.

6.1 Markowitch & Roggeman’s non-repudiation protocol

This case study analyses Markowitch & Roggeman’s non-repudiation protocol for information transfer [61]. Our models extend those presented previously in [57]. One party, the originator, sends information to a second party, the recipient. Repudiation is defined as the denial of either party of having participated in all or part of the information transfer. For example, in electronic commerce, if the information represents the transfer of a service, then non-repudiation ensures the client (the recipient) cannot deny receiving the service as a reason for non-payment.

The protocol of Markowitch & Roggeman is probabilistic and does not require a trusted third party. It achieves the following non-repudiation properties:

• “ε-fair”: at each step of the protocol run, either both parties receive their expected items, or the probability that a cheating party gains any valuable information about its expected items and the other party gains nothing is at most ε;

• “time-bounded”: if at least one party behaves correctly, then the protocol will complete within a finite amount of time (with probability 1);

• “viable”: if both parties behave correctly and finish the protocol, then they both receive their expected items at the end of the protocol (with probability 1).

The steps of the protocol are outlined in Fig. 3. First, to prevent replay attacks, the recipient R selects a date D which it sends, along with a request, to the originator O. Next, O randomly selects an integer n representing the number of steps of the protocol (which is never revealed to R during the execution) and computes functions f _i such that their composition satisfies the following:

$$f_n(\mathit{message}) \circ \bigl( f_{n-1} ( \mathit{message}) \circ \bigl(\cdots \circ \bigl(f_2(\mathit{message}) \circ f_1(\mathit{message}) \bigr)\cdots \bigr)\bigr) = \mathit{message}. $$

The composition operator ∘ needs to be non-commutative to ensure that the recipient cannot start to compute the message until the final message f ₁(message) has been received.

Fig. 3

The steps of Markowitch & Roggeman’s non-repudiation protocol

To prevent the recipient from gaining an advantage, if the originator does not receive an acknowledgement within a certain time bound (denoted AD), the protocol is stopped and the originator states that the recipient is trying to cheat. The time bound is chosen such that it is greater than the time it takes for a recipient to send a reply, but is not sufficient for the recipient to be able to compute the composition f _n (message)∘(⋯∘f _i (message)⋯) for any i<n, i.e., the recipient does not have time to check if it has received the complete message before sending an acknowledgement.

We consider two different versions of the protocol. In the first, both the originator and recipient act honestly, while in the second the recipient can act maliciously (i.e., stop early by not returning an acknowledgement). For each, we assume that the choice of n is made by the recipient according to a geometric distribution with parameter p and the minimum time for the recipient to send an acknowledgement is ad. For the malicious version, we consider two variants. The first corresponds to the one described in [61], where the only malicious behaviour corresponds to stopping early. In the second, we introduce a more powerful malicious recipient, which has access to a method that takes time less than AD and with probability $\frac{1}{4}$ correctly computes the composition while with probability $\frac{3}{4}$ fails to compute the composition.

Each model is the parallel composition of two PTAs, one representing the originator and one the recipient. These synchronise on the actions rec, send and ack, corresponding to the recipient initiating the transaction, the originator sending messages to the recipient and the recipient sending acknowledgements back. The PTAs for the originator and (honest) recipient are shown in Fig. 4. The probabilistic choice in the originator correctly models selection of n according to a geometric distribution with parameter p, since the probability of each message being the last one to be sent is p. Notice that, in the PTA for the honest recipient, an acknowledgement is sent after between ad and AD time units.

Fig. 4

PTAs used to model the non-repudiation protocol

We analysed these PTA models in PRISM using the stochastic games technique (since the originator PTA contains strict inequalities, the digital clocks method is not applicable). For the analysis, we assume AD=5 and ad=1.

For the honest version of the protocol, the first property we consider is “time-bounded”. More precisely, we check the formula ${\mathtt{P}}_{\mathtt{\geq 1}} [ {{\mathtt{F}}\ }\mathsf{done} ]$, stating that the minimum probability of the protocol terminating correctly is 1. Next, we investigate the performance of the protocol with the quantitative properties ${\mathtt{P}}_{\mathtt{min=?}} [ {{\mathtt{F}}\ }^{\leq T} \mathsf{done} ]$ and ${\mathtt{P}}_{\mathtt{max=?}} [ {{\mathtt{F}}\ }^{\leq T} \mathsf{done} ]$, i.e., the minimum and maximum probability of termination by time T. Figure 5 plots these values for T between 0 and 100, with p=0.01 and p=0.1. We see that increasing the parameter p improves the performance of the protocol when the parties behave honestly. However, as we shall see below, when the recipient behaves maliciously, increasing this parameter comes at a cost since it also increases the likelihood that the recipient gains an advantage.

Fig. 5

Probability that the protocol terminates successfully by time T (honest version)

For the two models with a malicious recipient, we find that the minimum and maximum probability of the protocol terminating correctly (${\mathtt{P}}_{\mathtt{min=?}} [ {{\mathtt{F}}\ }\mathsf{done} ]$ and ${\mathtt{P}}_{\mathtt{max=?}} [ {{\mathtt{F}}\ }\mathsf{done} ]$) are 0 and 1, respectively. The minimum probability is achieved when the (malicious) recipient returns no acknowledgements at all and the maximum when it acts honestly.

Figure 6 presents results for the properties ${\mathtt{P}}_{\mathtt{max=?}} [ {{\mathtt{F}}\ }\mathsf{unfair} ]$ and ${\mathtt{P}}_{\mathtt{max=?}} [ {{\mathtt{F}}\ }^{\leq T} \mathsf{unfair} ]$, for both variants of the malicious recipient and several values of parameter p. These correspond to the maximum probability that the recipient (eventually, or within time bound T) gains an advantage. For the first variant (describing the scenario in [61]), Fig. 6(a) shows that the protocol is indeed ε-fair with ε equal to p. Essentially, all this recipient can do to gain knowledge is to correctly guess which message is the last (which, when a message arrives, is true with probability p). As shown in Fig. 6(b), the probability of gaining an advantage over time remains constant after the arrival of the first message: since each message has an equal chance of being the last, there is nothing to be gained by waiting for a later one. The figures also show that the malicious recipient in the second variant of the model (which has a chance of correctly decoding the message before the deadline AD) has a greater chance of gaining knowledge, thanks to its additional power.

Fig. 6

Maximum probability that the recipient gains knowledge (malicious versions)

6.2 Task-graph scheduling

One common use of (non-probabilistic) timed automata is the formalisation and solution of scheduler optimisation problems. In this case study, we consider an extension of the task-graph scheduling problem described in [27]. We show how PTAs can be used to introduce uncertainty with regards to time delays and to consider the possibility of failures. We demonstrate how the digital clocks method can determine optimal schedulers for these problems, in terms of the (expected) time and energy consumption required to complete all tasks.

The basic model

First, we introduce the basic problem formalisation and model presented in [27]. This considers the example of evaluating the expression D×(C×(A+B))+((A+B)+(C×D)), where its subterms are evaluated on two processors, P ₁ and P ₂. Processor P ₁ is faster than P ₂, but also consumes more energy. Figure 7(a) shows the specifications of the processors, in terms of their processing times and energy usage for addition and multiplication operations. Figure 7(b) presents the task graph for this example, illustrating the set of tasks (corresponding to subterms of the expression) and the dependencies that exist between tasks (in terms of their required order of evaluation).

Fig. 7

Scheduling problem for computing the term D×(C×(A+B))+((A+B)+(C×D))

In [27], a (non-probabilistic) timed automaton model is built, consisting of the parallel composition of one automaton for each processor and one automaton for the scheduler which decides when tasks get performed and on which processors. The scheduler automaton includes integer-valued variables to indicate whether a task still has to be processed, is currently being processed or has been completed. To ensure that the restrictions of the task graph are met, there are conditions placed on enabling conditions such that a task cannot be scheduled until all of its dependencies have been computed.

The timed automaton for processor P ₁ is given in Fig. 8(a). The actions $\mathit{p1\_add}$ and $\mathit{p1\_mult}$ correspond to an addition and multiplication task being started on P ₁, and $\mathit{p1\_done}$ indicates the completion of a task. The clock x is used to record the time that a task has been running and is initialised when a task is started. The automaton for P ₂ is similar except that the action names change and the delays are modified to reflect the values in Fig. 7(a).

Fig. 8

PTAs for the task-graph scheduling case study

The time and energy consumed to complete all tasks are modelled as rewards (called prices in [27]). We introduce reward structures time and energy, respectively, to represent each of these quantities. For the case of time, only the scheduler automaton has a non-zero reward structure, where the location reward is 1 in each location and all action rewards are zero. For the case of energy consumption, the scheduler automaton has a zero reward structure, while each processor has a location reward equal to the current rate of energy usage (as shown in Fig. 7(a)) and has zero action rewards.

We built a PTA model for this case study using PRISM and, by applying the digital clocks method, calculated both the minimum (expected) time and energy consumption for completion of all tasks. For this, we used the two quantitative reward properties ${\mathtt{R}}^{\mathtt{time}}_{\mathtt{min=?}}[ \mathtt {F}\ {\mathsf{complete}} ]$ and ${\mathtt{R}}^{\mathtt{energy}}_{\mathtt{min=?}}[ \mathtt {F}\ {\mathsf{complete}} ]$. We also used PRISM to generate the corresponding schedulers that achieve these optimal values. The results agree with those reported in [27]. A scheduler that minimises the elapsed time requires 12 picoseconds to complete all tasks and schedules the tasks as follows:

On the other hand, a scheduler optimising the energy consumption requires 1.3200 nanojoules (and 19 picoseconds) and makes the following scheduling decisions:

Due to the additional energy consumption of processor P ₁, the first scheduler above, which optimises the time for task completion, requires 1.3900 nanojoules.

Random task execution times

Now, we extend the formalisation of the task-graph problem, making the time required for each processor to perform a task probabilistic (in a more general setting, we can easily envisage situations where the exact time required to complete a task is unknown, but can be represented by some probability distribution). More precisely, we consider the following simple scenario. If, in the original problem the time for a processor to perform a task was k∈ℕ, we suppose now that the time taken is uniformly distributed between the delays k−1, k and k+1, e.g. the time for P ₁ to perform a multiplication operation is either 1, 2 or 3 and the probability of each execution time is $\frac{1}{3}$.

The PTA for processor P ₁ with random delays is presented in Fig. 8(c) where, to ease notation, we have omitted action labels if they do not synchronise. Additional locations are added to encode the random delays. For example, in the case of multiplication, with probability $\frac{1}{3}$ the task completes after 2 time units; with probability $\frac{2}{3}$, the PTA moves to a location where, with probability $\frac{1}{2}$ the task completes after 1 additional time unit (i.e., of a total of 3 time units) or moves to a location where the task completes after 2 more time units (i.e., 4 time units in total). When the task completes, the PTA moves to a location where no time can pass (clock x is reset upon entering and the invariant of the location is x≤0) and immediately notifies the scheduler the task is computed through action $\mathit{p1\!\_done}$. To prevent the scheduler from seeing into the future when making decisions, the probabilistic choice for task completion is made on completion rather than on initialisation.

Analysing this model, we find that the optimal expected time and energy consumption to complete all tasks equals 12.226 picoseconds and 1.3201 nanojoules, respectively. This improves on the results obtained using the optimal schedulers for the original model, where the expected time and energy consumption equal 13.1852 picoseconds and 1.3211 nanojoules. Examining the optimal schedulers, we find that they change their decision based upon the delays of previously completed tasks. For example, for elapsed time, the optimal scheduler starts as for the non-probabilistic case, first scheduling task1 followed by task3 on P ₁ and task2 on P ₂. However, it is now possible for task2 to complete before task3 (if the execution times for task1, task2 and task3 are 3, 6 and 4 respectively), in which case the optimal scheduler now makes a different decision from the non-probabilistic case. Under one possible set of execution times for the remaining tasks, the optimal scheduling is as follows:

Adding a faulty processor

As a second extension of the scheduling problem, we add a third processor P ₃ which consumes the same energy as P ₂ but is faster (addition takes 3 picoseconds and multiplication 5 picoseconds). However, this comes at a cost: there is a chance (probability p) that the processor fails and the computation must be rescheduled and performed again.

In Fig. 8(b), we show the PTA for the faulty version of processor P ₁. In this PTA, when a task completes, there is a probabilistic choice between moving to a location corresponding to successful completion and one to failure. In both cases, we move to a location where no time can pass and immediate notify the scheduler of either the success or failure of the computation. The automaton for the scheduler also changes for this model since it must react to the failure signals from the processors. In addition, the reward structure energy is extended to include the energy consumed by the additional processor.

The graphs in Fig. 9 plot the optimal expected time and energy consumption for this extended model as the failure probability p varies. The dashed lines show the optimal results for the original model, i.e., when not using the processor P ₃. As can be seen, once the probability of failure becomes sufficiently large, there is no gain in using the processor P ₃ but, while when the probability of failure is small, it uses offers considerable gains in performance. To illustrate this fact, below we give a scheduler that optimises (minimises) the expected energy consumption when p=0.5. Dark boxes for tasks are used to denote processor P ₃ failing to complete a task correctly, meaning that the task needs to be rescheduled.

Notice that the scheduler uses the processor P ₃ for task1 and, if this task is completed successfully, it later uses P ₃ for task4. However, if task1 fails to complete, P ₃ is not used again.

Fig. 9

Optimal expected time and energy consumption as the failure probability of processor P ₃ varies

7 Conclusions

In this paper, we have presented an introduction to the model of probabilistic timed automata and summarised the various techniques developed to perform probabilistic model checking. Verification of probabilistic real-time systems is an active field of research and further progress is required in several important directions. Examples include the development of verification techniques for probabilistic timed games [6, 43] and for probabilistic hybrid automata [9, 36, 64]. The former have proved, in the non-probabilistic setting, to being applicable to a variety of useful synthesis problems [12]. The latter provide essential modelling capabilities for domains such as embedded systems and cyber-physical systems; they represent a useful, but more tractable, subclass of the model of stochastic hybrid automata. Other important issues to investigate in the context of PTAs include robustness [7] and continuously-distributed time delays [1, 53, 60].