Discounted Duration Calculus

Abstract

To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.

An early version of this work was presented at the Nordic Workshop of Programming Theory 2015.

H. Ody—This Work is supported by the Deutsche Forschungsgemeinschaft (DFG) within the Research Training Group DFG GRK 1765 SCARE.

M. Fränzle—This Work was partially supported by Deutsche Forschungsgemeinschaft within the Transregional Collaborative Research Center SFB/TR 14 AVACS.

M.R. Hansen—This Work was partially supported by the Danish Research Foundation for Basic Research within the IDEA4CPS project.

1 Introduction

In economics discounting represents that money earned soon can be reinvested earlier and hence yields more revenue than money earned later. Discounting has been introduced into temporal logics to represent that something happening earlier is more important than similar events happening later [14]. A typical example is a rail-road crossing. Consider the property “eventually the gates are open”. While a controller leaving the gates closed an hour after the train has passed might be safe and alive, it is not useful. We can use discounting to express that the controller should not wait unnecessarily long before opening the gates. The discount here is a scalar defining the decrease rate of an exponential function assigning weights to events based on their (relative) time of occurrence. In [1, 13, 14] such weighted evaluation of temporal properties has been described as quantifying the temporal quality of a system.

Duration Calculus (DC) [12] was introduced to reason about duration properties of real time systems. In the prominent gas burner case study [24] the following duration property was proven: “in any time interval of length ${\ge }{60}$ gas is leaking for at most 5 % of the time”. The great expressiveness of DC however, makes automated reasoning in most cases undecidable [10, 11, 15].

So far discounting in logics only has been studied for discrete-time temporal logics (LTL, CTL*, $\mu$-calculus) [1, 13, 14, 20, 21]. Here, we study discounting in the dense-time logic DC. Our interest in DC arises from its expressiveness, being able to express properties of accumulated durations instead of just temporal distances, and the consequential undecidability of most fragments over dense time. A primary objective of the work reported herein thus is to investigate the impact of discounting on effective approximability of model checking for DC formulas.

To this end we define discounted Duration Calculus (DDC), where the truth value is real-valued in the interval [0, 1], instead of Boolean. A truth value closer to 1 means higher temporal quality. We point out that we use exponential discounting because this is the most common from of discounting. However, other discounting mechanisms are possible. With DDC we can express properties such as $\lozenge \,^d \phi$ (meaning “soon with discount d the system satisfies $\phi$”), where $\phi$ is a DDC formula and $\lozenge \,$ is the right neighbourhood modality from [9]. To evaluate the truth value of $\lozenge \,^d \phi$ on the interval $[t_0,t_1]$ we search for a neighbouring interval $[t_1,t_2]$ such that the discounting factor $d^{t_2 - t_1}$ multiplied with the truth value of $\phi$ on $[t_1, t_2]$ is maximal.

Our main result is that for the fragment $\text {DDC}_{<1}$, which consists of all DDC formulas where all discounts are ${<}{1}$, model checking is approximable. This stems from the fact that the effect of the system behaviour on the satisfaction value becomes negligible as time advances. Hence, for approximation it suffices to only consider bounded prefixes of runs, which in turn enables us to use bounded model checking. Our model-checking method is extended to cope with modalities of the form $\mathrm {G}_{S} \phi$ (meaning “whenever S happens $\phi$ holds thereon”). We provide an extensive example illustrating the usefulness of our approach.

Related Work. Discounting in temporal logics was first studied in [14] and later in [1, 13, 20, 21]. However, in all of these works the logics are discrete and they cannot express duration properties. In [7] the authors introduce a method to perform model checking on weighted (or priced) timed automata with weighted versions of CTL and LTL. A cost in their work essentially corresponds to the duration of a state variable in our work. However, they do not consider discounting and in their case model checking becomes undecidable for automata with at least three clocks. For a fragment without duration properties called test formulas, which are used to express undesired behaviours, model checking has been shown decidable [22]. In [17] the authors define a model checking procedure for a fragment that allows duration properties, but disallows negation of the chop operator. In [16] the authors give a real-valued interpretation to DC and they provide an approximative procedure to check satisfiability. However, the authors do not consider model checking. Further, in none of the works on DC discounting is considered.

2 Discounted Duration Calculus (DDC)

We use an adapted version of Duration Calculus (DC), where the chop operator is replaced by a right neighbourhood modality. As atomic formulas, we allow comparison of linear combinations of durations with constants.

Definition 1 (Syntax of DDC)

Let $d, k_0,\dots ,k_n,c\in \mathbb {Q},$ where $d\in [0,1]$, $\gtrsim \,\in \{\ge ,>\}$ and let $P \in AP$ denote arbitrary atomic propositions (or state variables or just variables). Then the formulas $\phi$ of Discounted Duration Calculus (abbreviated DDC) and state expressions S are defined by the grammar

$$\begin{aligned} \phi&\;{:}{:}{=}\; \lozenge \,^d \phi \mid \lnot \phi \mid \phi \vee \phi \mid \varSigma _{i=0}^n k_i {\textstyle \int }S_i \gtrsim c \, ,\\ S&\;{:}{:}{=}\; P \mid \lnot S \mid S \vee S \, . \end{aligned}$$

We denote the fragment of DDC where all discounts are $<1$ as $\textit{DDC}_{<1}$.

Let $AP$ be a finite set of atomic propositions. The semantics of DC is defined in terms of timed words. A timed word is a (possibly infinite) sequence

$$\begin{aligned} \tau = (\sigma _0,t_0) (\sigma _1,t_1) \cdots (\sigma _i,t_i) \cdots \end{aligned}$$

where $\sigma _i \in 2^{ AP }$ and $t_0=0$ and $t_i \in \mathbb {R}_{\ge 0}$. The sequence of time stamps $t_0, t_1, \ldots$ occurring in $\tau$ must be weakly monotonically increasing, that is $t_i\le t_{i+1}$. Furthermore, we require progress in infinite timed words $\tau$, that is, for every $t\in R_{\ge 0}$ there is an $i > 0$ such that $t_i>t$.

