$\mathsf {dL}_{\iota }$: Definite Descriptions in Differential Dynamic Logic

Abstract

We introduce , which extends differential dynamic logic () for hybrid systems with definite descriptions and tuples, thus enabling its theoretical foundations to catch up with its implementation in the theorem prover . Definite descriptions enable partial, nondifferentiable, and discontinuous terms, which have many examples in applications, such as divisions, nth roots, and absolute values. Tuples enable systems of multiple differential equations, arising in almost every application. Together, definite description and tuples combine to support long-desired features such as vector arithmetic.

We overcome the unique challenges posed by extending with these features. Unlike in , definite descriptions enable non-locally-Lipschitz terms, so our differential equation (ODE) axioms now make their continuity requirements explicit. Tuples are simple when considered in isolation, but in the context of hybrid systems they demand that differentials are treated in full generality. The addition of definite descriptions also makes a free logic; we investigate the interaction of free logic and the ODEs of , showing that this combination is sound, and characterize its expressivity. We give an example system that can be defined and verified using these extensions.

This research was sponsored by NDSEG, the AFOSR under grant number FA9550-16-1-0288, and the Alexander von Humboldt Foundation.

1 Introduction

Cyber-physical systems (CPSs) such as self-driving cars, trains, and airplanes combine discrete control and continuous physical dynamics and are often safety-critical because they operate around humans. Thus, it is essential to achieve the highest possible confidence in their correctness, e.g., using formal methods with strong theoretical foundations. Differential dynamic logic () [18, 22, 23] is a logic for formal verification of hybrid systems [10], widely-used models of CPSs that incorporate both their discrete and continuous behaviors. Among formal methods for CPSs, is notable both for its case studies [12, 15, 16] using the  [9] theorem prover, and for its strong foundations, as evidenced by its completeness results [18, 22, 23, 25] and a formal proof of soundness in both Isabelle/HOL and Coq [4].

However, there is a tension between the goals of practical applicability and rigorous foundations. In practice, theorem prover implementations often demand new features which were not anticipated in theory. Formalizations of  [5], Coq [2], and NuPRL [1] all omit or simplify whichever practical features are most theoretically challenging for their specific logic: discontinuous and partial terms in , termination-checking in Coq, or context management in NuPRL. When formalizations of theorem provers do succeed in reflecting the implementation [13], they owe a credit to the generality of the underlying theory: it is much more feasible to formalize a general base theory than to formalize multiple ad-hoc extensions as they arise.

This paper introduces , a new, generalized foundation for where definite description $\iota {x}\,{\phi }$ denotes the unique x for which $\phi$ holds, enabling practical extensions like divisions $\theta _1/\theta _2$, roots $\root n \of {\theta }$, and the functions $\min (\theta _1,\theta _2),$ $\max (\theta _1,\theta _2),$ and , while pairs $(\theta _1,\theta _2)$ enable differential equation (ODE) systems. Useful new features like trigonometric functions and vectors are also definable, and existing features like differentials have elegant new axiomatizations in .

The term $\iota {x}\,{\phi }$ is the definite (i.e., requiring unique existence) counterpart of Hilbert’s choice $\varepsilon {x}\,{\phi };$ both have seen success in HOL-style theorem provers [17, 26]. We chose definite $\iota {x}\,{\phi }$ over $\varepsilon {x}\,{\phi }$ because uniqueness significantly simplifies continuity and differential reasoning. In adopting definite descriptions and tuples in , we solve the novel challenges of integrating them with differential equations, ’s distinguishing feature. Definite descriptions allow partiality, discontinuity, and nondifferentiability, all of which interact subtly with sound ODE reasoning. Multidimensional systems, enabled by tuples, demand a general treatment of differentials and expose subtle variable dependencies in some advanced ODE reasoning principles.

