Successive abstractions of hybrid automata for monotonic CTL model checking

R. Gentilini, K. Schneider, Bhubaneswar Mishra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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æ.

Original languageEnglish (US)
Title of host publicationLogical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings
Pages224-240
Number of pages17
Volume4514 LNCS
StatePublished - 2007
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2007 - New York, NY, United States
Duration: Jun 4 2007Jun 7 2007

Other

OtherInternational Symposium on Logical Foundations of Computer Science, LFCS 2007
CountryUnited States
CityNew York, NY
Period6/4/076/7/07

Fingerprint

Hybrid Automata
Model checking
Monotonic
Model Checking
Branching
Refinement
Reachable Set
Automated Reasoning
Preorder
Preservation
Monotonicity
Time Domain
Choose
Abstraction
Simulation

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Gentilini, R., Schneider, K., & Mishra, B. (2007). Successive abstractions of hybrid automata for monotonic CTL model checking. In Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings (Vol. 4514 LNCS, pp. 224-240)

Successive abstractions of hybrid automata for monotonic CTL model checking. / Gentilini, R.; Schneider, K.; Mishra, Bhubaneswar.

Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings. Vol. 4514 LNCS 2007. p. 224-240.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Gentilini, R, Schneider, K & Mishra, B 2007, Successive abstractions of hybrid automata for monotonic CTL model checking. in Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings. vol. 4514 LNCS, pp. 224-240, International Symposium on Logical Foundations of Computer Science, LFCS 2007, New York, NY, United States, 6/4/07.
Gentilini R, Schneider K, Mishra B. Successive abstractions of hybrid automata for monotonic CTL model checking. In Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings. Vol. 4514 LNCS. 2007. p. 224-240
Gentilini, R. ; Schneider, K. ; Mishra, Bhubaneswar. / Successive abstractions of hybrid automata for monotonic CTL model checking. Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings. Vol. 4514 LNCS 2007. pp. 224-240
@inproceedings{2bcc3397fe1740278be3e573a5d1126b,
title = "Successive abstractions of hybrid automata for monotonic CTL model checking",
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{\ae}. 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{\ae}.",
author = "R. Gentilini and K. Schneider and Bhubaneswar Mishra",
year = "2007",
language = "English (US)",
isbn = "3540727329",
volume = "4514 LNCS",
pages = "224--240",
booktitle = "Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings",

}

TY - GEN

T1 - Successive abstractions of hybrid automata for monotonic CTL model checking

AU - Gentilini, R.

AU - Schneider, K.

AU - Mishra, Bhubaneswar

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

M3 - Conference contribution

SN - 3540727329

SN - 9783540727323

VL - 4514 LNCS

SP - 224

EP - 240

BT - Logical Foundations of Computer Science - International Symposium, LFCS 2007, Proceedings

ER -