Unbounded-Time Safety Verification with Abstract Acceleration
Reachability analysis of continuous and discrete time models is a hard problem that has seen much progress in the last decades. In many cases the problem has been reduced to bisimulations with a number of limitations in the nature of the dynamics, soundness, or time horizon.
In this research we focus on sound safety verification of Unbounded-Time Linear Time-Invariant (LTI) models with inputs, over both continuous and discrete time, using reachability analysis. We achieve this using Abstract Acceleration: this over-approximates the reach tube of a model over unbounded time by using abstraction. The technique is applied to a number of discrete- and continuous-time models and the results show good performance when compared to state-of-the-art tools.
Themes: Automated Verification
People: Dario Cattaruzza, Alessandro Abate
Software: Axelerator
Publications:
- Sound Numerical Computations in Abstract Acceleration, , Numerical Software Verification - 10th International Workshop, {NSV} 2017, Heidelberg, Germany, July 22-23, 2017, Proceedings [collocated with {CAV} 2017], p.38–60, (2017)
- Unbounded-Time Analysis of Guarded {LTI} Systems with Inputs by Abstract Acceleration, , Static Analysis - 22nd International Symposium, {SAS} 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, (2015)
GET IN TOUCH WITH US
CONTACT US
Oxford Control and Verification (OXCAV) Group
C/O Department of Computer Science
Wolfson Building, Parks Rd, Oxford OX1 3QD
T: +44 (0) 18656 10767
Education - This is a contributing Drupal Theme
Design by WeebPal.
Design by WeebPal.