An example demonstrates the power of definite description: definite descriptions allow non-polynomial terms and thus non-polynomial ODEs, which need not have unique solutions. While non-polynomial ODEs (and all of ) are reducible to in theory, the reduction of $\iota {x}\,{\phi }$ is completely impractical [3]. Expressivity comes with deep semantic changes: supporting partiality makes a free logic, for which we adopt a 3-valued Łukasiewicz semantics. We show this profound change in foundations needs only small changes to the proof calculus with additional definedness conditions. We develop the theory of , show that the proof calculus is sound and show the nontrivial reduction from to .

2 Syntax

We present the core syntax of , which extends with definite descriptions and tuples. We describe the constructs informally here, deferring formal semantics to Sect. 3. As a free logic [8], contains terms that do not denote and formulas whose truth values are unknown (truth is indicated $\oplus$, falsehood by $\ominus$, and unknown by $\oslash$), a major point of difference between our semantics and proof calculus vs. those of . Our calculus uses uniform substitution [6, §35,§40], where symbols ranging over predicates, programs, etc. are explicitly represented in the syntax, because it has simplified the construction of calculi [23], implementations [9], and machine-checked correctness proofs [4]. This will ease implementing and mechanizing the soundness proof in future work. The syntax of is divided into terms, programs, and formulas, whose definitions, unlike in , are all mutually recursive. The terms $\theta$ of extend the terms of with definite descriptions, pairs, and reductions:

for literal $q \in \mathbb {Q}$ and variable , where is the set of all variable names, f is a function symbol, and $\phi$ is a formula. The first six cases, polynomials, differentials, and function symbols, are as in . Variables are flexible: they are modified by quantifiers and programs. Variables x always denote some value and so assignments succeed only when the RHS denotes a value. In contrast, $f(\theta )$ is an uninterpreted function f applied to term $\theta$, but both $\theta$ and $f(\theta )$ are allowed to be non-denoting. While function symbols f rarely appear in theorem statements, they are essential for the axioms of Sect. 5. The definite description $\iota {x}\,{\phi }$ denotes the unique value of x that makes formula $\phi$ true, if exactly one such value exists, else it does not denote (since description is definite). Pairs $(\theta _1,\theta _2)$ can be nested to arbitrary finite depth, so their eliminator is primitive recursion on binary trees with values at the leaves. Reduction $\textsf {red}(\theta _1,s~\theta _2,lr~\theta _3)$ reduces every leaf $t \in \mathbb {R}$ to and reduces every pair a, b of recursive results to , where is the capture-avoiding substitution of y for every x in e. For example, if $\theta _1 = ((-1,2),-3),$ then the reduction $\textsf {red}(\theta _1,s~s^2,lr~(r,l))$ is the elementwise square of the reverse tree, (9, (4, 1)).

The programs $\alpha ,\beta$ of are hybrid programs, a program syntax for hybrid systems combining discrete and continuous dynamics. Hybrid programs of are identical to those of with the exception that any formula or term contained therein is again any formula or term of , not necessarily just . For any starting state, a program $\alpha$ might transition to zero, one, or many final states. Whenever a program transitions to zero states, we say it aborts.

Assignments assign the value of term $\theta$ to variable x, if $\theta$ denotes a value, else they abort. Tests abort execution if formula $\phi$ is not true, else they are no-ops. Nondeterministic choices $\alpha \cup \beta$ behave as either $\alpha$ or $\beta ,$ nondeterministically. Sequential composition $\alpha ;\beta$ performs $\beta$ in any state resulting from $\alpha$. Loops repeat $\alpha$ sequentially any number of times, nondeterministically. The defining construct of hybrid programs are the differential equations , which continuously evolve x according to the differential equation for any duration such that term $\theta$ denotes and formula $\psi$ is true throughout. Note the core syntax of need only contain systems of a single variable x: in Sect. 4 we will derive systems with multiple variables from systems of one variable. Uninterpreted program constants a range over programs. We parenthesize programs $\alpha$ as $\{ \alpha \}$ with braces for disambiguation and readability. The formulas $\phi ,\psi$ of are defined inductively:

