Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

Abstract

Probabilistic timed automata (PTAs) are timed automata (TAs) extended with discrete probability distributions. They serve as a mathematical model for a wide range of applications that involve both stochastic and timed behaviours. In this work, we consider the problem of model-checking linear dense-time properties over PTAs. In particular, we study linear dense-time properties that can be encoded by TAs with infinite acceptance criterion. First, we show that the problem of model-checking PTAs against deterministic-TA specifications can be solved through a product construction. Based on the product construction, we prove that the computational complexity of the problem with deterministic-TA specifications is EXPTIME-complete. Then we show that when relaxed to general (nondeterministic) TAs, the model-checking problem becomes undecidable. Our results substantially extend state of the art with both the dense-time feature and the nondeterminism in TAs.

1 Introduction

Stochastic timed systems are systems that exhibit both timed and stochastic behaviours. Such systems play a dominant role in many applications [1], hence addressing fundamental issues such as safety and performance over these systems are important. Probabilistic timed automata (PTAs) [2,3,4] serve as a good mathematical model for these systems. They extend the well-known model of timed automata [5] (for nonprobabilistic timed systems) with discrete probability distributions, and Markov Decision Processes (MDPs) [6] (for untimed probabilistic systems) with timing constraints.

Formal verification of PTAs has received much attention in recent years [2]. For branching-time model-checking of PTAs, the problem is reduced to computation of reachability probabilities over MDPs through well-known finite abstraction for timed automata (namely regions and zones) [3, 4, 7]. Advanced techniques for branching-time model checking of PTAs such as inverse method and symbolic method have been further explored in [8,9,10,11]. Extension with cost or reward, resulting in priced PTAs, has also been well investigated. Jurdzinski et al. [12] and Kwiatkowska et al. [13] proved that several notions of accumulated or discounted cost are computable over priced PTAs, while cost-bounded reachability probability over priced PTAs is shown to be undecidable by Berendsen et al. [14]. Most verification algorithms for PTAs have been implemented in the model checker PRISM [15]. Computational complexity of several verification problems for PTAs has been studied, for example, [12, 16, 17].

For linear-time model-checking, much less is known. As far as we know, the only relevant result is by Sproston [18] who proved that the problem of model-checking PTAs against linear discrete-time properties encoded by untimed deterministic omega-regular automata (e.g., Rabin automata) can be solved by a product construction. In his paper, Sproston first devised a production construction that produces a PTA out of the input PTA and the automaton; then he proved that the problem can be reduced to omega-regular verification of MDPs through maximal end components.

In this paper, we study the problem of model-checking linear dense-time properties over PTAs. Compared with discrete-time properties, dense-time properties take into account timing constraints, and therefore is more expressive and applicable to time-critical systems. Simultaneously, verification of dense-time properties is more challenging since it requires to involve timing constraints. The extra feature of timing constraints also brings more theoretical difficulty, e.g., timed automata [5] (TAs) are generally not determinizable, which is in contrast to untimed automata (such as Rabin or Muller automata).

We focus on linear dense-time properties that can be encoded by TAs. Due to the ability to model dense-time behaviours, TAs can be used to model real-time systems, while they can also act as language recognizers for timed omega-regular languages. Here we treat TAs as language recognizers for timed paths from a PTA, and study the problem of computing the minimum or maximum probability that a timed path from the PTA is accepted by the TA. The intuition is that a TA can recognize the set of “good” (or “bad”) timed paths emitting from a PTA, so the problem is to compute the probability that the PTA behaves in a good (or bad) manner. The relationship between TAs and linear temporal logic (e.g., Metric Temporal Logic [19]) is studied in [20, 21].

Our Contributions. We distinguish between the subclass of deterministic TAs (DTAs) and general nondeterministic TAs. DTAs are the deterministic subclass of TAs. Although the class of DTAs is weaker than general timed automata, it can recognize a wide class of formal timed languages, and express interesting linear dense-time properties which cannot be expressed in branching-time logics (cf. [22]). We consider Rabin acceptance condition as the infinite acceptance criterion for TAs. We first show that the problem of model-checking PTAs against DTA specifications with Rabin acceptance condition can be solved through a nontrivial product construction which tackles the integrated feature of timing constraints and randomness. From the product construction, we further prove that the problem is EXPTIME-complete. Then we show that the problem becomes undecidable when one considers general TAs. Our results substantially extend previous ones (e.g. [18]) with both the dense-time feature and the nondeterminism in TAs.

Due to lack of space, detailed proofs of several results and some experimental results are put in the full version  [23].

2 Preliminaries

We denote by $\mathbb {N}$, $\mathbb {N}_0$, $\mathbb {Z}$, and $\mathbb {R}$ the sets of all positive integers, non-negative integers, integers and real numbers, respectively. For any infinite word $w=b_0b_1\dots$ over an alphabet $\varSigma$, we denote by ${\textit{inf} (w )}$ the set of symbols in $\varSigma$ that occur infinitely often in w. A clock is a variable for a nonnegative real number. Below we fix a finite set $\mathcal {X}$ of clocks.

Clock Valuations. A clock valuation is a function $\nu :\mathcal {X}\rightarrow [0,\infty )$. The set of clock valuations is denoted by $\textit{Val}\left( \mathcal {X}\right)$. Given a clock valuation $\nu$, a subset $X\subseteq \mathcal {X}$ of clocks and a non-negative real number t, we let (i) ${\nu }{\left[ X:=0\right] }$ be the clock valuation such that ${\nu }{\left[ X:=0\right] }(x)=0$ for $x\in X$ and ${\nu }{\left[ X:=0\right] }(x)=\nu (x)$ otherwise, and (ii) ${\nu }{\,+\,}{t}$ be the clock valuation such that $({\nu }{\,+\,}{t})(x)=\nu (x)+t$ for all $x\in \mathcal {X}$. We denote by $\mathbf {0}$ the clock valuation such that $\mathbf {0}(x)=0$ for $x\in \mathcal {X}$.

Clock Constraints. The set ${\textit{CC}\left( \mathcal {X}\right) }$ of clock constraints over $\mathcal {X}$ is generated by the following grammar: $\phi :=~\mathbf {true}~\mid ~x\le d~\mid ~c\le x~\mid ~x+c\le y+d~\mid ~\lnot \phi ~\mid ~\phi \wedge \phi$ where $x,y\in \mathcal {X}$ and $c,d\in \mathbb {N}_0$. We write $\mathbf {false}$ for a short hand of $\lnot \mathbf {true}$. The satisfaction relation $\models$ between valuations $\nu$ and clock constraints $\phi$ is defined through substituting every $x\in \mathcal {X}$ appearing in $\phi$ by $\nu (x)$ and standard semantics for logical connectives. For a given clock constraint $\phi$, we denote by ${\llbracket }{\phi }{\rrbracket }$ the set of all clock valuations that satisfy $\phi$.

2.1 Probabilistic Timed Automata

A discrete probability distribution over a countable non-empty set U is a function $q:U\rightarrow [0, 1]$ such that $\sum _{z\in U}q(z)=1$. The support of q is defined as ${\textit{supp}}(q):=\{z\in U\mid q(z)>0\}$. We denote the set of discrete probability distributions over U by ${\mathcal {D}}{\left( U\right) }$.

