Series of Abstractions of Hybrid Automata for Monotonic CTL Model Checking

In: International Symposium on Logical Foundations of Computer Science (LFCS '07). New York, U.S.A.. LNCS, Springer, 2007

Authors

• Raffaella Gentilini
• Klaus Schneider
• Bud Mishra

Abstract

"Current symbolic techniques for the automated reasoning on undecidable hybrid automata, force to choose between the refinement of either an overapproximation or an underapproximation of the set of reachable states. When the analysis of branching 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 formulae. In this paper, we deal with the problem of defining series of abstractions of hybrid automata that (1) allow the detection/refinement of both overapproximated and underapproximated reachable sets (2) preserve fully branching temporal properties (interpreted on a dense time domain). Moreover, we ask for our series of abstractions, to satisfy a monotonicity property with respect to the set of model checked formulae."

BibTeX

 
@Proceedings{ GenSchMish07, 
   title = { Series of Abstractions of Hybrid Automata for Monotonic CTL Model Checking }, 
   author = { Raffaella Gentilini and Klaus Schneider and Bud Mishra },   
   booktitle = { International Symposium on Logical Foundations of Computer Science (LFCS '07). New York, U.S.A. },  
   series = { LNCS },      
   publisher = { Springer },      
   year = 2007, 
} 

---

This publication belongs to the project VerSiS.