Predicate Transformer Semantics for Hybrid Systems

Hybrid systems combine continuous dynamics with discrete control. Their verification is receiving increasing attention as the number of computing systems controlling real-world physical systems is growing. Mathematically, hybrid system verification requires integrating continuous system dynamics, often modelled by systems of differential equations, and discrete control components into hybrid automata, hybrid programs or similar domain-specific modelling formalisms, and into analysis techniques for these. Such techniques include state space exploration, reachability or safety analyses by model checking and deductive verification with domain-specific logics [10].

One of the most prominent deductive approaches is differential dynamic logic \({\mathsf {d}}{\mathcal {L}}\) [47], an extension of dynamic logic [21] to hybrid programs for reasoning with autonomous systems of differential equations, their solutions and invariant sets. It is supported by the KeYmaera X tool [14] and has proved its worth in numerous case studies [33, 40, 47]. KeYmaera X verifies partial correctness specifications for hybrid programs using a combination of domain-specific sequent and Hilbert calculi, which itself is based on an intricate uniform substitution calculus. For pragmatic reasons, its language is restricted to differential terms of real arithmetic [14] (that of hybrid automata is usually restricted to polynomial or linear constraints [10]).

Our initial motivation for this work has been the formalisation of a \({\mathsf {d}}{\mathcal {L}}\)-style approach to hybrid program verification in the Isabelle/HOL proof assistant [28] by combining Isabelle’s mathematical components for analysis and ordinary differential equations [23, 29‐31] with verification components for modal Kleene algebras [17]. We are using a shallow embedding that, in general, encodes semantic representations of domain-specific formalisms within a host-language (deep embeddings start from syntactic representations using data types to program abstract syntax trees). This benefits not only from the well-known advantages of shallowness: more rapid developments and simpler, more adaptable components. It has also shifted our focus from encoding \({\mathsf {d}}{\mathcal {L}}\)’s complex syntactic proof system to developing denotational semantics for hybrid systems and supporting the natural style in which mathematicians, physicists or engineers reason about them—without proof-theoretic baggage. After all, we get Isabelle’s own proof system and proof methods for free, and our expressive power is only limited by its type theory and higher-order logic.

Our main contribution is an open compositional semantic framework for the deductive verification of hybrid programs in a general purpose proof assistant. In a nutshell, hybrid programs are while programs, or simply programs with control loops, in which an evolution command for the continuous system dynamics complements the standard assignment command for the discrete control. Evolution commands roughly specify vector fields (via systems of ordinary differential equations) together with guards that model boundary conditions. Here, we restrict our attention to abstract predicate transformer algebras using modal Kleene algebras [9], quantales of lattice endofunctions or quantaloids of functions between lattices [5]. They are instantiated first to intermediate relational or state transformer semantics for \({{\mathsf {d}}{\mathcal {L}}}\)-style hybrid programs, and then to concrete semantics over program stores for hybrid programs: for dynamical systems with global flows, Lipschitz continuous vector fields with local flows and continuous vector fields with multiple solutions. Another verification component is based directly on flows. This array of components demonstrates the compositionality and versatility of our framework. Figure 1 shows its basic anatomy.

Our framework benefits from compositionality and algebra in various ways. Using algebra allows us to derive most of the semantic properties needed for verification by equational reasoning, and it reduces the overhead of developing different concrete semantics to a minimum. Using modal Kleene algebras and predicate transformer algebras, in particular, makes large parts of verification condition generation equational, and thus accessible to Isabelle’s simplifiers. Compositionality of our extant framework for classical programs allows us to localise the development of concrete semantics for hybrid programs to the specification and formalisation of a semantics for evolutions commands. We only need to replace standard models of the program store by a hybrid store model. In our denotational state transformer semantics, evolution commands are interpreted as unions of all orbits of solutions of the vector field at some initial value, subject to the guards constraining the durations of evolutions. This covers situations beyond the remits of the Picard–Lindelöf theorem [22, 66] and supports general reasoning about guarded invariant sets. Ultimately, we can simply plug the predicate transformers for evolution commands into the generic algebras for while programs and their rules for verification condition generation.

Verification condition generation for evolution commands is supported by three workflows that are inspired by \({\mathsf {d}}{\mathcal {L}}\), but work differently in practice:With all three workflows, hybrid program verification is ultimately performed within the concrete semantics. But, as with classical program verification, verification condition generation eliminates all structural conditions automatically so that proof obligations are entirely about the dynamics of the hybrid program store. They can be calculated in mathematical textbook style by equational reasoning, and of course by external solvers and decision procedures for arithmetic. (Their integration, as oracles or as verified components, is very important, but left for future work.) For the introductory examples presented, we have merely formalised some simple tactics that help automating the computation of derivatives in multivariate Banach spaces or that of polynomials and transcendental functions. Yet for those who prefer \({\mathsf {d}}{\mathcal {L}}\)-style reasoning, we have formalised a rudimentary set of its inference rules that are sound relative to our semantics. Overall, unlike \({\mathsf {d}}{\mathcal {L}}\), which prescribes its domain-specific set of inference rules, we grant users the freedom of choice between various workflows and even of developing their own one within our semantic framework.

The entire framework, including the mathematical development in this article, has been formalised with Isabelle/HOL. All Isabelle components can be found in the Archive of Formal Proofs [16, 18, 25, 65]. We are currently using them to verify hybrid programs post hoc in the standard weakest liberal precondition style outlined above. Yet the approach is flexible enough to support the verification of hybrid systems using Hoare logic [11], symbolic execution with strongest postconditions, program refinement with predicate transformers in the style of Back and von Wright [5] and Morgan [11], and reasoning about hybrid program equivalences in the elegant equational style of Kleene algebra with tests [37].

While our approach is powerful enough to tackle most problems of a recent systems competition [45], the work documented in this article focuses mainly on the semantic foundations and the proof of concept that the approach works. A more user-friendly specification language, a less simplistic hybrid store model, enhanced tactics for reasoning with flows and invariants, and mathematical background theories for reasoning about affine and linear systems of differential equations have been added, while this article has been under review [12, 26]. The doctoral dissertation of the first author contains a more comprehensive description of the framework and further generalisations [27].

The remainder of this article is organised as follows: Sects. 2–6 introduce the algebras of relations, state and predicate transformers needed. Section 7 explains the shallow embedding used to formalise verification components for while programs. After recalling the basics of differential equations in Sect. 8, we introduce our semantics for evolution commands in Sects. 9–11 and explain our procedures for computing weakest liberal preconditions and reasoning with differential invariants for them. Sections 13–15 summarise the corresponding Isabelle components. Sections 12 and 16 briefly list the derivation and formalisation of semantic variants of \({\mathsf {d}}{\mathcal {L}}\) inference rules. Section 17 presents four verification examples in our framework using the main two workflows. Section 18 presents our third workflow and a brief example for it. Sections 19 and 20 discuss related work and conclude the article. A glossary of cross-references between theorems in the text and the Isabelle theories is presented in Appendix A.

This section summarises the mathematical foundations of our simplest and most developed predicate transformer algebra—modal Kleene algebra. It introduces the basics of Kleene algebras, and the state transformer model and relational model used. The relational model is standard for Kleene algebra. The state transformer model has so far received less attention and is therefore explained in detail.

A dioid \((S,+,\cdot ,0,1)\) is an additively idempotent semiring, \(\alpha +\alpha =\alpha \) holds for all \(\alpha \in S\). The underlying abelian monoid \((S,+,0)\) is therefore a semilattice with order defined by \(\alpha \le \beta \leftrightarrow \alpha +\beta =\beta \). The order is preserved by \(\cdot \) and \(+\) in both arguments; 0 is its least element.

A Kleene algebra \((K,+,\cdot ,0,1,^*)\) is a dioid expanded by the Kleene star \((-)^*:K\rightarrow K\) that satisfies the left and right unfold and induction axiomsBy these axioms, \(\alpha ^*\cdot \gamma \) is the least fixpoint of the function \(\gamma +\alpha \cdot (-)\) and \(\gamma \cdot \alpha ^*\) that of \(\gamma +(-)\cdot \alpha \), where we use − as a wildcard for function arguments. The fixpoint \(\alpha ^*\) arises as a special case. The more general induction axioms combine its definition with sup-preservation or continuity of left and right multiplication.

Opposition is an important duality of Kleene algebras: swapping the order of multiplication in any Kleene algebra yields another one. The class of Kleene algebras is therefore closed under opposition.

Kleene algebras were conceived as algebras of regular expressions. But here we interpret their elements as programs. Addition models their nondeterministic choice, multiplication their sequential composition and the Kleene star their unbounded finite iteration. The element 0 models abort; 1 models the ineffective program. Two programs are deemed equal if they lead from the same inputs to the same outputs. These intuitions are grounded in concrete program semantics.

With the relational composition of \(R\subseteq X\times Y\) and \(S\subseteq Y\times Z\) defined as \((R;S)\, x \,z\) if \(R\, x\, y\) and \(S\, y\, z\) for some \(y\in Y\), with \( Id _X\, x\, y\) if \(x=y\), and the reflexive-transitive closure of \(R\subseteq X\times X\) defined as \(R^*=\bigcup _{i\in {\mathbb {N}}} R^i\), where \(R^0= Id _X\) and \(R^{i+1}=R;R^i\), where we write \(R\, x\, y\) instead of \((x,y)\in R\), the following holds.

A relation Kleene algebra over X is thus any subalgebra of \(\mathsf {Rel}\, X\).

Opposition can be expressed in \(\mathsf {Rel}\, X\) by conversion, where the converse of relation R is defined by \(R^\smallsmile \, x\, y \leftrightarrow R\, y\, x\). It satisfies in particular \((R;S)^\smallsmile = S^\smallsmile ; R^\smallsmile \).

The isomorphism \({\mathcal {P}}\, (X\times Y) \cong ({\mathcal {P}}\, Y)^X\) between categories of relations and non-deterministic functions—so-called state transformers—yields an alternative representation. It is given by the bijections \({\mathcal {F}}:{\mathcal {P}}\, (X\times Y) \rightarrow ({\mathcal {P}}\, Y)^X\) and \({\mathcal {R}}:({\mathcal {P}}\, Y)^X\rightarrow {\mathcal {P}}(X\times Y)\) defined by \({\mathcal {F}}\, R\, x = \{y\in Y\mid R\, x\, y\}\) and by \({\mathcal {R}}\, f\, x\, y \Leftrightarrow y \in f\, x\). Following Isabelle syntax, we use juxtaposition with a space to denote function application. State transformers \(f:X\rightarrow {\mathcal {P}}\, Y\) and \(g:Y\rightarrow {\mathcal {P}}\, Z\) are composed by the (forward) Kleisli composition of the powerset monadThe function \(\eta _X = \{-\}\) is a unit of this monad. The functors \({\mathcal {F}}\) and \({\mathcal {R}}\) preserve arbitrary sups and infs, extended pointwise to state transformers, and stars \(f^{*_K}\, x = \bigcup _{i\in {\mathbb {N}}} f^{i_K}\, x\), which are defined with respect to Kleisli composition.