Definition 1

(Probabilistic Timed Automata [2]). A probabilistic timed automaton (PTA) $\mathcal {C}$ is a tuple

$$\begin{aligned} \mathcal {C}=\left( L, \ell ^*, \mathcal {X}, \textit{Act}, \textit{inv}, \textit{enab}, {\textit{prob}}, { AP}, \mathcal {L}\right) \end{aligned}$$

(1)

where:

• $L$ is a finite set of locations;

• $\ell ^*\in L$ is the initial location;

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

• $\textit{Act}$ is a finite set of actions;

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

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

• ${\textit{prob}}:L\times \textit{Act}\rightarrow {\mathcal {D}}{\left( 2^{\mathcal {X}}\times L\right) }$ is a probabilistic transition function;

• ${ AP}$ is a finite set of atomic propositions;

• $\mathcal {L}:L\rightarrow 2^{{ AP}}$ is a labelling function.

W.l.o.g, we consider that both $\textit{Act}$ and ${ AP}$ is disjoint from $[0,\infty )$. Below we fix a PTA $\mathcal {C}$. The semantics of PTAs is as follows.

States and Transition Relation. A state of $\mathcal {C}$ is a pair $(\ell , \nu )$ in $L\times \textit{Val}\left( \mathcal {X}\right)$ such that $\nu ~\models ~ \textit{inv}(\ell )$. The set of all states is denoted by $S_\mathcal {C}$. The transition relation $\rightarrow$ consists of all triples $((\ell ,\nu ),a,(\ell ',\nu '))$ satisfying the following conditions:

• $(\ell ,\nu ), (\ell ',\nu ')$ are states and $a\in \textit{Act}\cup [0,\infty )$;

• if $a\in [0,\infty )$ then $\nu +\tau \models \textit{inv}(\ell )$ for all $\tau \in [0, a]$ and $(\ell ',\nu ')=(\ell ,\nu +a)$;

• if $a\in \textit{Act}$ then $\nu \models \textit{enab}(\ell ,a)$ and there exists a pair $(X, \ell '')\in {\textit{supp}}({\textit{prob}}(\ell ,a))$ such that $(\ell ',\nu ')=(\ell '',{\nu }{\left[ X:=0\right] })$.

By convention, we write ${s}{\xrightarrow {a}}{s'}$ instead of $(s,a,s')\in \rightarrow$. We omit ‘$\mathcal {C}$’ in ‘$S_\mathcal {C}$’ if the underlying context is clear.

Probability Transition Kernel. The probability transition kernel $\mathbf {P}$ is the function $\mathbf {P}:S\times \textit{Act}\times S\rightarrow [0, 1]$ such that

