# A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid
Systems: Extended Technical Report

Hammad Ahmad<EMAIL_ADDRESS>University of Michigan, Ann ArborAnn
ArborMichigan48109 and  Jean-Baptiste Jeannin<EMAIL_ADDRESS>University of
Michigan, Ann ArborAnn ArborMichigan48109

###### Abstract.

Signal temporal logic (STL) was introduced for monitoring temporal properties
of continuous-time signals for continuous and hybrid systems. Differential
dynamic logic (d$\mathcal{L}$) was introduced to reason about the end states
of a hybrid program. Over the past decade, STL and its variants have
significantly gained in popularity in the industry for monitoring purposes,
while d$\mathcal{L}$ has gained in popularity for verification of hybrid
systems. In this paper, we bridge the gap between the two different logics by
introducing signal temporal dynamic logic (STd$\mathcal{L}$) – a dynamic logic
that reasons about a subset of STL specifications over executions of hybrid
systems. Our work demonstrates that STL can be used for deductive verification
of hybrid systems. STd$\mathcal{L}$ significantly augments the expressiveness
of d$\mathcal{L}$ by allowing reasoning about temporal properties in given
time intervals. We provide a semantics and a proof calculus for
STd$\mathcal{L}$, along with a proof of soundness and relative
completeness.111This technical report is an extended version with detailed
proofs of the paper “A Program Logic to Verify Signal Temporal Logic
Specifications of Hybrid Systems” that appeared at HSCC 2021(Ahmad and
Jeannin, 2021).

##  1\. Introduction

Recent technological advances have made our transportation, manufacturing and
communication facilities safer, cheaper, and more reliable. However, they have
also increased our reliance on computer systems modeling and controlling
objects of our physical world. Prime examples of such objects include cars on
our roads, robots in our manufacturing plants, and satellites orbiting our
planet. Such systems, referred to as cyber-physical systems (CPSs) (Rajkumar
et al., 2010), often fall under the category of hybrid systems: their
programmable controllers typically exhibit discrete behavior, while the laws
of physics that the systems are restricted by are continuous in nature.

The prevalence of hybrid systems around us, coupled with our increased
reliance on these systems, has necessitated further exploration of reasoning
about such systems. This process involves reasoning about the _states_ of the
hybrid system. A state is considered safe if it does not violate any safety
property of the system, and considered live if the system can make some useful
progress from that state. Verifying a system guarantees safety and liveness in
the system. Signal temporal logic (STL) (Maler and Nickovic, 2004; Maler and
Ničković, 2013) was introduced to monitor properties over continuous-time
signals of continuous and hybrid systems in given time intervals, and has
since been used primarily for monitoring purposes. Dynamic logic (Harel et
al., 2001) was introduced as a formal system for reasoning about programs.
Differential dynamic logic (d$\mathcal{L}$) (Platzer, 2008) was built on top
of dynamic logic to reason about the end states of a hybrid program, to ensure
that the end state is a safe state. However, a hybrid system that is in a safe
state at the end of a program’s execution may not have been in a safe state
throughout the program’s execution: it is possible for a safety property to be
violated during the execution of a program and be held at the termination of
the program. Therefore, it is vital to verify that hybrid systems are safe
during execution in addition to being safe upon termination. Differential
temporal dynamic logic (dTL) (Platzer, 2010a) and differential temporal
dynamic logic with nested temporalities (dTL2) (Jeannin and Platzer, 2014a, b)
use both dynamic logic – to reason about all possible executions of a program
– and a fragment linear temporal logic (LTL) – to reason about intermediate
states of each execution – to tackle this challenge.

While dTL and dTL2 are able to reason about intermediate states of a hybrid
system during program execution, the logics are still unable to reason about
intermediate states of a system in given time intervals. This is a major
limitation of the logics, since such reasoning abilities can be crucial in
ensuring safety of a hybrid system (e.g., ensuring that a self-driving car
applies its brakes within $x$ seconds of spotting a stop sign, as opposed to
ensuring that the car applies its brakes _eventually_ after spotting a stop
sign). STL is able to prove properties about a system in given time intervals,
but the logic reasons about only _one_ execution of a system, not all possible
executions. Therefore, using STL alone to reason about safety in hybrid
systems is not sufficient.

In this paper, we present signal temporal dynamic logic (STd$\mathcal{L}$), a
logic that integrates a fragment of STL with differential dynamic logic
(d$\mathcal{L}$) to reason both about the intermediate states of a hybrid
system in given time intervals, and about the final states of the system. This
reasoning is enabled by our use of STL, which natively supports formulas of
the form $\square_{[a,b]}\phi$ (i.e., for all times between $t+a$ and $t+b$,
where $t$ is the current time, the property $\phi$ is true) and
$\lozenge_{[a,b]}\phi$ (i.e., there exists a time between $t+a$ and $t+b$ such
that the property $\phi$ is true), but has historically been used mainly for
monitoring purposes. We show that STL can be used for full deductive reasoning
of hybrid systems.

The main contributions of this work are as follows:

  * –

We introduce STd$\mathcal{L}$– a logic that reasons about STL formulas for the
first time in the context of d$\mathcal{L}$, bringing together results from
two different communities with little overlap into a common framework.

  * –

We introduce a notion of timing hybrid programs to bridge the gap between
d$\mathcal{L}$ and STL for verification purposes.

  * –

We provide a semantics for STd$\mathcal{L}$ and sound proof calculus for the
logic, along with a proof of soundness and relative completeness.

The rest of the paper is organized as follows. Section 2 motivates
STd$\mathcal{L}$ by introducing a running example of a use-case from the
industry highlighting the power of the logic. Section 3 introduces the syntax
and semantics of STd$\mathcal{L}$. Section 4 motivates the concept of
normalization of trace formulas in STd$\mathcal{L}$ and presents the proof
system of STd$\mathcal{L}$. Section 5 discusses future directions for
STd$\mathcal{L}$. Section 6 outlines some related work, and Section 7 parts
with concluding thoughts.

##  2\. Motivation and Running Example

Throughout this paper, we use a simplified example of a use-case for
STd$\mathcal{L}$ inspired by industry. As we note in Section 1, a major
limitation of the program logics preceding STd$\mathcal{L}$ is their inability
to reason about temporal properties in specified time intervals. Such
reasoning abilities can be crucial in verifying a hybrid system. While STL is
able to handle formulas specifying properties in given time intervals, the
logic is only able to prove properties about _one_ execution of a hybrid
system, and not all possible executions; we need to be able to reason about
every execution of a hybrid system to be able to claim with certainty
correctness of the system. As such, none of differential dynamic logic,
differential temporal dynamic logic, or signal temporal logic – or other
variants of these logics – alone is sufficient to reason about safety and
liveness in hybrid systems.

To see why, let us examine a simplified version of traction assist from the
automobile industry. Consider a car with some accelerator input and braking
force cruising on the road. The car has a signal that streams a binary value
corresponding to whether or not the car’s sensors detect that the car is
skidding or losing traction, and a Boolean flag corresponding to whether or
not the vehicle’s traction control is engaged. For simplicity, assume the
accelerator input can have a positive or negative value corresponding to
acceleration and deceleration respectively, or a value of zero corresponding
to no acceleration. Assume further that the braking force is a non-negative
integer. Let the wheel rotation of the car’s wheels evolve according to some
differential equation. The car has a safety property requiring that in the
event that the car is skidding, a vehicle traction assist program executes to
help gain traction again and slow down the wheel spin to stop the skidding,
following which the car can accelerate again. According to the safety
property, after running the traction assist program, the car’s traction
control should turn on and within 1 to 5 seconds, the car’s wheel rotation
should fall to under some threshold value (to help regain control).

As we introduce key concepts in the following sections, we also present the
differential equation, the hybrid program, and the safety property for the car
in STd$\mathcal{L}$. We present a proof sketch of the safety property using
the STd$\mathcal{L}$ calculus. We note that safety properties of this class
(i.e., containing temporal references for specified time intervals) are
expressible directly in STd$\mathcal{L}$ (but, to the best of our knowledge,
not in any other logic preceding STd$\mathcal{L}$), and remain crucial in
verifying correctness of hybrid systems.

##  3\. Signal Temporal Dynamic Logic

This section formally defines the syntax and semantics of hybrid programs and
state and trace formulas in STd$\mathcal{L}$. We take special care to ensure
that STd$\mathcal{L}$ is a conservative extension of d$\mathcal{L}$, i.e. the
non-temporal aspects of the state semantics for STd$\mathcal{L}$ are
equivalent to the non-temporal transition semantics of d$\mathcal{L}$
(Definition 5 in (Platzer, 2008)).

###  3.1. Hybrid Programs

We use hybrid programs to model hybrid systems in our work. A hybrid program
$\alpha,\beta$ could be a discrete assignment ($x:=\theta$), a test ($?\chi$),
an ordinary differential equation ($x^{\prime}=\theta\ \&\ \chi$), a non-
deterministic choice ($\alpha\cup\beta$), a sequential composition
($\alpha;\beta$), or a non-deterministic finite repetition ($\alpha^{*}$). As
in d$\mathcal{L}$, a term $\theta$ can be any polynomial with a rational
coefficient, and a condition $\chi$ can be any first-order formula of real
arithmetic.

The syntax of hybrid programs can be summarized as:

$\alpha,\beta::=x:=\theta\ |\ ?\chi\ |\ x^{\prime}=\theta\ \&\ \chi\ |\
\alpha\cup\beta\ |\ \alpha;\beta\ |\ \alpha^{*}$

For the semantics of hybrid programs in STd$\mathcal{L}$, the set of states
${\sf Sta}\,$ is the set of functions from variables to $\mathbb{R}$. A
special state $\Lambda\notin{\sf Sta}\,$ denotes a failure state for the
hybrid system. The trace semantics of a hybrid program $\alpha$ assign a set
of traces $\llbracket\alpha\rrbracket$ to the program. For $v\in{\sf
Sta}\,\cup\\{\Lambda\\}$, we express the function
$\sigma:[0,0]\to\\{v\\},0\mapsto v$ using $\hat{v}$, and $\hat{v}$ is defined
only on the singleton interval [0,0].222We often informally refer to a trace
defined on a singleton interval $\\{i\\}$, e.g. $(\hat{v})$, as a trace that
executes in zero time. A trace, then, is a non-empty, finite sequence
$\sigma=(\sigma_{0},\sigma_{1},\dots,\sigma_{n})$ of subtraces $\sigma_{i}$.
For $0\leq i<n$, the piece $\sigma_{i}$ is a function
$\sigma_{i}:[r_{i-1},r_{i}]\to{\sf Sta}\,$, with the convention $r_{-1}=0$,
where $r_{i}-r_{i-1}$ is the duration of this step and $r_{i}\geq r_{i-1}$.
Where $i=n$, $\sigma_{n}$ can be defined as:

  * –

$\sigma_{n}:[r_{n-1},r_{n}]\to{\sf Sta}\,$, in which case we refer to $\sigma$
as a terminating trace;

  * –

$\sigma_{n}:[r_{n-1},+\infty)\to{\sf Sta}\,$, in which case we refer to
$\sigma$ as an infinite trace;

  * –

$\sigma_{n}:[r_{n-1},r_{n-1}]\to\\{\Lambda\\}$ with $\sigma(r_{n-1})=\Lambda$,
for $n\geq 1$, in which case we refer $\sigma$ as an error trace. $n\geq 1$
ensures that $(\hat{\Lambda})$ is not considered as a trace.

For a trace $\sigma=(\sigma_{0},\dots,\sigma_{n})$, we define a position of
$\sigma$ as a pair $(i,t)$ such that $0\leq i<n$ and $t$ is in the domain of
definition of $\sigma_{i}$. We write $\sigma_{i}(t)$ to refer to the state of
$\sigma$ at $(i,t)$, i.e. $\sigma(i,t)=\sigma_{i}(t)$, and define the domain
of $\sigma$ as:

${\sf dom}(\sigma)=\bigcup_{i=0}^{n}\left(\bigcup_{t\in{\sf
dom(\sigma_{i})}}(i,t)\right)$

We can now define the lengths of traces of hybrid programs.

###### Definition 3.1 (Length of traces of hybrid programs).

The length of a trace
$\sigma=(\sigma_{0},\sigma_{1},\dots,\sigma_{n})\in\llbracket\alpha\rrbracket$,
denoted by $|\sigma|\in\mathbb{R}_{+}\cup\\{+\infty\\}$, is defined
inductively as follows:

  * –

$|\sigma|=r_{n}$ if $\sigma_{n}:[r_{n-1},r_{n}]\to{\sf Sta}\,$;

  * –

$|\sigma|=+\infty$ if $\sigma_{n}:[r_{n-1},+\infty)\to{\sf Sta}\,$;

  * –

$|\sigma|=r_{n-1}$ if $\sigma_{n}:[r_{n-1},r_{n-1}]\to\\{\Lambda\\}$.

The set of all traces of a hybrid program is referred to as ${\sf Tra}\,$, and
we collectively refer to infinite traces and error traces as non-terminating
traces. For a trace $\sigma$, we refer to the state $\sigma_{0}(0)$ as ${\sf
first}\,\sigma$, and we often say that “$\sigma$ starts with $v$” if ${\sf
first}\,\sigma=v$. Likewise, for a finite trace $\sigma$, if $\sigma$
terminates in a non-error state, we refer to the state $\sigma_{n}(r_{n})$ as
${\sf last}\,\sigma$; otherwise, we refer to the state $\Lambda$ as ${\sf
last}\,\sigma$. Note that for any trace $\sigma$, ${\sf first}\,\sigma$ is
always well-defined, but ${\sf last}\,\sigma$ may not be (since infinite
traces have no last state). The value of term $\theta$ in state $v$ is denoted
by $val(v,\theta)$, and the valuation assigning variable $x$ to
$r\in\mathbb{R}$ while matching with $v$ on all other variables is denoted by
$v[x\mapsto r]$. If a state $v$ satisfies some condition $\chi$, we write
$v\vDash\chi$; if $v$ does not satisfy condition $\chi$, we write
$v\nvDash\chi$. Finally, given a trace $\sigma$ and an $x\in\mathbb{R}$, we
use the notation ${\sf dom}(\sigma)\oplus x$ to denote the domain of $\sigma$
shifted by a value of $+x$. For example, if ${\sf dom}(\sigma)=[a,b]$, then
${\sf dom}(\sigma)\oplus x=[a+x,b+x]$.

###### Definition 3.2 (Trace semantics of hybrid programs).

The trace semantics $\llbracket\alpha\rrbracket$ of a hybrid program $\alpha$
is defined as follows:

  * –

$\llbracket x:=\theta\rrbracket=\\{(\hat{v},\hat{w})\ |\ w=v[x\mapsto
val(v,\theta)]\\}$;

  * –

