Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Successive Abstractions of Hybrid Automata for Monotonic
CTL
Model Checking
| |
|
Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking
R. Gentilini2  , K. Schneider2 and B. Mishra1, 3
| (1) |
Courant Institute, New York University, New York, NY, U.S.A. |
| (2) |
University of Kaiserslautern, Department of Computer Science, Germany |
| (3) |
NYU School of Medicine, New York University, New York, NY, U.S.A. |
Abstract
Current symbolic techniques for the automated reasoning over undecidable hybrid automata, force one to choose between the
refinement of either an overapproximation or an underapproximation of the set of reachable states. When the analysis of branching
time temporal properties is considered, the literature has developed a number of abstractions techniques based on the simulation
preorder, that allow the preservation of only true universally quantified formulæ.
This paper suggests a way to surmount these difficulties by defining a succession of abstractions of hybrid automata, which
not only (1) allow the detection and the refinement of both over- and under-approximated reachable sets symmetrically, but
also (2) preserves the full set of branching time temporal properties (when interpreted on a dense time domain). Moreover,
our approach imposes on the corresponding set of abstractions a desirable monotonicity property with respect to the set of
model-checked formulaæ.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|