A state transformer Kleene algebra over X is any subalgebra of \(\mathsf {Sta}\, X\). Opposition is now expressed using the (contravariant) functor \((-)^{ op } = {\mathcal {F}}\circ (-)^\smallsmile \circ {\mathcal {R}}\) that associates \(f^{ op }:Y\rightarrow {\mathcal {P}}\, X\) with every \(f:X\rightarrow {\mathcal {P}}\, Y\).

The category \(\mathbf {Rel}\), with relations of type \(X\times Y\) or state transformers of type \(X\rightarrow {\mathcal {P}}\, Y\) as arrows, is beyond mono-type Kleene algebra.

For a more refined hierarchy of variants of Kleene algebras, their calculational properties and the most important computational models, see our formalisation in the Archive of Formal Proofs [3]. The state transformer model has been formalised with Isabelle for this article.

Kleene algebras must be extended to express conditionals or while loops more faithfully. This requires tests, which are not prima facie actions, but propositions. Assertions and correctness specifications cannot be expressed directly either.

Two standard extensions bring Kleene algebra closer to program semantics. Kleene algebra with tests [37] yields a simple algebraic semantics for while programs and a partial correctness semantics for these in terms of an algebraic propositional Hoare logic—ignoring assignments. Predicate transformer semantics, however, cannot be expressed [61]. Alternatively, Kleene algebras can be enriched by modal box and diamond operators in the style of propositional dynamic logic (\(\mathsf {PDL}\)), which yields test and assertions as well as predicate transformers. Yet once again, assignments cannot be expressed within the algebra. We outline the second approach.

An antidomain semiring [9] is a semiring S expanded by an antidomain operation \( ad :S\rightarrow S\) axiomatised byBy opposition, an antirange semiring [9] is a semiring S expanded by an antirange operation \( ar :S\rightarrow S\) axiomatised byAntidomain and antirange semirings are a fortiori dioids.

The antidomain \( ad \, \alpha \) of program \(\alpha \) models the set of those states from which \(\alpha \) cannot be executed. The operation \(d= ad ^2\) thus defines the domain of a program: the set of those states from which it can be executed. By opposition, the antirange \( ar \, \alpha \) of \(\alpha \) yields those states into which \(\alpha \) cannot be executed and \(r= ar ^2\) defines the range of \(\alpha \): those states into which it can be executed.

A modal Kleene algebra (\(\mathsf {MKA}\)) [9] is a Kleene algebra that is both an antidomain and an antirange Kleene algebra in which \(d\circ r=r\) and \(r\circ d = d\).

In a \(\mathsf {MKA}\)  K, the set \({\mathcal {P}}\, ad \, K\)—the image of K under \( ad \)—models the set of all tests or propositions. We henceforth often write \(p,q,\dots \) for its elements. Moreover, \({\mathcal {P}}\, ad \, K={\mathcal {P}}\, d\, K={\mathcal {P}}\, r\, K ={\mathcal {P}}\, ar\, K = K_d=K_r\), where \(K_f=\{\alpha \in S\mid f\, \alpha = \alpha \}\) for \(f\in \{d,r\}\). Hence, \(p\in {\mathcal {P}}\, ad \, K \leftrightarrow d\, p = p\). It follows that the class \(\mathsf {MKA}\) is closed under opposition. In addition, \(K_d\) forms a Boolean algebra with least element 0, greatest element 1, join \(+\), meet \(\cdot \) and complementation \( ad \)—the algebra of propositions, assertions or tests.

Axiomatising \(\mathsf {MKA}\) based on domain and range would lack the power to express complementation: \(K_d\) would only be a distributive lattice.

The programming intuitions for \(\mathsf {MKA}\) are once again grounded in concrete semantics.

Every subalgebra of a full relation \(\mathsf {MKA}\) is a relation \(\mathsf {MKA}\).

Similarly, \( ar = ad \circ (-)^\smallsmile \), \(d = r \circ (-)^\smallsmile \) and \(r = d\circ (-)^\smallsmile \). Furthermore,Henceforth, we often identify such relational subidentities, sets and predicates and their types via the isomorphisms \(({\mathcal {P}}\, (X\times X))_d\, \cong \, X\rightarrow {\mathbb {B}}\, \cong \, {\mathcal {P}}\, X\).

Every subalgebra of a full relation \(\mathsf {MKA}\) is a state transformer \(\mathsf {MKA}\). Similarly,These propositions generalise again beyond mono-types, but algebras of such typed relations and state transformers cannot be captured by \(\mathsf {MKA}\).

In every \(\mathsf {MKA}\), \(p\cdot \alpha \) and \(\alpha \cdot p\) model the domain and range restriction of \(\alpha \) to states satisfying p. Conditionals and while loops can thus be expressed:where we write \({\bar{p}} = ad \, p = ar \, p\). Together with sequential composition \(\alpha ; \beta = \alpha \cdot \beta \), this yields an algebraic semantics of while programs without assignments. It is grounded in the relational and the state transformer semantics. A more refined hierarchy of variants of \(\mathsf {MKA}\)s, starting from domain and antidomain semigroups, their calculational properties and the most important computational models, can be found in the Archive of Formal Proofs [16]. The state transformer model of \(\mathsf {MKA}\) has been formalised with Isabelle for this article.

\(\mathsf {MKA}\) can express the modal operators of \(\mathsf {PDL}\), both with a relational Kripke semantics and a coalgebraic state transformer semantics.This is consistent with Jónsson and Tarski’s Boolean algebras with operators [35]: Each of \(|\alpha \rangle \), \(\langle \alpha |\), \(|\alpha ]\) and \([\alpha |\) is an endofunction \(K_d\rightarrow K_d\) on the Boolean algebra \(K_d\). Yet another view of modal operators is that of predicate transformers. The function \(|-]-\) yields the weakest liberal precondition operator \( wlp \); \(\langle -|-\) the strongest postcondition operator.