$\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket=\\{(\sigma):\sigma$ is a
state flow of order 1 (Platzer, 2008) defined on $[0,r]$ or $[0,+\infty)$
solution of $x^{\prime}=\theta$, and for all $t$ in its definition domain,
$\sigma(t)\vDash\chi\\}\cup\\{(\hat{v},\hat{\Lambda})\ |\ v\nvDash\chi\\}$;

  * –

$\llbracket?\chi\rrbracket=\\{(\hat{v})\ |\
v\vDash\chi\\}\cup\\{(\hat{v},\hat{\Lambda})\ |\ v\nvDash\chi\\}$;

  * –

$\llbracket\alpha\cup\beta\rrbracket=\llbracket\alpha\rrbracket\cup\llbracket\beta\rrbracket$;

  * –

$\llbracket\alpha;\beta\rrbracket=\\{\sigma\circ\rho\ |\
\sigma\in\llbracket\alpha\rrbracket,\rho\in\llbracket\beta\rrbracket$ when
$\sigma\circ\rho$ is defined$\\}$, where the composition $\sigma\circ\rho$ of
$\sigma=(\sigma_{0},\dots,\sigma_{n})$ and $\rho=(\rho_{0},\dots,\rho_{m})$ is

    * –

$\sigma\circ\rho=(\sigma_{0},\dots,\sigma_{n},\bar{\rho}_{0},\dots,\bar{\rho}_{m})$
if $\sigma$ terminates and ${\sf last}\,\sigma={\sf first}\,\rho$, where
$\bar{\rho}=(\bar{\rho}_{0},\dots,\bar{\rho}_{m})$ is a trace with ${\sf
dom}(\bar{\rho})={\sf dom}(\rho)\oplus|\sigma|$ and for each $i\in\\{0\dots
m\\}$, for each $t\in{\sf dom}(\rho_{i})$,
$\bar{\rho}_{i}(t)=\rho_{i}(t-|\sigma|)$,333Informally, $\bar{\rho}$ is merely
the trace $\rho$ shifted to the right by a value of $+|\sigma|$.

    * –

$\sigma$ if $\sigma$ does not terminate,

    * –

undefined otherwise;

  * –

$\llbracket\alpha^{*}\rrbracket=\bigcup_{n\in\mathbb{N}}\llbracket\alpha^{n}\rrbracket,$
where $\alpha^{0}$ is defined as ?true, $\alpha^{1}$ is defined as $\alpha$,
and $\alpha^{n+1}$ is defined as $\alpha^{n};\alpha$ for $n\geq 1$.

These semantics for hybrid programs are adopted from dTL2 (Jeannin and
Platzer, 2014a). As in dTL2, an important property of the trace semantics of
hybrid programs is that for any hybrid program $\alpha$ and state $v$, there
always exists a trace $\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf
first}\,\sigma=v$ (even if $\sigma$ is an error trace). A key difference
between the semantics of dTL2 and our work is that for a trace
$\sigma=(\sigma_{0},\dots,\sigma_{n})$, while the former define the domain of
each $\sigma_{i}$ from 0 to $r_{i}$, we define the domain of each $\sigma_{i}$
from $r_{i-1}$ to $r_{i}$, to enable easier reasoning about temporal formulas
in given time intervals. As such, our semantics for the composition
$\sigma\circ\rho$ between traces $\sigma$ and $\rho$ requires trace $\rho$ to
be shifted in time by a value of $+|\sigma|$.

####  3.1.1. Running Example: Traction Assist in Cars

Having introduced the semantics of hybrid programs in STd$\mathcal{L}$, we now
formally specify a simplified version of the differential equation ${\sf
cruise}$ that varies the car’s wheel rotation $\rho$. For $\omega$ the
acceleration of the car, $\varphi$ the braking force applied to each of the
car’s wheels, and some positive constants $k$ and $j$, we have

${\sf cruise}(\omega,\varphi)::=\omega\times k-\varphi\times j$

Note that in practice, each of the car’s wheels could have a different wheel
rotation and braking force. For the sake of simplicity, and to avoid
presenting four separate proofs for this example, we assume that each wheel
has the same rotation and braking force.

A very simple version of the hybrid program ${\sf traction\\_assist}$ can then
take the form

(1) $\displaystyle{\sf traction\\_assist}::=$ $\displaystyle\ (?({\sf
no\\_traction});$ (2) $\displaystyle\ {\sf traction\\_control:=1};$ (3)
$\displaystyle\ \omega:=-1;\ \varphi:=10;\ \rho^{\prime}={\sf
cruise(\omega,\varphi)});$

where the signal ${\sf no\\_traction}$ is a binary value of ${\sf true}$ or
${\sf false}$ corresponding to whether or not the car’s sensors detect that
the car is losing traction and the Boolean flag ${\sf traction\\_control}$
keeps track of whether or not the vehicle’s traction control is engaged.444The
variable $\varphi$ is set to an arbitrary non-negative integer for the
purposes of this example.

Several properties of hybrid programs are present in the program ${\sf
traction\\_assist}$. (1) denotes a test to check whether the car has lost
traction; (2) represents an assignment statement setting ${\sf
traction\\_control}$ to on; and (3) shows an evolving ordinary differential
equation that changes the wheel rotation of the car. The sequential
composition operator joins the individual statements together to form a single
hybrid program.

###  3.2. State and Trace Formulas

State and trace formulas are used to reason about hybrid programs. A state
formula is used to express properties about a state, whereas a trace formula
is used to express properties about a trace. The syntax of state and trace
formulas in STd$\mathcal{L}$ can then be summarized as:

$\phi,\psi::=\theta_{1}\geq\theta_{2}\ |\ \neg\phi\ |\ \phi\wedge\psi\ |\
\forall x.\phi\ |\ [\alpha]\pi$ $\pi::=\phi\ |\ \neg\pi\ |\
\square_{{[a,b]}}\phi$ $a,b::=\theta\ |\ \max(\theta_{1},\theta_{2})\ |\
\min(\theta_{1},\theta_{2})\ |\ a+b\ |\ a-b$

A state formula $\phi$ or $\psi$ could express a comparison of two terms
($\theta_{1}\geq\theta_{2}$), a negation of a state formula ($\lnot\phi$), a
conjunction of two state formulas ($\phi\land\psi$), a universally quantified
($\forall x.\phi$) state formula over a variable $x\in\mathbb{R}$, or a
program necessity ($[\alpha]\pi$) indicating that all traces of program
$\alpha$ starting from the current state satisfy $\pi$. For a disjunction of
two state formulas ($\phi\lor\psi$), we define as an abbreviation
$\phi\lor\psi\equiv\lnot(\phi\land\psi)$; for an existentially quantified
($\exists x.\phi$) over a variable $x\in\mathbb{R}$, we define $\exists
x.\phi\equiv\lnot\forall x.\lnot\phi$; and for a program possibility
($\langle\alpha\rangle\pi$) over a trace formula $\pi$ indicating that there
exists a trace of program $\alpha$ starting from the current state that
satisfies $\pi$, we define
$\langle\alpha\rangle\pi\equiv\lnot[\alpha]\lnot\pi$.

A trace formula $\pi$ can express a state formula ($\phi$), a negation of a
trace formula ($\lnot\pi$), or a temporal necessity ($\square_{[a,b]}\phi$)
indicating that given the current time $t$, every trace starting in the
current state satisfies $\phi$ from time $t+a$ and $t+b$. A temporal
possibility ($\lozenge_{[a,b]}\phi$) indicating that every trace starting in
the current state satisfies $\phi$ at some point between time $t+a$ and time
$t+b$ is defined as the abbreviation
$\lozenge_{[a,b]}\phi\equiv\lnot\square_{[a,b]}\lnot\phi$. For time intervals
of the form $[a,b]$, $a$ and $b$ are terms in the hybrid program evaluated in
the first state of a trace (which is always well-defined, see Definition 3.5),
or the $\min$ or $\max$ of two terms in the hybrid program. We allow for $a$
and $b$ to be terms in the hybrid program, and not mere constants, since we
need to allow for a program variable to appear as the lower or upper bound of
an interval $[a,b]$ (see Section 3.5, where the timing variable $q$ is
introduced to appear inside the temporal intervals of an STd$\mathcal{L}$
formula for interval shifting).

###  3.3. Length of Traces and Trace Formulas

Previous works supporting temporal operators within the context of
d$\mathcal{L}$ did not need to reason about the length of a trace or a trace
formula, due to their use of linear temporal logic operators that do not
support reasoning about formulas in time intervals. However, since
STd$\mathcal{L}$ involves verifying a trace over specified time intervals, we
need to incorporate reasoning about lengths of traces and trace formulas to
determine the satisfaction of formulas over traces of hybrid programs. More
specifically, we require that for a hybrid program $\alpha$, a trace
$\sigma\in\llbracket\alpha\rrbracket$ needs to be sufficiently long to
determine the satisfaction of the program necessities and possibilities. This
requirement is inspired by that of STL with respect to signal lengths (Maler
and Nickovic, 2004; Maler and Ničković, 2013), and is similarly justified for
STd$\mathcal{L}$ since it is intuitively nonsensical to verify the
satisfaction of a trace formula of length $\varphi$ against a trace of length
$\varphi_{0}<\varphi$.

###### Definition 3.3 (Minimum length of trace formulas).

The necessary length associated with trace formula $\pi$, written as
$\|\pi\|$, to determine the satisfaction of a program necessity or possibility
is defined inductively as follows:

$\displaystyle\|\phi\|$ $\displaystyle=0$ $\displaystyle\|\lnot\pi\|$
$\displaystyle=\|\pi\|$ $\displaystyle\|\square_{[a,b]}\phi\|$
$\displaystyle=b$

###  3.4. Satisfaction of State and Trace Formulas

The satisfaction of state and trace formulas in STd$\mathcal{L}$ is defined as
follows:

###### Definition 3.4 (Satisfaction of state formulas).

For a state formula $\phi$ and state $v\in{\sf Sta}\,$, we say $v\vDash\phi$
if $v$ satisfies $\phi$. Satisfaction of state formulas with respect to state
$v$ is then defined inductively as follows:

  * –

$v\vDash\theta_{1}\geq\theta_{2}$ if and only if $val(v,\theta_{1})\geq
val(v,\theta_{2})$;

  * –

$v\vDash\neg\phi$ if and only if $v\nvDash\phi$;

  * –

$v\vDash\phi\wedge\psi$ if and only if $v\vDash\phi$ and $v\vDash\psi$;

  * –

$v\vDash\forall x.\phi$ if and only if $v[x\mapsto d]\vDash\phi$ for all
$d\in\mathbb{R}$;

  * –

For $\phi$ a state formula, $v\vDash[\alpha]\phi$ if and only if for every
trace $\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$,
if $\sigma$ terminates, then ${\sf last}\,\sigma\vDash\phi$;

  * –

For $\pi$ a trace formula, $v\vDash[\alpha]\pi$ if and only if for every trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$, if
$|\sigma|\geq val({\sf first}\,\sigma,\|\pi\|)$, then we also have that
$\sigma\vDash\pi$;

Definition 3.4 defines the satisfaction of formulas of the form $[\alpha]\pi$,
for $\pi$ a trace formula, as: “$v\vDash[\alpha]\pi$ iff for each trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$, if
$|\sigma|\geq val({\sf first}\,\sigma,\|\pi\|)$, we also have that
$\sigma\vDash\pi$.” The choice behind this definition for the semantics is not
an obvious one, and as such, is explained here for further clarity.

Since STd$\mathcal{L}$ supports full negation of state formulas, we had take
special care to ensure that the property for duals for program modalities is
not violated in the logic. One of our utmost concerns was to ensure that for
all hybrid programs $\alpha$ and all trace formulas $\pi$, it is always the
case that $[\alpha]\pi\equiv\lnot\langle\alpha\rangle\lnot\pi$. As such, we
had three possible choices for the definition of the semantics for formulas of
this form.

  1. (i)

$v\vDash[\alpha]\pi$ iff for each trace $\sigma\in\llbracket\alpha\rrbracket$
such that ${\sf first}\,\sigma=v$, we have that $\sigma\vDash\pi$.

To ensure that property for duals holds in this case, we would have to define
the dual as:

$v\vDash\langle\alpha\rangle\pi$ iff there exists a trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$ and
$\sigma\vDash\pi$.

  2. (ii)

$v\vDash[\alpha]\pi$ iff for each trace $\sigma\in\llbracket\alpha\rrbracket$
such that ${\sf first}\,\sigma=v$, if $|\sigma|\geq val({\sf
first}\,\sigma,\|\pi\|)$, we also have that $\sigma\vDash\pi$.

We would then have to define the dual as:

$v\vDash\langle\alpha\rangle\pi$ iff there exists a trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$, and
we have that $|\sigma|\geq val({\sf first}\,\sigma,\|\pi\|)$ and
$\sigma\vDash\pi$

  3. (iii)

$v\vDash[\alpha]\pi$ iff for each trace $\sigma\in\llbracket\alpha\rrbracket$
such that ${\sf first}\,\sigma=v$, we have that $|\sigma|\geq val({\sf
first}\,\sigma,\|\pi\|)$ and $\sigma\vDash\pi$.

We would then have to define the dual as:

$v\vDash\langle\alpha\rangle\pi$ iff there exists a trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$, and
if $|\sigma|\geq val({\sf first}\,\sigma,\|\pi\|)$, we also have that
$\sigma\vDash\pi$.

Option (i) is the least complicated and arguably the most intuitive one.
However, it has one major limitation: it fails to specify the behavior of the
logic when the trace being considered is simply not long enough to determine
the satisfaction of a trace formula. Consider the simple hybrid program that
$x:=5$. We could have a property that checks this program:
$[x:=5]\square_{[0,10]}(x=5)$. However, recall that a (discrete) trace of
assignment terminates in zero time. As such, we are left with the following
question: what does it mean for a trace to satisfy a property 10 seconds after
it has already terminated? Clearly, we need to consider the length of the
trace that the property has to be proven over, and ensure that the trace is of
necessary length. This idea is not novel: (Maler and Nickovic, 2004) uses the
same approach for defining satisfaction of formulas over signals.

