Paper Info
Title
Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Abstract
This paper is concerned with proof methods for the temporal property of eventuality (a type of liveness) in systems of polynomial ordinary differential equations (ODEs) evolving under constraints. This problem is of a more general interest to hybrid system verification, where reasoning about temporal properties in the continuous fragment is often a bottleneck. Much of the difficulty in handling continuous systems stems from the fact that closed-form solutions to non-linear ODEs are rarely available. We present a general method for proving eventuality properties that works with the differential equations directly, without the need to compute their solutions. Our method is intuitively simple, yet much less conservative than previously reported approaches, making it highly amenable to use as a rule of inference in a formal proof calculus for hybrid systems.
Year
DOI
Venue
2015
10.1007/978-3-319-19249-9_32
Lecture Notes in Computer Science
Field
DocType
Volume
Ordinary differential equation,Computer science,Theoretical computer science,Real-time computing,Dynamical systems theory,Hybrid system,Rule of inference,Liveness,Formal verification,Hybrid automaton,Formal proof
Conference
9109
ISSN
Citations 
PageRank 
0302-9743
3
0.37
References 
Authors
19
2
Name
Order
Citations
PageRank
Andrew Sogokon1196.16
Paul B. Jackson212814.62