$$\begin{aligned}&\mathbf {P}((\ell ,\nu ),a,(\ell ',\nu ')) = {\left\{ \begin{array}{ll} 1 &{} \text{ if } {(\ell ,\nu )}{\xrightarrow {a}}{(\ell ',\nu ')} \text{ and } a\in [0,\infty )\\ \sum _{Y\in B}{\textit{prob}}(\ell ,a)(Y,\ell ') &{} \text{ if } {(\ell ,\nu )}{\xrightarrow {a}}{(\ell ',\nu ')} \text{ and } a\in \textit{Act}\\ 0 &{} \text{ otherwise } \end{array}\right. } \end{aligned}$$

where $B:=\{X\subseteq \mathcal {X}\mid \nu '={\nu }{\left[ X:=0\right] }\}$.

Well-formedness. We say that $\mathcal {C}$ is well-formed if for every state $(\ell ,\nu )$ and action $a\in \textit{Act}$ such that $\nu \models \textit{enab}(\ell ,a)$ and every $(X,\ell ')\in {\textit{supp}}({\textit{prob}}(\ell ,a))$, one has that ${\nu }{\left[ X:=0\right] }\models \textit{inv}(\ell ')$. The well-formedness is to ensure that when an action is enabled, the next state after taking this action will always be legal. In the following, we always assume that the underlying PTA is well-formed. Non-well-formed PTAs can be repaired into well-formed PTAs [9].

Paths. A finite path $\rho$ (under $\mathcal {C}$) is a finite sequence $\left\langle s_0,a_0,s_1,\dots ,a_{n-1},s_n\right\rangle ~~(n\ge 0)$ in $S\times {\left( (\textit{Act}\cup [0,\infty ))\times S\right) }^*$ such that (i) $s_0=(\ell ^*,\mathbf {0})$, (ii) $a_{2k}\in [0,\infty )$ (resp. $a_{2k+1}\in \textit{Act}$) for all integers $0\le k\le \frac{n}{2}$ (resp. $0\le k\le \frac{n-1}{2}$) and (iii) for all $0\le k\le n-1$, ${s_k}{\xrightarrow {a_k}}{s_{k+1}}$. The length $\left| \rho \right|$ of $\rho$ is defined by $\left| \rho \right| :=n$. An infinite path (under $\mathcal {C}$) is an infinite sequence $\left\langle s_0,a_0,s_1,a_1,\dots \right\rangle$ in ${\left( S\times (\textit{Act}\cup [0,\infty ))\right) }^\omega$ such that for all $n\in \mathbb {N}_0$, the prefix $\left\langle s_0,a_0,\dots ,a_{n-1},s_n\right\rangle$ is a finite path. The set of finite (resp. infinite) paths under $\mathcal {C}$ is denoted by ${\textit{Paths}^*_{\mathcal {C}}}$ (resp. ${\textit{Paths}^\omega _{\mathcal {C}}}$).

Schedulers. A (deteterministic) scheduler is a function $\sigma$ from the set of finite paths into $\textit{Act}\cup [0,\infty )$ such that for all finite paths $\rho =s_0a_0\dots s_n$, (i) $\sigma (\rho )\in \textit{Act}$ (resp. $\sigma (\rho )\in [0,\infty )$) if n is odd (resp. even) and (ii) there exists a state $s'$ such that ${s_n}{\xrightarrow {\sigma (\rho )}}{s'}$.

Fig. 1.

A simple task-processing example

Fig. 2.

A DTRA specification

Paths under Schedulers. A finite path $s_0a_0\dots s_n$ follows a scheduler $\sigma$ if for all $0\le m< n$, $a_m=\sigma \left( s_0a_0\dots s_m\right)$. An infinite path $s_0a_0s_1a_1\dots$ follows $\sigma$ if for all $n\in \mathbb {N}_0$, $a_n=\sigma \left( s_0a_0\dots s_n\right)$. The set of finite (resp. infinite) paths following a scheduler $\sigma$ is denoted by ${\textit{Paths}^*_{\mathcal {C},\sigma }}$ (resp. ${\textit{Paths}^\omega _{\mathcal {C},\sigma }}$). We note that the set ${\textit{Paths}^*_{\mathcal {C},\sigma }}$ is countably infinite from definition.

Probability Spaces under Schedulers. Let $\sigma$ be any scheduler. The probability space w.r.t $\sigma$ is defined as $(\varOmega ^{\mathcal {C},\sigma }, \mathcal {F}^{\mathcal {C},\sigma }, \mathbb {P}^{\mathcal {C},\sigma })$ where (i) $\varOmega ^{\mathcal {C},\sigma }:={\textit{Paths}^\omega _{\mathcal {C},\sigma }}$, (ii) $\mathcal {F}^{\mathcal {C},\sigma }$ is the smallest sigma-algebra generated by all cylinder sets induced by finite paths for which a finite path $\rho$ induces the cylinder set ${\textit{Cyl}}(\rho )$ of all infinite paths in ${\textit{Paths}^\omega _{\mathcal {C},\sigma }}$ with $\rho$ being their (common) prefix, and (iii) $\mathbb {P}^{\mathcal {C},\sigma }$ is the unique probability measure such that for all finite paths $\rho =s_0a_0\dots a_{n-1}s_n$ in ${\textit{Paths}^*_{\mathcal {C},\sigma }}$,

$$ \textstyle {\mathbb {P}^{\mathcal {C},\sigma }({\textit{Cyl}}(\rho ))=\prod _{k=0}^{n-1} \mathbf {P}(s_k, \sigma (s_0a_0\dots a_{k-1}s_k), s_{k+1}).} $$

For details see [4].

Zenoness and Time-Divergent Schedulers. An infinite path $\pi =s_0a_0s_1a_1\dots$ is zeno if $\sum _{n=0}^\infty d_n<\infty$, where $d_n:=a_n$ if $a_n\in [0,\infty )$ and $d_n:=0$ otherwise. Then a scheduler $\sigma$ is time divergent if $\mathbb {P}^{\mathcal {C},\sigma }(\{\pi \mid \pi \text{ is } \text{ zeno }\})=0$. In the following, we only consider time-divergent schedulers. The purpose is to eliminate non-realistic zeno behaviours (i.e., performing infinitely many actions within a finite amount of time).

In the following example, we illustrate a PTA which models a simple task-processing example.

Example 1

Consider the PTA depicted in Fig. 1. ${\textit{WORK}}_{\alpha },{\textit{WORK}}_{\beta }$ are locations and x is the only clock. Below each location first comes (vertically) its invariant condition and then the set of labels assigned to the location. For example, $\textit{inv}({\textit{WORK}}_{\alpha })=x \le 10$ and $\mathcal {L}({\textit{WORK}}_{\alpha })=\{ \alpha \}$. The two dots together with their corresponding solid line and dashed arrows refer to two actions $\tau _\alpha ,\tau _\beta$ with their enabling conditions and transition probabilities given by the probabilistic transition function. For example, the upper dot at the right of ${\textit{WORK}}_{\alpha }$ refers to the action $\tau _\alpha$ for which $\textit{enab}({\textit{WORK}}_{\alpha }, \tau _\alpha )=\mathbf {true}$, ${\textit{prob}}({\textit{WORK}}_{\alpha }, \tau _\alpha )(\{x\},{\textit{WORK}}_{\alpha })=0.1$, and ${\textit{prob}}({\textit{WORK}}_{\alpha }, \tau _\alpha )(\{x\},{\textit{WORK}}_{\beta })=0.9$. The PTA models a faulty machine which processes two different kinds of jobs (i.e., $\alpha ,\beta$) in an alternating fashion. If the machine fails to complete the current job, then it will repeat processing the job until it completes the job. For job $\alpha$, the machine always processes the job within 10 time units (cf. the invariant condition $x\le 10$), but may fail to complete the job with probability 0.1; Analogously, the machine always processes the job $\beta$ within 15 time units (cf. the invariant condition $x\le 15$), but may fail to complete the job with probability 0.2. Note that we omit the initial location in this example.

2.2 Timed Automata

Definition 2

(Timed Automata [22, 24, 25]). A timed automaton (TA) $\mathcal {A}$ is a tuple

$$\begin{aligned} \mathcal {A}=(Q,\varSigma ,\mathcal {Y},\varDelta ) \end{aligned}$$

(2)

where

• $Q$ is a finite set of modes;

• $\varSigma$ is a finite alphabet of symbols disjoint from $[0,\infty )$;

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

• $\varDelta \subseteq Q\times \varSigma \times {\textit{CC}\left( \mathcal {Y}\right) }\times 2^{\mathcal {Y}}\times Q$ is a finite set of rules.

$\mathcal {A}$ is a deterministic TA (DTA) if the following holds:

• 1. (determinism) for $(q_i,b_i,\phi _i,X_i,q'_i)\in \varDelta$ ($i\in \{1,2\}$), if $(q_1,b_1)=(q_2,b_2)$ and ${\llbracket }{\phi _1}{\rrbracket }\cap {\llbracket }{\phi _2}{\rrbracket }\ne \emptyset$ then $(\phi _1,X_1,q'_1)=(\phi _2,X_2,q'_2)$;

• 2. (totality) for all $(q,b)\in Q\times \varSigma$ and $\nu \in \textit{Val}\left( \mathcal {X}\right)$, there exists $(q,b,\phi ,X,q')\in \varDelta$ such that $\nu \models \phi$.

Informally, A TA is deterministic if there is always exactly one rule applicable for the timed transition. We do not incorporate invariants in TAs as we use TAs as language acceptors.

Below we illustrate the semantics of TAs. We fix a TA $\mathcal {A}$ in the form (2).

Configurations and One-Step Transition Relation. A configuration is a pair $(q,\nu )$, where $q\in Q$ and $\nu \in \textit{Val}\left( \mathcal {Y}\right)$. The one-step transition relation

$$ \Rightarrow ~\subseteq ~ (Q\times \textit{Val}\left( \mathcal {Y}\right) ) \times (\varSigma \cup [0,\infty )) \times (Q\times \textit{Val}\left( \mathcal {Y}\right) ) $$

is defined by: $((q,\nu ),a,(q',\nu '))\in \Rightarrow$ iff either (i) $a\in [0,\infty )$ and $(q',\nu ')=(q,\nu +a)$ or (ii) $a\in \varSigma$ and there exists a rule $(q,a,\phi ,X,q')\in \varDelta$ such that $\nu \models \phi$ and $\nu '={\nu }{\left[ X:=0\right] }$. For the sake of convenience, we write instead of $((q,\nu ),a,(q',\nu '))\in \Rightarrow$. Note that if $\mathcal {A}$ is deterministic, then there is a unique $(q',\nu ')$ such that given any $(q,\nu ), a$.

Infinite Timed Words and Runs. An infinite timed word is an infinite sequence $w=\{a_n\}_{n\in \mathbb {N}_0}$ such that $a_{2n} \in [0,\infty ) \text{ and } a_{2n+1} \in \varSigma$ for all n; the infinite timed word w is time-divergent if $\sum _{n\in \mathbb {N}_0}a_{2n}=\infty$. A run of $\mathcal {A}$ on an infinite timed word $w=\{a_n\}_{n\in \mathbb {N}_0}$ with initial configuration $(q,\nu )$, is an infinite sequence $\xi =\{\left( q_n,\nu _n,a_n\right) \}_{n\in \mathbb {N}_0}$ satisfying that $(q_0,\nu _0)=(q,\nu )$ and for all $n\in \mathbb {N}_0$; the trajectory ${\textit{traj} ( \xi )}$ of the run $\xi$ is defined as an infinite word over $Q$ such that ${\textit{traj} ( \xi )} := q_0 q_1 \dots$ . Note that if $\mathcal {A}$ is deterministic, then there is a unique run on every infinite timed word.

Below we illustrate the acceptance condition for TAs. We consider Rabin acceptance condition as the infinite acceptance condition.

Definition 3

(Rabin Acceptance Condition [1]). A TA with Rabin acceptance condition (TRA) is a tuple

$$\begin{aligned} \mathcal {A}=(Q,\varSigma ,\mathcal {Y},\varDelta ,\mathcal {F}) \end{aligned}$$

(3)

where $(Q,\varSigma ,\mathcal {Y},\varDelta )$ is a TA and $\mathcal {F}$ is a finite set of pairs $\mathcal {F}= \{ (H_1,K_1 ), \dots , (H_n,K_n) \}$ representing a Rabin condition for which $H_i$ and $K_i$ are subsets of $Q$ for all $i\le n$. $\mathcal {A}$ is a deterministic TRA (DTRA) if $(Q,\varSigma ,\mathcal {Y},\varDelta )$ is a DTA. A set $Q' \subseteq Q$ is Rabin-accepting by $\mathcal {F}$, written as the predicate $\text{ ACC } \left( {Q'}, {\mathcal {F}} \right)$, if there is $1 \le i \le n$ such that $Q' \cap H_i= \emptyset$ and $Q' \cap K_i \ne \emptyset$. An infinite timed word w is Rabin-accepted by $\mathcal {A}$ with initial configuration $(q,\nu )$ iff there exists a run $\xi$ of $(Q,\varSigma ,\mathcal {Y},\varDelta )$ on w with $(q,\nu )$ such that ${\textit{inf} ( {\textit{traj} (\xi )} )}$ is Rabin-accepting by $\mathcal {F}$.

Example 2

Consider the DTRA depicted in Fig. 2. The alphabet of this DTRA is the powerset of atomic propositions in Fig. 1. In the figure, $\textit{INIT},{\textit{q}}_{\alpha },{\textit{q}}_{\beta }$ and $\textit{FAIL}$ are modes with the Rabin condition $\mathcal {F}= \{ (\{ \textit{FAIL}\}, \{ {\textit{q}}_{\alpha }, {\textit{q}}_{\beta } \}) \}$, y is a clock and arrows between modes are rules. $C_\gamma ,W_\gamma$ ($\gamma \in \{\alpha ,\beta \}$) are undetermined integer constants. For example, there are four rules emitting from ${\textit{q}}_{\alpha }$:

$$\begin{aligned} ({\textit{q}}_{\alpha }, \{ \alpha \}, y \le C_\alpha ,\emptyset , {\textit{q}}_{\alpha }),&~({\textit{q}}_{\alpha }, \{ \beta \}, y \le W_\beta , \{ y \}, {\textit{q}}_{\beta }),\\ ({\textit{q}}_{\alpha }, \{ \alpha \}, C_\alpha<y,\emptyset , \textit{FAIL}),&~({\textit{q}}_{\alpha }, \{ \beta \}, W_\beta <y, \emptyset , \textit{FAIL}). \end{aligned}$$

$\textit{INIT}$ is the initial mode to read the first symbol upon which transiting to either ${\textit{q}}_{\alpha }$ or ${\textit{q}}_{\beta }$. $\textit{FAIL}$ is a deadlock mode from which all rules go to itself. Note that the rules of the DTRA does not satisfy the totality condition. However, we assume that all missing rules lead to the mode $\textit{FAIL}$ and does not affect the Rabin acceptance condition. The mode ${\textit{q}}_{\alpha }$ does not reset the clock y until it reads $\beta$. Moreover, ${\textit{q}}_{\alpha }$ does not transit to $\textit{FAIL}$ only if the time spent within a maximal consecutive segment of $\alpha$’s (in an infinite timed word) is no greater than $C_\alpha$ time units (cf. the rule $({\textit{q}}_{\alpha }, \{ \alpha \}, y \le C_\alpha ,\emptyset , {\textit{q}}_{\alpha })$) and the total time from the start of the segment until $\beta$ is read (the time within a maximal consecutive segment of $\alpha$’s plus the time spent on the last $\alpha$ in the segment) is no greater than $W_\beta$ (cf. the rule $({\textit{q}}_{\alpha }, \{ \beta \}, y \le W_\beta , \{ y \}, {\textit{q}}_{\beta })$). The behaviour of the mode ${\textit{q}}_{\beta }$ can be argued similar to that of ${\textit{q}}_{\alpha }$ where the only difference is to flip $\alpha$ and $\beta$. From the Rabin acceptance condition, the DTRA specifies a property on infinite timed words that the time spent within a maximal consecutive segment of $\alpha$’s (resp. $\beta$’s) and the total time until $\beta$ (resp. $\alpha$) is read always satisfy the conditions specified by ${\textit{q}}_{\alpha }$ (resp. ${\textit{q}}_{\beta }$).

3 Problem Statement

In this part, we define the PTA-TRA problem of model-checking PTAs against TA-specifications. The problem takes a PTA and a TRA as input, and computes the minimum and the maximum probability that infinite paths under the PTA are accepted by the TRA. Informally, the TRA encodes the linear dense-time property by judging whether an infinite path is accepted or not through its external behaviour, then the problem is to compute the probability that an infinite path is accepted by the TRA. In practice, the TRA can be used to capture all good (or bad) behaviours, so the problem can be treated as a task to evaluate to what extent the PTA behaves in a good (or bad) way.

Below we fix a well-formed PTA $\mathcal {C}$ taking the form (1) and a TRA $\mathcal {A}$ taking the form (3). W.l.o.g., we assume that $\mathcal {X}\cap \mathcal {Y}=\emptyset$ and $\varSigma =2^{{ AP}}$. We first show how an infinite path in ${\textit{Paths}^\omega _{\mathcal {C}}}$ can be interpreted as an infinite timed word.

Definition 4

(Infinite Paths as Infinite Timed Words). Given an infinite path $\pi = (\ell _0,\nu _0) a_0 (\ell _1,\nu _1) a_1 (\ell _2,\nu _2)a_2 \dots$ under $\mathcal {C}$, the infinite timed word $\mathcal {L}(\pi )$ is defined as $\mathcal {L}(\pi ):=a_0\mathcal {L}(\ell _2)a_2\mathcal {L}(\ell _4)\dots a_{2n}\mathcal {L}(\ell _{2n+2}) \dots .$ Recall that $\nu _0=\mathbf {0}$, $a_{2n}\in [0,\infty )$ and $a_{2n+1}\in \textit{Act}$ for $n\in \mathbb {N}_0$.

Remark 1

Informally, the interpretation in Definition 4 works by (i) dropping (a) the initial location $\ell _0$, (b) all clock valuations $\nu _n$’s, (c) all locations $\ell _{2n+1}$’s following a time-elapse, (d) all internal actions $a_{2n+1}$’s of $\mathcal {C}$ and (ii) replacing every $\ell _{2n}$ ($n\ge 1$) by $\mathcal {L}(\ell _{2n})$. The interpretation captures only external behaviours including time-elapses and labels of locations upon state-change, and discards internal behaviours such as the concrete locations, clock valuations and actions. Although the interpretation ignores the initial location, we deal with it in our acceptance condition where the initial location is preprocessed by the TRA.

Definition 5

(Path Acceptance). An infinite path $\pi$ of $\mathcal {C}$ is accepted by $\mathcal {A}$ w.r.t initial configuration $(q,\nu )$, written as the single predicate $\text{ ACC } \left( {\mathcal {A}}, {(q,\nu )}, {\pi } \right)$, if there is a configuration $(q',\nu ')$ such that and the infinite word $\mathcal {L}(\pi )$ is Rabin-accepted by $\mathcal {A}$ with $\left( q',\nu '\right)$.

The initial location omitted in Definition 4 is preprocessed by specifying explicitly that the first label $\mathcal {L}(\ell ^*)$ is read by the initial configuration $(q,\nu )$. Below we define acceptance probabilities over infinite paths under $\mathcal {C}$.

Definition 6

(Acceptance Probabilities). The probability that $\mathcal {C}$ observes $\mathcal {A}$ under scheduler $\sigma$ and initial mode $q\in Q$, denoted by $\mathfrak {p}_{q}^{\sigma }$, is defined by:

$$ \mathfrak {p}_{q}^{\sigma } := \mathbb {P}^{\mathcal {C},\sigma }( \textit{AccPaths} _{\mathcal {C},\sigma } ^{\mathcal {A},q} ) $$

where $\textit{AccPaths} _{\mathcal {C},\sigma } ^{\mathcal {A},q}$ is the set of infinite paths under $\mathcal {C}$ that are accepted by the TRA $\mathcal {A}$ w.r.t $(q,\mathbf {0})$ i.e. $\textit{AccPaths} _{\mathcal {C},\sigma } ^{\mathcal {A},q} = \left\{ \pi \in {\textit{Paths}^\omega _{\mathcal {C},\sigma }} \mid \text{ ACC } \left( {\mathcal {A}}, {(q,\mathbf {0})}, {\pi } \right) \right\} .$

Since the set ${\textit{Paths}^*_{\mathcal {C},\sigma }}$ is countably-infinite, $\textit{AccPaths} _{\mathcal {C},\sigma } ^{\mathcal {A},q}$ is measurable since it can be represented as a countable intersection of certain countable unions of some cylinder sets (cf. [1, Remark 10.24] for details).

Now we introduce the PTA-TRA problem.

• Input: a well-formed PTA $\mathcal {C}$, a TRA $\mathcal {A}$ and an initial mode $q$ in $\mathcal {A}$;

• Output: $\inf _\sigma \mathfrak {p}_{q}^{\sigma }$ and $\sup _\sigma \mathfrak {p}_{q}^{\sigma }$, where $\sigma$ ranges over all time-divergent schedulers for $\mathcal {C}$.

We refer to the problem as PTA-DTRA if $\mathcal {A}$ is deterministic.

4 The PTA-DTRA Problem

In this section, we solve the PTA-DTRA problem through a product construction. Based on the product construction, we also settle the complexity of the problem. Below we fix a well-formed PTA $\mathcal {C}$ in the form (1) and a DTRA $\mathcal {A}$ in the form (3). W.l.o.g, we consider that $\mathcal {X}\cap \mathcal {Y}=\emptyset$ and $\varSigma =2^{{ AP}}$.

The Main Idea. The core part of the product construction is a PTA which preserves the probability of the set of infinite paths accepted by $\mathcal {A}$. The intuition is to let $\mathcal {A}$ reads external actions of $\mathcal {C}$ while $\mathcal {C}$ evolves along the time axis. The major difficulty is that when $\mathcal {C}$ performs actions in $\textit{Act}$, there is a probabilistic choice between the target locations. Then $\mathcal {A}$ needs to know the labelling of the target location and the rule (in $\varDelta$) used for the transition. A naive solution is to integrate each single rule in $\varDelta$ into the enabling condition $\textit{enab}$ in $\mathcal {C}$. However, this simple solution does not work since a single rule fixes the labelling of a location in $\mathcal {C}$, while the probability distribution (given by ${\textit{prob}}$) can jump to locations with different labels. We solve this difficulty by integrating into the enabling condition enough information on clock valuations under $\mathcal {A}$ so that the rule used for the transition is clear.

The Product Construction. For each $q\in Q$, we let

$$\begin{aligned} \mathcal {T}_{q}:=\{h:\varSigma \rightarrow {\textit{CC}\left( \mathcal {Y}\right) }\mid \forall b\in \varSigma .\left( q, b, h(b), X, q')\in \varDelta \text{ for } \text{ some } X, q'\right) \}. \end{aligned}$$

The totality of $\varDelta$ ensures that $\mathcal {T}_{q}$ is non-empty. Intuitively, every element of $\mathcal {T}_{q}$ is a tuple of clock constraints $\{\phi _b\}_{b\in \varSigma }$, where each clock constraint $\phi _b$ is chosen from the rules emitting from $q$ and b. The product PTA ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ (between $\mathcal {C}$ and $\mathcal {A}$ with initial mode $q$) is defined as $\left( {L}_\otimes , \ell ^*_\otimes , \mathcal {X}_\otimes , \textit{Act}_\otimes , \textit{inv}_\otimes , \textit{enab}_\otimes , {\textit{prob}}_\otimes , Q, \mathcal {L}_\otimes \right)$ where:

• $L_\otimes :=L\times Q$;

• $\ell ^*_\otimes :=(\ell ^*, q^\star )$ where $q^\star$ is the unique mode such that ;

• $\mathcal {X}_\otimes :=\mathcal {X}\cup \mathcal {Y}$;

• $\textit{Act}_\otimes :=\textit{Act}\times \bigcup _q\mathcal {T}_q$;

• $\textit{inv}_\otimes (\ell ,q):=\textit{inv}(\ell )$ for all $(\ell ,q)\in L_\otimes$;

• $\textit{enab}_\otimes \left( (\ell ,q), (a,h)\right) :=\textit{enab}(\ell ,a)\wedge \bigwedge _{b\in \varSigma } h(b)$ if $h\in \mathcal {T}_q$, and $\textit{enab}_\otimes$ $\left( (\ell ,q), (a,h)\right) :=\mathbf {false}$ otherwise, for all $(\ell ,q)\in L_\otimes$, $(a,h) \in \textit{Act}_\otimes$.

• $\mathcal {L}_\otimes \left( \ell ,q\right) := \left\{ q\right\} \text{ for } \text{ all } \left( \ell ,q\right) \in L_\otimes ;$

• ${\textit{prob}}_\otimes$ is given by

  $$\begin{aligned}&{\textit{prob}}_\otimes \left( (\ell ,q),(a,h)\right) (Y,(\ell ',q')):=\\&~~ {\left\{ \begin{array}{ll} {\textit{prob}}\left( \ell ,a\right) (Y\cap \mathcal {X},\ell ') &{} \text{ if } (q,\mathcal {L}\left( \ell '\right) , h(\mathcal {L}\left( \ell '\right) ), Y\cap \mathcal {Y}, q')\\ &{} \text{ is } \text{ a } \text{(unique) } \text{ rule } \text{ in } \varDelta \\ 0 &{} \text{ otherwise } \end{array}\right. } \end{aligned}$$

for all $(\ell ,q),(\ell ',q')\in L_\otimes$, $(a,h) \in \textit{Act}_\otimes$ and $Y \in \mathcal {X}_\otimes$.

Besides standard constructions (e.g., the Cartesian product between $L$ and $Q$), the product construction also has Cartesian product between $\textit{Act}$ and $\bigcup _q\mathcal {T}_q$. For each extended action (a, h), the enabling condition for this action is the conjunction between $\textit{enab}(\ell ,a)$ and all clock constraints from h. This is to ensure that when the action (a, h) is taken, the clock valuation under $\mathcal {A}$ satisfies every clock constraint in h. Then in the definition for ${\textit{prob}}_\otimes$, upon the action (a, h), the product PTA first perform probabilistic jump from $\mathcal {C}$ with the target location $\ell '$, then chooses the unique rule $(q,\mathcal {L}\left( \ell '\right) , h(\mathcal {L}\left( \ell '\right) ), Y\cap \mathcal {Y}, q')$ from the emitting mode $q$ and the label $\mathcal {L}\left( \ell '\right)$ for which the uniqueness comes from the determinism of $\varDelta$, then perform the discrete transition from $\mathcal {A}$. Finally, we label each $(\ell ,q)$ by $q$ to meet the Rabin acceptance condition.    $\square$

It is easy to see that the PTA ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ is well-formed as $\mathcal {C}$ is well-formed and $\mathcal {A}$ does not introduce extra invariant conditions.

Fig. 3.

The product PTA for our running example

Example 3

The product PTA between the PTA in Example 1 and the DTRA in Example 2 is depicted in Fig. 3. In the figure, $({{\textit{WORK}}_{\alpha }},{{\textit{q}}_{\alpha }}), ({{\textit{WORK}}_{\beta }},{{\textit{q}}_{\beta }})$ and $({{\textit{WORK}}_{\alpha }},{\textit{FAIL}}), ({{\textit{WORK}}_{\beta }},{\textit{FAIL}})$ are product locations. We omit the initial location and unreachable locations in the product construction. From the construction of $\mathcal {T}_{q}$’s, the functions $h_i$’s are as follows (we omit redundant labels such as $\emptyset$ and $\{\alpha ,\beta \}$ which never appear in the PTA):

• $h_0=\{\{ \alpha \} \mapsto y \le C_\alpha ,\{ \beta \} \mapsto y \le W_\beta \}$;

• $h_1=\{\{ \alpha \} \mapsto y \le C_\alpha ,\{ \beta \} \mapsto W_\beta < y\}$;

• $h_2=\{\{ \alpha \} \mapsto C_\alpha < y ,\{ \beta \} \mapsto y \le W_\beta \}$;

• $h_3=\{\{ \alpha \} \mapsto C_\alpha< y ,\{ \beta \} \mapsto W_\beta < y\}$;

• $h_4=\{\{ \beta \} \mapsto y \le C_\beta ,\{ \alpha \} \mapsto y\le W_\alpha \}$;

• $h_5=\{\{ \beta \} \mapsto y \le C_\beta ,\{ \alpha \} \mapsto W_\alpha < y\}$;

• $h_6=\{\{ \beta \} \mapsto C_\beta < y ,\{ \alpha \} \mapsto y \le W_\alpha \}$;

• $h_7=\{\{ \beta \} \mapsto C_\beta< y ,\{ \alpha \} \mapsto W_\alpha < y\}$.

The intuition is that the DTA accepts all infinite paths under the PTA such that the failing time for job $\gamma$ ($\gamma \in \{\alpha ,\beta \}$) (the time within the consecutive $\gamma$’s) should be no greater than $C_\gamma$ and the waiting time for job $\gamma$ (the failing time plus the time spent on the last $\gamma$) should be no greater than $W_\gamma$.

Below we clarify the correspondence between $\mathcal {C},\mathcal {A}$ and ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$. We first show the relationship between paths under $\mathcal {C}$ and those under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$. Informally, paths under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ are just paths under $\mathcal {C}$ extended with runs of $\mathcal {A}$.

Transformation $\mathcal {T}$ for Paths from $\mathcal {C}$  into ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$. The transformation is defined as the function $\mathcal {T}:{\textit{Paths}^*_{\mathcal {C}}}\cup {\textit{Paths}^\omega _{\mathcal {C}}}\rightarrow {\textit{Paths}^*_{{\mathcal {C}}{\otimes }{\mathcal {A}_q}}}\cup {\textit{Paths}^\omega _{{\mathcal {C}}{\otimes }{\mathcal {A}_q}}}$ which transform a finite or infinite path under $\mathcal {C}$ into one under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$. For a finite path $\rho =(\ell _0,\nu _0)a_0\dots a_{n-1}(\ell _n,\nu _n)$ under $\mathcal {C}$ (note that $(\ell _0,\nu _0)=(\ell ^*, \mathbf {0})$ by definition), we define $\mathcal {T}(\rho )$ to be the unique finite path

$$\begin{aligned} \mathcal {T}(\rho ):=((\ell _0,q_0),\nu _0\cup \mu _0)a'_0\dots a'_{n-1}((\ell _n,q_n),\nu _n\cup \mu _n) \end{aligned}$$

(4)

under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ such that the following conditions (†) hold:

• (note that $\mu _0=\mathbf {0}$);

• for all $0\le k< n$, if $a_k\in [0,\infty )$ then $a'_k=a_k$ and ;

• for all $0\le k< n$, if $a_k\in \textit{Act}$ then $a'_k=(a_k,\xi _k)$ and where $\xi _k$ is the unique function such that for each symbol $b\in \varSigma$, $\xi _k(b)$ is the unique clock constraint appearing in a rule emitting from $q_k$ and with symbol b such that $\mu _k\models \xi _k(b)$.

Likewise, for an infinite path $\pi =(\ell _0,\nu _0)a_0(\ell _1,\nu _1)a_1\dots$ under $\mathcal {C}$, we define $\mathcal {T}(\pi )$ to be the unique infinite path

$$\begin{aligned} \mathcal {T}(\pi ):=((\ell _0,q_0),\nu _0\cup \mu _0)a'_0((\ell _1,q_1),\nu _1\cup \mu _1)a'_1\dots \end{aligned}$$

(5)

under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ such that the three conditions in (†) hold for all $k\in \mathbb {N}_0$ instead of all $0\le k< n$. From the determinism and totality of $\mathcal {A}$, it is straightforward to prove the following result.

Lemma 1

The function $\mathcal {T}$ is a bijection. Moreover, for any infinite path $\pi$ under $\mathcal {C}$, $\pi$ is non-zeno iff $\mathcal {T}(\pi )$ is non-zeno.

Below we also show the correspondence on schedulers before and after the product construction.

Transformation $\theta$ for Schedulers from $\mathcal {C}$  into ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$. We define the function $\theta$ from the set of schedulers under $\mathcal {C}$ into the set of schedulers under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ as follows: for any scheduler $\sigma$ for $\mathcal {C}$, $\theta (\sigma )$ (for ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$) is defined such that for any finite path $\rho$ under $\mathcal {C}$ where $\rho =(\ell _0,\nu _0)a_0\dots a_{n-1}(\ell _n,\nu _n)$ and $\mathcal {T}(\rho )$ given as in (4),

$$ \theta (\sigma )(\mathcal {T}(\rho )):= {\left\{ \begin{array}{ll} \sigma (\rho ) &{} \text{ if } n \text{ is } \text{ even } \\ (\sigma (\rho ),\lambda (\rho )) &{} \text{ if } n \text{ is } \text{ odd } \end{array}\right. } $$

where $\lambda (\rho )$ is the unique function such that for each symbol $b\in \varSigma$, $\lambda (\rho )(b)$ is the clock constraint in the unique rule emitting from $q_n$ and with symbol b such that $\mu _n\models \lambda (\rho )(b)$. Note that the well-definedness of $\theta$ follows from Lemma 1.

From Lemma 1, the product construction, the determinism and totality of $\varDelta$, one can prove directly the following lemma.

Lemma 2

The function $\theta$ is a bijection.

Now we prove the relationship between infinite paths accepted by a DTRA before product construction and infinite paths satisfying certain Rabin condition.

We introduce more notations. First, we lift the function $\mathcal {T}$ to all subsets of paths in the standard fashion: for all subsets $A\subseteq {\textit{Paths}^*_{\mathcal {C}}}\cup {\textit{Paths}^\omega _{\mathcal {C}}}$, $\mathcal {T}(A):=\{\mathcal {T}(\omega )\mid \omega \in A\}$. Then for an infinite path $\pi$ under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ in the form (5), we define the trace of $\pi$ as an infinite word over $Q$ by ${\textit{trace}( \pi )} := q_0 q_1 \dots$. Finally, for any scheduler $\sigma$ for ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$, we define the set $\textit{RPaths}_{\sigma }$ by

$$ \textit{RPaths}_{\sigma }:=\left\{ \pi \in {\textit{Paths}^\omega _{{\mathcal {C}}{\otimes }{\mathcal {A}_q},\sigma }} \mid \text{ ACC } \left( { {\textit{inf} ( {\textit{trace}( \pi )} )} }, { \mathcal {F}} \right) \right\} . $$

Intuitively, $\textit{RPaths}_{\sigma }$ is the set of infinite paths under ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ that meet the Rabin condition $\mathcal {F}$ from $\mathcal {A}$. The following proposition clarifies the role of $\textit{RPaths}_{\sigma }$.

Proposition 1

For any scheduler $\sigma$ for $\mathcal {C}$ and any initial mode q for $\mathcal {A}$, we have $\mathcal {T}\left( \textit{AccPaths} _{\mathcal {C},\sigma } ^{\mathcal {A},q} \right) = \textit{RPaths}_{{\theta \left( {\sigma }\right) }}.$

Finally, we demonstrate the relationship between acceptance probabilities before product construction and Rabin(-accepting) probabilities after product construction. We also clarify the probability of zenoness before and after the product construction. The proof follows standard argument from measure theory.

Proposition 2

For any scheduler $\sigma$ for $\mathcal {C}$ and mode q, the followings hold:

• $\mathfrak {p}_{q}^{\sigma } = \mathbb {P}^{\mathcal {C},\sigma } \left( \textit{AccPaths} _{\mathcal {C},\sigma } ^{\mathcal {A},q} \right) = \mathbb {P}^{{\mathcal {C}}{\otimes }{\mathcal {A}_q},\theta (\sigma )} \left( \textit{RPaths}_{{\theta \left( {\sigma }\right) }}\right) ;$

• $\mathbb {P}^{\mathcal {C},\sigma } \left( \{ \pi \mid \pi \text{ is } \text{ zeno } \} \right) = \mathbb {P}^{{\mathcal {C}}{\otimes }{\mathcal {A}_q},\theta (\sigma )} \left( \{ \pi ' \mid \pi ' \text{ is } \text{ zeno } \} \right) .$

A side result from Proposition 2 says that $\theta$ preserves time-divergence for schedulers before and after product construction. From Proposition 2 and Lemma 2, one immediately obtains the following result which transforms the PTA-DTRA problem into Rabin(-accepting) probabilities under the product PTA.

Corollary 1

For any initial mode q, $\textit{opt}_\sigma \mathfrak {p}_{q}^{\sigma } = \textit{opt}_{\sigma '} \mathbb {P}^{{\mathcal {C}}{\otimes }{\mathcal {A}_q},\sigma '}\left( \textit{RPaths}_{\sigma '} \right)$ where $\textit{opt}$ refers to either $\inf$ (infimum) or $\sup$ (supremum), $\sigma$ (resp. $\sigma '$) range over all time-divergent schedulers for $\mathcal {C}$ (resp. ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$).

Solving Rabin Probabilities. We follow the approach in [18] to solve Rabin probabilities over PTAs. Below we briefly describe the approach. The approach can be divided into two steps. The first step is to ensure time-divergence. This is achieved by (i) making a copy for every location in the PTA, (ii) enforcing a transition from every location to its copy to happen after 1 time-unit elapses, (iii) enforcing a transition from every copy location back to the original one immediately with no time-delay, and (iv) putting a special label tick in every copy. Then time-divergence is guaranteed by adding the label tick to the Rabin condition. The second step is to transform the problem into limit Rabin properties over MDPs [1, Theorem 10.127]. This step constructs an MDP $\text {Reg}[ {{\mathcal {C}}{\otimes }{\mathcal {A}_q}} ]$ from the PTA ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$ through a region-graph construction so that the problem is reduced to solving limit Rabin properties over $\text {Reg}[ {{\mathcal {C}}{\otimes }{\mathcal {A}_q}} ]$. Regions are finitely-many equivalence classes of clock valuations that serve as a finite abstraction which capture exactly reachability behaviours over timed transitions (cf. [5]). Then standard methods based on maximal end components (MECs) are applied to $\text {Reg}[ {{\mathcal {C}}{\otimes }{\mathcal {A}_q}} ]$. In detail, the algorithm computes the reachability probability to MECs that satisfy the Rabin acceptance condition. In order to guarantee time-divergence, the algorithm only picks up MECs with at least one location that has a tick label. Based on this approach, our result leads to an algorithm for solving the problem PTA-DTRA.

Note that in ${\mathcal {C}}{\otimes }{\mathcal {A}_q}$, although the size of $\textit{Act}_\otimes$ may be exponential due to possible exponential blow-up from $\mathcal {T}_{q}$, one easily sees that $| L_\otimes |$ is $|L| \cdot |Q|$ and $| \mathcal {X}_\otimes | = | \mathcal {X}| + | \mathcal {Y}|$. Hence, the size of $\text {Reg}[ {{\mathcal {C}}{\otimes }{\mathcal {A}_q}} ]$ is still exponential in the sizes of $\mathcal {C}$ and $\mathcal {A}$. It follows that $\textit{opt}_\sigma \mathfrak {p}_{q}^{\sigma }$ can be calculated in exponential time from the MEC-based algorithm illustrated in [1, Theorem 10.127], as is demonstrated by the following proposition.

Proposition 3

The problem PTA-DTRA is in EXPTIME in the size of the input PTA and DTRA.

It is proved in [16] that the reachablity-probability problem for arbitrary PTAs is EXPTIME-complete. Since Rabin acceptance condition subsumes reachability, one obtains that the problem PTA-DTRA is EXPTIME-hard. Thus we obtain the main result of this section which settles the computational complexity of the problem PTA-DTRA.

Theorem 1

The PTA-DTRA problem is EXPTIME-complete.

Remark 2

The main novelty for our product construction is that by adopting extended actions (i.e. $\mathcal {T}_{q}$) and integrating them into enabling condition and probabilistic transition function, the product PTA can know which rule to use from the DTA upon any symbol to be read. This solves the problem that probabilistic jumps can lead to different locations, causing the usage of different rules from the DTA. Moreover, our product construction ensures EXPTIME-completeness of the problem.

5 The PTA-TRA Problem

In this section, we study the PTA-TRA problem where the input timed automaton needs not to be deterministic. In contrast to the deterministic case (which is shown to be decidable and EXPTIME-complete in the previous section), we show that the problem is undecidable.

The Main Idea. The main idea for the undecidability result is to reduce the universality problem of timed automata to the PTA-TRA problem. The universality problem over timed automata is well-known to be undecidable, as follows.

Lemma 3

([5, Theorem 5.2]). Given a timed automaton over an alphabet $\varSigma$ and an initial mode, the problem of deciding whether it accepts all time-divergent timed words w.r.t Büchi acceptance condition over $\varSigma$ is undecidable.

Although Lemma 3 is on Büchi acceptance condition, it holds also for Rabin acceptance condition since Rabin acceptance condition extends Büchi acceptance condition. Actually the two acceptance conditions are equivalent over timed automata (cf. [5, Theorem 3.20]). We also remark that Lemma 3 was originally for multiple initial modes, which can be mimicked by a single initial mode through aggregating all rules emitting from some initial mode as rules emitting from one initial mode.

Now we prove the undecidability result as follows. The proof idea is that we construct a PTA that can generate every time-divergent timed words with probability 1 by some time-divergent scheduler. Then the TRA accepts all time-divergent timed words iff the minimal probability that the PTA observes the TRA equals 1.

Theorem 2

Given a PTA $\mathcal {C}$ and a TRA $\mathcal {A}$, the problem to decide whether the minimal probability that $\mathcal {C}$ observes $\mathcal {A}$ (under a given initial mode) is equal to 1 is undecidable.

Proof

(Proof Sketch). Let $\mathcal {A}=(Q,\varSigma ,\mathcal {Y},\varDelta ,\mathcal {F})$ be any TRA where the alphabet $\varSigma = \{b_{1}, b_{2}, \cdots , b_{k}\}$ and the initial mode is $q_{{\textit{start}}}$. W.l.o.g, we consider that $\varSigma \subseteq 2^{{ AP}}$ for some finite set ${ AP}$. This assumption is not restrictive since what $b_{i}$’s concretely are is irrelevant, while the only thing that matters is that $\varSigma$ has k different symbols. We first construct the TRA $\mathcal {A}' = (Q', \varSigma ', \mathcal {Y}, \varDelta ',\mathcal {F})$ where $Q' = Q\cup \{ q_{{\textit{init}} }\}$ for which $q_{{\textit{init}} }$ is a fresh mode, $\varSigma ' = \varSigma \cup \{ b_{0} \}$ for which $b_{0}$ is a fresh symbol and $\varDelta ' = \varDelta \cup \{ \langle q_{{\textit{init}} }, b_{0}, \mathbf {true}, \mathcal {Y}, q_{{\textit{start}}}\rangle \}$. Then we construct the PTA:

• $L:= \varSigma '$, $\ell ^* := b_{0}$, $\mathcal {X}:= \emptyset$ and $\textit{Act}:= \varSigma$;

• $\textit{inv}(b_{i}) := \mathbf {true}\text { for } b_{i} \in L$;

• $\textit{enab}(b_{i},b_{j}) := \mathbf {true}\text { for } b_{i} \in L\text { and } b_{j} \in \textit{Act}$;

• ${\textit{prob}}(b_{i},b_{j})$ is the Dirac distribution at $(\emptyset ,b_{j})$ (i.e., ${\textit{prob}}(b_{i},b_{j})(\emptyset ,b_{j})=1$ and ${\textit{prob}}(b_{i},b_{j})(X,b)=0$ whenever $(X,b)\ne (\emptyset ,b_{j})$), for $b_{i} \in L$ and $b_{j} \in \textit{Act}$;

• $\mathcal {L}(b_{i}) := b_{i} \text { for } b_{i} \in L$.

Note that we allow no clocks in the construction since clocks are irrelevant for our result. Since we omit clocks, we also treat states (of $\mathcal {C}'$) as single locations. One can prove that $\mathcal {A}$ accepts all time-divergent timed words over $\varSigma$ with initial mode $q_{{\textit{start}}}$ iff the minimal probability that $\mathcal {C}'$ observes $\mathcal {A}'$ with initial mode $q_{{\textit{init}} }$ equals 1.    $\square$

Remark 3

Theorem 2 shows that the problem to qualitatively decide the minimal probability is undecidable. On the other hand, the decidability of the problem to decide maximum acceptance probabilities is left open.

6 Conclusion

In this paper, we studied the problem of model-checking PTAs against timed-automata specifications. We considered Rabin acceptance condition as the acceptance criterion. We first solved the problem with deterministic-timed-automata specifications through a product construction and proved that its computational complexity is EXPTIME-complete. Then we proved that the problem with general timed-automata specifications is undecidable through a reduction from the universality problem of timed automata.

A future direction is zone-based algorithms for Rabin acceptance condition. Another direction is to investigate timed-automata specifications with cost or reward. Besides, it is also interesting to explore model-checking PTAs against Metric Temporal Logic [19].

7 Related Works

Model-checking TAs or MDPs against omega-regular (dense-time) properties is well-studied (cf. [1, 20, 26], etc.). PTAs extend both TAs and MDPs with either probability or timing constraints, hence require new techniques for verification problems. On one hand, our technique extends techniques for MDPs (e.g. [26]) with timing constraints. On the other hand, our technique is incomparable to techniques for TAs since linear-time model checking of TAs focus mostly on proving decidability of temporal logic formulas (e.g. Metric Temporal logic [19,20,21]), while we prove that model-checking PTAs against TA-specifications is undecidable.

Model-checking probabilistic timed models against linear dense-time properties are mostly considered for continuous-time Markov processes (CTMPs). First, Donatelli et al. [22] proved an expressibility result that the class of linear dense-time properties encoded by DTAs is not subsumed by branching-time properties. They also demonstrated an efficient algorithm for verifying continuous-time Markov chains [22] against one-clock DTAs. Then various results on verifying CTMPs are obtained for specifications through DTAs and general timed automata (cf. e.g. [22, 24, 25, 27,28,29]). The fundamental difference between CTMPs and PTAs is that the former assign probability distributions to time elapses, while the latter treat time-elapses as pure nondeterminism. As a consequence, the techniques for CTMPs cannot be applied to PTAs.

For PTAs, the only relevant result is by Sproston [18] who developed an approach for verifying PTAs against deterministic discrete-time omega-regular automata by a similar product construction. Our results extend his result in two ways. First, our product construction has the extra ability to tackle timing constraints from the DTA. The extension is nontrivial since it needs to resolve the integration between randomness (from the PTA) and timing constraints (from the DTA), and still ensures the EXPTIME-completeness of the problem, matching the computational complexity in the discrete-time case [18]. Second, we have proved an undecidability result in the case of general nondeterministic timed automata, thus extending [18] with nondeterminism.