The boxes and diamonds of \(\mathsf {MKA}\) are related by De Morgan duality:their dualities are captured by the adjunctions and conjugationsIn \(\mathsf {Rel}\, X\), as in standard Kripke semantics of modal logics in general, and of \(\mathsf {PDL}\) in particular,where we identify predicates and subidentity relations. For the remaining two modalities, \(\langle -|=|-\rangle \circ (-)^\smallsmile \) and \( [-|=|-]\circ (-)^\smallsmile \). Hence, \(|R\rangle P\) is the preimage of P under R and \(\langle R|P\) the image of P under R. The isomorphism between subidentities, predicates and sets also allows us to see \(|R\rangle \), \(\langle R|\), |R] and [R| as operators on the complete atomic Boolean algebra \({\mathcal {P}}\, X\), which carries algebraic structure beyond \(K_d\) that is reminiscent of a module.

In \(\mathsf {Sta}\, X\), alternatively,Moreover, \(|-\rangle = \langle -|\circ (-)^{ op }\) and \([-| = |-]\circ (-)^{ op }\). Here, \(\langle f|\) is the Kleisli extension of f for the powerset monad and \(|f\rangle \) that of the opposite function (see Sect. 6).

The isomorphism \({\mathcal {P}}\, (X\times X) \cong ({\mathcal {P}}\, X)^X\) makes the approaches coherent:and, dually, \(\langle f| = \langle {\mathcal {R}}\, f|\), \(\langle R| = \langle {\mathcal {F}}\, R|\), \([f| = [{\mathcal {R}}\, f|\) and \([R| = [{\mathcal {F}}\, R|\).

Predicate transformers are useful for specifying program correctness conditions and for verification condition generation. The identitycaptures the standard partial correctness specification for programs: if \(\alpha \) is executed from states where precondition p holds, and if it terminates, then postcondition q holds in the states where it does. Verifying it amounts to computing \(|\alpha ]q\) recursively over the program structure from q and checking that the result is greater or equal to p. Intuitively, \(|\alpha ]q\) represents the largest set of states from which one must end up in set q when executing \(\alpha \), or alternatively the weakest precondition from which postcondition q must hold when executing \(\alpha \).

Calculating \(|\alpha ]q\) for straight-line programs is completely equational, but loops require invariants. To this end, one usually adds annotations to loops,where i is the loop invariant for \(\alpha \) and calculates \( wlp \)s as follows [17, 18]. For all \(p,q,i,t\in K_d\) and \(\alpha ,\beta \in K\),In the rule (wlp-star), i is an invariant for the star as well. In addition, we support a while rule without an invariant annotation.

More generally, beyond loops, an element \(i\in K_d\) is an invariant for \(\alpha \) if it is a postfixpoint of \(|\alpha ]\) in \(K_d\):By the adjunction between boxes and diamonds, this is the case if and only if \(\langle \alpha | i \le i\); that is, i is a prefixpoint of \(\langle \alpha |\) in \(K_d\). We return to this equivalence in the context of differential invariants and invariant sets of vector fields in Sect. 11. We write \(\mathsf {Inv}\, \alpha \) for the set of invariants of \(\alpha \).

As a generalisation of the rule (wlp-while) for annotated while loops, we can derive a rule for commands annotated with tentative invariants \(\alpha \, \mathbf {inv}\ i = \alpha \). For all \(i,p,q\in K_d\) and \(\alpha \in K\),Combining (wlp-cmd) with (wlp-star) then yields, for \(\mathbf {loop}\, \alpha \, \mathbf {inv}\, i = \alpha ^*\),We use such annotated commands for reasoning about differential invariants and loops of hybrid programs below.

The modal operators of \(\mathsf {MKA}\) have, of course, a much richer algebra beyond verification condition generation. For a comprehensive list, see the Archive of Formal Proofs [16]. We have already derived the rules of propositional Hoare logic, which ignores assignments, and those for verification condition generation for symbolic execution with strongest postconditions in this setting [18]. A component for total correctness is also available. It supports refinement proofs in the style of Back and von Wright [5]. But this is beyond the scope of this article. The other two abstract predicate transformer algebras from Fig. 1 are surveyed in the following two sections.

While \(\mathsf {MKA}\) has so far been our most developed setting for verifying (hybrid) programs, our framework is compositional and supports other predicate transformer algebras as well. Two of them are outlined in this and the following section. Their Isabelle formalisation [65] is discussed in Sect. 6.

The first approach follows Back and von Wright [5] in modelling predicate transformers, or simply transformers, as functions between complete lattices. Readers not familiar with lattice theory can freely skip this section. To obtain useful laws for program construction or verification, conditions are imposed.

A function \(f:L_1\rightarrow L_2\) between two complete lattices \((L_1,\le _1)\) and \((L_2,\le _2)\) is order-preserving if \(x\le _1 y \rightarrow f\, x \le _2 f\, y\), sup-preserving if \(f \circ \bigsqcup = \bigsqcup \mathop {\circ } {\mathcal {P}}\, f\) and inf-preserving if \(f \circ \sqcap = \sqcap \mathop {\circ } {\mathcal {P}}\, f\). All sup- or inf-preserving functions are order-preserving.

We write \({\mathcal {T}}(L)\) for the set of transformers over the complete lattice L, and \({\mathcal {T}}_\le (L)\), \({\mathcal {T}}_{\sqcup }(L)\), \({\mathcal {T}}_{\sqcap }(L)\) for the subsets of order-, sup- and inf-preserving transformers. Obviously, \({\mathcal {T}}_{\sqcap }(L)={\mathcal {T}}_{\sqcup }(L^ op )\). The following fact is well known [5, 15].

Infs, least and greatest elements can then be defined from sups on \(L^X\) as usual. Function spaces \(L^L\), in particular, form monoids with respect to function composition \(\circ \) and \( id _L\). In addition, \(\circ \) preserves sups and infs in its first argument, but not necessarily in its second one. Algebraically, this is captured as follows.

A near-quantale \((Q,\le ,\cdot )\) is a complete lattice \((Q,\le )\) with an associative composition \(\cdot \) that preserves sups in its first argument. It is unital if composition has a unit 1. A prequantale is a near-quantale in which composition is order-preserving in its second argument. A quantale is a near quantale in which composition preserves sups in its second argument. See [56] for more information about quantales.

Transformers for while loops are obtained by connecting quantales with Kleene algebras. This requires fixpoints of \(\varphi _{\alpha \gamma }= \gamma \sqcup \alpha \cdot (-)\) and \(\varphi _\alpha =1\sqcup \alpha \cdot (-)\) as well as the Kleene star \(\alpha ^*=\bigsqcup _{i\in {\mathbb {N}}}\alpha ^i\). A left Kleene algebra is a dioid in which \(\varphi \) has a least fixpoint that satisfies \( lfp \, \varphi _{\alpha \gamma } = lfp \, \varphi _\alpha \cdot \gamma \). Hence, \(\varphi _\alpha \) satisfies the left unfold and left induction axioms \(1\sqcup \alpha \cdot \varphi _\alpha \le \varphi _\alpha \) and \(\gamma \sqcup \alpha \cdot \beta \le \beta \rightarrow \varphi _\alpha \cdot \gamma \le \beta \). By opposition, a right Kleene algebra is a dioid in which the least fixpoint of a dual function \(1\sqcup (-)\cdot \alpha \) satisfies the right unfold and right induction axioms.

The proofs of (1) and (3) use sup-preservation and Kleene’s fixpoint theorem. That of (2) uses the Knaster–Tarski fixpoint theorem to show that \(\varphi _{\alpha \gamma }\) has a least fixpoint, and fixpoint fusion [44] to derive \( lfp \, \varphi _{\alpha \gamma } = lfp \, \varphi _\alpha \cdot \gamma \), which yields the left Kleene algebra axioms. In prequantales, \( lfp \, \varphi _\alpha \cdot \gamma \le \alpha ^*\cdot \gamma \); equality generally requires sup-preservation in the first argument of composition.

The fixpoint and iteration laws on functions spaces, which follow from Propositions 5.3 and 5.2, still need to be translated into laws for transformers operating on the underlying lattice. This is achieved again by fixpoint fusion [5]. In \({\mathcal {T}}_\le (L)\),and \( lfp \) preserves isotonicity. In \({\mathcal {T}}_\sqcup (L)\), moreover,\( id _L\sqcup f\circ f^*= f^*=f^*\circ f \sqcup id _L\) and \((-)^*\) preserves sups. All results dualise to inf-preserving transformers.

Relative to \(\mathsf {MKA}\), backward diamonds correspond to sup-preserving forward transformers and forward boxes to inf-preserving backward transformers in the opposite quantale, where the lattice has been dualised and the order of composition been swapped. An analogous correspondence holds for forward diamonds and backward boxes. Sup- and inf-preserving transformers over complete lattices are less general than \(\mathsf {MKA}\) in that preservation of arbitrary sups or infs is required, whereas that of \(\mathsf {MKA}\) is restricted to finite sups and infs. Isotone transformers, however, are more general, as not even finite sups or infs need to be preserved, and finite sup- or inf-preservation implies order preservation.

We are mainly using the \( wlp \) operator for verification condition generation and hence briefly outline \( wlp \)s for conditionals and loops in this setting. We assume that the underlying lattice L is a complete Boolean algebra, that is, a complete lattice as well as a complemented distributive lattice. We can then lift elements of L to \( wlp \)s as \(|p]q= p \rightarrow q\) and define, in \({\mathcal {T}}_\le (L^ op )\),In \({\mathcal {T}}_\sqcap (L)\), we even obtainThese equations allow generating verification conditions as with (wlp-cond) and (wlp-while) from Sect. 4. Overall, our Isabelle components for lattice-based predicate transformers in the Archive of Formal Proofs [65] contain essentially the same equations and rules for verification condition generation as those for \(\mathsf {MKA}\).

We have so far restricted the approach to endofunctions on a complete lattice to relate it to \(\mathsf {MKA}\). Yet it generalises to functions in \(L_2^{L_1}\) and hence to categories [5]. The corresponding poly-typed generalisations of quantales are known as quantaloids [55]. In particular, composition is then a partial operation.

A second, more coalgebraic approach to predicate transformers starts from monads [41]. In addition, it details the relational and state transformer semantics of \(\mathsf {MKA}\) in a more modern algebraic approach. We need to assume basic knowledge of categories and monads. Once again, readers unfamiliar with these concepts can freely skip it.

Recall that \(({\mathcal {P}},\eta _X,\mu _X)\), for \({\mathcal {P}}:\mathbf {Set}\rightarrow \mathbf {Set}\), \(\eta _X:X\rightarrow {\mathcal {P}}\, X\) defined by \(\eta _X= \{-\}\) and \(\mu _X:{\mathcal {P}}^2\, X\rightarrow {\mathcal {P}}\, X\) defined by \(\mu _X = \bigcup \) is the monad of the powerset functor in the category \(\mathbf {Set}\) of sets and functions. The morphisms \(\eta \) and \(\mu \) are natural transformations. They satisfy, for every \(f:X\rightarrow Y\),From the monadic point of view, state transformers \(X\rightarrow {\mathcal {P}}\, Y\) are arrows \(X\rightarrow Y\) in the Kleisli category \(\mathbf {Set}_{\mathcal {P}}\) of \({\mathcal {P}}\) over \(\mathbf {Set}\). They are composed by (forward) Kleisli composition \(f\circ _K g = \mu \circ {\mathcal {P}}\, g\circ f\) as explained before Proposition 2.2 in Sect. 2. The category \(\mathbf {Set}_{\mathcal {P}}\) is known to be isomorphic to \(\mathbf {Rel}\), the category of sets and binary relations.

The isomorphism between state and forward predicate transformers is based on the contravariant functor \((-)^\dagger :\mathbf {Set}_{\mathcal {P}}(X,{\mathcal {P}}\, Y)\rightarrow \mathbf {Set}_{\mathcal {P}}({\mathcal {P}}\, X,{\mathcal {P}}\, Y)\)—the Kleisli extension. Its definition \(f^\dagger = \mu \circ {\mathcal {P}}\, f\) implies that \((-)^\dagger =\langle - |\) on morphisms, which is the strongest postcondition operator.

The structure of state spaces—Boolean algebras for \(\mathsf {MKA}\), complete lattices in Back and von Wright’s approach—is captured by the Eilenberg–Moore algebras of the powerset monad. It is well known that \((-)^\dagger \) embeds \(\mathbf {Set}_{\mathcal {P}}\) into their category. Its objects are complete (sup-semi)lattices; its morphisms sup-preserving functions, hence transformers. More precisely, \((-)^\dagger \) embeds into powerset algebras, complete atomic Boolean algebras that are the free objects in this category.

The isomorphism \(\mathbf {Set}_{\mathcal {P}}(X, {\mathcal {P}}\, Y)\cong \mathbf {Set}^\sqcup ({\mathcal {P}}\, X,{\mathcal {P}}\, Y)\) between state transformers and sup-preserving predicate transformers then arises as follows. The embedding \(\langle -|\) has an injective inverse \(\langle -|^{-1}\) on the subcategory of sup-preserving transformers. It is defined by \(\langle -|^{-1} = (-)\circ \eta \), which can be spelled out as \(\langle \varphi |^{-1}\, x = \{y\mid y \in \varphi \, \{x\}\}\). The isomorphism preserves the quantaloid structures of state and predicate transformers that is, compositions (contravariantly), units and sups, hence least elements, but not necessarily infs and greatest elements. These results extend to \(\mathbf {Set}^\sqcup ({\mathcal {P}}\, X,{\mathcal {P}}\, Y) \cong \mathbf {Rel}(X, Y)\) via \(\mathbf {Set}_{\mathcal {P}}\cong \mathbf {Rel}\). In addition, predicate transformers \(\langle f|: {\mathcal {P}}\, X\rightarrow {\mathcal {P}}\, Y\) preserve of course sups in powerset lattices, hence least elements, but not necessarily infs and greatest elements.

Forward boxes or \( wlp \hbox {s}\) can be obtained from state transformers via a (covariant) functor \(|-]:\mathbf {Set}_{\mathcal {P}}(X,{\mathcal {P}}\, Y)\rightarrow \mathbf {Set}({\mathcal {P}}\, Y,{\mathcal {P}}\, X)\), embedding Kleisli arrows into the opposite of the category of Eilenberg–Moore algebras formed by complete (inf-semi)lattices and inf-preserving functions. It is defined on morphisms as \(|-]=\partial _F\circ \langle - |\circ (-)^{ op }\), where \(\partial _F\, f = \partial \circ f \circ \partial \) and \(\partial \) dualises the lattice. Unfolding definitions, once again \(|f]\, P=\{x\mid f\, x\subseteq P\}\).

Furthermore, its inverse \(|-]^{-1}\) on the subcategory of inf-preserving transformers is \(|\varphi ]^{-1}\, x = \bigcap \{P\mid x \in \varphi \, P\}\). The duality \(\mathbf {Set}_{\mathcal {P}}(X,{\mathcal {P}}\, Y)\cong \mathbf {Set}^\sqcap ({\mathcal {P}}\, Y,{\mathcal {P}}\, X)\) reverses Kleisli arrows and preserves the quantaloid structures up to lattice duality, mapping sups to infs and vice versa. It extends to relations as before. In addition, predicate transformers |f] preserve of course infs of powerset lattices, hence greatest elements, but not necessarily sups and least elements.

