-A A +A

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 CattaruzzaAlessandro Abate

Software:  Axelerator



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.