Successive abstractions of hybrid automata for monotonic CTL model checking

R. Gentilini, K. Schneider, B. Mishra

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


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
PublisherSpringer Verlag
Number of pages17
ISBN (Print)3540727329, 9783540727323
StatePublished - 2007
EventInternational Symposium on Logical Foundations of Computer Science, LFCS 2007 - New York, NY, United States
Duration: Jun 4 2007Jun 7 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4514 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


OtherInternational Symposium on Logical Foundations of Computer Science, LFCS 2007
Country/TerritoryUnited States
CityNew York, NY

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Successive abstractions of hybrid automata for monotonic CTL model checking'. Together they form a unique fingerprint.

Cite this