With option (i) eliminated, we are left with options (ii) and (iii) as the
most obvious candidates for the definition of trace semantics of
STd$\mathcal{L}$. Having one of the definitions be an implication and the dual
be a conjunction is the only way to ensure that the property for duals holds –
it is not possible to have both definitions be implications or conjunctions.
With that in mind, we first look at (iii). It is fairly easy to notice that
the definition provided in (iii) make it virtually impossible for
$[\alpha]\pi$ to be true: it requires _every_ trace
$\sigma\in\llbracket\alpha\rrbracket$ to be of the required length – a trait
that is simply not likely in practice. Similarly, it makes it too easy for
$\langle\alpha\rangle\pi$ to be true: any trace
$\sigma\in\llbracket\alpha\rrbracket$ with length $|\sigma|<\|\pi\|$ can
trivially satisfy the formula. This leaves option (ii), which provides a
definition that makes most sense intuitively. For the $[\alpha]$ case, it
might not be reasonable to require that _all_ traces have the required length.
But for the $\langle\alpha\rangle$ case, since the presence of just one
satisfying trace is sufficient, it should be the case that that one trace is
of the required length. This behavior is captured in the definition in (ii),
and we employ that definition in the state and trace semantics of
STd$\mathcal{L}$.

###### Definition 3.5 (Satisfaction of trace formulas).

For a trace formula $\pi$ and trace
$\sigma=(\sigma_{0},\dots,\sigma_{n})\in{\sf Tra}\,$, we say
$(\sigma,(i,t))\vDash\pi$ if $\sigma$ satisfies $\pi$ starting from subtrace
$\sigma_{i}$ at time $t$. We use $\sigma\vDash\pi$ to say that
$(\sigma,(0,0))\vDash\pi$. Satisfaction of trace formulas with respect to a
trace $\sigma$ is then defined inductively as follows:

  * –

For $\phi$ a state formula, $(\sigma,(i,t))\vDash\phi$ if and only if
$|\sigma|\geq t$ and $\sigma_{i}(t)\vDash\phi$;

  * –

$(\sigma,(i,t))\vDash\neg\pi$ if and only if $(\sigma,(i,t))\nvDash\pi$;

  * –

$(\sigma,(i,t))\vDash\square_{[a,b]}\phi$ if and only if for every
$t^{\prime}\in[t+val({\sf first}\,\sigma,$ $a),t+val({\sf first}\,\sigma,b)]$
and for every $i$ such that $(i,t^{\prime})\in{\sf dom}(\sigma)$, it follows
that $(\sigma,(i,t^{\prime}))\vDash\phi$.

Since we define duals as abbreviations, we can build on Definitions 3.4 and
3.5 to say that:

  * –

$v\vDash\phi\vee\psi$ if and only if $v\vDash\phi$ or $v\vDash\psi$;

  * –

$v\vDash\exists x.\phi$ if and only if $v[x\mapsto d]\vDash\phi$ for some
$d\in\mathbb{R}$;

  * –

For $\phi$ a state formula, $v\vDash\langle\alpha\rangle\phi$ if and only if
there exists a trace $\sigma\in\llbracket\alpha\rrbracket$ such that $\sigma$
terminates with ${\sf first}\,\sigma=v$ and ${\sf last}\,\sigma\vDash\phi$;

  * –

For $\pi$ a trace formula, $v\vDash\langle\alpha\rangle\pi$ if and only if
there exists a trace $\sigma\in\llbracket\alpha\rrbracket$ such that
$|\sigma|\geq val({\sf first}\,\sigma,\|\pi\|)$ and ${\sf first}\,\sigma=v$
and $\sigma\vDash\pi$;

  * –

$(\sigma,(i,t))\vDash\lozenge_{[a,b]}\phi$ if and only if there exists some
$t^{\prime}\in[t+val({\sf first}\,\sigma,a),t+val({\sf first}\,\sigma,b)]$ and
there exists some $i$ such that $(i,t^{\prime})\in{\sf dom}(\sigma)$ and
$(\sigma,(i,t^{\prime}))\vDash\phi$.

Given a trace $\sigma$ and an interval $[a,b]$ such that $val({\sf
first}\,\sigma,b)<val({\sf first}\,\sigma,a)$, we define the interval to be an
empty set. As such, formulas such as $\square_{[a,b]}\phi$ and
$\lozenge_{[a,b]}\phi$ are defined to be trivially true and trivially false
respectively over this empty interval. This choice deviates from the norm set
by STL: formulas like $\square_{[a,b]}\phi$ and $\lozenge_{[a,b]}\phi$ in STL
require that for constants $a$ and $b$, we have $a\geq 0$ and $b\geq a$. This
requirement is more difficult to impose in STd$\mathcal{L}$, since time
interval shifting due to sequential composition (see Section 3.5) could result
in a formula where $val({\sf first}\,\sigma,b)<val({\sf first}\,\sigma,a)$,
and we need the semantics of STd$\mathcal{L}$ to handle such cases
appropriately. In the rest of the paper, given a trace $\sigma$ and an
interval $[a,b]$, we refer to $val({\sf first}\,\sigma,a)$ and $val({\sf
first}\,\sigma,b)$ as simply $a$ and $b$ respectively for easier readability.

###  3.5. Timing Hybrid Programs

A major technical difficulty arising from our integration of STL with
d$\mathcal{L}$ is the fact that we now need to reason about not only the time
intervals where a certain temporal property holds, but also about how the
length of a trace of a hybrid program affects the time intervals under
consideration. This problem surfaces immediately for the sequential
composition of two programs $\alpha$ and $\beta$, but is in fact a general
challenge with the integration of continuous traces from d$\mathcal{L}$ and
temporal operators from STL.

Let us consider a trace
$\sigma=\sigma_{\alpha}\circ\sigma_{\beta}\in\llbracket\alpha;\beta\rrbracket$
such that $\sigma_{\alpha}\in\llbracket\alpha\rrbracket$ terminates at time
$c$, following which $\sigma_{\beta}\in\llbracket\beta\rrbracket$ begins. For
simplicity, let us also assume that $a<c<b$ in determining the satisfiability
of $\square_{[a,b]}\psi$ by $\sigma$. Note that
$\sigma\vDash\square_{[a,b]}\psi$ if and only if
$\sigma_{\alpha}\vDash\square_{[a,c]}\psi$ and
$\sigma_{\beta}\vDash\square_{[0,b-c]}\psi$. Intuitively, this means that
$\alpha$ runs first _until time $c$_ and $\sigma_{\alpha}$ satisfies $\psi$
from time $t+a$ to time $t+c$ (where $t$ is the current time), following which
$\beta$ runs and $\sigma_{\beta}$ satisfies $\psi$ from the time it starts to
the time $t+(b-c)$ (due to a shifting of the time interval, since part of the
interval $[a,b]$ was already satisfied by $\sigma_{\alpha}$). A key property
that this rule relies on is the termination of program $\alpha$ at time $c$.
The value of $c$ is not known by a programmer in advance (since a program can
have non-deterministic properties), although a programmer could annotate the
code to enforce the termination of a program at a certain time. A more elegant
solution, however, is to measure the time it takes for a program $\alpha$ to
run, and use the measured value for the time offset for any subsequent
temporal operators that may need interval shifting.

###### Definition 3.6 (Timing of hybrid programs).

Given hybrid programs $\alpha$ and $\beta$, and a variable $q$ _fresh_ in
$\alpha$ and $\beta$, the timing of hybrid programs is defined inductively as
follows:

  * –

$time(x:=\theta)\triangleq x:=\theta$

  * –

$time(x^{\prime}=\theta\ \&\ \chi)\triangleq\\{x^{\prime}=\theta,q^{\prime}=1\
\&\ \chi\\}$

  * –

$time(?\chi)\triangleq\ ?\chi$

  * –

$time(\alpha\cup\beta)\triangleq time(\alpha)\cup time(\beta)$

  * –

$time(\alpha;\beta)\triangleq time(\alpha);time(\beta)$

  * –

$time(\alpha^{*})\triangleq(time(\alpha))^{*}$

The time taken $q$ by a hybrid program $\alpha$ is then given by the program:

$timed(\alpha,q)\equiv q:=0;\ time(\alpha)$

Recall that a trace $\sigma$ is a function that maps a pair $(i,t)$ to a state
$v\in{\sf Sta}\,$, whereas a state $v$ is a function from the set of variables
${\sf Var}\,$ to $\mathbb{R}$. For
$\sigma_{\alpha}\in\llbracket\alpha\rrbracket$, we write
$\sigma_{\alpha}|_{S}$ to refer to $\sigma$ restricted to variables in the set
$S\subseteq{\sf Var}\,$. Mathematically,
$\sigma_{\alpha}|_{S}:(\mathbb{R}\times\mathbb{N})\rightarrow
S\rightarrow\mathbb{R}$, where $(i,t)\mapsto\sigma_{\alpha}(i,t)|_{S}$. We can
then define an equality between timed and untimed hybrid programs as follows:

###### Lemma 3.7 (Equality of timed and untimed hybrid programs).

Given a hybrid program $\alpha$, the following set equality always holds:

$\displaystyle\\{\sigma_{\alpha}|_{{\sf
Var}\,-\\{q\\}}:\sigma_{\alpha}\in\llbracket\alpha\rrbracket\\}$
$\displaystyle=$ $\displaystyle\\{\sigma_{timed(\alpha,q)}|_{{\sf
Var}\,-\\{q\\}}$ $\displaystyle:\sigma_{timed(\alpha,q)}\in\llbracket
timed(\alpha,q)\rrbracket\\}$

###### Proof.

The proof of Lemma 3.7 is true by Definition 3.6, keeping in mind the fact
that $q$ is fresh in $timed(\alpha,q)$. ∎

Intuitively, Lemma 3.7 expresses that for a trace
$\sigma_{\alpha}\in\llbracket timed(\alpha,q)\rrbracket$, there always exists
a corresponding trace $\sigma_{\alpha}^{\prime}\in\llbracket\alpha\rrbracket$,
and vice versa, such that $\sigma_{\alpha}$ and $\sigma_{\alpha}^{\prime}$ are
identical with respect to every variable except the fresh variable $q$
introduced by $timed(\alpha,q)$. We rely on this lemma for the proof of
soundness of the STd$\mathcal{L}$ calculus.

##  4\. Proof Calculus

In this section, we outline a proof calculus for STd$\mathcal{L}$, and present
a proof of soundness for the rules in the schemata of the proof calculus.

###  4.1. Normalization of Trace Formulas

Sequential composition of two traces is a major challenge in a calculus
handling alternating program and temporal modalities. To see why, let us
consider a state formula $\langle\alpha;\beta\rangle\square_{[a,b]}\phi$
limited to terminating traces only for simplicity. This formula states that
there exists a trace $\sigma_{\alpha}\in\llbracket\alpha\rrbracket$ followed
by the trace $\sigma_{\beta}\in\llbracket\beta\rrbracket$ such that sequential
composition of the traces satisfies $\square_{[a,b]}\phi$. Let us assume
further for simplicity that all traces
$\sigma_{\alpha}\in\llbracket\alpha\rrbracket$ terminate between time $a$ and
$b$. A first attempt at writing a rule for this state formula could take the
form:

$\frac{\langle\alpha\rangle\square_{[a,b]}\phi\land\langle
timed(\alpha,q)\rangle\langle\beta\rangle\square_{[0,b-q]}\phi}{\langle\alpha;\beta\rangle\square_{[a,b]}\phi}$

Unfortunately, this rule is intuitive but not sound, since the choice of
$\sigma_{\alpha}$ and $\sigma_{\beta}$ could be non-deterministic. The premise
says that there exists a trace $\sigma_{\alpha}\in\llbracket\alpha\rrbracket$
in which $\square_{[a,b]}\phi$ is true, and a trace trace
$\sigma_{\alpha}^{\prime}\in\llbracket\alpha\rrbracket$ followed by
$\sigma_{\beta}$ in which $\square_{[0,b-q]}\phi$ is true, but
$\sigma_{\alpha}$ and $\sigma_{\alpha}^{\prime}$ need not necessarily be the
same trace. To capture the fact that $\sigma_{\alpha}$ and
$\sigma_{\alpha}^{\prime}$ are indeed the same traces, we need a premise
resembling:

$\langle
timed(\alpha,q)\rangle(\square_{[a,b]}\phi\land\langle\beta\rangle\square_{[0,b-q]}\phi)$

The rule is not in the syntax of STd$\mathcal{L}$, since it involves a
conjunction between a state formula and a trace formula. We could choose to
add this conjunction to the syntax of the logic, but we would still need to
reason about the meaning of this conjunction if the trace $\sigma_{\alpha}$ is
non-terminating.

To circumvent this problem cleanly, we need a conjunction operator that
reasons about properties like $\phi$ that are true at the end of a trace and
properties like $\square_{[a,b]}\phi$ that are true during a trace. dTL2
introduces a notion of normalized trace formulas to achieve the expressibility
needed for sequential composition for LTL formulas within the context of
hybrid systems by introducing a conjunction operator $\sqcap$ and a
disjunction operator $\sqcup$ (Jeannin and Platzer, 2014a). We extend
STd$\mathcal{L}$ with a similar normalization of trace formulas to reason
about time-bounded trace properties during the execution of a trace and state
properties at the end of a trace. We augment the syntax of state formulas to
accept normalized trace formulas, and define the syntax of a normalized trace
formula $\xi$ as:

$\displaystyle\phi,\psi::=$ $\displaystyle\ \dots\ |\ [\alpha]\xi\ |\
\langle\alpha\rangle\xi$ $\displaystyle\xi::=$ $\displaystyle\
\phi\sqcap\square_{[a,b]}\psi\ |\ \phi\sqcup\lozenge_{[a,b]}\psi$

###### Definition 4.1 (Semantics of normalized trace formulas).

For a normalized trace formula $\xi$ and trace
$\sigma=(\sigma_{0},\dots,\sigma_{n})\in{\sf Tra}\,$, we say
$(\sigma,(i,t))\vDash\xi$ if $\sigma$ satisfies $\xi$ starting from subtrace
$\sigma_{i}$ at time $t$. We say that $\sigma\vDash\xi$ if
$(\sigma,(0,0))\vDash\xi$. Satisfaction of normalized trace formulas with
respect to a trace $\sigma$ is then defined inductively as follows:

  * –

$\sigma\vDash\phi\sqcap\square_{[a,b]}\psi$ if and only if

    * –

${\sf last}\,\sigma\vDash\phi$ and $\sigma\vDash\square_{[a,b]}\psi$, if
$\sigma$ terminates,

    * –

$\sigma\vDash\square_{[a,b]}\psi$ otherwise;

  * –

$\sigma\vDash\phi\sqcup\lozenge_{[a,b]}\psi$ if and only if

    * –

${\sf last}\,\sigma\vDash\phi$ or $\sigma\vDash\lozenge_{[a,b]}\psi$, if
$\sigma$ terminates,

    * –

$\sigma\vDash\lozenge_{[a,b]}\psi$ otherwise.

Given a normalized state formula $\xi$, we use the notation $\xi_{sta}$ to
refer to the state formula in $\xi$, and we use the notation $\xi_{tra}$ to
refer to the trace formula in $\xi$. For example,
$(\phi\sqcap\square_{[a,b]}\psi)_{sta}=\phi$, and
$(\phi\sqcap\square_{[a,b]}\psi)_{tra}=\square_{[a,b]}\psi$.