If $\tau$ is an infinite sequence, then we say that the time span (or just span) of $\tau$ comprises the non-negative reals and we write $\mathrm {span}(\tau ) = \mathbb {R}_{\ge 0}$. If $\tau$ is a finite sequence having $(\sigma _n,t_n)$ as its last element, the span of $\tau$ is the bounded (right-open) interval $[0,t_n)$ and we write $\mathrm {span}(\tau ) = [0,t_n)$. We shall from now on restrict our attention to timed words having a non-empty time span.

For a timed word $\tau = (\sigma _0,t_0) (\sigma _1,t_1) \cdots (\sigma _i,t_i) \cdots$ and $\delta \in \mathrm {span}(\tau )$, where $\delta > 0$, we define the time-bounded prefix $\tau _\delta$ of $\tau$ as the timed word:

$$\begin{aligned} \tau _\delta = (\sigma _0,t_0) (\sigma _1,t_1) \cdots (\sigma _i,t_i) (\sigma _i,\delta ) \end{aligned}$$

where i is given by $t_i \le \delta < t_{i+1}$. Note that there is exactly one such i since $\delta \in \mathrm {span}(\tau )$.

A timed word $\tau = (\sigma _0,t_0) (\sigma _1,t_1) \cdots (\sigma _i,t_i) \cdots$ induces a function

$$\begin{aligned} \tau (P): \mathrm {span}(\tau ) \rightarrow \{0,1\} \end{aligned}$$

for every atomic proposition P, as follows:

$$\begin{aligned} \tau (P)(t) = \left\{ \begin{array}{lcl} 1 &{} &{} \text {if }P\in \sigma _i\text {, for some }i\text { where }t_i\le t < t_{i+1},\\ 0 &{} &{} \text {otherwise} \,. \end{array} \right. \end{aligned}$$

The function $\tau (P)$ is also called a trajectory for P. Trajectories are lifted to state expressions by a point-wise extension in a straightforward manner, for example, $\tau (S_0 \vee S_1)(t) = \tau (S_0)(t) \vee \tau (S_1)(t)$. We use the abbreviation $S_\tau$ for $\tau (S)$. Notice that the progress requirement for infinite timed words guarantees that for every variable P, every finite part of $P_\tau$ has a finite number of discontinuity points, i.e. $P_\tau$ is of finite variability.

The semantics of a DDC formula $\phi$ on the basis of a timed word $\tau = (\sigma _0,t_0) (\sigma _1,t_1) \cdots (\sigma _i,t_i) \cdots$ is a function:

$$\begin{aligned} \tau (\phi ) : Intv \rightarrow [0,1] \end{aligned}$$

where $Intv = \{[t,t'] \subseteq \mathrm {span}(\tau ) \mid t \le t' \}$ denotes the set of bounded and closed real intervals contained in $\mathrm {span}(\tau )$. The function assigns to $\tau (\phi )\, [a,b]$ a satisfaction value in the real interval [0, 1], where closer to 1 means better.

Discounts d occur only in connection with the right neighbourhood modality $\lozenge \,^d \phi$, which expresses that an adjacent interval to the right of the current interval satisfies $\phi$. The discount d is used to decrease the satisfaction value as the length of the adjacent interval necessary to find a satisfaction of $\phi$ increases. The modal formula $\lozenge \,^d \phi$ can be understood as “soon $\phi$ holds”.

Definition 2 (Semantics of DDC)

The semantics of a formula, given a timed word $\tau$ and an interval $[t_0,t_1]$, is defined as

$$\begin{aligned} \tau (\lozenge \,^d \phi )\,[t_0,t_1]&= \sup \{ d^{t_2-t_1}\cdot \tau (\phi )\, [t_1,t_2] \mid t_2\ge t_1 \wedge t_2 \in \mathrm {span}(\tau ) \} \\ \tau (\varSigma _{i=0}^n k_i {\textstyle \int }S_i \gtrsim c )\,[t_0,t_1]&= {\left\{ \begin{array}{ll} 1 &{} \mathrm {if}\; \varSigma _{i=0}^n k_i \int _{t=t_0}^{t_1} \tau (S_{i})(t)\,\mathrm {d}t \gtrsim c \\ 0 &{} \mathrm {otherwise} \end{array}\right. } \\ \tau (\lnot \phi )\,[t_0,t_1]&= 1-\tau (\phi ) \,[t_0,t_1] \\ \tau (\phi _0 \vee \phi _1)\,[t_0,t_1]&= \max \{\tau (\phi _0)\,[t_0,t_1], \tau (\phi _1)\,[t_0,t_1] \} \end{aligned}$$

where $\gtrsim \,\in \{>,\ge \}$.

If we want to use the standard neighbourhood modalities without discounting then we use a discount of 1. In this case we do not explicitly write the discount.

We define as abbreviation a modality

$$\begin{aligned} \square \,^d \phi =\lnot \lozenge \,^d \lnot \phi \,, \end{aligned}$$

which can be understood as “$\phi$ holds for a long time”. For some interval $[t_0, t_1]$ the semantics is

$$\begin{aligned} \tau (\square \,^d \phi ) \, [t_0, t_1] = 1 - \sup \{d^{t_2 - t_1} \cdot (1- \tau (\phi )\,[t_1, t_2] \mid t_2\ge t_1 \wedge t_2 \in \mathrm {span}(\tau ))\} \, . \end{aligned}$$

We point out that the supremum searches for a small $t_2\ge t_1$ that makes the truth value of $\tau (\phi )$ on $[t_1, t_2]$ small. Further, the greater the interval $[t_1, t_2]$ is chosen, the greater the truth value of $\square \,^d \phi$ becomes. Note that the truth value of $\square \,^d\phi$ increases with the decrease of d, while the truth value of $\lozenge \,^d\phi$ decreases with the decrease of d.

To express that a state expression S holds throughout an interval, we use the abbreviation:

$$\begin{aligned} \lceil S\rceil ={\textstyle \int }\lnot S = 0 \wedge \ell > 0 \end{aligned}$$

where $\ell$ is an abbreviation of ${\textstyle \int }(S' \vee \lnot S')$ for an arbitrary state expression $S'$.

With $\lozenge \,\lozenge \,\phi$ we express that on some right interval, which may or may not be adjacent to the current interval, $\phi$ holds. We shall use the abbreviation $\mathrm {F}_{S} \phi$ to denote that there is some future point interval, say [t, t], where S “happens” and $\phi$ holds, that is, $\phi$ holds on [t, t] and S changes from 0 to 1 at t and keeps the value 1 for some nonzero time:

$$\begin{aligned} \mathrm {F}_{S} \phi =\lozenge \,\lozenge \,\left( \lceil \lnot S\rceil \wedge \left( \begin{array}{ll} &{} \lozenge \,\lceil S\rceil \\ \wedge &{} \lozenge \,(\ell =0 \wedge \phi ) \end{array}\right) \right) \end{aligned}$$

Let $\mathrm {G}_{S} \phi =\lnot \mathrm {F}_{S} \lnot \phi$. The formula $\mathrm {G}_{S} \phi$ thus means that for all future time points t, if S happens at t, then $\phi$ holds on [t, t].

Example 1

As an example we consider the three formulas:

$$\begin{aligned} \phi _0&=\lozenge \,^{0.8} ({\textstyle \int }P \ge 3) \\ \phi _1&=\lozenge \,^{0.9}\ \square \,^{0.8} ({\textstyle \int }P - {\textstyle \int }\lnot P \le 3) \\ \phi _2&=\mathrm {G}_{Q} \lozenge \,^{0.8} ({\textstyle \int }P \ge 2) \end{aligned}$$

and the two timed words:

• $\tau _0 = \begin{array}[t]{l} (\{P\},0)\ (\{\},2)\ (\{P\},3)\ (\{\},5)\ (\{P\},6)\ \\ \qquad \qquad (\{\},8)\ (\{P\},9)\ (\{\},11)\ (\{P\},12) (\{\},14), \end{array}$

• $\tau _1 = \begin{array}[t]{l} (\{\},0)\ (\{Q\},1)\ (\{P\},2)\ (\{Q\},4)\ (\{P,Q\},5)\ \\ \qquad \qquad (\{\},6)\ (\{P\},7)\ (\{\},8)\ (\{Q\},9)\ (\{\},10)\ \\ \qquad \qquad \qquad \qquad (\{P\},11)\ (\{\},12)\ (\{P\},13)\ (\{\},14), \end{array}$

which induce the trajectories depicted in Fig. 1.

Fig. 1.

Graphical representation of two timed words. The word $\tau _1$ contains two atomic propositions P and Q. We assume that all values remain 0 after time point 14.

These above formulas can be explained as follows:

• $\phi _0$ reads “soon P has held for at least 3 time units”,

• $\phi _1$ reads “soon P should hold no more than 3 time units more than $\lnot P$, for a long time”, and

• $\phi _2$ reads “every time Q changes its value from 0 to 1, then soon P has held for 2 time units”.

Evaluate $\phi _0$ on ${\tau _0}$ : The earliest point when ${\textstyle \int }P\ge 3$ is satisfied is at $t=4$. We calculate:

$$\begin{aligned} \begin{array}{ll} &{} \tau _0(\lozenge \,^{0.8} ({\textstyle \int }P\ge 3))\ [0,0]\\ &{}\quad = \sup \{0.8^t \cdot \tau _0({\textstyle \int }P\ge 3)\, [0,t]\ |\ t \in \mathrm {span}(\tau _0) \}\\ &{}\quad = 0.8^4 \eqsim 0.41 \end{array} \end{aligned}$$

Evaluate $\phi _1$ on ${\tau _0}$ : In $\phi _1$ the inner modality is given $t_0$ and chooses the smallest $t_1$ such that ${\textstyle \int }P - {\textstyle \int }\lnot P \le 3$ is violated. The outer modality chooses $t_0$ such that the product of its discount $0.9^{t_0}$ multiplied with the truth value archived by the inner modality becomes maximal. We calculate (assuming that $t_0, t_1 \in \mathrm {span}(\tau _0)$):

$$\begin{aligned} \begin{array}{ll} &{} \tau _0(\lozenge \,^{0.9}\ \square \,^{0.8} ({\textstyle \int }P - {\textstyle \int }\lnot P \le 3))\, [0,0]\\ &{}\quad = \mathop {\sup }\nolimits _{t_0\ge 0} \{0.9^{t_0} \cdot (1- \mathop {\sup }\nolimits _{t_1 \ge t_0}\{0.8^{t_1 - t_0} \cdot (1 -\tau _{0}({\textstyle \int }P - {\textstyle \int }\lnot P \le 3)\, [t_0,t_1]) \}) \}\\ &{}\quad = 0.9^{2} \cdot (1 - 0.8^{12 - 2} \cdot (1 - \tau _0({\textstyle \int }P - {\textstyle \int }\lnot P \le 3)\, [t_0,t_1])\\ &{}\quad = 0.9^{2} \cdot (1 - 0.8^{12 - 2} \cdot (1 - 0)) \eqsim 0.72 \end{array} \end{aligned}$$

Evaluate $\phi _2$ on ${\tau _1}$ : We evaluate $\psi =\lozenge \,^{0.8} ({\textstyle \int }P \ge 2)$ on all point intervals [t, t], where Q changes its value from 0 to 1. For $\tau _1$ these points are 1, 4 and 9. The truth value is $\min \{\tau _1(\psi )\, [1,1], \tau _1(\psi )\, [4,4], \tau _1(\psi )\, [9,9] \}$, which evaluates to $\min \{0.8^{4-1}, 0.8^{8-4}, 0.8^{14-9}\} \eqsim 0.33$.

3 Model Checking

In this section we prove that model checking for a relevent fragment of DDC is approximable, where the model is given as a timed automaton [2]. To this end we first show that for approximation it is sufficient to consider only bounded prefixes of runs. Then we give a reduction to quantified linear real arithmetic.

3.1 The Model

As model we use timed automata that have atomic propositions that hold in states (denoted by $\varLambda$) instead of events on edges. Additionally, our timed automata have a set of allowed initial clock valuations, where the initial value of a clock may be different from 0. Further, we assume that our timed automata are strongly non-Zeno [3]. This is the case, iff there is a non-zero constant $c\in \mathbb {R}_{>0}$ such that in every control cycle at least c units of time passes. Formally, for every path $l_0 \xrightarrow {e_0} \dots \xrightarrow {e_{n-1}} l_n$ with $l_0=l_n$ there is an edge that resets some clock x and an edge or a location with a constraint $x\ge c$. For ease of exposition we assume this constant to be a natural number greater than 0.

Definition 3 (Timed Automata)

Let $\mathcal {X}$ be a finite set of non-negative real-valued variables, called clocks and let $\mathbb {V}$ be the set of all clock valuations. Then $\mathbb {B}(\mathcal {X})$ is the set of all conjunctions of constraints of the form $x - y \bowtie c$ or $x \bowtie c$ with $x,y\in \mathcal {X},c \in \mathbb {Q}, \bowtie \, \in \{<,>,\ge , \le \}$. Further, let $AP$ be a finite set of atomic propositions. A timed automaton is a tuple $A=(L,E,I, Inv ,\varLambda ,\mathcal {X})$, where $L$ is the set of locations, $E\subseteq L\times \mathbb {B}(\mathcal {X}) \times 2^\mathcal {X}\times L$ is the set of edges, $I\subseteq L\times \mathbb {V}$ is the set of initial states, $Inv : L\rightarrow \mathbb {B}(\mathcal {X})$ are the invariants per location and $\varLambda :L\rightarrow \mathbb {B}( AP )$ assigns a set of atomic propositions which hold in a location.

Note that commonly $I$ is defined as $L' \times \{\mathbf {0}\}$, where $L'\subseteq L$ and $\mathbf {0}\in \mathbb {V}$ is the clock valuation where all clocks have value 0.

Let $\nu$ be a clock valuation, R a set of clocks and g a guard. We define $\nu +t$ is the clock valuation where the values of all clocks are increased by t. With $\nu [R \mapsto 0]$ we denote the clock valuation resulting from $\nu$ by setting all clock values in R to 0. And with $\nu \in g$ we denote that $\nu$ satisfies the constraints in g.

Definition 4 (Runs of Timed Automata)

Given a timed automaton $A=(L,E,I, Inv ,\varLambda ,\mathcal {X})$ and a possibly infinite timed word $\tau = (\sigma _0,t_0) \dots (\sigma _i,t_i) \dots$ let $\varDelta _i = t_{i+1}-t_i$ and let N be the set of integers such that $i\in N$ iff there is an element $(\sigma _i,t_i)$ in $\tau$. This means that $N=\mathbb {N}$ if $\tau$ is infinite. A run of A on $\tau$ is a sequence

$$\begin{aligned} \pi = (l_0,\nu _0) \dots (l_i,\nu _i) \dots \end{aligned}$$

with $(l_0,\nu _0) \in I$, for every $j\in N$ we have $\sigma _j \implies \varLambda (l_j)$ and for every $j,j+1 \in N$ there exists an edge $(l_j,g_j,R_j,l_{j+1})\in E$ such that $\forall t\in \mathbb {R}{.} 0 \le t \le \varDelta _j \implies \nu _j + t \in Inv (l_j)$, $\nu _j + \varDelta _j \in g$, $\nu _{j+1} \in Inv (l_{j+1})$ and $\nu _{j+1} = (\nu _j + \varDelta _j)[R_j \mapsto 0]$.

With L(A) we denote the set of all timed words for which there exists a run on A.

As we work with real-valued truth values, here model checking gives a value in the interval [0, 1].

Definition 5 (Model Checking Timed Automata)

Let A be a timed automaton and $\phi$ be a DDC formula. We define model checking as computing

$$\begin{aligned} \min _{\tau \in L(A)} \{ \tau (\phi )\,[0,0] \} \,. \end{aligned}$$

When the timed automaton has upper bounds for the values of all clocks in all locations the set of reachable states is computable with a finite representation. The goal of this constraint is to avoid over approximation introduced by the normalisation step of reachability algorithms [5]. We use this to reduce computing the satisfaction value of $\mathrm {G}_{S} \phi$ by A to computing the satisfaction value of $\phi$ by a transformed automaton $A'$.

Lemma 1

Let $\phi$ be a $\textit{DDC}_{<1}$ formula, $A=(L,E,I, Inv ,\varLambda ,\mathcal {X})$ a timed automaton with $\forall l \in L, x\in \mathcal {X}{.} \exists c\in \mathbb {Q}{.} x \lesssim c \in Inv (l), \lesssim \, \in \{<,\le \}$, and S a state expression. Then

$$\begin{aligned} \min _{\tau \in L(A)} \{ \tau (\mathrm {G}_{S} \phi )\,[0,0] \} = \min _{\tau ' \in L(A')} \{ \tau '(\phi )\,[0,0] \} \end{aligned}$$

where $A'=(L,E,I', Inv ,\varLambda ,\mathcal {X})$ is the timed automaton obtained from A, by letting the initial states $I'$ be those where the state expression S just has become true. Let $Reach$ be the set of reachable states in A, let $L_S$ be the set of locations where S holds and define

$$\begin{aligned} I' =\{ (l,\nu ) \mid l\in L_S&\wedge (l',g,R,l)\in E\wedge (l',\nu ')\in Reach \\&\quad \wedge \nu '\in g {}\wedge \nu \in Inv (l){} \wedge \nu '[R\mapsto 0] = \nu \wedge l'\in L\setminus L_S \} \,. \end{aligned}$$

Furthermore, $I'$ is computable and has a finite representation using linear arithmetic [5].

We give our definition of approximate model checking.

Definition 6 (Approximate Model Checking)

Let A be a timed automaton, $\phi$ be a $\textit{DDC}_{<1}$ formula and let $\epsilon \in (0,1]$ be the desired precision. Then approximate model checking is to compute a truth value $v \in \mathbb {R}$ with $0 \le v \le 1$ such that

$$\begin{aligned} v \in \min _{\tau \in L(A)} \{\tau (\phi )\,[0,0]\} \pm \epsilon \,. \end{aligned}$$

For this we compute the point in time $\delta =\log _d \epsilon$ such that the value of v is almost not affected by any suffix of the timed word starting at time $\delta$. This is possible because all modalities in $\text {DDC}_{<1}$ are discounted by less than 1 and hence the effect of a timed word on the truth value becomes less and less as time advances. Note that for other discounting functions, e.g. $\frac{1}{1+d\cdot (t-t')}$ other computations are necessary. However, for any computable strictly monotonic discounting function with limit 0 such a point, after which the effect on the truth value is $\le \epsilon$, is computable.

Lemma 2

Given a $\textit{DDC}_{<1}$ formula $\phi$ and an allowed error $\epsilon$, let $d_{\mathrm {m}}$ be the largest discount constant occurring in $\phi$ such that for all other discounts d in $\phi$ we have $d \le d_\mathrm {m}$ and let $\delta = \log _{d_{\mathrm {m}}} \epsilon$. Then for any timed word $\tau$ we have

$$\begin{aligned} |\tau (\phi )\,[0,0] - \tau _\delta (\phi )\,[0,0] | \le \epsilon \,. \end{aligned}$$

We transform the approximate model checking problem for $\text {DDC}_{<1}$ to quantified linear real arithmetic, which we now define.

Definition 7 (Quantified Linear Real Arithmetic (QLRA))

We define the syntax of quantified linear real arithmetic (QLRA) as

$$\begin{aligned} \phi&\;{:}{:}{=}\; \lnot \phi \mid \phi \vee \phi \mid term \lesssim term \mid \exists x{.} \phi \,,\\ term&\;{:}{:}{=}\; a \mid term + term \mid a \cdot term \mid x \,,\\ a&\;{:}{:}{\in }\; \mathbb {Q}\end{aligned}$$

where $\lesssim \,\in \{<,\le \}$ and x is a variable over $\mathbb {R}$.

With linear arithmetic we denote the fragment of QLRA where all quantifiers are located under an even number of negations.

To check to what extent a timed automaton satisfies a formula we use bounded reachability checking via linear arithmetic. The following lemma specifies which variables we use in the bounded reachability checking encoding. The construction can be found, e.g., in [4, 25].

Lemma 3

(Bounded Reachability, e.g. [4, 25]). Given a timed automaton A, an initial zone and a step bound l, we can encode the existence of a run of length ${\le }{l}$, starting at any state in the initial zone, in linear arithmetic. We shall assume that this run is described using variables $\underline{t_i}, \underline{P_i}$, for $0\le i \le l$, describing whether in the interval $[t_i,t_{i+1})$ the propositional variable P holds or not.

3.2 Encoding of the Semantics for Formulas

We encode the semantics of DDC in QLRA. As the semantics of DDC uses exponentials we cannot encode the exact semantics. However, we can approximate the truth value with finite but arbitrary high precision. We use this encoding to prove that approximative model checking for strongly non-Zeno timed automata is computable.

Suppose that $F(\bar{y})$ is a formula of QLRA having $\bar{y}$ as free variables (and possibly others) and suppose that $e(\bar{y})$ is a linear term, then we can express

$$\begin{aligned} x = \mathrm {lub} \{ e(\bar{y}) \in \mathbb {R}\ |\ F(\bar{y}) \} \end{aligned}$$

in QLRA, using the abbreviations:

$$\begin{aligned} \begin{array}{lcl} \mathrm {UB}(x,e(\bar{y}), F(\bar{y})) &{} =&{} \forall \bar{y}. F(\bar{y}) \implies x \ge e(\bar{y})\\ \mathrm {LUB}(x,e(\bar{y}), F(\bar{y})) &{} =&{} \mathrm {UB}(x,e(\bar{y}), F(\bar{y})) \wedge \forall z. \mathrm {UB}(z,e(\bar{y}), F(\bar{y})) \implies z \ge x \end{array} \end{aligned}$$

Furthermore, we shall use the following QLRA abbreviation to express that $x= \mathrm {max}(e_1,e_2)$:

$$\begin{aligned} \mathrm {MAX}(x,e_1, e_2) =(e_1 < e_2 \implies x = e_2) \wedge (e_1 \ge e_2 \implies x=e_1) \end{aligned}$$

When v, t, d range over a bounded domain we can approximate an exponential function $v \cdot d^t$ with an arbitrary precision using linear approximations. Below we will use the abbreviation $x\ \mathrm {isApproxOf}\ v\ d\ t$ to denote that x is an approximation of $v \cdot d^t$.

The encoding of a formula $\phi$ in an interval $[t_0,t_1]$ is based on a symbolic first-order formula representation of a bounded model guaranteed by Lemma 3. We shall now show how the semantics of formulas on bounded runs are encoded in QLRA, by defining a QLRA formula $x\ \mathrm {isSemOf}^l\ \phi \ t_0\ t_1$ denoting that x is (an approximation of) the semantics of $\phi$ in the interval $[t_0,t_1]$. This formula is defined by recursion over the structure of $\phi$.

Encoding for ${\tau (\varSigma _{j=0}^n k_j {\textstyle \int }S_j \gtrsim c )\,[t_0,t_1]}$

We show the encoding of $k{\textstyle \int }S \gtrsim c$. The generalisation to linear combinations of durations is easily done in QLRA.

For every interval from $\underline{t_i}$ to $\underline{t_{i+1}}$ we introduce a variable $x_i$ denoting the duration of S on this interval. To this end we introduce the following abbreviations:

$$\begin{aligned} \begin{array}{lcl} z\ \mathrm {isOverlap}_i\ t_0\ t_1 &{} \text {denotes that} &{} z\text { is the length of }[t_0,t_1] \cap [\underline{t_i}, \underline{t_{i+1}}]\text { and}\\ y\ \mathrm {isDur}_i\ S\ t_0\ t_1 &{} \text {denotes that} &{} y\text { is the duration of }S\text { on }[t_0,t_1]\cap [\underline{t_i}, \underline{t_{i+1}}]\text {.} \end{array} \end{aligned}$$

where the definitions are provided below.

For the formula $x\ \mathrm {isSemOf}^l\ k {\textstyle \int }S \gtrsim c\ t_0\ t_1$ we define that if the inequality ($k{\textstyle \int }S \gtrsim c$) holds $x=1$, and otherwise $x=0$:

$$\begin{aligned} \bigl ((\exists y_0, \ldots , y_{l-1}{.} k \cdot \varSigma _{i=0}^{l-1} y_i \gtrsim c \wedge \bigwedge _{i=0}^{l-1} (y_i\ \mathrm {isDur}_i\ S\ t_0\ t_1)) \implies x=1\bigr ) \wedge {} \\ \bigl (\lnot (\exists y_0, \ldots , y_{l-1}{.} k \cdot \varSigma _{i=0}^{l-1} y_i \gtrsim c \wedge \bigwedge _{i=0}^{l-1} (y_i\ \mathrm {isDur}_i\ S\ t_0\ t_1)) \implies x=0 \bigr ) \end{aligned}$$

It is easy to generalize this to cover linear sums of accumulated durations.

The abbreviation $z\ \mathrm {isOverlap}_i\ t_0\ t_1$ is as follows:

$$\begin{aligned} \begin{array}{ll} &{} (t_0 \ge \underline{t_{i+1}} \vee t_1 \le \underline{t_{i}} \implies z=0 ) \\ &{}\quad \wedge (t_0 \le \underline{t_{i}} \wedge \underline{t_{i+1}} \le t_1 \implies z = \underline{t_{i+1}} - \underline{t_{i}} ) \\ &{}\quad \wedge (\underline{t_{i}}\le t_0 \wedge \underline{t_{i+1}} \le t_1 \implies z = \underline{t_{i+1}} - t_0 ) \\ &{}\quad \wedge (t_0 \le \underline{t_{i}} \wedge t_1 \le \underline{t_{i+1}} \implies z = t_1 - \underline{t_{i}} )\\ &{}\quad \wedge ( \underline{t_{i}}\le t_0 \wedge t_1 \le \underline{t_{i+1}} \implies z = t_1 - t_0 ) \end{array} \end{aligned}$$

and the abbreviation $y\ \mathrm {isDur}_i\ S\ t_0\ t_1$ is:

$$\begin{aligned} \begin{array}{llll} &{} (\underline{S} &{} \implies &{} y\ \mathrm {isOverlap}_i\ t_0\ t_1 )\\ \wedge &{} ( \lnot \underline{S} &{}\implies &{} y=0 ) \end{array} \end{aligned}$$

where $\underline{S}$ is the formula obtained from S by replacing every occurrence of a state variable P with $\underline{P_i}$.

Encoding of $\tau (\phi _0 \vee \phi _1)\,[t_0,t_1]$

The formula $x\ \mathrm {isSemOf}^l\ (\phi _0 \vee \phi _1)\ t_0\ t_1$ is defined by:

$$\begin{aligned} \exists y_0,y_1{.} (y_0\ \mathrm {isSemOf}^l\ \phi _0\ t_0\ t_1) \wedge (y_1\ \mathrm {isSemOf}^l\ \phi _1\ t_0\ t_1) \wedge \mathrm {MAX}(x,y_0,y_1) \end{aligned}$$

Encoding of ${\tau (\lnot \phi )\,[t_0,t_1]}$

The formula $x\ \mathrm {isSemOf}^l\ (\lnot \phi )\ t_0\ t_1$ is defined by $\exists y{.} \,(y\ \mathrm {isSemOf}^l\ \phi \ t_0\ t_1) \wedge x = 1- y$

Encoding of ${\tau (\lozenge \,^d \phi )\,[t_0,t_1]}$

The formula $x\ \mathrm {isSemOf}^l\ (\lozenge \,^d \phi )\ t_0\ t_1$ is defined by $\exists t_2, r{.} \mathrm {LUB}(x, e(y), F(t_2,y,r ))$, where

$$\begin{aligned} \begin{array}{llll} e(y) &{} = y\\ F(t_2,y,r) &{} = (r\ \mathrm {isSemOf}^l \phi \ t_1\ t_2) &{} {}\wedge (y\ \mathrm {isApproxOf}\ r\ d\ (t_2-t_1)) \\ &{}&{} {}\wedge t_2 \ge t_1\wedge t_2 \le \underline{t_l} \end{array} \end{aligned}$$

We use our approximation of the semantics in QLRA and the bounded model checking approach to prove that approximate model checking is computable.

Theorem 1 (Approximate Model Checking)

Given a strongly non-Zeno timed automaton A and a $\textit{DDC}_{<1}$ formula $\phi$ and a desired precision $\epsilon \in \mathbb {R}_{>0}$, the approximate model-checking problem is effectively computable: There is a procedure computing $v\in [0,1]$ such that

$$\begin{aligned} v \in \min _{\tau \in L(A)} \{ \tau (\phi )\,[0,0] \} \pm \epsilon \,. \end{aligned}$$

Proof

Let $\epsilon _1,\epsilon _2 > 0$ be such that $\epsilon _1+\epsilon _2=\epsilon$. According to Lemma 2, we can bound the time horizon of interest to $\delta = \log _{d_{\mathrm {m}}} \epsilon _1$ with $d_\mathrm {m}$ again being the largest discount constant occurring in $\phi$, thereby obtaining

$$\begin{aligned} |\tau (\phi )\,[0,0] - \tau _\delta (\phi )\,[0,0] | \le \epsilon _1 \,. \end{aligned}$$

(1)

As A is strongly non-Zeno, the number of transitions occurring in A within $\delta$ time units is bounded by a constant $l\in \mathbb N$, which can be computed as $\lceil M\delta \rceil$ with M being the length of the longest cycle in the transition graph of A.

Given this bound l on the length of the runs to be considered, we can easily obtain (Q)LRA encodings of both the runs of A of the appropriate length ${\le }{l}$ and of the l-bounded DDC semantics: Let

$$\begin{aligned} R_j = F_A^j(\underline{t}, \underline{P})\, , \end{aligned}$$

where $F_A^j(\underline{t}, \underline{P})$ is the LRA-encoding of the runs of A of length j according to Lemma 3, and let

$$\begin{aligned} Sem _j(y) = (y\ \mathrm {isSemOf}^j\ \phi \ 0\ 0) \, , \end{aligned}$$

where $y\ \mathrm {isSemOf}^j\ \phi \ 0\ 0$ is the above encoding of the DDC semantics, with the look-up tables for approximating exponentials being developed to accuracy $\epsilon _2$ over the argument range $[0,\delta ]$.

We furthermore introduce an abbreviation $\mathrm {GLB}(x, y, F(y))$ for a formula defining $x = \mathrm {glb}\ \{ y\ |\ F(y) \}$ just as we did for the least upper bound. Then the satisfying valuation of $\mathrm {GLB}(x, y, \bigvee _{j=1}^l (R_j\wedge Sem _j(y)))$, which can be determined effectively by QLRA solving, satisfies

$$\begin{aligned} |x-\min _{\tau \in L(A)} \{ \tau _\delta (\phi )\,[0,0] \}| \le \epsilon _2 \end{aligned}$$

due to the accuracy of approximating the exponentials, which together with Eq. (1) in turn implies

$$\begin{aligned}&|x-\min _{\tau \in L(A)}\{\tau (\phi )\,[0,0] \}| \le \epsilon _2+\epsilon _1 = \epsilon \\ \iff&x \in \min _{\tau \in L(A)} \{ \tau _\delta (\phi )\,[0,0] \} \pm \epsilon \,. \end{aligned}$$

   $\square$

4 Example

To support our claims that we can reason about interesting problems with DDC we provide an example in this section.

4.1 Production Cell

We consider two drilling machines that generate heat while drilling. These machines independently of each other process work pieces of different sizes, and the drilling time needed to finish a work piece depends on the size of the piece. If a machine drills for a long time without interruption the machine becomes too hot. If the machine is too hot, it will gradually take damage. It is undesirable to always avoid that the machine becomes too hot, because then production will be too low. The desired property is that the machine soon cools down, after it became too hot.

Let $i\in \{0,1\}$. We represent that machine i is too hot by a propositional variable $H_i$, that the machine is drilling by $D_i$ and the durability of the machine by the discount (here 0.9, where closer to 1 means more durable). Further, there are coefficients (here 1, 2) representing how quickly the temperature changes over time in the respective locations and here 5 is the desired cooldown to achieve after the machine has become too hot. We formalise the desired property as

$$\begin{aligned} \mathrm {G} _{H_0}(\lozenge \,^{0.9} ({\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5)) \wedge \mathrm {G} _{H_1}(\lozenge \,^{0.9} ({\textstyle \int }\lnot D_1 -2 {\textstyle \int }D_1 \ge 5))\,. \end{aligned}$$

The controllers $A_0$ and $A_1$ of the machines are depicted on the left hand side of Fig. 2. On the right hand side of Fig. 2 we depict the automaton B that determines how quickly the working pieces may appear and that assigns the working pieces nondeterministically to the machines.

Fig. 2.

On the left hand side we see the controller $A_i$ with $i\in \{0,1\}$ of a drilling machine. The upper bounds of 100, serve to make Lemma 1 applicable, the other upper bounds restrict the maximal drilling time needed for small and big working pieces. The self loop in $\mathrm {free}_i$ serves to make the parallel composition $A_0 \parallel A_1 \parallel B$ deadlock free. On the right hand side we see B, which controls how quickly work pieces may appear.

4.2 Computing the Satisfaction Value

Here we focus on the satisfaction value of the subformula $\mathrm {G} _{H_0}(\lozenge \,^{0.9} ({\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5))$. However, the satisfaction value for the other subformula is equal.

Let $C =(A_0 \parallel A_1 \parallel B) = (L,E,I, Inv ,\varLambda ,\mathcal {X})$ be the parallel composition of $A_0, A_1$ and B. To approximate the satisfaction value of $\mathrm {G} _{H_0}(\lozenge \,^{0.9} ({\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5))$ by C we apply Lemma 1 for the first subformula and create $C'=(L,E,I', Inv ,\varLambda ,\mathcal {X})$ that has all states as initial states in which the edge from $\mathrm {db}_0$ to $\mathrm {hot}_0$ was just taken. The set $I'$ is defined as¹

$$\begin{aligned} I'=&\{((\mathrm {db}_0, \mathrm {free}_1, \mathrm {init}), \nu ) \mid \nu \in \bigl ( 7 \le x_0 \le 8 \wedge x_0 = x_\mathrm {b} \wedge x_\mathrm {s} \le 100 \wedge {} \\&\qquad ((x_1 - x_\mathrm {s} \le -2 \wedge x_1 \le x_\mathrm {b}) \vee (x_\mathrm {b}- x_\mathrm {s} \le -2 \wedge x_1 \le 100) ) \bigr ) \}\cup {} \\&\{((\mathrm {db}_0, \mathrm {ds}_1, \mathrm {init}), \nu ) \mid \nu \in (7 \le x_0 \le 8 \wedge x_0 = x_\mathrm {b} \wedge x_\mathrm {s} \le 3 \wedge x_1 = x_\mathrm {s} ) \} \,. \end{aligned}$$

Let the desired precision be $\epsilon =0.1$. According to Lemma 2 we have $\delta = \log _{0.9} \epsilon$, which is less than 22. Let $\delta =22$ and note that by choosing a larger $\delta$ than necessary we increase the precision of the computation. The approximation of the satisfaction value is

$$\begin{aligned} \min _{\tau \in L(C')}\{ \sup \{ 0.9^t \cdot \tau _{22}( {\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5)\,[0,t]\mid 0\le t \le 22 \} \} \pm \epsilon \,. \end{aligned}$$

Hence, we are looking for a run $\pi$ in $C'$, such that in the timed word induced by $\pi$ the smallest t for which $\tau _{22}({\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5)\,[0,t]$ holds, is large.

A run that maximises the time t needed to satisfy ${\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5$ is depicted below. The intuition of the run is that directly after the machine finished a big working piece, it has to work on a small working piece. The location of B always is $\mathrm {init}$. Hence, the states in the run have the form $(l_0,l_1,\nu (x_0),\nu (x_1),\nu (x_\mathrm {s}),\nu (x_\mathrm {b}))$ where $l_i$ is a location from $A_i$ with $i\in \{0,1\}$ and $\nu (y)$ is the value of the clock y under the clock valuation $\nu$:

$$\begin{aligned} \pi =&(\mathrm {hot}_0,\mathrm {free}_1,7,0,19,7) (\mathrm {hot}_0,\mathrm {free}_1,8,1,20,8) (\mathrm {free}_0,\mathrm {free}_1,8,1,20,8) \\&\qquad (\mathrm {ds}_0,\mathrm {free}_1,0,1,0,8) (\mathrm {ds}_0,\mathrm {free}_1,3,4,3,11) \\&\qquad (\mathrm {free}_0,\mathrm {free}_1,3,4,3,11) (\mathrm {free}_0,\mathrm {free}_1,16,17,16,24) \end{aligned}$$

The run spends 4 time units in locations where $D_0$ holds ($\mathrm {hot}_0$, $\mathrm {ds}_0$), and 13 time units in locations where $\lnot D_0$ holds ($\mathrm {free}_0$). Hence, it satisfies ${\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5$ after $t=17$ time units and we have

$$\begin{aligned} \min _{\tau \in L(C')}\{\tau (\lozenge \,^{0.9} ({\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5))\} \in \ 0.9^{17} \pm 0.1 \eqsim 0.17 \pm 0.1 \,. \end{aligned}$$

In general, by considering only bounded prefixes of all runs we introduce an error of at most $\epsilon$. However, in our example the result $0.9^{17}$ is exact, because in $C'$ all runs starting from $I'$ satisfy ${\textstyle \int }\lnot D_0 -2 {\textstyle \int }D_0 \ge 5$ in less than $\delta =22$ time units.

We see that the controllers of the drilling machines satisfy our cooldown property poorly. To fix this we could introduce a scheduler in between the controllers $A_0,A_1$ and the spawner of the working pieces B. This scheduler would then assign the working pieces to machines in a way that avoids assigning two successive working pieces to the same machine. As the model then would be quite big, we would need automation to compute the satisfaction value for the larger example. Fortunately, for strongly non-Zeno timed automata and properties of the form $\lozenge \,^d \varSigma _{i=0}^{n-1} k_i{\textstyle \int }S_i \sim c$ and $\square \,^d \varSigma _{i=0}^{n-1} k_i{\textstyle \int }S_i \sim c$ we can compute the satisfaction value via optimisation modulo theories [6, 23].

5 Conclusion

Discounting has been introduced to temporal logics to formalise reasoning about temporal quality of systems [1, 13], where temporal quality quantifies how soon events of interest happen, rather than just answering the qualitative question whether they happen at all. We introduced discounting to Duration Calculus to be able to analyse the quality of real-time systems w.r.t. duration properties. Our main result is that, with the fragment $\text {DDC}_{<1}$ consisting of all formulas where the discounts are ${<}{1}$, we identified a fragment of DDC where model checking for timed automata is approximable under mild assumptions. While this only allows us to reason about bounded prefixes of runs, our reduction of approximating the satisfaction value for formulas $\mathrm {G}_{S} \phi$ (read: “whenever S happens $\phi$ holds thereon”) to model checking $\text {DDC}_{<1}$ enables us to also reason about infinite runs. At last, we provided an extensive example to demonstrate the usefulness of discounting in temporal logics in general and of discounting duration properties in particular.

For future work it is interesting to see how large the fragment of DDC is, for which model checking is approximable.

In Sect. 4 we mentioned that for properties of the form $\lozenge \,^d \varSigma _{i=0}^{n-1} k_i{\textstyle \int }S_i \sim c$ and $\square \,^d \varSigma _{i=0}^{n-1} k_i{\textstyle \int }S_i \sim c$ with $d<1$ the satisfaction value can be approximated efficiently via a reduction to optimisation modulo theories [6, 23]. Naturally, it is desirable to find efficient algorithms for larger fragments of DDC.

Further, in [1, 13] operators, such as taking the average of two formulas, that are not available in qualitative logics, were studied. To find or define such operators and evaluate their usefulness and their effect on computability is another interesting challenge. One such operator may be $\phi \rightarrow \psi =\min \{1,1-u+v\}$ from Łukasiewicz logics [18], where u, v are the truth values of $\phi ,\psi$. This definition of implication allows for a closer connection between the truth values of $\phi$ and $\psi$ than the definitions we used.

Durations in our setting correspond to costs in the setting of multi-priced timed automata (MPTA) [19]. In our work we discovered that often we are interested in the costs of handling a temporal event (as indicated by our use of $\mathrm {G}_{S} \phi$). This could be modelled in MPTA by resetting the cost variable. As this reset action would not depend on the costs, but only on observable behaviour these enhanced MPTA might have interesting decidable problems.