Verifying Hybrid Systems with Modal Kleene Algebra

Abstract

Modal Kleene algebras have been used for building verification components for imperative programs with Isabelle/HOL. We integrate this approach with recent Isabelle components for ordinary differential equations to build two verification components for hybrid systems, where continuous phase space dynamics complement the discrete dynamics on program stores. We demonstrate their feasibility by deriving the most important domain-specific rules of differential dynamic logic and discussing four simple examples.

Appendices

A Axioms and Definitions

Semiring. A semiring is a structure $(S,+,\cdot ,0,1)$ that, for all $\alpha ,\beta ,\gamma \in S$ satisfies

$$\begin{aligned} \begin{array}{c} \alpha \cdot (\beta \cdot \gamma ) = (\alpha \cdot \beta )\cdot \gamma ,\qquad 1\cdot \alpha =\alpha ,\qquad \alpha \cdot 1=\alpha ,\\ \alpha +(\beta +\gamma )= (\alpha +\beta )+ \gamma ,\qquad \alpha +\beta =\beta +\alpha ,\qquad \alpha +0=\alpha ,\qquad 0+\alpha =\alpha ,\\ \alpha \cdot (\beta +\gamma ) = \alpha \cdot \beta +\alpha \cdot \gamma ,\qquad (\alpha +\beta )\cdot \gamma = \alpha \cdot \gamma +\beta \cdot \gamma , \\ 0\cdot \alpha =0,\qquad \alpha \cdot 0=0. \end{array} \end{aligned}$$

Dioid. A dioid is a semiring S that satisfies $\alpha +\alpha =\alpha$ for all $x\in S$.

Kleene Algebra. A Kleene algebra is a structure $(K,+,\cdot ,0,1,^*)$ such that $(K,+,\cdot ,0,1)$ is a dioid and, for all $x,y,z\in K$,

$$\begin{aligned} 1+\alpha \cdot \alpha ^*\le \alpha ^*,\qquad \gamma +\alpha \cdot \beta \le \beta \rightarrow \alpha ^*\cdot \gamma \le \beta ,\\ 1+\alpha ^*\cdot \alpha \le \alpha ^*,\qquad \gamma +\beta \cdot \alpha \le \beta \rightarrow \gamma \cdot \alpha ^*\le \beta . \end{aligned}$$

Modal Kleene Algebra. A modal Kleene algebra is a tuple $(K,+,\cdot ,0,$ $1,^*, ad , ar )$ such that $(K,+,\cdot ,0,1,^*)$ is a Kleene algebra and, for all $x,y\in K$,

$$\begin{aligned} \begin{array}{c} ad \, \alpha \cdot \alpha = 0,\qquad ad \, \alpha + ad ^2\, \alpha = 1,\qquad ad \, (\alpha \cdot \beta ) \le ad \, (\alpha \cdot ad ^2\, \beta ),\\ \alpha \cdot ( ar \, \alpha ) = 0,\qquad ar \, \alpha + ar ^2\, \alpha = 1,\qquad ar \, (\alpha \cdot \beta ) \le ar \, ( ar ^2\, \alpha \cdot \beta ),\\ ad ^2\, ( ar ^2\, \alpha )= ar ^2\, \alpha ,\qquad ar ^2\, ( ad ^2\, \alpha )= ad ^2\, \alpha . \end{array} \end{aligned}$$

Syntax of Differential Rings. $\mathcal {R}{:}{:}= 0\mid 1\mid x\mid c\mid \mathcal {R}+\mathcal {R}\mid \mathcal {R} -\mathcal {R}\mid \mathcal {R}\cdot \mathcal {R}\mid \mathcal {R}'$, where x is drawn from a set of variables and c from a set of constants.

$\varvec{\mathsf {d}\mathcal {L}}$-Style Syntax of Hybrid Programs

$$ \begin{aligned} \mathcal {C} {:}{:}= x:=e \mid x' = f \ \& \ G \mid \mathcal {C};\mathcal {C}\mid \mathbf {if}\ P\ \mathbf {then}\ \mathcal {C}\ \mathbf {else}\ \mathcal {C} \mid \mathbf {while}\ P\ \mathbf {inv}\ I\ \mathbf {do}\ \mathcal {C}, \end{aligned}$$