We define the minimum length of normalized trace formulas required to
determine the satisfaction of program necessities and possibilities as
follows:

###### Definition 4.2 (Minimum length of normalized trace formulas).

The minimum length associated with a normalized trace formula $\xi$, denoted
by $\|\xi\|$, to determine the satisfaction of a program necessity or
possibility is defined as follows:

$\displaystyle\|\phi\sqcap\square_{[a,b]}\psi\|$ $\displaystyle=b$
$\displaystyle\|\phi\sqcup\lozenge_{[a,b]}\psi\|$ $\displaystyle=b$

We build on Definition 3.4 for state formulas as follows:

  * –

$v\vDash[\alpha]\xi$ if and only if for each trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$ and if
$\sigma$ terminates then ${\sf last}\,\sigma\vDash\xi_{sta}$, and if
$|\sigma|\geq val({\sf first}\,\sigma,\|\xi\|)$, we also have that
$\sigma\vDash\xi$;

  * –

$v\vDash\langle\alpha\rangle\xi$ if and only if there exists trace
$\sigma\in\llbracket\alpha\rrbracket$ such that ${\sf first}\,\sigma=v$ and if
$\sigma$ terminates then ${\sf last}\,\sigma\vDash\xi_{sta}$, and
$|\sigma|\geq val({\sf first}\,\sigma,\|\xi\|)$ and $\sigma\vDash\xi$.

Given the semantics of normalized trace formulas in STd$\mathcal{L}$, we
derive rules to transform any trace formula in STd$\mathcal{L}$ into a
normalized trace formula. The rules for normalization are shown in Figure 1.
The relation $\leadsto$ allows us to only consider normalized trace formulas
for the rules of the proof calculus of STd$\mathcal{L}$, thereby simplifying
the proof system greatly.

$\displaystyle\phi\leadsto\phi\ $ $\displaystyle(\leadsto\phi)$
$\displaystyle\square_{[a,b]}\phi\leadsto{\sf
true}\,\sqcap\square_{[a,b]}\phi\ $ $\displaystyle(\leadsto\square_{I})$
$\displaystyle\lozenge_{[a,b]}\phi\leadsto{\sf
false}\,\sqcup\lozenge_{[a,b]}\phi\ $ $\displaystyle(\leadsto\lozenge_{I})$
Figure 1. Normalization of trace formulas in STd$\mathcal{L}$.

###### Lemma 4.3 (Soundness of normalized trace formulas).

If $\pi\leadsto\xi$, then for all traces $\sigma$, it follows that
$\sigma\vDash\pi$ if and only if $\sigma\vDash\xi$.

###### Proof.

Soundness of rule $(\leadsto\phi)$ is trivial. Soundness of rules
$(\leadsto\square_{I})$, $(\leadsto\lozenge_{I})$ is true by the semantics in
Definition 4.1. ∎

###### Lemma 4.4 (Existence of a normalized trace formula).

For any trace formula $\pi$, there exists a state formula $\phi$ such that
$\pi\leadsto\phi$, or a normalized trace formula $\xi$ such that
$\pi\leadsto\xi$.

###### Proof.

This lemma is a consequent of the $\leadsto$ relation presented in Figure 1. ∎

Lemma 4.4 allows the proof system of STd$\mathcal{L}$ to just focus on
axiomatizing only formulas that use normalized traces, and inherit non-
temporal rules from d$\mathcal{L}$ (Platzer, 2010b, 2012, 2008). This results
in a cleaner, simpler proof calculus for STd$\mathcal{L}$.

####  4.1.1. Running Example: Traction Assist in Cars

Recall that our running example introduced a safety property, $\phi$, that
required a skidding car’s traction assist to reduce the wheel rotation $\rho$
of the car to some constant, $\rho_{0}$, within 1 to 5 seconds to help regain
traction. This property can be expressed as a normalized STd$\mathcal{L}$
formula as follows:

$\phi::={\sf[traction\\_assist]}\left(\begin{tabular}[]{c}$\lnot{\sf
no\\_traction}$ $\sqcup$
$\lozenge_{[1,5]}(\rho<\rho_{0})$\end{tabular}\right)$

For ease of understanding, the normalized disjunction $\lnot{\sf
no\\_traction}$ $\sqcup$ $\lozenge_{[1,5]}(\rho<\rho_{0})$ can be thought of
as the implication ${\sf no\\_traction}$ $\Rightarrow$
$\lozenge_{[1,5]}(\rho<\rho_{0})$ (although this implication is not directly
supported in the sytax of STd$\mathcal{L}$). We provide a proof sketch of this
property in Section 4.2.3.

###  4.2. Proof Calculus

This section presents the proof calculus of STd$\mathcal{L}$. As in
d$\mathcal{L}$, the rules in the proof calculus of STd$\mathcal{L}$ typically
follow a symbolic decomposition pattern whereby hybrid programs may be
decomposed syntactically as needed. The proof calculus transforms STL formulas
into temporal-free formulas to leverage the non-temporal rules of
d$\mathcal{L}$. As such, the proof system inherits its non-temporal rules from
d$\mathcal{L}$ (Platzer, 2008, 2012, 2010b), and adds its own temporal rules
to allow for expressing temporal formulas for given time intervals. All rules
should be used in the same way as in the d$\mathcal{L}$ proof calculus.

Note that with the exceptions of rules (ind $\sqcup_{t}$) and (con
$\sqcap_{t}$) (see Figure 2), all rules are actually equivalences between the
premise and the conclusion. In other words, each rule has a dual such that the
negation of both the premise and the conclusion is also true. Therefore, when
we write rule $\displaystyle\frac{\rho}{\phi}$, the following two rules are
both true:

$\frac{\rho}{\phi}\qquad\qquad\frac{\lnot\rho}{\lnot\phi}$

Such duals for the rules contain the proof rules for $\langle\alpha\rangle$
when the original rule contains the proof rules for $[\alpha]$, and vice versa
(again, except for rules (ind $\sqcup_{t}$) and (con $\sqcap_{t}$)).

####  4.2.1. Inheritance of Non-Temporal and Temporal Rules

In addition to the temporal rules introduced in Figure 2, STd$\mathcal{L}$
also uses the proof system of d$\mathcal{L}$. Indeed, the goal of the proof
calculus introduced here is to leverage the non-temporal rules of
d$\mathcal{L}$ to reason about temporal properties of formulas. Since we build
STd$\mathcal{L}$ to conservatively extend d$\mathcal{L}$, it is sound to
inherit the proof calculus of d$\mathcal{L}$.

####  4.2.2. Introduction of New Temporal Rules

This subsection introduces the temporal rules, grouped by program construct
for hybrid programs, for the proof calculus of STd$\mathcal{L}$. A detailed
rule schemata for the proof calculus is included in Figure 2.

Normalization of Trace Formulas

$\frac{\pi\leadsto\xi\ \ [\alpha]\xi}{[\alpha]\pi}\ ([\ ]\leadsto)\ \ \
\frac{\pi\leadsto\xi\ \ \langle\alpha\rangle\xi}{\langle\alpha\rangle\pi}\
(\langle\rangle\leadsto)$

Assignment

$\frac{\left(\begin{tabular}[]{c}$(a=0\land
b=0)\land(\psi\land[x:=\theta](\phi\land\psi))\ \lor$\\\ $((a>0\land b\geq
a)\land[x:=\theta]\phi)$\end{tabular}\right)}{[x:=\theta](\phi\sqcap\square_{[a,b]}\psi)}\
([:=]\ \sqcap_{t})$

$\frac{\left(\begin{tabular}[]{c}$(a=0\land
b=0)\land(\psi\lor[x:=\theta](\phi\lor\psi))\ \lor$\\\ $((a>0\land b\geq
a)\land[x:=\theta]\phi)$\end{tabular}\right)}{[x:=\theta](\phi\sqcup\lozenge_{[a,b]}\psi)}\
([:=]\ \sqcup_{t})$