The remaining transformers \(|-\rangle \) and \([-|\) and their inverses arise from \(\langle -|\) and \(|-]\) by opposition: \(|-\rangle = \langle -| \circ (-)^ op \), \(|-\rangle ^{-1} = (-)^ op \circ \langle -|^{-1}\), \([-|= |-] \circ (-)^ op \) and \([-|^{-1} = (-)^ op \circ |-]^{-1}\). Taken together, the four modal operators satisfy the laws of the \(\mathsf {MKA}\) modalities outlined in Sect. 4 and those of the abstract sup/inf-preserving transformers discussed in Sect. 5. They give in fact semantics to the algebraic developments, when restricted to mono-types, and once again yield the same rules for verification condition in the state transformer and the relational semantics, albeit in a more general categorical setting.

The categorical approach to predicate transformers outlined is not new, apart perhaps from the emphasis on quantales and quantaloids. The emphasis on monads is due at least to Manes [43]. More recently, Jacob’s work on state-and-effect triangles [32] has explored similar connections and their generalisation beyond sequential programs. A formalisation with Isabelle, which is further discussed in Sect. 13, is a contribution of this article.

Two important ingredients for concrete program semantics and verification condition generation are still missing: a mathematical model of the program store and program assignments, and rules for calculating \( wlp \hbox {s}\) for these basic commands. To prepare for hybrid programs (see Sect. 9 for a syntax), we model stores and assignments as discrete dynamical systems over state spaces.

Formally, a dynamical system [4, 66] is an action of a monoid \((M,\star ,u)\) on a set or state space S, that is, a monoid morphism \(\varphi :M\rightarrow S\rightarrow S\) into the transformation monoid \((S^S,\circ , id _S)\) on \(S^S\). Thus, by definition,The first action axiom captures the inherent determinism of dynamical systems. Conversely, each transformation monoid \((S^S,\circ , id _S)\) determines a monoid action in which the action \(\varphi :S^S\rightarrow S\rightarrow S\) is function application.

States of simple while programs can be modelled simply as maps \(s:V\rightarrow E\) from program variables in V to values in E. State spaces for such discrete dynamical systems are function spaces \(S=E^V\).

An update function \(f_a:V\rightarrow (S \rightarrow E) \rightarrow S\rightarrow S\) for assignment commands can be defined aswhere \(f[a\mapsto b]\) updates \(f:A\rightarrow B\) by associating \(a\in A\) with b and every \(y\ne a\) with \(f\, y\). The “expression” \({e:S\rightarrow E}\) is evaluated in state s to \(e\, s\). The maps \(f_a\, v\, e\) generate a transformation monoid, hence a monoid action \(S^S\rightarrow S \rightarrow S\) on \(S^S\). They also connect the concrete program store semantics with the \( wlp \) semantics used for verification condition generation.

We lift \(f_a\, v\, e:S\rightarrow S\) to a state transformer \(v:=_{\mathcal {F}} e:S \rightarrow {\mathcal {P}}\, S\) asthus creating a semantic illusion for syntactic assignment commands in the \(\mathsf {MKA}\)  \(\mathsf {Sta}\, S\). For \(\mathsf {Rel}\, S\), the isomorphism between \(\mathbf {Set}_{\mathcal {P}}\) and \(\mathbf {Rel}\) yieldshence \((v :=_{\mathcal {R}} e) = \{(s,f_a\, v\, e\, s)\mid s\in E^V\}=\{(s,s[v\mapsto e\, s])\mid s\in E^V\}\). Alternatively, we could have defined the state transformer semantics from the relational one via \((v :=_{\mathcal {F}} e) = {\mathcal {F}}\, (v:=_{\mathcal {R}} e)\).

The \( wlp \hbox {s}\) for assignment commands in \(\mathsf {Rel}\, S\) and \(\mathsf {Sta}\, S\) are of course the same. Hence, we drop the indices \({\mathcal {F}}\) and \({\mathcal {R}}\) and writeAdding the \( wlp \) law for assignments in either semantics to the algebraic ones for the program structure suffices to generate data-level verification conditions for while programs.

The approach outlined so far is suited for building verification components via shallow embeddings with proof assistants such as Isabelle. The predicate transformer algebras of the previous sections, as shown in the first row of Fig. 1, can all be instantiated to intermediate state transformer and relational semantics, as shown in Propositions 3.1 and 3.2 for \(\mathsf {MKA}\). These form the second row in Fig. 1. Each of these can be instantiated further to concrete semantics with predicate transformers for assignments, as described in this section.

In Isabelle, these instantiations are enabled by type polymorphism. If modal Kleene algebras have type , then the intermediate semantics have the type of relations or state transformers over , and Propositions 3.1 and 3.2 can be formalised, so that all facts known for \(\mathsf {MKA}\) are available in the intermediate semantics. The concrete semantics then require another simple instantiation of the types of relations or state transformers to those of program stores. All facts known for \(\mathsf {MKA}\) and the two intermediate semantics are then available in the concrete predicate transformer semantics for while programs. A particularity of the semantic approach and the shallow embedding is that assignment semantics are based on function updates instead of substitutions—see the rule (wlp-asgn)—so that an explicit substitution calculus like that of \({\mathsf {d}}{\mathcal {L}}\) is not needed. We can simply rely on that of Isabelle/HOL.

The use of algebra and the modularity of the shallow semantics simplify the construction of program verification components [18] considerably. The overall approach discussed has been developed initially for Hoare logics in [2]. It has been extended to predicate transformer semantics based on \(\mathsf {MKA}\) in [17].

Before developing relational and state transformer models for the basic evolution commands of hybrid programs in the next section, we briefly review some basic facts about continuous dynamical systems and ordinary differential equations.

Continuous dynamical systems \(\varphi :T\rightarrow S\rightarrow S\) are flows, which often represent solutions to systems of ordinary differential equations (ODEs) [4, 22, 66]. They are called continuous because T, which models time, is assumed to form a non-discrete submonoid of \(({\mathbb {R}},+,0)\), and the state space or phase space S is usually a manifold with topological structure. By definition, flows are monoid actions. Hence, \(\varphi \) satisfies, for all \(t_1,t_2\in T\),We always assume that T is an open interval in \({\mathbb {R}}\) and S an open subset of \({\mathbb {R}}^n\). Beyond that, one usually assumes that actions are compatible with the structure on S. As S is a manifold, we assume that flows are continuously differentiable.

The trajectory of \(\varphi \) through state \(s\in S\) is the function \(\varphi _s:T \rightarrow S\) defined by \(\varphi _s = \lambda t.\ \varphi \, t\, s\), that is, \(\varphi _s\, t=\varphi \, t\, s\). It describes the system’s evolution in time passing through state s.

The orbit of s is the set of all states on the trajectory passing through s, but not necessarily starting in this state. We model it as the function \(\gamma ^\varphi :S\rightarrow {\mathcal {P}}\, S\) defined bythe canonical map sending each \(s\in S\) to its equivalence class \(\gamma ^\varphi \, s\). Orbit functions are state transformers, as their type indicates. They form our basic semantics for evolution commands and hybrid programs.