where x is a variable, e an expression, f a vector field expression, G a guard and P a test. However we do not work with an explicit syntax for hybrid programs in Isabelle. The entire development is within the relational flow semantics. We are only creating syntactic illusions within the semantics.

B Background on Differential Equations

Ordinary Differential Equations A system of n ordinary differential equations (ODEs) can be described by a vector field $f\in C(X,\mathbb {R}^n)$, where X is an open subset of $\mathbb {R}^{n+1}$. Its solutions are integral curves $x:I\rightarrow \mathbb {R}^n$ that is, differentiable functions that satisfy $x'\, t=f\, (t, x\, t)$, where $t\in I\subseteq \pi _1[X]$ (and $\pi _1$ is the standard first projection map). An initial value problem for this system of ODEs is specified with an initial condition $x\ t_0=x_0$ where $x_0\in X$ and $t_0\in I$.

Autonomous Systems of ODEs. The vector fields described above are time dependent. Time independent vector fields satisfy $f\in C(X,\mathbb {R}^n)$ with $X\subseteq R^n$. The system of ODEs is then called autonomous [30] and its solutions satisfy the equation $x'\ t = f\ (x\ t)$ for $t\in I\subseteq \mathbb {R}$.

Lipschitz Continuity. A function $f:V\rightarrow W$ between normed vector spaces V and W is Lipschitz continuous on $X\subseteq V$ if there is a constant $k\ge 0$ such that $||f\, x-f\, y||\le k||x-y||$ holds for all $x,y\in X$. The function f is a contraction if it is Lipschitz continuous with $k<1$.

Solutions to ODEs: Existence and Uniqueness. A Banach space is a complete normed vector space, that is, all Cauchy sequences converge. Let $B\ne \emptyset$ be a closed subset of a Banach space. Then, by Banach’s fixpoint theorem, every contraction $f:B\rightarrow B$ has a unique fixpoint. This theorem is essential for proving the Picard-Lindelöf Theorem, which guarantees unique solutions for initial value problems. We state a special case for autonomous systems of ODEs.

Theorem B.1

(Picard-Lindelöf Theorem). For every Lipschitz continuous vector field $f:X\subseteq \mathbb {R}^n\rightarrow \mathbb {R}^n$ and $x_0\in X$ there exists a unique integral curve $x\in C^1(I(x_0))$ that satisfies the initial value problem for the autonomous system $x'\ t=f\, (x\, t)$ and $x\, t_0=x_0$. $I(x_0)$ is the maximal interval of existence for x around $t_0$.

Flow of an Autonomous System of ODEs. Let $f:X\subseteq \mathbb {R}^n\rightarrow X$ be a Lipschitz continuous vector field that admits, for each $x\in X$, a unique integral curve $\phi _x\in C^1(I(x))$ such that $\phi _x\ 0=x$ by Picard-Lindelöf’s theorem. The local flow $\varphi :T\rightarrow X\rightarrow X$ for f is defined by $\varphi \ t\ x=\phi _x\ t$, where $T=\bigcap _{x\in X}I(x)$.

For $\mathbb {R}= T$, the group action equations $\varphi \ 0= id$ and $\varphi \ (s+ t) = \varphi \ s \circ \varphi \ t$ are immediately derivable from this definition. The flow is thus indeed an action of the additive group $\mathbb {R}$ on X, and hence a dynamical system.

C Cross-References to Isabelle Proofs

The following table links the results in this article with facts from the Isabelle repository. The repository contains a readme file with further instructions.

Result in article	Result in Isabelle theories
Definition of evolution statements	subsumed by
Definition of $\mathsf {Flow}$	(no uniqueness)
Proposition 5.2	subsumed by
Lemma 5.3	subsumed by
Definition of guarded evolution statement
Proposition 6.1
Lemma 6.2	subsumed by ,
Lemma 6.3	subsumed by
Definition of differential ring language	,
Lemma 7.2	implied by
Rules for solving ODEs in $\mathbb {R}^{V\cup V'}$
Differential weakening rule for $\mathbb {R}^{V\cup V'}$
Lemma 7.3
Corollary 7.5
Lemma 7.6