Space-time interpolants Conference Paper


Author(s): Frehse, Goran; Giacobbe, Mirco; Henzinger, Thomas A
Title: Space-time interpolants
Title Series: LNCS
Affiliation IST Austria
Abstract: Reachability analysis is difficult for hybrid automata with affine differential equations, because the reach set needs to be approximated. Promising abstraction techniques usually employ interval methods or template polyhedra. Interval methods account for dense time and guarantee soundness, and there are interval-based tools that overapproximate affine flowpipes. But interval methods impose bounded and rigid shapes, which make refinement expensive and fixpoint detection difficult. Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded, but sound template refinement for unbounded reachability analysis has been implemented only for systems with piecewise constant dynamics. We capitalize on the advantages of both techniques, combining interval arithmetic and template polyhedra, using the former to abstract time and the latter to abstract space. During a CEGAR loop, whenever a spurious error trajectory is found, we compute additional space constraints and split time intervals, and use these space-time interpolants to eliminate the counterexample. Space-time interpolation offers a lazy, flexible framework for increasing precision while guaranteeing soundness, both for error avoidance and fixpoint detection. To the best of out knowledge, this is the first abstraction refinement scheme for the reachability analysis over unbounded and dense time of affine hybrid systems, which is both sound and automatic. We demonstrate the effectiveness of our algorithm with several benchmark examples, which cannot be handled by other tools.
Keywords: abstraction refinement; Hybrid systems; Abstracting; Geometry; Interpolation; Differential equations; Flexible framework; Reachability analysis; Computer aided analysis; Computer circuits; Interval arithmetic; Computer programming languages; Abstraction techniques; Affine hybrid systems; Error trajectories; Piece-wise constants
Conference Title: CAV: Computer Aided Verification
Volume: 10981
Conference Dates: 14 - 17 July, 2018
Conference Location: Oxford, UK
ISBN: 03029743 (ISSN); 9783319961446 (ISBN)
Publisher: Springer  
Date Published: 2018-07-18
Start Page: 468
End Page: 486
Copyright Statement: CC BY 4.0
DOI: 10.1007/978-3-319-96145-3_25
Notes: Research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the European Commission under grant 643921 (UnCoVerCPS).
Open access: yes (OA journal)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work