$\frac{\left(\begin{tabular}[]{c}$(((a=0\land b=0)\land(\psi\lor\langle
x:=\theta\rangle(\phi\lor\psi))\ \lor$\\\ $((a>0\land b\geq a)\land\langle
x:=\theta\rangle\phi$\end{tabular}\right)}{\langle
x:=\theta\rangle(\phi\sqcup\lozenge_{[a,b]}\psi)}\ (\langle:=\rangle\
\sqcup_{t})$

$\frac{\left(\begin{tabular}[]{c}$((a=0\land b=0)\land(\psi\land\langle
x:=\theta\rangle(\phi\land\psi))\ \lor$\\\ $((a>0\land b\geq a)\land\langle
x:=\theta\rangle\phi)$\end{tabular}\right)}{\langle
x:=\theta\rangle(\phi\sqcap\square_{[a,b]}\psi)}\ (\langle:=\rangle\
\sqcap_{t})$

Test

$\frac{\left(\begin{tabular}[]{c}$((a=0\land
b=0)\land((\chi\wedge(\phi\wedge\psi))\vee(\neg\chi\wedge\psi))\ \lor$\\\
$((a>0\land b\geq
a)\land(\lnot\chi\lor(\chi\land\phi)))$\end{tabular}\right)}{[?\chi](\phi\sqcap\square_{[a,b]}\psi)}\
([?]\ \sqcap_{t})$

$\frac{\left(\begin{tabular}[]{c}$((a=0\land
b=0)\land((\chi\wedge(\phi\lor\psi))\vee(\neg\chi\wedge\psi))\ \lor$\\\
$((a>0\land b\geq
a)\land(\lnot\chi\lor(\chi\land\phi)))$\end{tabular}\right)}{[?\chi](\phi\sqcup\lozenge_{[a,b]}\psi)}\
([?]\ \sqcup_{t})$

$\frac{\left(\begin{tabular}[]{c}$((a=0\land
b=0)\land((\chi\wedge(\phi\lor\psi))\vee(\neg\chi\wedge\psi))\ \lor$\\\
$((a>0\land b\geq
a)\land(\lnot\chi\lor(\chi\land\phi)))$\end{tabular}\right)}{\langle?\chi\rangle(\phi\sqcup\lozenge_{[a,b]}\psi)}\
(\langle?\rangle\ \sqcup_{t})$

$\frac{\left(\begin{tabular}[]{c}$((a=0\land
b=0)\land((\chi\wedge(\phi\wedge\psi))\vee(\neg\chi\wedge\psi))\ \lor$\\\
$((a>0\land b\geq
a)\land(\lnot\chi\lor(\chi\land\phi)))$\end{tabular}\right)}{\langle?\chi\rangle(\phi\sqcap\square_{[a,b]}\psi)}\
(\langle?\rangle\ \sqcap_{t})$

Non-deterministic Choice

$\frac{[\alpha]\xi\land[\beta]\xi}{[\alpha\cup\beta]\xi}\ ([\cup]\ \xi)\ \ \ \
\ \ \ \ \ \ \
\frac{\langle\alpha\rangle\xi\lor\langle\beta\rangle\xi}{\langle\alpha\cup\beta\rangle\xi}\
(\langle\cup\rangle\ \xi)$

Sequential Composition

$\frac{[timed(\alpha,q)]([\beta](\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi)\sqcap\square_{[a,\min(b,q)]}\psi)}{[\alpha;\beta](\phi\sqcap\square_{[a,b]}\psi)}\
([;]\sqcap_{t})$

$\frac{[timed(\alpha,q)]([\beta](\phi\sqcup\lozenge_{[\max(0,a-q),b-q]}\psi)\sqcup\lozenge_{[a,\min(b,q)]}\psi)}{[\alpha;\beta](\phi\sqcup\lozenge_{[a,b]}\psi)}\
([;]\sqcup_{t})$

$\frac{\langle
timed(\alpha,q)\rangle(\langle\beta\rangle(\phi\sqcup\lozenge_{[\max(0,a-q),b-q]}\psi)\sqcup\lozenge_{[a,\min(b,q)]}\psi)}{\langle\alpha;\beta\rangle(\phi\sqcup\lozenge_{[a,b]}\psi)}\
(\langle;\rangle\sqcup_{t})$

$\frac{\langle
timed(\alpha,q)\rangle(\langle\beta\rangle(\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi)\sqcap\square_{[a,\min(b,q)]}\psi)}{\langle\alpha;\beta\rangle(\phi\sqcap\square_{[a,b]}\psi)}\
(\langle;\rangle\sqcap_{t})$

Figure 2. Rule schemata of the proof calculus for STd$\mathcal{L}$.

Ordinary Differential Equation

$\frac{\left(\begin{tabular}[]{c}$(b<a\land[x^{\prime}=\theta\ \&\ \chi]\phi)\
\lor$\\\ $(\lnot\chi\land(\lnot(a=0\land b\geq a)\lor\psi))\ \lor$\\\
$([t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]$\\\ $[\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
b)\\}]\psi\land[x^{\prime}=\theta\ \&\
\chi]\phi)$\end{tabular}\right)}{[x^{\prime}=\theta\ \&\
\chi](\phi\sqcap\square_{[a,b]}\psi)}\text{ ($[^{\prime}]\ \sqcap_{t}$)}$

$\frac{\left(\scalebox{0.94}{\begin{tabular}[]{c}$(b<a\land[x^{\prime}=\theta\
\&\ \chi]\phi)\ \lor$\\\ $((\chi\lor[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\
\&\ (\chi\land t\leq a)\\};?(t=a)]\psi)\ \land$\\\ $[x^{\prime}=\theta\ \&\
(\chi\land\lnot\psi)]\phi\ \land$\\\ $[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\
\&\ (\chi\land t\leq a)\\};?(t=a)]$\\\
$\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle(\lnot\chi\lor\psi))$\end{tabular}}\right)}{[x^{\prime}=\theta\
\&\ \chi](\phi\sqcup\lozenge_{[a,b]}\psi)}\text{ ($[^{\prime}]\ \sqcup_{t}$)}$

$\frac{\left(\begin{tabular}[]{c}$(b<a\land[x^{\prime}=\theta\ \&\ \chi]\phi)\
\lor$\\\ $(\lnot\chi\land(\lnot(a=0\land b\geq a)\lor\psi))\ \lor$\\\
$([t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]$\\\ $[\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
b)\\}]\psi\land[x^{\prime}=\theta\ \&\
\chi]\phi)$\end{tabular}\right)}{[x^{\prime}=\theta\ \&\
\chi](\phi\sqcap\square_{[a,b]}\psi)}\text{ ($[^{\prime}]\ \sqcap_{t}$)}$

$\frac{\left(\scalebox{0.93}{
\begin{tabular}[]{c}$(b<a\land[x^{\prime}=\theta\ \&\ \chi]\phi)\ \lor$\\\
$((\chi\lor[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\psi)\ \land$\\\ $[x^{\prime}=\theta\ \&\
(\chi\land\lnot\psi)]\phi\ \land$\\\ $[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\
\&\ (\chi\land t\leq a)\\};?(t=a)]$\\\
$\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle(\lnot\chi\lor\psi))$\end{tabular}}\right)}{[x^{\prime}=\theta\
\&\ \chi](\phi\sqcup\lozenge_{[a,b]}\psi)}\text{ ($[^{\prime}]\ \sqcup_{t}$)}$

Non-deterministic Finite Repetition

$\frac{\left(\begin{tabular}[]{c}$(\phi\land(\lnot(a=0\land b=0)\lor\psi))\
\land$\\\
$[timed(\alpha^{*},q)][\alpha](\phi\sqcap\square_{[max(0,a-q),b-q]}\psi)$\end{tabular}\right)}{[\alpha^{*}](\phi\sqcap\square_{[a,b]}\psi)}\text{
([*] $\sqcap_{t}$)}$

$\frac{(\psi\land(a=0\land b\geq
a))\lor(\phi\wedge[\alpha^{*};\alpha](\phi\sqcup\lozenge_{[a,b]}\psi))}{[\alpha^{*}](\phi\sqcup\lozenge_{[a,b]}\psi)}\text{
([${}^{*n}$] $\sqcup_{t}$)}$

$\frac{\phi\implies[\alpha](\phi\sqcup\lozenge_{[a,b]}\psi)}{\forall^{\alpha}(\phi\implies[\alpha^{*}](\phi\sqcup\lozenge_{[a,b]}\psi))}\text{
(ind $\sqcup_{t}$)}$

$\frac{\forall^{\alpha}\forall r>0\
(\varphi(r)\implies\langle\alpha\rangle(\varphi(r-1)\sqcap\square_{[a,b]}\psi))}{(\exists
r.\varphi(r))\wedge\psi\implies\langle\alpha^{*}\rangle((\exists r.r\leq
0\land\varphi(r))\sqcap\square_{[a,b]}\psi)}\ (\textrm{con }\sqcap_{t})$

$\frac{\left(\begin{tabular}[]{c}$(\psi\land(a=0\land b\geq a))\ \lor$\\\
$\langle
timed(\alpha^{*},q)\rangle\langle\alpha\rangle(\phi\sqcup\lozenge_{[max(0,a-q),b-q]}\psi)$\end{tabular}\right)}{\langle\alpha^{*}\rangle(\phi\sqcup\lozenge_{[a,b]}\psi)}\text{
$(\langle^{*}\rangle\sqcup_{t})$}$

$\frac{\left(\begin{tabular}[]{c}$(\phi\land(\lnot(a=0\land b=0)\lor\psi))\
\land$\\\
$(\phi\lor\langle\alpha^{*};\alpha\rangle(\phi\sqcap\square_{[a,b]}\psi))$\end{tabular}\right)}{\langle\alpha^{*}\rangle(\phi\sqcap\square_{[a,b]}\psi)}\text{
($\langle^{*n}\rangle$ $\sqcap_{t}$)}$

Figure 2 (continued): Rule schemata of the proof calculus for
STd$\mathcal{L}$.

Rules $([\ ]\leadsto)$ and $(\langle\rangle\leadsto)$ lift normalization of
trace formulas to program necessities and possibilities respectively.

For assignment rule ([$:=]\ \sqcap_{t}$), the first disjunct expresses that
for the time interval $[0,0]$, $\psi$ must hold initially, and after the
execution of the program, must continue to hold in addition to $\phi$, as
summarized in clause $\psi\wedge[x:=\theta](\phi\wedge\psi)$. The second
disjunct expresses that for any interval $[a,b]$ where $a>0$ and $b\geq a$,
only $\phi$ needs to be true after execution of the assignment, since
assignment occurs in zero time, and as such, the trace of $x:=\theta$ would
not be long enough to determine the satisfiability of $\square_{[a,b]}\psi$
for $a>0$. Similar reasoning is used for rule $(\textrm{[:=]}\ \sqcup_{t})$.

For the rules for test, as a reminder, a test trace only terminates if the
test passes, and is a trace of the error state if the test fails. Rule ($[?]\
\sqcap_{t}$) encapsulates the fact that a trace of $?\chi$ satisfies
$\phi\sqcap\square_{[a,b]}\psi$ if and only if

  * –

for $a=0$ and $b=0$, its initial state satisfies $\phi\land\psi$ if the test
passes, or satisfies only $\psi$ if the test fails;

  * –

for $a>0$ and $b\geq a$, its initial state satisfies just $\phi$ if the test
passes.

Note that there is no satisfaction requirement on the trace of a failing test
(i.e., $\lnot\chi$ is true) when $a>0$ and $b\geq a$, since the test also
occurs in zero time, and as such, the trace of $?\chi$ would not be long
enough to determine the satisfiability of $\square_{[a,b]}\psi$ in this case.
Similar reasoning is used for rule ($[?]\ \sqcup_{t}$).

Rules for ordinary differential equations (ODEs) look complex at first glance,
but can be broken down in slightly simpler sub-rules. It is first important to
remember that ODEs could have terminating traces or error traces, and the
rules for ODEs need to account of both possibilities. With that in mind, we
conclude that an error trace of $x^{\prime}=\theta\ \&\ \chi$ satisfies
$\phi\sqcap\square_{[a,b]}\psi$ if and only if $a=0$ and $b\geq a$ implies
$\psi$, as the second disjunct in rule ($[^{\prime}]\ \sqcap_{t}$). For non-
error traces of $x^{\prime}=\theta\ \&\ \chi$, we first transform the program
into a program of the form $t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\
(\chi\land t\leq a)\\};?(t=a)$ and $\\{x^{\prime}=\theta,t^{\prime}=1\ \&\
(\chi\land t\leq b)\\}$ to enforce that the differential equation first runs
from time $t=0$ to time $t=a$ without any satisfaction requirements on $\psi$,
followed by running the equation from time $t=a$ to $t=b$, during which $\psi$
must be true. In addition to this, $\phi$ must be true after running the
program $x^{\prime}=\theta\ \&\ \chi$, to deal with the case where the
execution exits the differential equation before time $a$. This is summarized
in the third disjunct of the rule ($[^{\prime}]\ \sqcap_{t}$). Note that the
first disjunct of the rule deals with the case where $b<a$, so
$\square_{[a,b]}\psi$ is defined to be trivially true, and any trace of
$x^{\prime}=\theta\ \&\ \chi$ need only satisfy $\phi$. Rule ($[^{\prime}]\
\sqcup_{t}$) expresses that a trace of $x^{\prime}=\theta\ \&\ \chi$ satisfies
$\phi\sqcup\lozenge_{[a,b]}\psi$ if and only if either $b<a$ and the trace
satisfies $\phi$ upon termination, or

  * –

the differential equation can evolve or has satisfied $\psi$ at time $t=a$ (as
in the first conjunct of the rule),

  * –

if no trace of the differential equation can satisfy $\psi$, all traces must
satisfy $\phi$ instead (as in the second conjunct of the rule),

  * –

either there does not exist a non-terminating trace of the differential
equation – transformed to a program as in rule ($[^{\prime}]\ \sqcap_{t}$) –
or such a trace satisfies $\psi$ between times $a$ and $b$.

Rule $([\cup]\ \xi)$ for non-deterministic choice is lifted directly from the
corresponding rule $[\cup]\square$ in d$\mathcal{L}$.

…
$[timed(\alpha_{1},q_{1})]([timed(\alpha_{2},q_{2})](\psi_{3}\sqcup\lozenge_{[\max(0,1-q_{1}),\min(5-q_{1},q_{2})]})\sqcup\lozenge_{[1,\min(5,q_{1})]}\psi_{2})$
$[^{\prime}]\sqcup_{t}$
$[timed(\alpha_{1},q_{1})]([timed(\alpha_{2},q_{2})]([\alpha_{3}](\psi_{1}\sqcup\lozenge_{[\max(0,\max(0,1-q_{1})-q_{2}),5-q_{1}-q_{2}]}\psi_{2})\sqcup\lozenge_{[\max(0,1-q_{1}),\min(5-q_{1},q_{2})]})\sqcup\lozenge_{[1,\min(5,q_{1})]}\psi_{2})$
$[;]\sqcup_{t}$
$[timed(\alpha_{1},q_{1})]([\alpha_{2};\alpha_{3}](\psi_{1}\sqcup\lozenge_{[\max(0,1-q_{1}),5-q_{1}]}\psi_{2})\sqcup\lozenge_{[1,\min(5,q_{1})]}\psi_{2})$
$[;]\sqcup_{t}$ $[\alpha](\psi_{1}\sqcup\lozenge_{[1,5]}\psi_{2})$

Figure 3. Proof sketch of our running example. The state formula $\psi_{3}$
can be further proven using rules from d$\mathcal{L}$.

The rules for sequential composition were one of the most challenging aspects
of STd$\mathcal{L}$. Indeed, sequential composition is the sole reason why we
use normalized trace formulas in STd$\mathcal{L}$ (see Section 4.1), and a
primary reason why introduce the notion of recording the amount of time it
takes for a hybrid program $\alpha$ to execute (see Section 3.5). As a
reminder here, for a hybrid program $\alpha$, executing $timed(\alpha,q)$ is
equivalent to executing $\alpha$ while recording the amount of time the
program takes to execute, following which the timed value is output as a fresh
variable $q$. With that in mind, a trace of $\alpha;\beta$ satisfies
$\phi\sqcap\square_{[a,b]}\psi$ if and only if

  * –

for $a\leq q\leq b$, all traces of $\alpha$ satisfy $\square_{[a,q]}\psi$, and
for traces of $\alpha$ that terminate at time $q$, all following traces of
$\beta$ satisfy $\phi\sqcap\square_{[0,b-q]}\psi$,

  * –

for $a\leq b\leq q$, all traces of $\alpha$ satisfy $\square_{[a,b]}\psi$, and
for traces of $\alpha$ that terminate at time $q$, all following traces of
$\beta$ satisfy $\phi$,

  * –

for $q\leq a\leq b$, for traces of $\alpha$ that terminate at time $q$, all
following traces of $\beta$ satisfy $\phi\sqcap\square_{[a-q,b-q]}\psi$.

These properties for the cases of the relative ordering of $a,b$ and $q$ are
captured succinctly in rule ([;] $\sqcap_{t}$) using min and max. Rule ([;]
$\sqcup_{t}$) is similar.

For the rules for non-deterministic finite repetition, let us first remember
that as long as a trace $\alpha$ is finite, its finite repetition $\alpha^{*}$
will also be finite. In general, the rules attempt to reduce temporal
properties of loops into either non-temporal properties of loops, or slightly
more complex temporal properties on a program but without any loops. The idea
here is to make the rules provable by ordinary, non-temporal induction. The
key intuition behind rule ([*] $\sqcup_{t}$) comes from a very useful rule for
repetition from d$\mathcal{L}$, which says that for a given trace formula
$\pi$, the following is true:

$\frac{[?true]\pi\land[\alpha^{*};\alpha]\pi}{[\alpha^{*}]\pi}\text{ [;]}$

Rule ([*] $\sqcap_{t}$) captures the fact that a trace of $\alpha^{*}$
satisfies $\phi\sqcap\square_{[a,b]}\psi$ if and only if when $\alpha$ repeats
zero times, $\phi$ is true, and if $a=0$ and $b=0$ then $\psi$ is true as
well, or $\alpha^{*}$ runs first followed by $\alpha$, during which
$\phi\sqcap\square_{[a,b]}\psi$ with time interval shifting (similar to that
for the sequential composition rules) holds. In rule ([*] $\sqcup_{t}$), the
first disjunct expresses that $\lozenge_{[a,b]}\psi$ holds without repeating
$\alpha$ if $a=0$ and $b\geq a$ and $\psi$ is true initially; the first
conjunct of the second disjunct deals with the case where $\alpha$ repeats
zero times and $\psi$ is false initially, while the second conjunct requires a
sequential composition of $\alpha^{*};\alpha$ to satisfy
$\phi\sqcup\lozenge_{[a,b]}\psi$ according to the rule ([;]) from
d$\mathcal{L}$ mentioned above. Note that for rule ([*] $\sqcup_{t}$), the use
of $\alpha^{*};\alpha$ is equivalent to the use of $\alpha;\alpha^{*}$, and
either variant of the sequential composition may be used. The rules (ind
$\sqcup_{t}$) and (con $\sqcap_{t}$) extend the rules of induction (ind) and
convergence (con) from d$\mathcal{L}$ to normalized trace formulas. Consistent
with the rules from d$\mathcal{L}$, the rules (ind $\sqcup_{t}$) and (con
$\sqcap_{t}$) are not equivalence relations (i.e., they do not have dual
counterparts such that the negation of the premise and the conclusion is also
a rule). The notation $\forall^{\alpha}$ from d$\mathcal{L}$ is a
quantification over all variables that could be assigned by a hybrid program
$\alpha$ in assignments or differential equations. Rule (ind $\sqcup$)
expresses that $\phi$ is inductive with exit clause $\lozenge_{[a,b]}\psi$
(i.e., $\phi$ is true after all traces $\sigma\in\llbracket\alpha\rrbracket$
where ${\sf first}\,\sigma\vDash\phi$, except when $\psi$ was true at some
point in the interval $I$ during the execution of $\sigma$), while rule (con
$\sqcap$) shows that $\varphi$ is a variant of some trace
$\sigma\in\llbracket\alpha\rrbracket$ (as in, its level $r$ decreases) during
which $\psi$ is always true, and starting from an initial $r$, for an $r$ for
which $\varphi(r)$ holds, it will ultimately be the case that $r\leq 0$
without $\psi$ being false if we repeat $\alpha^{*}$ often enough (Jeannin and
Platzer, 2014b).

####  4.2.3. Running Example: Traction Assist in Cars

In this subsection, we present a proof sketch of the safety property for our
example, highlighting how the property expressed in STd$\mathcal{L}$ is
reduced to an equivalent d$\mathcal{L}$ formula to leverage the d$\mathcal{L}$
calculus. For ease of understanding of the proof sketch, we only consider the
second half of the hybrid program traction_assist (referred to as $\alpha$) –
though the application of the STd$\mathcal{L}$ proof rules to the first half
of the program is also fairly straightforward. We refer to the sequential
composition components $\omega:=-1$, $\varphi:=10$ and $\rho^{\prime}={\sf
cruise(\omega)})$ in $\alpha$ as $\alpha_{1}$, $\alpha_{2}$, and $\alpha_{3}$
respectively. We then refer to the safety property $\phi$ as
$[\alpha](\psi_{1}\sqcup\lozenge_{[1,5]}\psi_{2})$, where
$\psi_{1}\equiv\lnot{\sf no\\_traction}$ and $\psi_{2}\equiv(\rho<\rho_{0})$.