Conjunctions $\phi \wedge \psi ,$ negations $\lnot \phi ,$ and quantifiers are as is standard in first-order Łukasiewicz [14] logic. The quantifier is also as in first-order Łukasiewicz logic and can be derived . In comparing $\theta _1 \ge \theta _2,$ if terms $\theta _1$ and $\theta _2$ both denote reals, those reals are compared, if they both denote tuples they are compared elementwise, in all other cases the result is unknown ($\oslash$). The defining construct of dynamic logics is which says $\phi$ holds in all states reachable by running $\alpha$. Its dual, , says there exists a state reachable by running $\alpha$ where $\phi$ holds, and can be derived by the equivalence . Uninterpreted predicate symbols p expect terms $\theta ,$ which are also allowed not to denote, as arguments, and are allowed truth value unknown ($\oslash$). We write P, Q for predicates which take all variables as arguments. We sometimes write the implication as $\psi \leftarrow \phi$ for emphasis on $\psi$.

Example 1

(Robot Water Cooler). The textbook examples of non-Lipschitz ODEs are those of form for constant k. In , in contrast to , non-Lipschitz terms simplify describing a hybrid system with such ODEs, which we base on Hubbard’s leaky bucket [11, §4.2]. Consider a water cooler of height h and an opening of surface area a in its bottom of surface area A, where g is acceleration due to gravity. Suppose an enterprising student has equipped the cooler’s valve with robotic control. We could then model the cooler as:

This says that so long as there is water in the cooler () we can choose to open the valve (), but we can always close the valve (). Then the water drains out the cooler at a rate proportional to the square root of the current volume by Torricelli’s Law [7], or rate 0 if the valve is closed. This control process repeats arbitrarily often. The constructs $\sqrt{2gh}$ (root) and $\frac{a}{A}$ (division) are not core , but we can rewrite $\alpha _B$ using definite descriptions:

This example is representative because the ODE is non-Lipschitz: the solution is unique at $h=0$ only within the constraint $h \ge 0$. The terms $\sqrt{2gh}$ and $\frac{a}{A}$ are also both partial: defined only assuming $gh \ge 0$ and $A \ne 0$, respectively. The interactions between partiality, uniqueness, and the constraint combine to make the proof subtle, even if short.

Common (and likewise, ) theorems include safety assertions of the form which say that if $\phi$ holds initially, then $\psi$ will necessarily hold after $\alpha$. For example, we might wish to prove the final water height of $\alpha _B$ never exceeds the initial height, so it is actually leaky (or at least is not filling up):

Proposition 1

(Leakiness). This is valid (definitely true $\oplus$ in all states):

We will prove Proposition 1 after we have introduced a proof calculus for in Sect. 5.

3 Denotational Semantics

We now formally define the semantics of terms, formulas, and programs. Due to the presence of definite descriptions $\iota {x}\,{\phi (x)},$ not every term denotes in every state, i.e., is a free logic [8]. We write $\bot$ for the interpretation of a term that does not denote any value. When a term denotes, it denotes a finite, binary tree with real values at the leaves: a scalar denotes a singleton tree, while (arbitrarily nested) pairs denote non-singleton trees. We refer to the set of all real trees as $\mathbf {Tree}(\mathbb {R})$, where for any S, $\mathbf {Tree}(S)$ is the smallest set such that: (i) S $\subseteq \mathbf {Tree}(S),$ and (ii) for any l and $r \in \mathbf {Tree}(S)$, $(l,r) \in \mathbf {Tree}(S)$. Typing is extrinsic, i.e., we do not make typing distinctions between $\mathbb {R}$ and $\mathbf {Tree}(\mathbb {R})$ in the semantics; typing constraints will be expressed explicitly as predicates. To account for non-denoting terms, formulas can take on three truth values: $\oplus$ (definitely true), $\oslash$ (unknown), and $\ominus$ (definitely false). Thus is a 3-valued logic, and first-order connectives use the Łukasiewicz [14] interpretation.

