Computer Laboratory

Technical reports

Automated verification of continuous and hybrid dynamical systems

William Denman

July 2017, 178 pages

This technical report is based on a dissertation submitted September 2014 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Clare College.

Abstract

The standard method used for verifying the behaviour of a dynamical system is simulation. But simulation can check only a finite number of operating conditions and system parameters, leading to a potentially incomplete verification result. This dissertation presents several automated theorem proving based methods that can, in contrast to simulation, completely guarantee the safety of a dynamical system model.

To completely verify a purely continuous dynamical system requires proving a universally quantified first order conjecture, which represents all possible trajectories of the system. Such a closed form solution may contain transcendental functions, rendering the problem undecidable in the general case. The automated theorem prover MetiTarski can be used to solve such a problem by reducing it to one over the real closed fields. The main issue is the doubly exponential complexity of the back-end decision procedures that it depends on. This dissertation proposes several techniques that make the required conjectures easier for MetiTarski to prove. The techniques are shown to be effective at reducing the amount of time required to prove high dimensional problems and are further demonstrated on a flight collision avoidance case study.

For hybrid systems, which contain both continuous and discrete behaviours, a different approach is proposed. In this case, qualitative reasoning is used to abstract the continuous state space into a set of discrete cells. Then, standard discrete state formal verification tools are used to verify properties over the abstraction. MetiTarski is employed to determine the feasibility of the cells and the transitions between them. As these checks are reduced to proving inequalities over the theory of the reals, it facilitates the analysis of nonpolynomial hybrid systems that contain transcendental functions in their vector fields, invariants and guards. This qualitative abstraction framework has been implemented in the QUANTUM tool and is demonstrated on several hybrid system benchmark problems.

Full text

PDF (3.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-910,
  author =	 {Denman, William},
  title = 	 {{Automated verification of continuous and hybrid dynamical
         	   systems}},
  year = 	 2017,
  month = 	 jul,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-910.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-910}
}