For $\alpha\equiv(\alpha_{1};(\alpha_{2};\alpha_{3}))$, using the
STd$\mathcal{L}$ proof calculus, we get a proof tree of the form presented in
Figure 3, where $\psi_{3}$ is obtained by applying rule $[^{\prime}]\
\sqcup_{t}$ with $a=\max(0,\max(0,1-q_{1})-q_{2})$ and $b=5-q_{1}-q_{2}$ as
follows:

$\psi_{3}\equiv[\alpha_{3}]\left(\scalebox{0.93}{\begin{tabular}[]{c}$(b<a\land[\rho^{\prime}=\omega\times
k-\varphi\times j]\psi_{1})\ \lor$\\\
$(([t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\psi_{2})\ \land$\\\ $[\rho^{\prime}=\omega\times k-\varphi\times
j\ \&\ (\lnot\psi_{2})]\psi_{1}\ \land$\\\
$[t:=0;\\{\rho^{\prime}=\omega\times k-\varphi\times j,t^{\prime}=1\ \&\
(t\leq a)\\};?(t=a)]$\\\ $\langle\\{\rho^{\prime}=\omega\times k-\varphi\times
j,t^{\prime}=1\ \&\ (t\leq b)\\}\rangle\psi_{2})$\end{tabular}}\right)$

The STd$\mathcal{L}$ state formula $\psi_{3}$ can be proven further using
solely the non-temporal rules from d$\mathcal{L}$.

###  4.3. Soundness and Completeness of the STd$\mathcal{L}$ Proof Calculus

###### Theorem 4.5.

The proof calculus for STd$\mathcal{L}$ is sound.

Since STd$\mathcal{L}$ conservatively extends d$\mathcal{L}$, the soundness of
the proof calculus of d$\mathcal{L}$ applies to STd$\mathcal{L}$ as well. We
present the proof of soundness for the rules introduced by the
STd$\mathcal{L}$ calculus.

###### Proof.

We prove the soundness of individual rules. By induction on the proof trees,
soundness of the entire proof system is a corollary.

$([:=]\ \sqcap_{t})$: For any state $v$, there is a unique terminating trace
$\sigma\in\llbracket x:=\theta\rrbracket$ such that ${\sf first}\,\sigma=v$.
From the trace semantics of hybrid programs, we know that
$\sigma=(\hat{v},\hat{w})$ with $w=[x\mapsto val(v,\theta)]$. Therefore,
$v\vDash[x:=\theta](\phi\sqcap\square_{I}\psi)$ if and only if

  * –

for $I_{s}=0$ and $I_{e}=0$, $w\vDash\phi$, $v\vDash\psi$, and $w\vDash\psi$,
which is true if and only if $v\vDash\psi\land[x:=\theta](\phi\land\psi)$;

  * –

for $I_{s}>0$ and $I_{e}\geq I_{s}$, $w\vDash\phi$, which is true if and only
if $v\vDash[x:=\theta]\phi$.

In either case, it follows that
$v\vDash[x:=\theta](\phi\sqcap\square_{I}\psi)$ if and only if
$v\vDash((I_{s}=0\land
I_{e}=0)\land(\psi\land[x:=\theta](\phi\land\psi))\lor((I_{s}>0\land I_{e}\geq
I_{s})\land[x:=\theta]\phi)$.

$([:=]\ \sqcup_{t})$: Similar to the proof of soundness of $([:=]\
\sqcap_{t})$.

([?] $\sqcap_{t}$): ($\rightarrow$) Let $v\vDash((a=0\land
b=0)\land((\chi\wedge(\phi\lor\psi))\vee(\neg\chi\wedge\psi))\lor((a>0\land
b\geq a)\land(\lnot\chi\lor(\chi\land\phi)))$, and let
$\sigma\in\llbracket?\chi\rrbracket$ with ${\sf first}\,\sigma=v$. If
$v\vDash\lnot\chi$, then $\sigma=(\hat{v},\hat{\Lambda})$ (i.e., $\sigma$ is
the error trace). If $a=0$ and $b=0$, by our assumption, it follows that
$v\vDash\psi$ (otherwise $v$ does not satisfy anything). Since $\sigma$ is a
trace that occurs in zero time, it follows that
$\sigma\vDash(\phi\sqcap\square_{[a,b]}\psi)$. If, however, $v\vDash\chi$,
then $\sigma=(\hat{v})$, and by our assumption, if $a>0$ and $b\geq a$, then
$v\vDash\phi$ only (since the length of $\sigma$ is not long enough to
determine the satisfiability of $\square_{[a,b]}\psi$). Therefore,
$\sigma\vDash(\phi\sqcap\square_{[a,b]}\psi)$ in this case as well.
($\leftarrow$) Conversely, assume that
$v\vDash[?\chi](\phi\sqcap\square_{[a,b]}\psi)$. Now, if $v\vDash\lnot\chi$,
then $\sigma=(\hat{v},\hat{\Lambda})$ (which is a non-terminating state), and
$v\vDash\psi$ only when $a=0$ and $b=0$. Otherwise, $v\vDash\chi$ and
$\sigma=(\hat{v})$, and therefore $v\vDash(\phi\land\psi)$ when $a=0$ and
$b=0$, or $v\vDash\phi$ when $a>0$ and $b\geq a$. In either case,
$v\vDash((a=0\land
b=0)\land((\chi\wedge(\phi\lor\psi))\vee(\neg\chi\wedge\psi))\lor((a>0\land
b\geq a)\land(\lnot\chi\lor(\chi\land\phi)))$.

([?] $\sqcup_{t}$): Similar to the proof of soundness of [?] $\sqcap_{t}$.

([’] $\sqcap_{t}$): ($\rightarrow$) Let $v\vDash(b<a\land[x^{\prime}=\theta\
\&\ \chi]\phi)\lor(\lnot\chi\land(\lnot(a=0\land b\geq
a)\lor\psi))\lor([t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)][\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
b)\\}]\psi\land[x^{\prime}=\theta\ \&\ \chi]\phi)$, and let
$\sigma\in\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket$ such that ${\sf
first}\,\sigma=v$. If $b<a$, it is only required that $\sigma\vDash\phi$
(since $\square_{[a,b]}\psi$ is trivially true in this case). If
$v\vDash\lnot\chi$, then $\sigma$ is the non-terminating error trace
$(\hat{v},\hat{\Lambda})$ and $\sigma\vDash\square_{[a,b]}\psi$ (since $\psi$
is true when $a=0$ and $b\leq a$). Therefore,
$\sigma\vDash(\phi\sqcap\square_{[a,b]}\psi)$. If $v\vDash\chi$, however, then
$\sigma=\\{f\\}$ for a real function $f$ defined on $D=[0,r]$ solution of
$x^{\prime}=\theta$, which satisfies $\chi$ on its domain of definition. Since
$v\vDash[x^{\prime}=\theta\ \&\ \chi]\phi$, for any $\sigma$ that terminates,
$\sigma\vDash\phi$. For a $\sigma$ that does not terminate,
$v\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)][\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
b)\\}]\psi$, and therefore $\sigma\vDash\square_{[a,b]}\psi$. In either case,
$\sigma\vDash(\phi\sqcap\square_{[a,b]}\psi)$.
($\leftarrow$) Conversely, assume $v\vDash[x^{\prime}=\theta\ \&\
\chi](\phi\sqcap\square_{[a,b]}\psi)$. By definition, there exists at least
one trace $\sigma\in\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket$ such
that ${\sf first}\,\sigma=v$ and $\sigma\vDash\square_{[a,b]}\psi$. Now, if
$v\vDash\lnot\chi$, then $v\vDash\psi$ if $a=0$ and $b\geq a$. Otherwise, for
non-error traces of $x^{\prime}=\theta\ \&\ \chi$,

  * –

for a terminating trace $\sigma\in\llbracket x^{\prime}=\theta\ \&\
\chi\rrbracket$, we have that $\sigma\vDash\phi\sqcap\square_{[a,b]}\psi$, and
in particular, we have that $\sigma\vDash\phi$

  * –

for any trace $\sigma\in\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket$
(terminating or otherwise), since $\sigma\vDash\phi\sqcap\square_{[a,b]}\psi$,
in particular we have that $\sigma\vDash\square_{[a,b]}\psi$, and hence,
$\sigma\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)][\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
b)\\}]\psi$.

Therefore, $v\vDash(b<a\land[x^{\prime}=\theta\ \&\
\chi]\phi)\lor(\lnot\chi\land(\lnot(a=0\land b\geq
a)\lor\psi))\lor([t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)][\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
b)\\}]\psi\land[x^{\prime}=\theta\ \&\ \chi]\phi)$.