The interpretation functions are parameterized by state mapping variables to values, and by an interpretation I mapping function symbols, predicate symbols, and program constants to their interpretation, including the possibility of not denoting a value. Writing $\mathcal {S}$ for the set of all states, we have $I(f):(\mathbf {Tree}(\mathbb {R}) \cup \bot ) \rightarrow (\mathbf {Tree}(\mathbb {R}) \cup \bot ),$ $I(p):(\mathbf {Tree}(\mathbb {R}) \cup \bot ) \rightarrow \{\oplus , \oslash , \ominus \},$ and where is the power set of a set U. Below, is the state that is equal to $\omega$ except at x, where .

Definition 1

(Term semantics). The denotation of a term is either a tree or undefined, i.e. , and is inductively defined as:

where abuses notation: when $\omega (x)$ is a tuple, the partial is taken w.r.t. each leaf in x,  scaled by the corresponding component of ; the subtleties of semantics for differentials are discussed at greater length in the companion report [3]. In previous formalisms for  [23] the semantics of do not explicitly require that $\theta$ is totally differentiable because all pure terms are already smooth, thus totally differentiable. In contrast, not all terms are smooth, thus we require total differentiability explicitly, as it is required for soundness (specifically of $\text {DI}_{\ge }$, Sect. 5). If differentiability conditions are not met, then . Reductions $\mathsf {Fold}(t,s~\theta _R,lr~\theta _T,I\omega )$ recurse on t:

That is, they reduce singletons t by binding s to t in $\theta _R,$ and reduce node (L, R) by binding l, r to the reductions of the respective branches in $\theta _T$.

Definition 2

(Formula semantics). The formula semantics are 3-valued:

Implication can be intuited as $p \le q,$ (where $\ominus< \oslash < \oplus$) so is $\oplus$ even when $p = q = \oslash$. Conjunction $p \sqcap q$ takes the minimum value of the arguments, and is unknown $\oslash$ when the least conjunct is $\oslash$. Equivalence $p \leftrightarrow q$ is reflexive (even $(\oslash \leftrightarrow \oslash )$ is $\oplus$), but is $\oslash$ in all other cases where some argument is $\oslash$. We say a formula $\phi$ is valid if for all $\omega$ and I. Comparisons $\theta _1 \ge \theta _2$ are taken elementwise and are unknown ($\oslash$) for differing shapes. Predicates p are interpreted by the interpretation I. The meaning of quantifiers and are taken as conjunctions $\sqcap _S$ over potentially-uncountable index sets S. The value of $\sqcap _S$ is the least value of any conjunct, one of $\{\ominus ,\oslash ,\oplus \}$.

Definition 3

(Program semantics). Program semantics generalize those of as conservatively as possible so that verification finds as many bugs as possible: e.g. assignments of non-denoting terms and tests of unknown formulas abort. The denotation of a program $\alpha$ is a relation where whenever final state $\nu$ is reachable from initial state $\omega$ by running $\alpha$.

where $X^\complement$ is the complement of set X. ODEs are initial value problems: if some solution $\varphi$ of some duration $r\in \mathbb {R}_{\ge 0}$ takes $\omega$ to $\nu$ while satisfying $\psi$ throughout. A solution $\varphi$ must satisfy as an equation, satisfy constraint $\psi ,$ and assign the time-derivative of each x to each . The initial value of is overwritten and variables except are not changed. Assignments are strict: they store the value of $\theta$ in variable x,  or abort if $\theta$ does not denote a value. Tests succeed if $\phi$ is definitely true ($\oplus$); both the unknown ($\oslash$) and definitely false ($\ominus$) cases abort execution. Likewise, the domain constraint $\psi$ of a differential equation must be definitely-true ($\oplus$) throughout the entire evolution and the term $\theta$ implicitly must denote values throughout the evolution, since .

4 Derived Constructs

