Specification and verification in continuous problem domains are key topics for the practical application of formal methods and mechanized reasoning. I discuss one approach to linear continuous control systems and consider the challenges and opportunities raised for mechanized reasoning. These include practical implementation and integration issues, algorithms in computational real algebraic geometry and hard open questions such as the Schanuel conjecture. I conclude with an overview of some recent new results on decidability and undecidability for vector spaces and related theories.
For some years, I have been involved with tools used for formally specifying and
verifying digital subsystems of avionics control systems [
To understand the challenges that formal vericfiation of continuous systems offers for mechanized reasoning, it is helpful to do some methodological thinking. In the first part of the talk, I give an overview of an approach to linear continuous systems that builds on the well-known ideas of Hoare logic that have proved so fruitful in program verification. It turns out that linearity makes this approach very tractable given adequate support for reasoning about the mathematical problem domains involved, namely vector spaces, typically with some additional structure such as an inner product or a norm.
However, some signicfiant problems arise from this. While the first order theory of the real field is decidable, in practice, engineers will want to work with the kind of rich vocabulary supported by typical computer algebra systems; so even to deal with the efild of scalars in our vector spaces, we may need to go well beyond the usual first order theory of the real numbers. Moreover, even if we have some solution to this problem or have an application in which a simple language for the scalars is adequate, we need methods for reasoning about vector spaces. In the second part of the talk, I will describe some new results on decidability and undecidability for various theories of inner product spaces and normed vector spaces (including Hilbert spaces and Banach spaces). It turns out that the very uniform geometric and algebraic properties of inner product spaces lead to decidable theories, while, with only trivial exceptions, theories of normed vector spaces are undecidable. Nonetheless, the universal fragment admits a decision procedure. I believe there is plenty of scope for interesting and useful further research in this area. 2
Let us consider an approach to reasoning about linear systems proposed in [
As an example, Figure 1 represents a mechanical system in which a force f acts on a cart of mass m attached to a wall by a spring with spring constant, k. It is a graphical representation of the following differential equation: mx¨(t) + kx(t) − f (t) = 0. f - 1 m
x¨ -+h 6
R x˙ - R x
− k m
The arrows in the diagram suggest a distinction between inputs and outputs that is missing from the differential equation. They let us view figure 1 as specifying the function mapping the force function f to the position function x. With this intensional viewpoint, the diagram might serve, for example. as a design for an analogue computer that simulates the mechanical system.
The lists of real-valued functions of time that appear as the lists of inputs and outputs to the primitive components in our diagram form vector spaces over the efild R of real numbers. Moreover, the primitive components of the diagram represent linear transformations on those vector spaces (integration, scalar multiplication and addition). Such diagrams are called linear signal flow graphs and are very common in engineering practice. From now on we restrict our attention to linear signal flow graphs.
In the example of figure 1 the diagram happens to be a function, but, in general, a differential equation may not have a unique solution for a given initial condition. So in general a diagram denotes an input/output relation that is not necessarily total or single-valued. Rather than trying to ban partial or multivalued relations, we will deal with them by borrowing some ideas from the world of relational specicfiation of programs. This turns out to work particularly nicely given the algebraic structure we have to hand.
We write r : X ↔ Y to denote that r is a relation between the sets X and Y , i.e., a subset of X × Y , and use x r y as a shorthand for (x, y) ∈ r. If r and s are relations, (r; s) denotes the relational composition r followed by s, so that x (r; s) y iff there is a z with x r z and z s y. If r : X ↔ Y , r− 1 : Y ↔ X is the relational inverse of r, defined by taking x r− 1 y iff y r x. We write Ar for the image of a set A under the relation r. So if r : X ↔ Y , then dom(r) = Y r− 1 is the domain of r, ran(r) = Xr is its range and r acts as a relation between any sets A and B such that dom(r) ⊆ A and ran(r) ⊆ B.
If r : X ↔ Y , A ⊆ X and B ⊆ Y , a Hoare triple, {A} r {B}, is the logical judgement which holds whenever A ⊆ dom(r) and Ar ⊆ B. A and B are referred to as the pre-condition and post-condition respectively. Hoare triples may be characterised in terms of weakest pre-conditions: the weakest pre-condition, wp(r, B), of B through r is the set of all points in the domain of r whose image under r is contained entirely in B. As is easily verified, the Hoare triple {A} r {B} holds, iff A ⊆ wp(r, B).
The weakest pre-condition wp(r, B) contrasts with the pre-image Br− 1 of B under r comprising all points whose image under r meets B. In general wp(r, B) is a proper subset of Br− 1. But if r is a function (not necessarily total), one has that wp(r, B) = Br− 1. It turns out that something quite similar holds for the input/output relations denfied by linear signal flow graphs.
In fact, the input/output relation between vector spaces V and W
determined by a a linear signal oflw graph is what is called an additive relation [
In gfiure 2 we show a set of constructors for forming new signal flow graphs
from old. We call a signal oflw graph a structured block diagram if it is formed
from primitive components using these constructors. In [
F
G
Using the characterisation of the weakest pre-condition given above, we can then derive a Hoare logic for structured block diagrams. For example, we have the linear combination rule {A} r {B} {A} s {B1} {A} βr + γs {βB + γB 1}
Assuming we have a tractable characterisation of the primitive blocks, the Hoare logic reduces the problem of verifying any structured block diagram against given pre- and post-conditions reduces to a problem in the assertion language we are using to express the pre- and post-conditions.
For example, assume that we are working with finite-dimensional vector
spaces Rm, m ∈ N and that our primitive blocks are given by matrices with
constant rational coefficients. Let us make assertions about vectors ( v1, . . . , vm) ∈
Rm using rfist order formulae in the language of the real field with free variables
drawn from v1, . . . vm. Then our approach automatically reduces any verification
problem to a problem in the language of the real field. Thus, in contrast with
the situation for programming languages, a large and natural class of signal flow
graphs has a decidable vericfiation problem, since, by a classic result of Tarski
[
However, there are practical concerns: the time complexity of the decision
procedure for the first order theory of the reals is provably doubly exponential
in the number of bound variables in the formula (this theoretical bound being
achieved by Collins’ method of cylindrical algebraic decomposition [
the number of quantifier alternations [
As suggested in [
A few years ago, on being asked by John Harrison about decidability for vector
spaces, Robert M. Solovay promptly invented quantiefir elimination procedures
for a range of theories. Some special cases of these have so far been implemented
and found very useful in practice [
We work in a two-sorted rfist order language with sorts R for scalars and V for vectors. The intended interpretation of the sort R is the set R of real numbers. We have function symbols + , × : R × R → R and − : R → R which in the intended interpretations are the usual efild operations on R. We have function symbols + : V × V → V , − : V → V and × : R × V → V which in the intended interpretations make the set denoted by V into a real vector space. We have scalar constants m/n : R for each rational number m/n and we have the vector constant 0 : V to be interpreted as the zero vector. The first order theory of real vector spaces is the set of sentences in our language that are valid in all the intended interpretations.
The theory of normed spaces is obtained by adding to the language a function symbol || || : V → R whose intended interpretation is a norm on the vector space. A norm denfies a metric on the set of vectors via d(v, w) = ||v − w||. Recall that a normed space is called a Banach space if it is complete with respect to this metric (i.e., if every Cauchy sequence converges).
The theory of inner product spaces is obtained by adding a function symbol h , i : V × V → R whose intended interpretation is an inner product. Recall that an inner product space that is also a Banach space under the norm denfied by ||v|| = phv, vi is called a Hilbert space.
We consider the theories of vector spaces, normed spaces, Banach spaces etc. with various restrictions on the dimension, e.g., the theory of all finite dimensional inner product spaces. We write IP, resp., IPF, resp., IP∞ for the theories of real inner product spaces where the dimension is unconstrained, resp., constrained to be finite, resp., constrained to be innfiite, and HS, HSF and HS∞ for the theories of Hilbert spaces with the corresponding constraints on the dimension. Completeness is guaranteed if the dimension is finite, so IPF = HSF.
A sentence in any of these languages that contains no vector-valued subexpressions is just a sentence in the first order language of the real field and its truth is independent of the interpretation of the vector sort. If we can eliminate all the vector quantiefirs from a formula, then occurrences of the vector constant 0 can readily be eliminated to give an equivalent formula in the first order language of the real efild.
If B is a basis for a vector space V , then we can define an inner product on V by requiring hb, bi = 1 for b ∈ B and hb, ci = 0 for b, c ∈ B with b 6= c and extending to V by bilinearity. Thus the theory of inner product spaces is a conservative extension of the theory of vector spaces and a decision procedure for the theory of inner product spaces is also a decision procedure for the theory of vector spaces.
The key to decidability for inner product spaces is the fact that it takes at most k degrees of freedom to decide a sentence containing k vector variables. I.e., a sentence P containing k vector variables is valid in all inner product spaces iff it is valid in Rn for 0 ≤ n ≤ k. This is proved by considering a process that replaces vector quantiefirs by blocks of scalar quantiefirs. The process transforms a formula containing k vector variables into one which is equivalent in spaces of dimension at least k and in which vector variables only appear within arithmetic constraints on inner products (v, w), with v, w free. Applying the process to a sentence P with k vector variables results in a sentence in the language of a real field which is equivalent in dimensions k or higher. From P one can effectively construct a sentence P |n containing no vector-valued subexpressions which is valid iff P is valid in Rn. Writing Dn (resp. D≤ n) for a sentence asserting that the dimension of the space is n (resp. at most n), one finds that P is equivalent to:
(D0 ∧ P |0) ∨ (D1 ∧ P |1) ∨ . . . ∨ (Dk− 1 ∧ P |k− 1) ∨ (¬D≤ (k− 1) ∧ P |k) Applying the quantifier elimination algorithm for the rfist order theory of the reals to the subformulae P |n, this leads to the following result: Theorem 1 The theories IP, IPF, IP∞, HS, HSF and HS∞ are all decidable.
When we consider decidability for normed spaces we find that even the theory of 2-dimensional spaces is undecidable and actually admits a primitive recursive reduction of second order arithmetic. The proof uses the following fact that is well-known to descriptive set theorists and others, but seems not to have appeared in the literature in quite the form we need. Theorem 2 Let K be a (many-sorted) first-order language including a sort R, constants 0 : R and 1 : R and function symbols + , × : R × R → R whose intended interpretations form the field of the real numbers. Let M be some class of structures for K in which R and these symbols have their intended interpretations and let T be the theory of M, i.e., the set of all sentences valid in every member of M. If there is a formula N (x) of K with one free variable x of sort R such that in some structure in the class M, N (x) defines the set of natural numbers (i.e., {x : R | N (x)} = N), then there is a primitive recursive reduction of second order arithmetic to T .
Here is a sketch of the proof: one can write down a sentence Nat which asserts that the subset of the reals denfied by N (x) satisefis the Peano axioms, and then, in any structure for the language in which the reals have their intended interpretation, Nat holds iff N (x) does indeed denfie the natural numbers. Now if P is any sentence in the language of Peano arithmetic, we may view P as a sentence in the first order language of the reals and then construct a new sentence P ∗ by relativizing all quantifiers to N (x) (i.e., ∀x· Q is replaced by ∀x· N (x) ⇒ Q and ∃x· Q is replaced by ∃x· N (x) ∧ Q). But then the sentence Nat ⇒ P ∗ is in T iff it P is valid in arithmetic. This gives a reduction of first order arithmetic to T . A reduction of second order arithmetic is obtained in a similar way using real numbers to represent sets of natural numbers, e.g., using n-ary expansions.
So, for example, this gives a very simple proof that the first order theory of metric spaces is undecidable: in the metric space Z whose elements are the integers with the distance defined by d(p, q) = |p − q|, we can clearly define the natural numbers by the formula N (x) := ∃p q· x = d(p, q). By the above theorem, the theory of metric spaces must therefore admit a primitive recursive reduction of second order arithmetic and hence is undecidable.
Write NS, resp., NSn, resp., NSF, resp., NS∞ for the theories of normed spaces where the dimension is unconstrained, resp., constrained to be n, resp., constrained to be finite, resp., constrained to be infinite, and write BS, BSn etc. for the theories of Banach spaces with the corresponding constraints on the dimension. We have the following theorem which implies that with the exception of NS1 = BS1 (which is the same as the the theory of the real efild) all of these theories are undecidable.
Theorem 3 There is a primitive recursive reduction of second order arithmetic to each of the theories BS, BS∞, NS, NSn = BSn, NSF = BSF, and NS∞ (n ≥ 2).
The proof is based on a construction of a 2-dimensional normed space X in which a certain first order formula denfies the natural numbers as a subset of the field of scalars. By theorem 2, this immediately gives the result for NS2 = BS2 and NSF = BSF. The other parts of the result follow by considering the cartesian product of X and a Hilbert space of appropriate dimension. X is constructed by taking the norm whose unit disc is the “innfiigon” D shown in gfiure 3. D is the convex hull of the set comprising the two vectors ± e1 together with the unit vectors ± vi on the lines through the origin and the points (i, 1), i ∈ Z.
Observing that the points ± vi are the isolated extreme points of the unit disc, while the only non-isolated extreme points are the points ± e1, one finds that the language of normed spaces is sufficiently expressive for us to characterise the set of points (i, 1) for i ∈ Z and then it is easy to give a formula N (x) which denfies the natural numbers in X.
We say a formula is additive if the left operand of all multiplications in the formula are rational constants. With a little care one can arrange for the formula N (x) above to be additive and then with a little more geometric effort, one can give an additive formula M (x, y, z) that in X denfies the graph of the multiplication function × : R × R → R. A variant of theorem 2 can then be used to show that the that even the purely additive fragments of the various theories of normed spaces and Banach spaces are undecidable.
On the positive side for normed spaces, we have the following result on the existence of norms: Theorem 4 Let x1, . . . , xn be vectors in a real vector space V and b1, . . . , bn be real numbers. Then there exists a norm || || on V such that ||xi|| = bi for all 1 ≤ i ≤ n iff: – For all 1 ≤ i ≤ n, bi ≥ 0. – For all 1 ≤ i ≤ n, if bi = 0 then xi = 0 – For each 1 ≤ k ≤ n there are no real numbers c1, . . . , cn such that some xk = Pn i=1 |ci|bi < bk.
i=1 c1xi with Pn
Now a quantifier-free formula P in the language of normed spaces containing k free vector variables has a model iff it has a model of dimension k (since in any model the subspace W spanned by the interpretations of the free vector variables is again a model of dimension n ≤ k and then W × Rk− n gives a model of dimension k). From this observation and theorem 4, one can effectively transform P into a formula in the rfist order language of the real field that is satisfiable iff P is. This gives a decision procedure for purely universal formulae in the language of normed spaces. For purely additive formulae, there is a more efficient procedure which uses a parametrised linear programming algorithm to reduce the problem to linear real arithmetic. An implementation of the latter procedure in HOL Light has proved to be a useful tool. The approach to specicfiation and vericfiation of linear systems presented in section 2 is simple and natural. But even in the simple case of nfiite-dimensional inner product spaces, there are difficult issues to be addressed for mechanized proof support. The decision procedures of section 3 give a starting point, but our undecidability results show that there is much to be done in identifying useful tractable fragments of theories and good heuristics. There are many fascinating challenges ahead for mechanized reasoning in continuous problem domains.
I thank Colin O’Halloran and Nick Tudor of QinetiQ for encouraging and informing my interest in control systems. The approach to reasoning about linear systems is joint work with Ursula Martin, Erik Arne Mathiesen and Paulo Oliva and was supported by EPSRC grants GR/M98340 and GR/L48256. The work on decidability and undecidability for vector spaces is joint work with Robert M. Solovay and John Harrison.