TY - GEN
T1 - Successive abstractions of hybrid automata for monotonic CTL model checking
AU - Gentilini, R.
AU - Schneider, K.
AU - Mishra, B.
PY - 2007
Y1 - 2007
N2 - 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æ.
AB - 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æ.
UR - http://www.scopus.com/inward/record.url?scp=35448997281&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35448997281&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-72734-7_16
DO - 10.1007/978-3-540-72734-7_16
M3 - Conference contribution
AN - SCOPUS:35448997281
SN - 3540727329
SN - 9783540727323
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 224
EP - 240
BT - Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings
PB - Springer Verlag
T2 - International Symposium on Logical Foundations of Computer Science, LFCS 2007
Y2 - 4 June 2007 through 7 June 2007
ER -