A key benefit of is extensibility: Many term constructs can be defined with definite descriptions $\iota {x}\,{\phi }$ and tuples which otherwise require unwieldy encodings as formulas. In this section we reap the benefits of extensibility by defining such new term constructs.

Arithmetic Operations. In practice, we often wish to use arithmetic operations beyond the core operations. Figure 1 demonstrates basic arithmetic operations which have simple definitions in but not as terms in : Of these, $\max ,\ \min ,$ and preserve Lipschitz-continuity but not differentiability. Roots $\sqrt{\theta }$ can violate even Lipschitz-continuity and both roots and divisions are non-total. In practice (as in Example 1), these operators are used in ODE models, making their continuity properties essential. Since pure requires smooth terms [23], even functions $\max$ and $\min$ would be encoded as formulas in pure .

Fig. 1.

Derived arithmetic operations (for fresh x, t, c, s, z)

Tuples. We make tuples first-class in to simultaneously simplify the treatment of ODEs compared to prior work [18] and provide support for data structures such as vectors, widely used in physical computations. In contrast to the flexible function symbols (think: unbounded arrays) of  [20], they are equipped with a primitive recursion operator, making it easier to write sophisticated functional computations. These structures can be used in systems with non-scalar inputs, for example a robot which avoids a list of obstacles [16].

While pairs $(\theta _1,\theta _2)$ are core constructs, the left and right projections $\pi _{1}{\theta }$ and $\pi _{2}{\theta }$ are derivable, as are convenience predicates $\textsf {in}{\mathbb {R}}(\theta )$ and $\textsf {isT}(\theta )$ which hold exactly for scalars and tuples, respectively:

When combined with the reduce operation on trees, these operations can be used to implement a variety of data structures. Figure 2 shows an example library of operations on lists. Lists are represented as nested pairs, with no special terminator. We name an argument L to indicate its intended use as a list rather than an arbitrary tree. Lists are trees whose left-projections are never pairs. Additional data structures are shown in the report [3].

Systems of ODEs. Tuples reduce ODE systems to individual ODEs, e.g.:

While this encoding is simple, it will enable us in Sect. 5 to support systems of any finite dimension in axiom DG, which implementation experience [9] has shown challenging due to the variable dependencies involved.

Fig. 2.

Example vector functions

Types and Definedness. Many of the operations in expect, for example, reals or terms that denote values. For simplicity, we make these type distinctions extrinsically: core terms are untyped, and proposition $\textsf {in}{\mathbb {R}}(\theta )$ says $\theta$ belongs to type $\mathbb {R}$. Typed quantifiers are definable, e.g., . Whether a term denotes is also treated extrinsically. Formula $\mathsf {E}(\theta )\equiv \mathsf {D}(\theta = \theta )$ only holds for terms that denote, where $\mathsf {D}(\phi )$ says $\phi$ is definitely true, which has truth value $\oplus$ when $\phi$ has truth value $\oplus$ and has value $\ominus$ otherwise. We give its truth table and a definition:

That is, $\mathsf {D}(\phi )$ collapses $\oslash$ into $\ominus$. These constructs are used in the axioms of Sect. 5. In the same spirit, we sometimes need to know that a function f(x) (of any dimension) is continuous, but derive this notion. We write $\mathsf {Con}(f(x))$ to say that f(x) is continuous as x varies around its current value:

Note that when $\mathsf {Con}(f(x))$ holds, the shape of f(x) is constant in a neighborhood of x, since the Euclidean norm does not exist when f(y) and f(x) differ in shape. Likewise, $\mathsf {Con}(f(x))$ requires only continuity on y whose shape agrees with that of x,  since the Euclidean norm does not otherwise exist.

5 Axioms

Our proof system is given in the Hilbert style, with a minimum number of proof rules and larger number of axioms, each of which is an individual concrete formula. The core proof rule is uniform substitution [23][6, §35,§40]: from the validity of $\phi$ we can conclude validity of $\sigma (\phi )$ where the uniform substitution $\sigma$ specifies concrete replacements for some or all predicates, functions, and program constants in a formula $\phi$:

The soundness side-conditions to US about $\sigma$ are non-trivial, and make up much of its soundness proof in Sect. 6. The payoff is that uniform substitution enables a modular design where such subtle arguments need only be done once in the soundness proof of the US rule, and every axiom, which is now an individual concrete formula, is significantly simpler to prove valid and to implement.

Fig. 3.

Discrete axioms

Figure 3 gives axioms and rules for the discrete programming constructs, which are generalizations of corresponding axioms [23] for to account for non-denoting terms and unknown formulas. Axioms are augmented with definedness conditions whenever multiple occurrences of terms or formulas differ in their tolerance for partiality. The conclusion (in canonical usage) of each axiom is highlighted in , while any difference from the axioms is highlighted in . Recall the operator $\mathsf {D}(\phi )$ says $\phi$ is definitely true. For example, axiom [?] says that a test succeeds when Q is definitely true. The induction axiom I requires the inductive step proved definitely true, but concludes definite truth. The other axioms for program constructs ($[\cdot ],[\cup ],[;],[*]$) carry over from without modification, since partiality primarily demands changes when mediating between formulas and programs or between terms and program variables. As is standard in free logics, axiom $\forall$i says that since quantifiers range over values, they must be instantiated only to terms that denote values. Assignments [:=] require the assigned term to denote a value, since program variables x range over values.

Fig. 4.

Differential equation axioms and differential axioms