([’] $\sqcup_{t}$): ($\rightarrow$) Assume
$v\vDash(b<a\land[x^{\prime}=\theta\ \&\
\chi]\phi)\lor((\chi\lor[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\
(\chi\land t\leq a)\\};?(t=a)]\psi)\land[x^{\prime}=\theta\ \&\
(\chi\land\lnot\psi)]\phi\land[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\
(\chi\land t\leq a)\\};?(t=a)]\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\
(t\leq b)\\}\rangle(\lnot\chi\lor\psi))$ and let $\sigma\in\llbracket
x^{\prime}=\theta\ \&\ \chi\rrbracket$ such that ${\sf first}\,\sigma=v$. If
$b<a$, then $v\vDash[x^{\prime}=\theta\ \&\ \chi]\phi$. If $v\vDash\lnot\chi$,
then $\sigma$ is the non-terminating trace $(\hat{v},\hat{\Lambda})$ such that
$\sigma\vDash\lozenge_{[a,b]}\psi$. Therefore,
$\sigma\vDash\phi\sqcup\lozenge_{[a,b]}\psi$. If $v\vDash\chi$, however, then
$\sigma=\\{f\\}$ for a real function $f$ defined on $D=[0,r]$ solution of
$x^{\prime}=\theta$, which satisfies $\chi$ on its domain of definition. If
$\sigma\vDash\lozenge_{[a,b]}\psi$, then by definition,
$\sigma\vDash\phi\sqcup\lozenge_{[a,b]}\psi$. Otherwise, if $\sigma$ is
terminating and no state of $\sigma$ satisfies $\psi$, we have that
$\sigma\in\llbracket x^{\prime}=\theta\ \&\ (\chi\land\lnot\psi\rrbracket$.
From our assumption, we have that $\sigma\vDash\phi$, and as such,
$\sigma\vDash\phi\sqcup\lozenge_{[a,b]}\psi$. Lastly, for the case case where
$\sigma\nvDash\lozenge_{[a,b]}\psi$, we cannot have a non-terminating
$\sigma$. This is because such a $\sigma$ would verify $\chi\land\lnot\psi$ in
all states, and could follow any trace $\sigma_{\alpha}\in\llbracket
x^{\prime}=\theta\rrbracket$, contradicting
$v\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle(\lnot\chi\lor\psi)$ in the process.
($\leftarrow$) Conversely, let $v\vDash[x^{\prime}=\theta\ \&\
\chi](\phi\sqcup\lozenge_{[a,b]}\psi)$, and let $\sigma\in\llbracket
x^{\prime}=\theta\ \&\ \chi\rrbracket$ such that ${\sf first}\,\sigma=v$.
First, if $b<a$, the $\lozenge_{[a,b]}\psi$ is vacuously false, and since
$\sigma\vDash(\phi\sqcup\lozenge_{[a,b]}\psi)$, it must be the case that
$\sigma\vDash\phi$. Otherwise, if $v\vDash\lnot\chi$, the only trace of
$\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket$ such that ${\sf
first}\,\sigma=v$ is the trace $(\hat{v},\hat{\Lambda})$. Since this trace
satisfies $\lozenge_{[a,b]}\psi$, we have that
$v\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\psi$. Therefore, in all cases, we have
$v\vDash\chi\lor[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\psi$. To prove that $v\vDash[x^{\prime}=\theta\ \&\
(\chi\land\lnot\psi)]\phi$, we need only consider terminating tracing. Let
$\sigma$ be a terminating trace of $\llbracket x^{\prime}=\theta\ \&\
(\chi\land\lnot\psi)\rrbracket$. Then, in particular, $\sigma\in\llbracket
x^{\prime}=\theta\ \&\ \chi\rrbracket$, and as such,
$\sigma\vDash\phi\sqcup\lozenge_{[a,b]}\psi$. Since $\sigma$ also has
$\lnot\psi$ as domain constraint, it follows that
$\sigma\nvDash\lozenge_{[a,b]}\psi$, and as such, $\sigma\vDash\phi$. Finally,
to prove the third conjunct of the rule, let us first consider the case where
$v\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle\lnot\chi$. In this case, there is no non-terminating trace
$\sigma\in\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket$ such that ${\sf
first}\,\sigma=v$. For the case where
$v\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle\psi$, there exists a unique non-terminating trace
$\sigma\in\llbracket x^{\prime}=\theta\ \&\ \chi\rrbracket$ such that ${\sf
first}\,\sigma=v$. By our assumption, we have that
$\sigma\vDash\lozenge_{[a,b]}\psi$. This means that $\psi$ has to be true in
some state that is reached by trace $\sigma$, and this notion is logically
equivalent to $[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle\psi$. From both of the cases mentioned above, we get
$v\vDash[t:=0;\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (\chi\land t\leq
a)\\};?(t=a)]\langle\\{x^{\prime}=\theta,t^{\prime}=1\ \&\ (t\leq
b)\\}\rangle(\lnot\chi\lor\psi)$.

$([\ ]\leadsto)$, $(\langle\rangle\leadsto)$: Soundness of rules $([\
]\leadsto)$ and $(\langle\rangle\leadsto)$ is a corollary of Lemma 4.3.

$([\cup]\ \xi)$: For any state $v$, we have
$v\vDash[\alpha]\xi\land[\beta]\xi$ if and only if for all traces
$\sigma_{\alpha}\in\llbracket\alpha\rrbracket$ such that ${\sf
first}\,\sigma_{\alpha}=v$, it follows that $\sigma_{\alpha}\vDash\xi$, and
for all traces $\sigma_{\beta}\in\llbracket\beta\rrbracket$ such that ${\sf
first}\,\sigma_{\beta}=v$, it follows that $\sigma_{\beta}\vDash\xi$. This is
true if and only if for all traces
$\sigma\in\llbracket\alpha\cup\beta\rrbracket$ such that ${\sf
first}\,\sigma=v$, it follows that $\sigma\vDash\xi$, which in turn is true if
and only if $v\vDash[\alpha\cup\beta]\xi$.

Before we can prove soundness for the rules for sequential composition, we
need the following lemma describing the relationship between $q$ and
$|\sigma|$ for $\sigma\in\llbracket timed(\alpha,q)\rrbracket$:

###### Lemma 4.6 (Timing and the lengths of traces of hybrid programs).

Given a hybrid program $\alpha$ and a trace $\sigma\in\llbracket
timed(\alpha,q)\rrbracket$ that the execution of $timed(\alpha,q)$ follows,
the time taken to execute the program is equal to the length of $\sigma$
(i.e., $q=|\sigma|$).

###### Proof.

Lemma 4.6 is a direct consequent of Definition 3.1 and Definition 3.6, keeping
in mind the semantics of hybrid programs from Definition 3.2. ∎

We can now continue with the proof of soundness of the STd$\mathcal{L}$
calculus.

([;] $\sqcap_{t}$): ($\rightarrow$) Assume that for some state $v$, it is true
that
$v\vDash[timed(\alpha,q)]([\beta](\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi)\sqcap\square_{[a,\min(b,q)]}\psi)$,
and let $\sigma|_{{\sf Var}\,-\\{q\\}}\in\llbracket\alpha;\beta\rrbracket$
such that $v={\sf first}\,\sigma$. If $\sigma|_{{\sf
Var}\,-\\{q\\}}\in\llbracket\alpha\rrbracket$ is an infinite trace, then by
Lemma 3.7, $\sigma|_{{\sf Var}\,-\\{q\\}}\in\llbracket
timed(\alpha,q)\rrbracket$ and by the assumption, $\sigma|_{{\sf
Var}\,-\\{q\\}}\vDash\square_{[a,\min(b,+\infty)]}\psi\equiv\square_{[a,b]}\psi$.
Otherwise, there exists a terminating trace
$\sigma_{\alpha}\in\llbracket\alpha\rrbracket$ such that $|\sigma_{\alpha}|=q$
(by Lemma 4.6) and a trace (infinite or otherwise)
$\sigma_{\beta}\in\llbracket\beta\rrbracket$ such that
$\sigma=\sigma_{\alpha}\circ\sigma_{\beta}$. By the assumption,
$\sigma_{\alpha}|_{{\sf Var}\,-\\{q\\}}\vDash\square_{[a,\min(b,q)]}\psi$ and
$\sigma_{\beta}\vDash(\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi$. Now,
depending on the value of $q$, there are three possible orders of $a$, $b$,
and $q$: $a\leq q\leq b$, $q\leq a\leq b$, and $a\leq b\leq q$. Keeping in
mind the fact that for $b<a$, $\square_{[a,b]}\psi$ is vacuously true while
$\lozenge_{[a,b]}\psi$ is vacuously false, we can see that

  * –

for $a\leq q\leq b$, $\sigma_{\alpha}\vDash\square_{[a,q]}\psi$ and
$\sigma_{\beta}\vDash(\phi\sqcap\square_{[0,b-q]}\psi)$;

  * –

for $q\leq a\leq b$,
$\sigma_{\beta}\vDash(\phi\sqcap\square_{[a-q,b-q]}\psi)$;

  * –

for $a\leq b\leq q$, $\sigma_{\alpha}\vDash\square_{[a,b]}\psi$ and
$\sigma_{\beta}\vDash\phi$.

In all cases, $\sigma_{\alpha}|_{{\sf
Var}\,-\\{q\\}}\circ\sigma_{\beta}\vDash(\phi\sqcap\square_{[a,b]}\psi)$. By
Lemma 3.7, we get $\sigma_{\alpha}|_{{\sf
Var}\,-\\{q\\}}\circ\sigma_{\beta}\equiv\sigma$. Therefore,
$\sigma\vDash(\phi\sqcap\square_{[a,b]}\psi)$.
($\leftarrow$) Conversely, let
$v\vDash[\alpha;\beta](\phi\sqcap\square_{[a,b]}\psi)$. Let
$\sigma_{\alpha}\in\llbracket\alpha\rrbracket$ such that $v={\sf
first}\,\sigma_{\alpha}$. If $\sigma_{\alpha}$ is infinite, then
$\sigma_{\alpha}\in\llbracket\alpha;\beta\rrbracket$, and as such,
$\sigma_{\alpha}\vDash\square_{[a,b]}\psi$. Otherwise, let
$\sigma_{\beta}\in\llbracket\beta\rrbracket$ such that
$\sigma_{\alpha}\circ\sigma_{\beta}$ is well-defined. Again, since
$|\alpha|=q$ (by Lemma 4.6), there are three possible orders of $a$, $b$, and
$q$. It is easy to see that for any relative ordering of $a$, $b$, and $q$,
$\sigma_{\alpha}\vDash\square_{[a,\min(b,q)]}\psi$, and
$\sigma_{\beta}\vDash(\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi)$. There is a
universal quantifier on $\sigma_{\beta}$, so
$\sigma_{\alpha}\vDash[\beta](\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi)$.
Keeping in mind that the choice of $\sigma_{\alpha}$ was arbitrary, and by
using Lemma 3.7, it follows that
$v\vDash[timed(\alpha,q)]([\beta](\phi\sqcap\square_{[\max(0,a-q),b-q]}\psi)\sqcap\square_{[a,\min(b,q)]}\psi)$.

([;] $\sqcup_{t}$): Similar to the proof of soundness of [;] $\sqcap_{t}$.

([*] $\sqcap_{t}$): ($\rightarrow$) Assume $v\vDash(\phi\land(\lnot(a=0\land
b=0)\lor\psi))\wedge[timed(\alpha^{*},q)][\alpha](\phi\sqcap\square_{[max(0,a-q),b-q]}\psi)$
and let $\sigma\in\llbracket\alpha^{*}\rrbracket$. If
$\sigma\in\llbracket\alpha^{0}\rrbracket=\llbracket?{\sf true}\,\rrbracket$,
then $\sigma=(\hat{v})$. Since we have $v\vDash\phi$ and
$v\vDash[timed(\alpha^{0},q)][\alpha]\phi\sqcap\square_{[a,b]}\psi$ (note that
for $timed(\alpha^{0},q)$, we have $q=0$, and such a trace satisfies $\psi$
only if $a=0$ and $b=0$), it follows that
$\sigma\vDash(\phi\sqcap\square_{[a,b]}\psi)$. Otherwise, there exits $n\geq
1$ such that $\sigma=\sigma_{1}\circ\dots\circ\sigma_{n}$, where
$\sigma_{i}\in\llbracket\alpha\rrbracket$ for any $i\in\\{1,\dots,n\\}$. Then,
$\sigma_{1}\circ\dots\circ\sigma_{n-1}\in\llbracket\alpha^{*}\rrbracket$ and
$\sigma_{n}\in\llbracket\alpha\rrbracket$. By our assumption,
$\sigma_{n}\vDash\square_{[max(0,a-q),b-q]}\psi$, and as such,
$\sigma\vDash\square_{[a,b]}\psi$. Furthermore, if $\sigma$ terminates, then
$\sigma_{n}$ terminates, and as such, we get $\sigma_{n}\vDash\phi$ from our
assumption. Therefore, we have $\sigma\vDash\phi\sqcap\square_{[a,b]}\psi$.
($\leftarrow$) Conversely, if
$v\vDash[\alpha^{*}](\phi\sqcap\square_{[a,b]}\psi)$, then in particular, we
have $(\hat{v})\vDash(\phi\sqcap\square_{[a,b]}\psi)$. This implies that
$v\vDash\phi$. Now, let $\sigma_{\alpha}\in\llbracket\alpha^{*}\rrbracket$
such that ${\sf first}\,\sigma_{\alpha}=v$ and $\sigma_{\alpha}$ terminates,
and let $\sigma_{\beta}\in\llbracket\alpha\rrbracket$ such that ${\sf
first}\,\sigma_{\beta}={\sf last}\,\sigma_{\alpha}$. Then,
$\sigma_{\alpha}\circ\sigma_{\beta}\in\llbracket\alpha^{*}\rrbracket$.
Therefore, by our assumption, we get
$\sigma_{\alpha}\circ\sigma_{\beta}\vDash\phi\sqcap\square_{[a,b]}\psi$. In
particular, for a value of $q$ returned from $timed(\alpha^{*},q)$ for
$\sigma_{\alpha}$, we get
$\sigma_{\beta}\vDash\phi\sqcap\square_{[max(0,a-q),b-q]}\psi$. Therefore, it
follows that $v\vDash(\phi\land(\lnot(a=0\land
b=0)\lor\psi))\wedge[timed(\alpha^{*},q)][\alpha](\phi\sqcap\square_{[max(0,a-q),b-q]}\psi)$.

([∗n] $\sqcup_{t}$): From the semantics of hybrid programs, we know that
$\llbracket\alpha^{*}\rrbracket=\llbracket?{\sf
true}\,\cup\alpha^{*};\alpha\rrbracket$. Therefore,
$v\vDash\llbracket\alpha^{*}\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$ if and
only if $v\vDash\llbracket?{\sf
true}\,\cup\alpha^{*};\alpha\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$. By
rule $([\cup]\ \xi)$, this is true if and only if $v\vDash\llbracket?{\sf
true}\,\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$ and
$v\vDash\llbracket\alpha^{*};\alpha\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$.
By rule $([?]\ \sqcup_{t})$, $v\vDash\llbracket?{\sf
true}\,\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$ is itself equivalent to
$v\vDash((a=0\land b=0)\land(\phi\lor\psi))\lor((a>0\land b\geq a)\land\phi)$.
Therefore,
$v\vDash\llbracket\alpha^{*}\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$ if and
only if $v\vDash((a=0\land b=0)\land(\phi\lor\psi))\lor((a>0\land b\geq
a)\land\phi)\land\llbracket\alpha^{*};\alpha\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$.
However, $v\vDash((a=0\land b\geq a)\land\psi)$ implies
$v\vDash\llbracket\alpha^{*};\alpha\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$.
As such, we get
$v\vDash\llbracket\alpha^{*}\rrbracket(\phi\sqcup\lozenge_{[a,b]}\psi)$ if and
only if $v\vDash(\psi\land(a=0\land b\geq
a))\lor(\phi\wedge[\alpha^{*};\alpha](\phi\sqcup\lozenge_{[a,b]}\psi)$.

(ind $\sqcup_{t}$): Assume
$v\vDash(\phi\implies[\alpha](\phi\sqcup\lozenge_{[a,b]}\psi))$ and
$v\vDash\phi$. Let $\sigma\in\llbracket\alpha^{*}\rrbracket$. The proof is
trivial for the case where $\sigma=(\hat{v})$. For any other $\sigma$, there
exists $n\geq 1$ such that $\sigma=\sigma_{1}\circ\dots\circ\sigma_{n}$. If
there exists a $\sigma_{i}$ such that $\sigma_{i}\vDash\lozenge_{[a,b]}\psi$,
as is always the case where $\sigma$ is non-terminating, we get that
$\sigma\vDash\lozenge_{[a,b]}\psi$. Otherwise, for any $i\in\\{1,\dots,n\\}$,
since $\sigma_{i}\in\llbracket\alpha\rrbracket$, instantiating the premise
using the universal $\forall^{\alpha}$ (this is necessary since the premise
may behave differently for different states otherwise), if ${\sf
first}\,\sigma_{i}\vDash\phi$, we get
$\sigma_{i}\vDash\phi\sqcup\lozenge_{[a,b]}\psi$. However, since
$\sigma_{i}\nvDash\lozenge_{[a,b]}\psi$, we have ${\sf
last}\,\sigma_{i}\vDash\phi$. Since $v\vDash\phi$, by induction on $i$, we get
$\sigma\vDash\phi$, which leads to the conclusion of the rule.

(con $\sqcap_{t}$): Assume $v\vDash\forall^{\alpha}\forall r>0\
(\varphi(r)\implies\langle\alpha\rangle(\varphi(r-1)\sqcap\square_{[a,b]}\psi))$
and $v\vDash(\exists r.\varphi(r))\wedge\psi$. Then, there exists a
$d\in\mathbb{R}$ such that $v\vDash\varphi(d)$. We prove the rule using well-
founded induction on $d$. If $d\leq 0$, we have $(\hat{v})\vDash((\exists
r.r\leq 0\land\varphi(r))\sqcap\square_{[a,b]}\psi)$, where
$(\hat{v})\in\llbracket\alpha^{*}\rrbracket$ for the case where $\alpha$
repeats zero times. If, however, $d>0$, we know that $v\vDash\varphi(d)$ and
$v\vDash\varphi(d)\implies\langle\alpha\rangle(\varphi(d-1)\sqcap\square_{[a,b]}\psi)$.
Therefore, there exists an trace $\sigma_{1}\in\llbracket\alpha\rrbracket$
such that $\sigma_{1}\vDash(\varphi(d-1)\sqcap\square_{[a,b]}\psi)$. Since
${\sf last}\,\sigma_{1}\vDash\varphi(d-1)$, if $d-1\leq 0$, we are done with
the proof; otherwise, we can construct a similar $\sigma_{2}$ such that
$\sigma_{2}\vDash(\varphi(d-2)\sqcap\square_{[a,b]}\psi)$. We can continue
until $d\leq 0$, and this induction is well-founded because $d$ decrease by 1
for each step. We have thus constructed
$\sigma=\sigma_{1}\circ\dots\circ\sigma_{n}\in\llbracket\alpha^{*}\rrbracket$
such that each $\sigma_{i}\vDash\square_{[a,b]}\psi$ – and thus
$\sigma\vDash\square_{[a,b]}\psi$ – and ${\sf last}\,\sigma_{n}={\sf
last}\,\sigma\vDash(\exists r.r\leq 0\land\varphi(r))$. Therefore, we have
$\sigma\vDash(\exists r.r\leq 0\land\varphi(r))\sqcap\square_{[a,b]}\psi$. ∎

###### Theorem 4.7.

STd$\mathcal{L}$ is non-axiomatizable.

###### Proof.

Discrete and continuous fragments of d$\mathcal{L}$ were proved to not be
axiomatizable in (Platzer, 2008, 2012). Since STd$\mathcal{L}$ extends
d$\mathcal{L}$, discrete and continuous fragments of STd$\mathcal{L}$ are also
non-axiomatizable. Therefore, in general, STd$\mathcal{L}$ is non-
axiomatizable. ∎

Even though STd$\mathcal{L}$ is non-axiomatizable in general, its proof system
restricted programs without repetitions is complete relative to first-order
logic of differential equations (i.e., first-order real arithmetic augmented
with formulas expressing properties of differential equations) (Platzer, 2008,
2012), as was shown to be the case for d$\mathcal{L}$.

###### Theorem 4.8.

The proof calculus for STd$\mathcal{L}$ restricted to programs without non-
deterministic finite repetitions is complete relative to first-order logic of
differential equations.

###### Proof.

If we restrict STd$\mathcal{L}$ to programs without repetition, the proof
calculus for STd$\mathcal{L}$ reduces temporal properties to non-temporal
properties to leverage the calculus of d$\mathcal{L}$, which is proven to be
complete relative to first-order logic of differential equations (Platzer,
2008, 2012, 2010a). More specifically, any temporal rule in the
STd$\mathcal{L}$ calculus transforms a normalized trace formula to a simpler
normalized trace formula either without a temporal operator or with a temporal
operator following a simpler, decomposed program. Every proof rule is an
equivalence relation (i.e., the premise is equivalent to the conclusion), and
Lemma 4.4 ensures that every trace formula in the syntax of STd$\mathcal{L}$
can be converted into a normalized trace formula able to be handled by the
STd$\mathcal{L}$ calculus. Therefore, the relative completeness result of
d$\mathcal{L}$ extends to STd$\mathcal{L}$ limited to programs without
repetition. ∎

Indeed, we conjecture that the STd$\mathcal{L}$ proof calculus is complete
relative to first-order logic of differential equations for all
STd$\mathcal{L}$ programs. We leave a formal proof of full relative
completeness as future work.

##  5\. Future Work

We plan on working on the following improvements to STd$\mathcal{L}$ as future
work:

  * –

Proving full relative completeness of STd$\mathcal{L}$: While we prove that
the calculus presented in STd$\mathcal{L}$ restricted to programs without non-
deterministic repetition is complete relative to first-order logic of
differential equations, we conjecture that the calculus is indeed complete
relative to first-order logic of differential equations for all programs. We
have yet to prove this conjecture formally.

  * –

Allowing for nested temporal operators in STd$\mathcal{L}$: The fragment of
STL currently supported by our work does not include properties with nested
temporal operators, such as $\square_{[a,b]}\lozenge_{[c,d]}\phi$, to simplify
the proof system. We do not consider this to be a significant drawback, since
the fragment of STL considered is sufficient to cover a large amount of
properties of interest expressed in previous case studies involving STL (Bae
and Lee, 2019; Raman et al., 2014; Jha et al., 2019; Donzé et al., 2012; Raman
et al., 2015). Nevertheless, we hope to remove this restriction in the future
to further increase the expressive power of STd$\mathcal{L}$.

  * –

Implementing the rules for STd$\mathcal{L}$: We hope to implement the rules
for the STd$\mathcal{L}$ proof system into a theorem prover for hybrid systems
such as KeYmaera (Platzer and Quesel, 2008; Fulton et al., 2015).

##  6\. Related Work

In this section, we explore works related to reasoning about properties of
hybrid systems and using STL for monitoring and verfication purposes.

STL (Maler and Nickovic, 2004; Maler and Ničković, 2013) was introduced for
monitoring properties over continuous signals, and has since been studied
widely, e.g., in Deshmukh et al. (Deshmukh et al., 2017), Donzé and Maler
(Donzé and Maler, 2010), Maler et al. (Maler et al., 2008). Most uses of STL
have been mainly for monitoring purposes. However, there has been some work
done on studying temporal properties of hybrid systems in the context of model
checking. Mysore et al. (Mysore et al., 2005) examine model checking of semi-
algebraic hybrid systems for Timed Computation Tree Logic properties. Their
work focuses on bounded model checking for differential equations with
polynomial solutions only, while we allow for more general polynomial
differential equations. Roehm et al. (Roehm et al., 2016) define a new
reachset temporal logic (RTL) and transform STL properties to RTL properties
to perform model checking of continuous and hybrid systems. More recently, Bae
and Lee (Bae and Lee, 2019) explore a bounded model checking of signal
temporal logic properties using syntactic separation of STL. For both (Bae and
Lee, 2019) and (Mysore et al., 2005), the applications presented focus on
bounded safety verification, while our work allows unbounded safety
verification. Better still, our proof system enables proving strong liveness
properties for hybrid systems, a trait not present in works like (Bae and Lee,
2019), (Roehm et al., 2016), and (Mysore et al., 2005).

Process logic (Harel et al., 1982; Nishimura, 1980; Pratt, 1979) originally
used Pnueli’s temporal logic (Pnueli, 1977) in the context of Harel et al.’s
dynamic logic (Harel et al., 2001) for temporal reasoning of hybrid systems.
However, it is restricted to discrete programs and only considers an abstract
notion of atomic programs, without supporting explicit assignments and tests.
Platzer (Platzer, 2008, 2012, 2010b) introduce differential dynamic logic
(d$\mathcal{L}$) to reason about the end states of a hybrid program, later
followed by differential temporal dynamic logic (dTL) (Platzer, 2010a) to
reason about intermediate states of hybrid programs throughout the execution
of the program using some temporal operators of linear temporal logic. Jeannin
and Platzer (Jeannin and Platzer, 2014a) present dTL2, a logic that extends
dTL and allows for alternating program and temporal modalities. While our work
draws on the technical machinery from dTL2, the logic has a significant
drawback compared to STd$\mathcal{L}$ in that it does not support reasoning
about properties in given time intervals. This nature of reasoning not only is
often crucial to proving safety of hybrid systems, but also allows for
expressing a significantly richer set of liveness properties.

Sogokon et al. present a proof method for proving eventuality properties
(Sogokon and Jackson, 2015) and persistence properties (Sogokon et al., 2017)
in hybrid systems. Their methods focus on properties of the form
$\lozenge_{[0,t]}\square_{[0,\infty)}P$, whereas our formalism is more general
but does not support alternating temporal modalities – the properties that the
two results focus on are complementary to each other. Note, however, that
their formalism operates on the level of hybrid automata (Alur et al., 1992;
Henzinger, 2000), which unlike hybrid programs, do not enjoy the property of
having a compositional semantics that can be used to verify systems by
verifying properties of their parts in a theorem prover. Tan and Platzer (Tan
and Platzer, 2020) present an axiomatic approach for deductive verification of
existence and liveness for ordinary differential equations with
d$\mathcal{L}$, but their approach only focuses on liveness for differential
equations, and not entire hybrid systems. They also only work on formulas of
the form $\langle\alpha\rangle P$, which is a fairly limited form of liveness.

Zhou et al. (Chaochen et al., 1992) present a duration calculus for hybrid
real-time systems extended by mathematical expressions with derivatives of
state variables. The system that they present requires external mathematical
reasoning about continuity and derivatives. Davoren and Nerode (Davoren and
Nerode, 2000) study hybrid systems in the context of the propositional
$\mu$-calculus. They provide a calculus to prove formulas in their systems,
but with a propositional system (and not a first-order one). Furthermore, they
do not provide specific rules in their proof system to handle ordinary
differential equations.

##  7\. Conclusion

In this work, we introduce signal temporal dynamic logic (STd$\mathcal{L}$), a
logic that extends and combines differential dynamic logic (d$\mathcal{L}$)
with a fragment of signal temporal logic (STL). STd$\mathcal{L}$ is a
conservative extension of d$\mathcal{L}$ and allows reasoning not only about
the final states of a hybrid system, but also the intermediate states of a
hybrid system in given time intervals. While STL was originally intended to be
a logic for monitoring systems, and has widely been used for exactly that
purpose, we show that STL can very well be used for deductive verification of
hybrid systems. STd$\mathcal{L}$ allows us to prove a greater set of both
safety and liveness properties than was possible with logics preceding
STd$\mathcal{L}$. We provide a semantics and a sound proof calculus for
STd$\mathcal{L}$, along with proofs of soundness and relative completeness.

### Acknowledgements

The authors would like to thank Nikos Aréchiga for insightful discussions.
Toyota Research Institute (“TRI”) provided funds to assist the authors with
their research, but this article solely reflects the opinions and conclusions
of its authors and not TRI or any other Toyota entity.

## References

  * (1)
  * Ahmad and Jeannin (2021) Hammad Ahmad and Jean-Baptiste Jeannin. 2021.  A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems. In _Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control_.
  * Alur et al. (1992) Rajeev Alur, Costas Courcoubetis, Thomas A Henzinger, and Pei-Hsin Ho. 1992.  Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems.  In _Hybrid systems_. Springer, 209–229.
  * Bae and Lee (2019) Kyungmin Bae and Jia Lee. 2019.  Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation.  _Proc. ACM Program. Lang._ 3, POPL, Article 51 (Jan. 2019), 30 pages.  https://doi.org/10.1145/3290364
  * Chaochen et al. (1992) Zhou Chaochen, Anders P Ravn, and Michael R Hansen. 1992\.  An extended duration calculus for hybrid real-time systems.  In _Hybrid Systems_. Springer, 36–59.
  * Davoren and Nerode (2000) Jennifer Mary Davoren and Anil Nerode. 2000.  Logics for hybrid systems.  _Proc. IEEE_ 88, 7 (2000), 985–1010.
  * Deshmukh et al. (2017) Jyotirmoy V Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A Seshia. 2017.  Robust online monitoring of signal temporal logic.  _Formal Methods in System Design_ 51, 1 (2017), 5–30.
  * Donzé and Maler (2010) Alexandre Donzé and Oded Maler. 2010.  Robust satisfaction of temporal logic over real-valued signals. In _International Conference on Formal Modeling and Analysis of Timed Systems_. Springer, 92–106.
  * Donzé et al. (2012) Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu, and Scott Smolka. 2012\.  On temporal logic and signal processing. In _International Symposium on Automated Technology for Verification and Analysis_. Springer, 92–106.
  * Fulton et al. (2015) Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015\.  KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In _International Conference on Automated Deduction_. Springer, 527–538.
  * Harel et al. (1982) David Harel, Dexter Kozen, and Rohit Parikh. 1982\.  Process logic: Expressiveness, decidability, completeness.  _Journal of computer and system sciences_ 25, 2 (1982), 144–170.
  * Harel et al. (2001) David Harel, Dexter Kozen, and Jerzy Tiuryn. 2001\.  Dynamic logic.  In _Handbook of philosophical logic_. Springer, 99–217.
  * Henzinger (2000) Thomas A Henzinger. 2000\.  The theory of hybrid automata.  In _Verification of digital and hybrid systems_. Springer, 265–292.
  * Jeannin and Platzer (2014a) Jean-Baptiste Jeannin and André Platzer. 2014a.  dTL2: Differential temporal dynamic logic with nested temporalities for hybrid systems. In _International Joint Conference on Automated Reasoning_. Springer, 292–306.
  * Jeannin and Platzer (2014b) Jean-Baptiste Jeannin and André Platzer. 2014b.  _dTL 2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems_.  Technical Report CMU-CS-14-109. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 15213.  http://reports-archive.adm.cs.cmu.edu/anon/2013/abstracts/14-109.html
  * Jha et al. (2019) Susmit Jha, Ashish Tiwari, Sanjit A Seshia, Tuhin Sahai, and Natarajan Shankar. 2019.  TeLEx: learning signal temporal logic from positive examples using tightness metric.  _Formal Methods in System Design_ 54, 3 (2019), 364–387.
  * Maler and Nickovic (2004) Oded Maler and Dejan Nickovic. 2004.  Monitoring temporal properties of continuous signals.  In _Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems_. Springer, 152–166.
  * Maler and Ničković (2013) Oded Maler and Dejan Ničković. 2013.  Monitoring properties of analog and mixed-signal circuits.  _International Journal on Software Tools for Technology Transfer_ 15, 3 (2013), 247–268.
  * Maler et al. (2008) Oded Maler, Dejan Nickovic, and Amir Pnueli. 2008\.  Checking temporal properties of discrete, timed and continuous behaviors.  In _Pillars of computer science_. Springer, 475–505.
  * Mysore et al. (2005) Venkatesh Mysore, Carla Piazza, and Bud Mishra. 2005\.  Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology. In _International Symposium on Automated Technology for Verification and Analysis_. Springer, 217–233.
  * Nishimura (1980) Hirokazu Nishimura. 1980\.  Descriptively complete process logic.  _Acta Informatica_ 14, 4 (1980), 359–369.
  * Platzer (2008) André Platzer. 2008\.  Differential dynamic logic for hybrid systems.  _Journal of Automated Reasoning_ 41, 2 (2008), 143–189.
  * Platzer (2010a) André Platzer. 2010a.  _Differential Temporal Dynamic Logic dTL_.  Springer Berlin Heidelberg, Berlin, Heidelberg, 203–230.  https://doi.org/10.1007/978-3-642-14509-4_4
  * Platzer (2010b) André Platzer. 2010b.  _Logical analysis of hybrid systems: proving theorems for complex dynamics_.  Springer Science & Business Media.
  * Platzer (2012) André Platzer. 2012\.  Logics of dynamical systems. In _Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science_. IEEE Computer Society, 13–24.
  * Platzer and Quesel (2008) André Platzer and Jan-David Quesel. 2008.  KeYmaera: A hybrid theorem prover for hybrid systems (system description). In _International Joint Conference on Automated Reasoning_. Springer, 171–178.
  * Pnueli (1977) Amir Pnueli. 1977\.  The temporal logic of programs. In _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_. IEEE, 46–57.
  * Pratt (1979) V. R. Pratt. 1979\.  Process Logic: Preliminary Report. In _Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages_ (San Antonio, Texas) _(POPL ’79)_. Association for Computing Machinery, New York, NY, USA, 93–100.  https://doi.org/10.1145/567752.567761
  * Rajkumar et al. (2010) Ragunathan Rajkumar, Insup Lee, Lui Sha, and John Stankovic. 2010\.  Cyber-physical systems: the next computing revolution. In _Design automation conference_. IEEE, 731–736.
  * Raman et al. (2014) Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A Seshia. 2014.  Model predictive control with signal temporal logic specifications. In _53rd IEEE Conference on Decision and Control_. IEEE, 81–87.
  * Raman et al. (2015) Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M Murray, and Sanjit A Seshia. 2015\.  Reactive synthesis from signal temporal logic specifications. In _Proceedings of the 18th international conference on hybrid systems: Computation and control_. 239–248.
  * Roehm et al. (2016) Hendrik Roehm, Jens Oehlerking, Thomas Heinz, and Matthias Althoff. 2016.  STL Model Checking of Continuous and Hybrid Systems. In _Automated Technology for Verification and Analysis_ , Cyrille Artho, Axel Legay, and Doron Peled (Eds.). Springer International Publishing, Cham, 412–427.
  * Sogokon and Jackson (2015) Andrew Sogokon and Paul B Jackson. 2015.  Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In _International Symposium on Formal Methods_. Springer, 514–531.
  * Sogokon et al. (2017) Andrew Sogokon, Paul B Jackson, and Taylor T Johnson. 2017\.  Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants. In _NASA Formal Methods Symposium_. Springer, 194–211.
  * Tan and Platzer (2020) Yong Kiam Tan and André Platzer. 2020.  An Axiomatic Approach to Existence and Liveness for Differential Equations.  arXiv:2004.14561 [cs.LO]