Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration

Dario Cattaruzza; Alessandro Abate; Peter Schrammel; Daniel Kroening

doi:10.1007/s10817-020-09562-z

Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration

J Autom Reason. 2021;65(2):157-203. doi: 10.1007/s10817-020-09562-z. Epub 2020 May 29.

Authors

Dario Cattaruzza¹, Alessandro Abate¹, Peter Schrammel², Daniel Kroening¹

Affiliations

¹ Department of Computer Science, University of Oxford, Oxford, UK.
² School of Engineering and Informatics, University of Sussex, Brighton, UK.

Abstract

Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools.

Keywords: Abstract acceleration; CEGAR; Dynamical models; Invariant generation; LTI models; Reachability computation; Safety analysis.