Figure 4 gives the generalizations of ’s axioms for reasoning about differential equations: DC is generalized by analogy to [?] to require definite truth and DG is generalized to require continuity, otherwise the axioms carry over unchanged. DW says the constraint of an ODE always holds as a postcondition. DC says any postcondition which is proven (definitely) true may be added to the constraint. DE says the ODE holds as an equation in the postcondition. $\text {DI}_{\ge }$ is the differential induction [19] axiom for proving nonstrict inequalities $f(x) \ge g(x)$ follow from their differential formula . The strict case $f(x) > g(x)$ is analogous; axioms for equality, inequality, conjunction, and disjunction can be derived from these. Note the assumptions in $\text {DI}_{\ge }$ hold only when f(x) and g(x) are totally differentiable within the constraint, as required for soundness. DG allows extending a system with an additional ghost dimension, and is used for everything from solving systems to reasoning about exponentially-decaying systems [25]. The new dimension is required to be Lipschitz so that solutions exist and is required to be linear in the new variables so that the solutions of the extended system exist as long as those of the initial system. DS says the solution of a constant ODE system is linear. To solve multidimensional systems with DS, interpret $x+fs$ and $x+ft$ as pairwise vector sums per Fig. 2. Axiom $(\theta )'$ expands a differential according to the definition of total differential. It assumes because equalities are not allowed to hold between non-denoting terms; proving these assumptions is enabled by axiom $\text {E}(')$. In practice, axioms are derived from $\text {E}(')$ for each case and applied recursively to automatically prove existence, for example:

is used to show differentials of sums exist. Likewise, axiom $(\theta )'$ is long-winded for practical proving, so we will use it to implement simpler special-case axioms in Example 2. The definition of $(\theta )'$ above only supports real-valued x and f(x), because scalar differences $f(y)-f(x)$ and $y-x$ only denote a value when x, y, f(x),  and f(y) are reals. The report [3] discusses its generalization to tree-valued functions of tree-valued arguments.

Fig. 5.

Axioms for datatypes

Figure 5 gives axioms for definite descriptions and tuples. Axiom $\iota$ fully characterizes definite descriptions, and it is used to derive axioms for defined term constructs like those in Example 2. Axiom =T enables comparisons on tuples. Quantifier elimination rule QE uses that first-order real arithmetic, a fragment, is decidable [27]. Since variables of may range over tuples, which are not part of first-order arithmetic, it must first check that all variables of the formula (written ) are indeed real-valued. Axioms redT and redR evaluate reductions when their shape is known, and axiom TreeI allows proving a property of an arbitrary value by induction on its shape, including a second base case $p(\iota {x}\,{0=1})$ where the argument to p does not denote.

Example 2

(Derived axioms). The following are examples of derived axiom schemata that have been proved from those above. Proofs are in the report [3].

It is significant that the differential axioms of Example 2 are derived: when new term constructs are added in the future, we expect to derive their differential axioms as well, so that these extensions lie entirely outside the core calculus. Note that these axioms also conclude (by applying axiom $\text {E}(')$) that the differential of the larger term exists, because it equals something. Thus, these axioms are suitable both for showing differentials exist and what form differentials take.

Example 3

(Proof of leakiness). Proposition 1 of Sect. 2 is provable in .

Proof

(Sketch). By axiom I with loop invariant $P \equiv \left( g \mathop {>} 0 \wedge A \mathop {>} 0 \wedge 0 \mathop {\le } h \mathop {\le } h_0\right)$. The first two conditions are trivially invariant by axiom V because g and A are constant throughout $\alpha _B$. Proceed by cases with axiom [U]. In each case, show $h \le h_0$ to be an invariant of the ODE by $\text {DI}_{\ge }$ . Because $h \le h_0$ holds initially and the ODE is locally Lipschitz-continuous given constraint $h \ge 0,$ it suffices to show throughout. Then by algebra and DE, which is true by DW, showing $h \le h_0$.   $\square$

6 Theory

Proofchecking is decidable, and provable formulas are valid.

Theorem 1

(Proofchecking decidability). There exists an algorithm which decides whether a derivation $\mathcal {D}$ is a proof of a given formula $\phi$.

Theorem 2

(Soundness of ). If $\phi$ is provable in , then $\phi$ is valid.

The proof of soundness proceeds by induction on the structure of derivations. That is, we prove each axiom (which is an individual formula) to be valid and prove every proof rule to be sound (producing valid conclusions from valid premisses). Because supports the formula and program connectives of , many of the axioms are extensions of corresponding axioms. The axiom validity proofs also have a similar flavor to those of : each axiom is proven valid by direct proof, showing truth of the axiom according to the denotational semantics in an arbitrary state. The full proofs for each axiom and rule are given in the report [3]; Lemma 1 gives an example.

Lemma 1

(Assignment axiom is valid). The following formula is valid:

Proof

Assume (1) for some state $\omega$ and interpretation I, then observe by the chain of equalities    $\square$

6.1 Uniform Substitution

The uniform substitution proof rule in is analogous to that in :

In , the US rule is sound when the substitution $\sigma$ does not introduce free references to bound variables, in a sense made precise elsewhere [23]. Such substitutions are called admissible, a condition which can be checked syntactically.

We show that the same holds of when adding terms $\iota {x}\,{\phi }, (\theta _1, \theta _2)$ and $\textsf {red}(\theta _1,s~\theta _2,lr~\theta _3)$ and generalizing to a three-valued semantics. As in , we formulate admissibility in terms of U-admissibility (Definition 4) checks.

Definition 4

(Admissible uniform substitution). A substitution $\sigma$ is U-admissible for $\phi$ (or $\theta$ or $\alpha$) with respect to a set iff where $\sigma |_{\varSigma (\phi )}$ is the restriction of $\sigma$ that only replaces symbols that occur in $\phi$ and are the free variables that $\sigma$ introduces, and where . The substitution $\sigma$ is admissible for $\phi$ (or $\theta$ or $\alpha$) if all such checks during its applications hold, per Fig. 6.

Fig. 6.

Uniform substitution algorithm (selected cases)

In Fig. 6, $\sigma f$ denotes the replacement for symbol f provided by $\sigma$. We give the new cases of here and the full static semantics in the report [3]:

Admissibility checks employ static semantics consisting of free-variable (), may-bound-variable (), and must-bound-variable () computations. Generally speaking, the free variables of a compound expression $\theta$ are the free variables of its immediate subexpressions, minus any variables that it binds Formally, (or $\phi , \alpha$) contains all variables that influence meaning:

Lemma 2

(Coincidence). The interpretation of an expression depends only on the values of its free variables and constants, e.g. for any term $\theta$, any interpretations I and J that agree on the signature (mentioned predicate symbols, function symbols, and program constants) $\varSigma (\theta )$ of $\theta$, and any states $\omega$ and $\tilde{\omega }$ that agree on , we have .

The substitution result for a compound expression is found by substituting in each immediate subexpression, and is defined so long as all admissibility checks hold recursively. In general, the admissibility check for each constructor says that the substitution result must not contain any new occurrences of the variables bound at that constructor.

Theorem 3

(Uniform substitution). Rule US is sound.

Soundness of the proof system then follows from validity of the axioms and soundness of US and of the other proof rules.

6.2 Expressive Power

After showing soundness of , we explore its expressive power: can express formulas that are inexpressible in , or is its advantage the ease with which certain formulas are expressed? Conversely, are all formulas expressible in ? Because is an extension of , it is unsurprising that it can express all formulas. However, a valid formula $\phi$ is not always valid in .

Remark 1

(Conservativity counterexample). There exist valid formulas of that are not valid formulas of .

Proof

The formula $\phi \equiv \left( x \cdot x \ge 0\right)$ is not conserved, because it is true for all real values of x,  but fails when x is a tuple such as (0, 0), outside the domain of multiplication. This is why rule QE requires $\textsf {in}{\mathbb {R}}(x)$ for each mentioned x.    $\square$

We transform quantifiers to real-valued quantifiers to close the gap:

Theorem 4

(Converse reducibility). There exists a linear-time transformation T such that for all $\phi$ in , $T(\phi )$ is valid in iff $\phi$ is valid in .

The greater challenge is to show that also suffices to express all formulas and thus and are equiexpressive:

Theorem 5

(Reducibility). There is a computable T s.t. for all formulas $\phi ,$ interpretations I,  and states in , in iff in .

While this result might be misread to suggest that is not truly necessary, definite descriptions enable us to define constructs that have no description as terms in , even if they can be expressed through a sufficiently complex formula translation. The key is that the reduction from to is indeed complex, exploiting for example Gödel encodings for tuples and continuous functions [21, 24]. On the contrary, the complexity of the reduction shows that native support for definite descriptions is essential for practical proving. The equiexpressiveness result is of theoretical interest because it allows us to inherit results from  [18]:

Theorem 6

(Completeness and decidability). is reducible to , and therefore semidecidable relative to properties of differential equations.

While the reduction gives a semi-decision procedure for in principle, it is infeasible for implementation, especially since deciding even core is hard in practice. Moreover, this would defeat our purpose: easing implementation of practical term language extensions in , where interactive proof is common.

7 Conclusion and Future Work

In this paper we developed , an extension to differential dynamic logic () for formal verification of hybrid systems models of safety-critical cyber-physical systems. The key feature of is definite description $\iota {x}\,{\phi },$ which provides a foundation for defining new term language constructs from their characteristic formulas. We develop the theory of , including semantics, a proof calculus, and soundness and expressiveness proofs. We apply to verify a classic example of a non-Lipschitz ODE, which could not be directly verified in .

In particular, we give a novel axiomatization that accounts for the interactions between non-differentiable and partially defined operators with systems of differential equations, an interaction which does not occur for ’s simpler language where all terms are smooth. More generally, example applications abound: almost every serious case study of employs these constructs in practice; we give a fully rigorous foundation to these case studies. In future work, implementing in would enable case studies to soundly employ the constructs given herein and to define their own. We expect few core changes would be needed, thanks to our use of uniform substitution, rather the challenge is to efficiently prove and track the new assumptions on existence and continuity.