Paper Info
Title
SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
Abstract
In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving ordinary differential equations (ODEs), we provide a seamless integration of safe numeric overapproximation of initial-value problems into a SAT-modulo-theory (SMT) approach to interval-based arithmetic constraint solving. Interval-based safe numeric approximation of ODEs is used as an interval contractor being able to narrow candidate sets in phase space in both temporal directions: post-images of ODEs (i.e., sets of states reachable from a set of initial values) are narrowed based on partial information about the initial values and, vice versa, pre-images are narrowed based on partial knowledge about post-sets.In contrast to the related CLP(F) approach of Hickey and Wittenberg [12], we do (a) support coordinate transformations mitigating the wrapping effect encountered upon iterating interval-based overapproximations of reachable state sets and (b) embed the approach into an SMT framework, thus accelerating the solving process through the algorithmic enhancements of recent SAT solving technology.
Year
DOI
Venue
2008
10.1007/978-3-540-88387-6_14
ATVA
Keywords
Field
DocType
hybrid systems,safe numeric overapproximation,partial knowledge,non-linear arithmetic constraint,interval-based arithmetic constraint,smt framework,reachable state set,initial value,partial information,sat modulo ode,direct sat approach,interval-based overapproximations,interval-based safe numeric approximation,differential equation,initial value problem,automated reasoning,hybrid system,phase space
Discrete mathematics,Automated reasoning,Ordinary differential equation,Modulo,Computer science,Phase space,Hybrid system,Ode
Conference
Volume
ISSN
Citations 
5311
0302-9743
28
PageRank 
References 
Authors
1.20
9
3
Name
Order
Citations
PageRank
Andreas Eggers1995.68
Martin Fränzle278661.58
Christian Herde333815.19