Flows arise from ODEs as follows. In a system of ODEseach \(f_i\) is a continuous real-valued function and \(t\in T\subseteq {\mathbb {R}}\). Any such system can be made time-independent—or autonomous—by adding the equation \(x_0'\, t=1\). We henceforth restrict our attention to autonomous systems and writeThe continuous function \(f:S\rightarrow S\) on \(S\subseteq {\mathbb {R}}^n\) is a vector field. It assigns a vector to each point in S.

An autonomous system of ODEs is thus simply a vector field f, and a solution a continuously differentiable function \(X:T\rightarrow S\) that satisfies \(X'\, t=f\, (X\,t)\) for all \(t\in T\), or more briefly \(X'=f\circ X\).

An initial value problem (IVP) is a pair (f, s) of a vector field f and an initial value \((0,s)\in T\times S\) [22, 66], where \(t_0=0\) and s represent the initial time and initial state of the system. A solution to the IVP (f, s) satisfiesIf solutions X to an IVP (f, s) are unique and \(T={\mathbb {R}}\), then it is easy to show that \(X = \varphi ^f_s\) is the trajectory of the flow \(\varphi ^f\) through s.

Geometrically, \(\varphi _s^f\) is the unique curve in S that is parametrised by t, passes through s and is tangential to f at any point. As trajectories arise from integrating both sides of \((\varphi _s^f)'=f\circ \varphi _s^f\), they are also called integral curves. We henceforth write \(\varphi _s\) when the dependency on f is clear.

The following example provides some physical intuition for readers unfamiliar with these concepts.

It is well known that not all IVPs admit flows: not all of them have unique solutions, and in many situations, flows exist locally on a subset of \({\mathbb {R}}\) that does not form a submonoid. Peano’s theorem guarantees the local existence of solutions for systems of ODEs whose associated vector field is continuous. Conditions for local existence and uniqueness are provided by the Picard–Lindelöf theorem [22, 66], which we briefly discuss, as we use it for our first workflow.

By the fundamental theorem of calculus, any solution to an IVP must satisfyIt can be shown that this equation holds if, for \(X\, 0= s\), the functionhas a fixpoint. This, in turn, is the case if the limit X of the sequence \((h^n)_{n\in {\mathbb {N}}}\), defined by \(h^0\, x\, t= s\) and \(h^{n+1}= h\circ h^n\), exists. Indeed, with this assumption,using continuity of addition, integration and f in the second step. Finally, existence of the limit of \((h^n)_{n\in {\mathbb {N}}}\) is guaranteed by constraining the domain of the \(h^n\), and by Banach’s fixpoint theorem, there must be a Lipschitz constant \(\ell \ge 0\) such thatfor any \(s_1,s_2\in S\), where \(\Vert -\Vert \) is the Euclidean norm on \({\mathbb {R}}^n\). Vector fields satisfying this condition are called Lipschitz continuous.

The Picard–Lindelöf theorem makes it possible to patch together intervals \(T_s\) to a set \(U=\bigcup _{s \in S} T_s \times \{s\}\subseteq {\mathbb {R}}\times S\), from which a largest interval of existence \(T=\bigcup _{s\in S} T_s\) can be extracted. One can then define a local flow \(\varphi :T\rightarrow S\rightarrow S\) such that \(\varphi _s\, t\) is the maximal integral curve at s. The monoid action identities \(\varphi \, 0 = id \) and \(\varphi \, (t_1+t_2)\, s = \varphi \, t_1 (\varphi \, t_2\, s)\) can thus be shown for all \(t_2,t_1+t_2\in T_s\) [66], but U need not be closed under addition. The Picard–Lindelöf theorem, in the form presented, thus provides sufficient conditions for the existence and uniqueness of local flows for autonomous systems of ODEs. Flows are global and hence monoid actions if T is equal to \({\mathbb {R}}\) or its nonnegative or non-positive subset.

Hybrid systems often deal with dynamical systems where \(T=T_s= {\mathbb {R}}\) for any \(s\in S\) and S is isomorphic to \({\mathbb {R}}^n\) for some \(n\in {\mathbb {N}}\). Our approach supports local flows with \(T\subset {\mathbb {R}}\) and \(S\subset {\mathbb {R}}^n\) as well, and even IVPs with multiple solutions beyond the realm of Picard–Lindelöf.

Simple hybrid programs of \({\mathsf {d}}{\mathcal {L}}\) [47] are defined by the syntaxwhich adds evolution commands \( x' = f \ \& \ G\) to the program syntax of dynamic logic. Intuitively, evolution commands introduce a vector field f for an autonomous system of ODEs and a guard G, which models boundary conditions or similar constraints that restrict temporal evolutions. Guards are also known as evolution domain restrictions or invariants in the hybrid automata literature [10], but henceforth we consistently refer to them as “guards”. Nondeterministic choice and finite iteration can be adapted for modelling conditionals and while loops as with \(\mathsf {MKA}\) or predicate transformer semantics.

We are only interested in the semantics of hybrid programs. Relative to the semantics of standard while programs, it thus remains to define the \( wlp \hbox {s}\) for evolution commands. This requires relational and state transformer semantics for evolution commands over hybrid program stores. In this section, we describe our first workflow that certifies solutions using the Picard–Lindelöf theorem. We thus assume that vector fields are Lipschitz continuous, such that the Picard–Lindelöf theorem guarantees at least local flows. This is more general than needed for dynamical systems. A further generalisation to continuous vector fields is presented in the next section in preparation for our second, more powerful workflow.

We begin with hybrid program stores for \({\mathsf {d}}{\mathcal {L}}\) [46]. These are maps \(s:V\rightarrow {\mathbb {R}}\) that assign real numbers to program variables in V. Variables may appear both in differential equations and the discrete control of a hybrid system. One usually assumes that \(|V|=n\) for some \(n\in {\mathbb {N}}\), which makes \({\mathbb {R}}^V\) isomorphic to the vector space \({\mathbb {R}}^n\). The results from Sect. 8 then apply to any state space \(S\subseteq {\mathbb {R}}^V\).

Next, we describe a state transformer semantics and a \({\mathsf {d}}{\mathcal {L}}\)-style relational semantics of evolution commands with Lipschitz continuous vector fields. Intuitively, the semantics of \( x' = f \, \& \, G\) in state \(s\in S\subseteq {\mathbb {R}}^V\) is the longest segment of the trajectory \(\varphi ^f_s\) at s along which all points satisfy G.

For the remainder of this section, we fix a Lipschitz continuous vector field \(f:S\rightarrow S\) and a guard \(G:S\rightarrow {\mathbb {B}}\), for \(S\subseteq {\mathbb {R}}^V\). We freely consider G, and any other function of that type, as a set or a predicate. As explained in Sect. 8, there is a (local) flow \(\varphi :T\rightarrow S\rightarrow S\) defined on a maximal interval \(T\subseteq {\mathbb {R}}\) with \(0\in T\). Thus, we can pick any interval \(U\subseteq T\) with \(0 \in U\) to compute wlps over subintervals of the interval of existence T. In examples, we typically use the subinterval [0, t], from the time at which the system dynamics starts to a maximal time t of interest, or the subinterval \({\mathbb {R}}_+\), the set of nonnegative real numbers.

For each \(t\in U\), let \({\downarrow } t= \{t'\in U \mid t' \le t\}\). The G-guarded orbit on U at \(s\in S\) is then defined as \(\gamma ^\varphi _{G,U}:S\rightarrow {\mathcal {P}}\, S\) byIntuitively, \(\gamma ^\varphi _{G,U}\, s\) is the orbit at s defined along the longest interval of time in U that satisfies guard G. This intuition is more apparent in the following lemma.

We have not formalised (1) with Isabelle because reasoning with partial functions may be tedious. As a special case, for \(U=T_+\), any subinterval of \({\mathbb {R}}_+\),We can now define the state transformer semantics of \( x'= f\, \& \, G\) simply asHence, the denotation of an evolution command in state s is the guarded orbit at s in time interval U. Alternatively, in \(\mathsf {Rel}\, S\),like in Sect. 7. Restricting this further to \(U={\mathbb {R}}_+\) yields the standard semantics of evolution commands of \({\mathsf {d}}{\mathcal {L}}\).

It remains to derive the \( wlp \)s for evolution commands. These are the same in \(\mathsf {Rel}\, S\) and \(\mathsf {Sta}\, S\), so we drop \({\mathcal {F}}\) and \({\mathcal {R}}\).

By Lemma 9.1, alternatively,For verification condition generation, the following variant is most useful.

In particular, for \(T={\mathbb {R}}\) and \(U={\mathbb {R}}_+\),Accordingly, and consistently with \({\mathsf {d}}{\mathcal {L}}\), Q is no longer a postcondition in the traditional sense: by definition, it is supposed to hold along the trajectory and therefore on any orbit at any particular initial condition s guarded by G.

For a more categorical view on the \( wlp \) of evolution commands, remember from Sect. 6 that \( \langle (x'=f\, \& \, G)_U| = (\gamma ^\varphi _{G,U})^\dagger \), where \((-)^\dagger \) is the Kleisli extension map, and that the \( wlp \) of \( (x'=f\, \& \, G)_U\) is its right adjoint. It therefore satisfiesThe identity in Proposition 9.2 can then be calculated from there.

The \( wlp \) laws in Proposition 9.2 and Lemma 9.3 complete the laws for verification condition generation for hybrid programs in the relational and state transformer semantics. In practice, Proposition 9.2, Lemma 9.3 and the Picard–Lindelöf theorem support our first workflow for computing the \( wlp \) of an evolution command \( x'=f\, \& \, G\) on a set U for a Lipschitz continuous vector field: In practice, computer algebra tools are helpful for finding flows. Their integration into proof assistants for this purpose is routine and therefore not pursued in this article. The existence of unique solutions can be guaranteed uniformly, for instance, for affine or linear systems of ordinary differential equations. See [26] for the formalisation of such an approach with Isabelle.

The following classical example illustrates our algebraic approach and gives a first glimpse of the mathematics involved. It should be noted that we are not embellishing our natural semantical notation with any façade program syntax in this article; see [12] for such an extension. A formal verification with Isabelle can be found in Example 17.1.

Certifying solutions of systems of ODEs can be tedious and hard to automate, and many ODEs do not admit analytic solutions. It is possible to circumvent these obstacles to practical verification applications in various ways. One approach, using invariant sets for systems of ODEs, is pursued by \({\mathsf {d}}{\mathcal {L}}\) and described in the following sections. It constitutes the second workflow supported by our framework. Another approach aims at particular types of vector fields for which (global) flows always exist and are easy to compute. A classical example is linear systems of ODEs [22, 66], for which the first author has already developed methods in a successor article [26]. A final approach abandons differential equations and vector fields altogether and starts from flows—as known from hybrid automata [10]. This requires changing the syntax of hybrid programs. The approach is outlined in Sect. 18. It constitutes the third workflow supported by our framework.

As the semantic approach to evolution commands developed in the previous section depends mainly on orbits, which are nothing but sets of states, it can be generalised beyond trajectories and flows. In this section, we drop the requirement of uniqueness of solutions to IVPs and hence assume that vector fields are merely continuous. In fact, if vector fields are non-continuous, the set of solutions defined below will simply be empty. We therefore generalise the definitions in the previous section to obtain weakest liberal preconditions for evolution commands that do not admit unique solutions, for instance, IVPs of the form \(x'\, t=k\sqrt{x\, t}\) with \(x\, 0=0\) for any \(k\in {\mathbb {R}}\) [24]. Our second workflow using invariant sets is based on this generalisation.

Consider the IVP (f, s) for continuous vector field \(f:S\rightarrow S\) and initial state \(s\in S\subseteq {\mathbb {R}}^V\). Letdenote its set of solutions on \(T\subseteq {\mathbb {R}}\) with \(0\in T\). Here, T is no longer the maximal interval of existence defined by the Picard–Lindelöf theorem; it can be changed like the set U in the previous section. Then, each solution X is still continuously differentiable and thus \(f\circ X\) integrable in T.

For all \(X\in {\mathsf {Sols}}\, f\, T\, s\) and \(G:S\rightarrow {\mathbb {B}}\), we define the G-guarded orbit of X along T in s via the function \(\gamma ^X_G:S\rightarrow {\mathcal {P}}\, S\) aswhich simplifies to \(\gamma ^X_{G}\, s= \{X\, t\mid t\in T\wedge \forall \tau \in {\downarrow }t.\ G\, (X\, \tau )\}\). By Kneser’s theorem [36], when non-uniqueness occurs at some point, infinitely many solutions exist for it. Thus, we define the G-guarded orbital of f along T in s via the function \(\gamma ^f_G:S\rightarrow {\mathcal {P}}\, S\) asWe thus patch the guarded orbit of each solution to the associated IVP together so that \(\gamma ^f_G\ s\) represents all possible evolutions in time that pass through s. This is evident from the following result.

If \(G=\top \), the constantly true predicate on S or the set S itself, we simply write \(\gamma ^f\) instead of \(\gamma ^f_\top \).

The state transformer semantics of the evolution command for a continuous vector field f can then be defined asThe corresponding relational semantics isOnce again, \( \langle x'= f\, \& \, G| = (\gamma ^f_G)^\dagger \). This leads to a \( wlp \) for evolution commands.

This identity can be rewritten, for predicates, asWhether this fact is useful for verification applications, as outlined above, remains to be seen. Yet the next section shows that it is certainly useful for reasoning with invariant sets. The following corollary is important for verification proofs with invariants as well.

In \({\mathsf {d}}{\mathcal {L}}\), differential invariants are predicates I that satisfy \( I\le |{x'=f\ \& \ G}] I\) [46]. In the terminology of Sect. 4, they are simply invariants for evolution commands. They play a crucial role in \({\mathsf {d}}{\mathcal {L}}\) and KeYmaera X because of the limited support for solving ODEs and their greater generality.

In dynamical systems theory, when all guards are \(\top \) and global flows exist, and in (semi)group theory, invariant sets for actions or flows \(\varphi :T\rightarrow S\rightarrow S\) are sets \(I\subseteq S\) satisfying \(\gamma ^\varphi \, s\subseteq I\) for all \(s\in I\) [66]. Based on the results from Sect. 10, we generalise both notions uniformly.

A predicate or set \(I:S\rightarrow {\mathbb {B}}\) is an invariant of the continuous vector field \(f:S\rightarrow S\) and guard \(G:S\rightarrow {\mathbb {B}}\) along \(T\subseteq {\mathbb {R}}\) ifNote that the parameter T is hidden in the definition of \(\gamma ^f_G\). For \(G=\top \), when \((\gamma ^f)^\dagger \, I\subseteq I\), we call I simply an invariant of f along T.

The following proposition yields a structural insight in the relationship between invariant sets of dynamical systems and differential invariants of \({\mathsf {d}}{\mathcal {L}}\) in terms of an adjunction.

For our \( wlp \)-calculus, condition (3) is of course most useful. Yet instead of checking that a flow is a solution to a vector field, as previously, we now need to check whether a predicate is an invariant—without having to solve the system of ODEs. This may in some case be a condicio sine qua non and in others a considerable simplification of reasoning. The following lemmas lead to our second workflow. We show some proofs although they have been formalised with Isabelle, as they explain why the approach works.

First, towards Corollary 11.4, we may ignore guards when checking for invariants and we can use a simple second-order formula.

Second, we can recurse over predicates as follows.

Proposition 10.3, the properties in this section—in particular Lemma 11.3—and Lemma 4.1 about invariants that are conjunctions or disjunctions support our second workflow for proving a correctness specification \( P\le |x' = f\, \& \, G]Q\). For \(G=\top \) and Lipschitz continuous vector fields, the notions of invariant can be strengthened.

The identities (2) and (3) hold because \(0\in T\).

Next, we revisit the bouncing ball example from Sect. 9 to illustrate our second work flow that reasons with differential invariants. Once again, we give detailed mathematical calculations to indicate the kind of mathematical reasoning involved. A verification with Isabelle, which is much more automatic, can be found in Example 17.2.

This example shows that one can reason about invariants of evolution commands in a natural mathematical style as it can be found in textbooks on differential equations [4, 22, 66]. By contrast, \({\mathsf {d}}{\mathcal {L}}\) relies on syntactic substitution-based reasoning in the term algebra of differential rings [46] to check invariants, and complex domain-specific inference rules to manipulate them. The following section shows that we can derive semantic variants of most of the \({\mathsf {d}}{\mathcal {L}}\) inference rules for those who like this style of reasoning, see [12] for a complete list.

Next, we briefly specialise our approach to \({\mathsf {d}}{\mathcal {L}}\)-invariants, the invariants sets used in dynamical systems theory and those in (semi)group theory. We assume a setting where global flows exist and indices U can be dropped.

It remains to point out that the difference between the definition of invariant sets for dynamical systems and that for (semi)group actions is merely notational: In group theory, an invariant set I of a (semi)group action \(\varphi :T\rightarrow S\rightarrow S\) satisfies \(T\cdot I\subseteq I\), where \(T\cdot I= \{\varphi \, t\, s \mid t\in T\wedge s\in I\}\). In the presence of a unit, therefore \(T\cdot I = I\). Yet of course \((\gamma ^\varphi )^\dagger \, I = \{\varphi \, t\, s \mid t\in T\wedge s\in I\}\) as well.

At the end of this section, we summarise the two main workflows presented. Both use the standard laws for predicate transformer algebras for automating verification condition generation with respect to the structural part of hybrid programs. For straight-line programs, this requires only equational reasoning and can be dealt with by Isabelle’s simplifiers. The remaining verification conditions for basic commands—evolution and assignment commands—are generated by equational reasoning in the concrete semantics of the hybrid program store. In fact, only this concrete semantics had to be added to a standard Isabelle verification component to make our verification components work.

The verification conditions generated are then at the level of reasoning with functions over \({\mathbb {R}}^n\), and in some cases in linear algebra [26]. At this level, by contrast with \({\mathsf {d}}{\mathcal {L}}\), we do not require any domain-specific inference rules and can rely on Isabelle’s support for semantic reason about the hybrid dynamics within its higher-order logic, an approach that has allowed us to verify a large number of benchmark examples [45]. Yet our approach is versatile enough to derive inference rules in the style of \({\mathsf {d}}{\mathcal {L}}\), as the following section shows.

As a proof of concept, we derive semantic variants of some axioms and inference rules of \({\mathsf {d}}{\mathcal {L}}\), thus proving their soundness with respect to our semantics. The first one introduces solutions of IVPs with constant vector fields [6]. It is a trivial instance of Proposition 9.2 with \(f = \lambda s.\ c\) for some \(c\in {\mathbb {R}}\). Such vector fields are Lipschitz continuous; their flows are \(\varphi \, t\, s = s + ct\). Hence,For a second \({\mathsf {d}}{\mathcal {L}}\) inference rule, we simply rewrite the \( wlp \) in Proposition 9.2 as a Hoare-style inference rule.

To apply this rule in our setting, the procedure in Sect. 9 must be followed.

Next, we derive five semantic counterparts of the \({\mathsf {d}}{\mathcal {L}}\) axioms and inference rules for differential invariants in the setting of Sect. 11. The differential cut axiom (DC) and rule (dC), differential weakening, (DW) and (dW), and the differential induction rule (dI). These rules are typically applied backwards as follows: \( dC \) introduces an invariant. Its left premise is discharged via \( dI \), Proposition 11.1 and logical reasoning, while its right premise is discharged via \( dW \). Note that the conclusions of all these rules are semantically equivalent to Hoare triples. Verification examples using these rules and the \({\mathsf {d}}{\mathcal {L}}\) approach can be found in our Isabelle components.

Axiom (DC) and rule (dC) introduce differential invariants in guards of evolution commands. Axiom and rule (DW) and (dW) summarise the fact that if a guard is strong enough to imply a postcondition, then no invariant or solution needs to be found. Finally, the differential induction rule follows from Proposition 11.1(3), transitivity and isotonicity of boxes.

A differential ghost rule [51] (dG) and sometimes a differential effect axiom [48] have also been proposed for reasoning with invariants in \({\mathsf {d}}{\mathcal {L}}\). Our semantics approach has so far no need for these [45]—we do not anticipate any reason why we should not be able to freely introduce ghost variables for the continuous dynamics as we have so far done for the discrete one using Isabelle’s higher-order logic—but see [12] for a derivation of (dG) within our semantic framework.

The entire mathematical development of \(\mathsf {MKA}\) in Sects. 2–4 has been formalised with Isabelle [3, 16]. Verification components for Isabelle and the relational store model in Sect. 7 have been developed, too [17, 18], using the shallow embedding approach discussed in Sects. 1 and 7. Predicate transformers à la Back and von Wright have been formalised previously in Isabelle by Preoteasa [52, 53]. Our alternative formalisation emphasises the quantalic structure of transformers [64, 65], as in Sect. 5, and we have added a third component based on quantaloids [65]. It is based on a formalisation of the powerset monad [65], as outlined in Sect. 6. Our formalisation is compositional in that all three approaches to predicate transformers can be combined with relational and state transformer semantics and different models of the (hybrid) program store, as shown in Fig. 1.

This section summarises the Isabelle components for predicate transformers and the verification component based on \(\mathsf {MKA}\). More detailed information can be found in the proof documents for these components [18, 65].

The \(\mathsf {MKA}\) component is integrated into the Kleene algebra hierarchy that formalises variants of Kleene algebras [3] and modal Kleene algebras [16], as outlined in Sects. 2 and 3. In these mathematical components, algebras are formalised as type classes, their models via instantiation and interpretation statements. For Kleene algebras, many computationally interesting models have been formalised; for \(\mathsf {MKA}\), only the relational model is present in the Archive of Formal Proofs. The state transformer model has been formalised for quantales in a different component [65].

Instantiation and interpretation statements have several purposes in Isabelle. They make algebraic facts available in all models, establish soundness of algebraic hierarchies and ultimately make the axiomatic approaches consistent with respect to Isabelle’s small trustworthy core. Finally, they unify developments of multiple concrete semantics.

In our \(\mathsf {MKA}\)-based verification components [18], program syntax is absent and semantic illusions of program syntax are provided in the concrete program semantics, as outlined in Sect. 7. Consequently, verification conditions for the control structure of programs are generated within the algebra; those for assignments in the concrete store semantics. We currently model stores simply as functions from strings representing variables to values of arbitrary type. Expressions are simulated by functions from stores to values, as outlined in Sect. 7; stores with poly-typed values are modelled via sum-types. An extension to verification components for hybrid programs is described in the following sections.

A second component is based on predicate transformers à la Back and von Wright [5], for which we have built special purpose components with advanced features for orderings and lattices [63] and for quantales [64]. These structures are once again formalised as type classes. Predicate transformers, however, are modelled as global functions that may have different source and target types. Isabelle’s simple type system can infer most general types for definitions. These can be associated with predicate transformers by sort constraints; definitions can often be declared in the point-free style of functional programming. This makes the formalisation of quantaloids of transformers with partial compositions straightforward. Mono-typed transformer algebras are obtained from these via subtyping. They are linked with quantales and Kleene algebras by interpretation or instantiation.

Isabelle’s type system is too weak for a deep embedding of general categorical concepts, but formalising instances such as the powerset monad, its Kleisli category and Eilenberg–Moore algebras is straightforward. We have formalised the isomorphisms and dualities between relations, state transformers and the four predicate transformers corresponding to backward and forward boxes and diamonds in this setting. Using these dualities to transport theorems automatically requires Isabelle’s transfer package, which is ongoing work.

We have created a second verification component for hybrid systems based on Back and von Wright’s approach, using the monadic transformers to obtain a concrete semantics. Finally, we have once again restricted the categorical approach to the mono-typed case in a third component. Via subtyping, we can then show that the categorical transformers form quantales, and more specifically \(\mathsf {MKA}\)s. Everything Isabelle knows about \(\mathsf {MKA}\) is then available in this instance.

This section and the two following ones describe the formalisation of the material in Sects. 8–12 in Isabelle, from mathematical components for ODEs and orbits to verification components for hybrid programs based on (local) flows, differential invariants and \({\mathsf {d}}{\mathcal {L}}\)-style inference rules.

We begin with summarising Immler and Hölzl’s formalisation of the Picard–Lindelöf theorem based on the Isabelle hierarchy for analysis and ordinary differential equations [23, 29‐31]. We have adapted their results to show that unique solutions to IVPs for autonomous systems of ODEs guaranteed by this theorem satisfy the local flow conditions, as discussed in previous sections.

Hölzl and Immler have proved the Picard–Lindelöf theorem for time-dependent vector fields of type [30]. They have called their theorem and have formalised it within a locale called to bundle the assumptions for the local existence of unique solutions within a closed interval in \({\mathbb {R}}\). They have specialised and hence extended this locale in various ways.

Our approach builds on top of their extension that bundles more or less the conditions of Theorem 8.2, but for the time-dependent case. In our formalisation, we add the condition \(t_0\in T\) to have this parameter available in the following developments. Thus, we have generated the following variant.

The locale declaration lists the assumptions of the Picard–Lindelöf theorem: the vector field f—which is still time-dependent—is defined on an open time interval T that contains the initial time \(t_0\), and an open subset S of the state space. The vector field f is continuous in time and, for each \((t,s)\in T\times S\), Lipschitz continuous on a closed subset of \(T\times S\) around (t, s). The sublocale statement shows that these assumptions imply those of the locale . Lemma ensures that the Picard–Lindelöf theorem is derivable within this locale. The notation \(D\, X\) stands for \(X'\), and \(g\in A\rightarrow B\) indicates that function g maps from the set A into the set B, as opposed to the type of g, which can be larger. The notation indicates the set of real numbers between and t (including both), where t may be above or below \(t_0\). The formalisation of the Picard–Lindelöf theorem comprises a formal definition of solutions to IVPs of system of ODEs in Isabelle. As an abbreviation, we have defined the set \({\mathsf {Sols}}\, f\, T\, s\) of Sect. 10 with the additional requirement that \(X\in T\rightarrow S\).

We restrict locale to autonomous systems and to \(t_0=0\), while introducing the variable \(\varphi \) for the local flow of the vector field. In support of our open approach to hybrid program verification, this allows users to supply any characterisation of the flow that suits them best, as a successor paper illustrates [26].

The assumptions force T to coincide with its largest subinterval ( ) where solutions exist (lemma below). Thus, \(\varphi \) is the unique solution on the whole of T —and not only on its subsets unlike or . This allows users of the locale to choose T as small as they wish.

Finally, in this locale we can prove that if the maximal interval of existence T equals \({\mathbb {R}}\), then the flow \(\varphi \) is global and hence a proper monoid action.

We have not generated a locale for this case, as the assumptions needed to remain unchanged. Locale thus guarantees the existence of unique solutions for IVPs of time-dependent systems. Locale specialises it to autonomous systems with Lipschitz continuous vector fields and local flows. It covers dynamical systems with global flows and thus the verification of hybrid systems. This provides the basic Isabelle infrastructure for formalising the concrete semantics for hybrid systems with Lipschitz continuous vector fields from Fig. 1.

Next, we describe our formalisation of the orbits and orbitals from Sect. 10. These form the basis for our verification components for continuous vector fields beyond the scope of the Picard–Lindelöf theorem, as shown in Fig. 1. Yet we can instantiate all concepts to settings where (local) flows exist. First, we have formalised the G-guarded orbit \(\gamma ^X_{G}\) of X along T, with standing for \({\downarrow }t\).

We have also formalised the G-guarded orbital of f along T in s (as \(\gamma ^f_G\, s\)) together with Lemma 10.1.

We have shown that their counterparts from dynamical systems are special cases by instantiating our definitions to the parameters of the locale . Hence, the \(\top \)-guarded orbital of f along T in s becomes the standard orbit of s, and its G-guarded version is the set in Lemma 9.1.

Overall, the set-theoretic concepts introduced in Sect. 10 are easily definable in Isabelle. Similarly, lemmas formalising their properties and relating them are often proved automatically in one or two lines. Analytical properties like the existence of derivatives in a region of space or the uniqueness of solutions for IVPs are harder to prove. Such lemmas often require long structured proofs with proofs by cases and explicit calculations, that is, a considerable amount of user interaction. Yet most proofs remain at least roughly at the level of textbook reasoning.

This section describes the integration of the state transformer and relational semantics for dynamical systems and Lipschitz-continuous vector fields from Sect. 9 and the continuous vector fields from Sect. 10 into the three verification components for predicate transformers outlined in Sect. 13 and Fig. 1. This requires formalising hybrid stores and the semantics of evolution commands for dynamical systems, Lipschitz continuous vector fields with local flows and continuous vector fields. As explained in Sect. 9 and 11, this supports two different workflows using the procedures introduced in these sections: the first one is for reasoning with (local) flows and orbits, the second, more general one, for reasoning with invariants.

First, we explain our formalisation of the hybrid store type \({\mathbb {R}}^V\). We use Isabelle’s type (abbreviated as ) of real valued vectors of dimension n, formalised as the type of functions from the finite type into \({\mathbb {R}}\). This represents hybrid stores in \({\mathbb {R}}^V\) with \(|V|=n\). Isabelle uses the notation for the \(i\hbox {th}\) coordinate of a vector s and hence the value of store s at variable i. More mathematically, is the bijection from to . Its inverse is written using a binder that replaces \(\lambda \)-abstraction. Thus, for any and for any . As a consequence of this simple approach, variables are formalised as natural numbers. More general namespaces have been included in our framework more recently [11, 12] to make it more user friendly.

Our state transformer semantics uses functions of type , which we abbreviate as (for non-deterministic functions). These are instances of the more general type of nondeterministic endofunctions.

Alternatively, we use relations of type , which are instances of . For both intermediate semantics, we have shown with Isabelle that they form \(\mathsf {MKA}\hbox {s}\), but we have also integrated them into the two quantalic predicate transformer semantics in Fig. 1.

After these proofs, all statements proved in Isabelle’s \(\mathsf {MKA}\) components are available for state transformers and relations. We have formalised \( wlp \hbox {s}\) for both models, where ambiguously denotes the isomorphism between predicates and binary relations or nondeterministic functions.

Alternatively, we use the categorical forward box operator for Kleisli arrows of type described in Sect. 6,

or its relational counterpart .

We now switch to the categorical approach to predicate transformers based on state transformers and the Kleisli monad of the powerset functor, as a preliminary \(\mathsf {MKA}\)-based one with relations has already been described elsewhere [28]. Apart from typing and some minor syntactic differences, the other approaches—predicate transformers based on \(\mathsf {MKA}\) and quantales, and an intermediate relational semantics for these—yield analogous results and are equally suitable for verification. This evidences the compositionality of our approach.

The state and predicate transformer semantics of assignment commands is based on store update functions, as described in Sect. 7. For hybrid programs, it must be adapted to type .

The applies the bijection as a function in prefix notation.

We write for the semantic illusion for a syntactic assignment commands, as Isabelle uses for function update \(f[i\mapsto a]\). Lemma is then a direct consequence of , and it coincides with (wlp-asgn) in Sect. 7 up to minor syntactic differences. In the verification examples that feature in this article, we have not attempted to hide the functions that impersonate syntactic expressions and the lambda abstractions they require. This may be unwieldy for users. It is nevertheless routine to program more elegant notation with Isabelle [12].

Similarly, \( wlp \hbox {s}\) for the control structure commands of hybrid programs (Eqs. wlp-seq, wlp-cond, wlp-star) are easily derivable.

In these lemmas, is syntactic sugar for the forward Kleisli composition \(\circ _K\) and stands for the Kleene star for state transformers with its annotated loop-invariant after the keyword , along the lines of Sect. 4.

As in Sect. 10, the general semantics of evolution commands for continuous vector fields is given by G-guarded orbitals of f along T. We have formalised the \( wlp \hbox {s}\) in Proposition 10.2, and a specialisation to local flows in the context of our locale given by Lemma 9.3 [Eq. (wlp-evl)].

As Lemma is defined in locale , users are required to check the conditions of the Picard–Lindelöf theorem to access this locale and certify that \(\varphi \) is indeed a solution of the IVP as part of our first workflow.

Finally, we describe our component for reasoning with differential invariants in the general setting of continuous vector fields, using our second workflow. We start with definitions and a basic property from Proposition 11.1.

We have formalised the most important rules for reasoning with differential invariants, including those for the procedure of Sect. 11 via Corollary 10.3 and Lemmas 4.1 and 11.3. The formalisation of the first two is straightforward. We have proved the clauses of 11.3 in various lemmas and bundled them under the name . We show one of these clauses as an example.

Lemma completes the procedure of Sect. 11 by formalising step 2, which annotates invariants in evolution commands, following the approach outlined for loops and general commands in \(\mathsf {MKA}\) at the end of Sect. 4. With Isabelle, we use the keyword.

The two workflows for proving partial correctness specifications with evolution commands require users to discharge proof obligations for derivatives. In the case of flows, these must be solutions for vector fields; in the case of differential invariants, the procedure of Sect. 11 requires proving the assumptions of Lemma 11.3. To increase proof automation when reasoning about derivatives, we have bundled several derivative properties under the name as a proof method.

Isabelle can now apply rules iteratively and check, for pairs of functions, if one is a derivative of the other. This is often fully automatic. The following lemma shows an example that involves a mix of polynomials and transcendental functions beyond differential fields with \(a_0\) to \(a_5\) being constants and t the polynomial variable.

The formalisation of more advanced heuristics for such functions, and the integration of decision procedures for suitable classes, is left for future work.

The complete Isabelle formalisation, including the other two predicate transformer algebras and the relational semantics, can be found in the Archive of Formal Proofs [25].

We briefly reflect on our experience with the Isabelle formalisation of our framework. \(\mathsf {MKA}\), its relational model and the concrete relational semantics for traditional while programs are so far the most developed and versatile starting point for our hybrid systems verification components. The full formalisation of a rudimentary Hoare logic component for this setting using a generalised Kleene algebra from Isabelle’s main libraries fits on two A4 pages [62]; a similar development for a Hoare logic for hybrid programs is discussed in a successor paper [11]. Our standalone \(\mathsf {MKA}\)-based verification component for traditional while programs fills about seven A4 pages. For hybrid programs, in theory, only a concrete semantics for hybrid programs needs to be plugged in as a replacement of the semantics described in Sect. 7. In practice, however, Isabelle’s instantiations often make theory hierarchies non-compositional as each type can only be instantiated in one way. We faced such a clash of instances between Isabelle’s Kleene algebra and analysis hierarchies and hence had to customise the former for our purposes.

Replacing the intermediate relational semantics by state transformers required some background work, simply because the former are well supported by Isabelle, whereas the latter are new. Interestingly, it is possible to propagate theorems automatically along the isomorphisms between these semantics like for type classes, locales and their instantiations and interpretation. Isabelle’s transfer and lifting packages provide an infrastructure for this, which remains by and large unexplored. We leave this for future work.

The categorical approach to transformer quantaloids is more complex—both conceptually and from a formalisation point of view—than the \(\mathsf {MKA}\) based one, in particular when state transformers are integrated via the powerset monad. At the level of verification conditions generation, however, there are almost no differences. Once again a stripped down component can be generated that just suffices for verification condition generation, and we are using it in subsequent work [12]. Relative to Isabelle’s main libraries, it fills merely four pages [25]. Working with quantales instead of quantaloids might seem mathematically simpler, but with Isabelle it is actually more tedious, as subtypes for endofunctions need to be created.

In sum, for simple verification tasks, the lightweight stripped down predicate transformer algebras obtained from \(\mathsf {MKA}\) or quantaloids seem preferable; for more complex program transformations or refinements, the integration into the full \(\mathsf {MKA}\) hierarchy or categorical predicate transformer component is certainly beneficial.

This section lists our formalisation of semantic variants of the most important axioms and inference rules of \({\mathsf {d}}{\mathcal {L}}\) in Isabelle outlined in Sect. 12. It covers all three predicate transformer semantics as well as the relational and state transformer model. Once again, we only show state transformers in the categorical approach.

We have formalised a generalised version of the \({\mathsf {d}}{\mathcal {L}}\)-rules with parameters T, S and \(t_0\) with intervals U and for orbitals. We can easily instantiate them to \({\mathbb {R}}\), \({\mathbb {R}}^V\) and 0, respectively. This enables users to perform verification proofs in the style of \({\mathsf {d}}{\mathcal {L}}\) and establishes soundness of these rules relative to our semantics as a side effect. First, we show our formalisations of (DS) and (dSolve).

Next, we list semantic variants of the five \({\mathsf {d}}{\mathcal {L}}\) axioms and inference rules for reasoning with differential invariants discussed in Sect. 12. Recall that due to our semantic approach, evolution commands in these rules only require the vector field , while the is just syntactic sugar to resemble ODEs.

Additional \({\mathsf {d}}{\mathcal {L}}\) rules can easily be formalised. More recent work features, for instance, a ghost rule [12], which is heavily used for reasoning with invariants in \({\mathsf {d}}{\mathcal {L}}\), but seems less relevant to our semantic approach [45].

This section explains the formalisation of the bouncing ball examples from Sect. 9 and 11 with Isabelle, and we add two further verification examples using a simple circular pendulum. All four of them use Isabelle’s type of two elements. It denotes the set of variables V of hybrid programs over the state space \({\mathbb {R}}^V\) for \(|V|=2\). We follow Isabelle’s notation and write and for the two variables and their type. As such a formalisation of variables is rather unwieldy, more recent extensions to our framework support more general name spaces, more sophisticated store models and a more user-friendly specification language for hybrid programs and assertions [12]. The examples in this section should therefore be taken cum grano salis.

All four examples have been based on the categorical approach and the state transformer semantics. Alternative formalisations for the other predicate transformer algebras and the relational semantics can be found in other verification components [25]. In the \(\mathsf {MKA}\)-based component, the proofs using the relational and the state transformer semantics are precisely the same, which underpins the modularity of our approach. In the other components, we could certainly achieve the same effect by simply rewriting names and adjusting some types.

Transcendental functions cannot be expressed directly in \({\mathsf {d}}{\mathcal {L}}\)’s term language, yet we can use them smoothly and easily with Isabelle with the tactic outlined in Sect. 15. Both the differential invariant workflow and the flow-based workflow benefit from these rules. In fact, both approaches are very similar for the pendulum example: both need a handful of lemmas to prove the partial correctness specification \( I = |{x'=f\ \& \ \top }] I\), and both require a creative step in the form of introducing a differential invariant or the flow for the system.

We have presented the pendulum example in matrix notation as this points to a common feature of many applications: their dynamics can be described by linear systems of ODEs that are representable by matrices and have uniform solutions given by a matrix exponential that can be computed with standard methods from linear algebra. The development of domain-specific techniques for linear systems with Isabelle has been the subject of a successor article [26]. Beyond these simple examples, our approach has successfully tackled a large set of benchmarks from a systems competition [45] and been fine-tuned for proof automation, so that the size of proofs and level of user interaction reported in this article is no longer representative. More information about the background theory development with Isabelle and the methods and heuristics programmed can be found in the first author’s doctoral dissertation [27]. A more far-reaching integration of solvers and decision procedures, or procedures for invariant learning, as oracles or with correctness guarantees, is of course crucial to the applicability of this framework, but beyond the semantic considerations of this article. It is left for future work.

The verification components presented so far adhered very much to the pessimistic interactive theorem proving mindset that prefers the internal reconstruction of all external results. This section briefly outlines a fourth, more optimistic verification component that deviates entirely from the vector-field-based approach of \({\mathsf {d}}{\mathcal {L}}\) and works directly with flows or solutions to IVPs. It shifts responsibility for the correctness of solutions entirely to users—or the computer algebra system they could or should use. This is common practice for instance when working with hybrid automata [10], and of course it simplifies proofs considerably.

For this third workflow supported by our framework, the topological or differentiable structure of the underlying state space is of secondary interest. With Isabelle, this kind of structure and additional conditions can always be imposed by instantiating types with sort constraints as they arise. Hence, we start from a setting that covers both discrete and continuous evolutions and use a general type for time instead of , or . The evolution commands now specify arbitrary guarded \(\varphi \)-type functions instead of vector fields. The type of time needs to admit an order relation, which is indicated by the sort constraint below, yet specific properties, such as reflexivity or transitivity, need not be imposed ab initio.

Apart from that, the definition of the guarded-orbit semantics and the \( wlp \) rule are as before, but side conditions on Lipschitz continuity or the Picard–Lindelöf theorem are superfluous.

Using the flows of the bouncing ball and the circular pendulum from previous examples, verification proofs are now fully automatic.

These examples no longer link flows with initial specifications in terms of system of ODEs, from which a user might have started. Hence, there is no longer any formal guarantee from Isabelle that the function \(\varphi \) specified satisfies any continuity of differentiability assumptions such as those of .

Further elaboration of this approach, in particular towards discrete systems or in the direction of hybrid automata, is left for future work.

Methods for automated verification condition generation for partial and total correctness assertions with proof assistants date back to the early days of hardware and software verification by Gordon and colleagues [19]. Discussions on the benefits of shallow embeddings of verification methods in proof assistants—among them faster developments and increased modularity—can be traced back to the same group of researchers. We generally follow an approach described in [2] that starts from algebras of programs to generate verification conditions for the structural commands of programs, while developing those for basic commands in concrete semantics of the program store dynamics.

Mathematical components for classical real analysis have been developed for the Coq proof assistant in the Coquelicot library [7], others for constructive analysis in the CoRN library [8]. The Picard–Lindelöf theorem seems to be available only in the latter [42]. The proof assistant HOL-light includes a library with formalised n-dimensional Euclidean spaces. The first formalisation of the Picard–Lindelöf theorem in Isabelle, which we rewrite for our purposes and specialise to local flows, can be found in the AFP entry for ordinary differential equations [30].

Hybrid systems verification in general-purpose proof assistants has also been investigated. Examples in PVS include semantic invariant reasoning with hybrid automata [1] and, after submission of this article and publication of its precursor [28], \({\mathsf {d}}{\mathcal {L}}\)-style verification with semi-algebraic sets and real analytic functions [59]. An earlier formalisation of the control function of an inverted pendulum [57] uses the Coquelicot library. Also in Coq, the robot operating system (ROSCoq) framework uses a shallowly embedded logic of events to reason about hybrid systems but only with \({\mathsf {d}}{\mathcal {L}}\)’s differential induction rule. The HHL prover [67] formalises a Hoare-logic for hybrid systems verification within its calculus of hybrid communicating sequential processes in Isabelle [38]; part of their approach has been deeply embedded. Their semantics is very different from ours. An integration of their LZZ method [39] for finding semi-algebraic invariants for polynomial dynamical systems could probably be integrated into our framework to increase proof automation. Finally, a term-checker for KeYmaera X [6] and, after submission of this article, a formalisation of differential game logic (\({\mathsf {d}}\mathcal {GL}\)) [50] have been deeply embedded recently in Isabelle/HOL. None of them aim at hybrid program verification.

For an in-depth description of \({\mathsf {d}}{\mathcal {L}}\) see [49], a thorough study of differential invariants has been pursued in [46].

In theory, our own framework should therefore allow the integration of much of the related work mentioned, so long as it is consistent with our hybrid store semantics. It is not even necessary to delegate every task to the proof assistant. One can use external tools implementing decision procedures as oracles or at least certify their outputs with Isabelle. The oracle-based approach, however, may jeopardise the desirable conservative extension property relative to Isabelle’s own kernel. Translations between different proof assistants may not always be straightforward. For instance, it is yet to be seen if dependent types or multi-parameter type classes are needed for more flexible implementations of functions spaces (bounded, linear and continuous) or complex vector spaces, or if alternative formalisations of Picard–Lindelöf theorem and other existence theorems might help us to alleviate some of the requirements in our workflows.

We have presented a new semantic framework for the deductive verification of hybrid systems with the Isabelle/HOL proof assistant. The approach is inspired by differential dynamic logic, but the design of our verification components, the focus of our framework and the workflows for verifying hybrid systems are different.

First of all, as we use a shallow embedding, the basic verification components generated are quite minimalist and conceptually simple. They merely require the integration of a \( wlp \) semantics for basic evolution commands of hybrid programs into standard predicate transformer algebras. Our preferred semantics for such commands are state transformers, which in most cases simply map states to the guarded orbits of their temporal evolutions. Beyond that, no domain-specific inference rules are needed, verification condition generation is fully automatic, and even our approach to differential invariants is based entirely on general purpose algebraic invariance laws. Our examples show that mathematical reasoning about differential equations follows standard textbook style and hence comes close to the way mathematicians, physicists or control engineers have been trained to reason about such systems. Whether this is preferable to the proof-theoretic approach advocated by KeYmaera X remains to be seen.

Secondly, our approach aims at an open experimental platform that is only limited by Isabelle’s ODE and analysis components, the expressivity of its higher-order logic and type system and the proof methods it provides. We could, for instance, have developed our semantics for time-dependent vector fields, but the restriction to autonomous systems, which does not affect generality, seems preferable in practice. The integration of internal or external solvers for differential algebras, transcendental functions or computer algebra systems for computing Lipschitz constants or flows in the style of Isabelle’s Sledgehammer tactic is certainly interesting and a very important avenue for future work, but not a main concern in this article. So far, our open approach simply offers semantic alternatives that users may explore, adapt and extend.

Two specialisations of our framework are the topic of successor papers. The first one restricts our approach to linear systems of differential equations, where exponential solutions exist and can be computed with standard methods from linear algebra [26]. The second one [11] specialises the predicate transformer semantics to algebraic variants of Hoare logics and to refinement calculi for hybrid programs along the lines of previous components for traditional while programs [2]. This shows that our denotational semantics for hybrid programs are compatible with any Hoare logic, which constitutes another significant conceptual simplification relative to \({\mathsf {d}}{\mathcal {L}}\) and KeYmaera X.

Beyond that we expect that a recent formalisation of Poincaré maps with Isabelle [31] might allow us to extend our framework to discrete dynamical systems and more computational approaches to hybrid systems.

Moreover, differential-algebraic systems of equations [20], which mix differential equations and algebraic equations, and partial differential equations [34] are important for many applications in control engineering and physics. Extending our approach is likely to require significant background work on mathematical components with Isabelle. While, in both settings, some simple cases can be reduced to systems of ODEs, numerical methods are usually needed for working with such systems. Whether the workflow of mathematicians, physicists and engineers with such more computational approaches can be approximated easily with Isabelle remains to be seen.

Finally, much work is needed to transform our framework into an applicable verification tool for hybrid systems. First steps have meanwhile been taken [12] with respect to more refined hybrid stores and a more user-friendly specification language for hybrid programs and their correctness properties, as already mentioned. More important, however, seems the integration of external solvers and decision procedures, to which much work in the hybrid systems community has already been devoted [13, 39, 54, 58, 60]. Such procedures already increase the proof automation of KeYmaera X, and we foresee no reason why similar integrations should not lead to similar benefits within our own framework.