Sciweavers

WOLLIC
2009
Springer

Property Driven Three-Valued Model Checking on Hybrid Automata

13 years 10 months ago
Property Driven Three-Valued Model Checking on Hybrid Automata
Abstract. In this paper, we present a three-valued property driven model checking algorithm for the logic CTL on hybrid automata. The technique of multivalued model checking for hybrid automata aims at combining the advantages of classical methods based either on the preorder of simulation or on bounded reachability. However, as originally defined, it relies on the preliminary definition of special abstractions for combined over- and under-approximated reachability analysis, whose size is crucial and can be infinite. Our procedure avoids the oblem, since it is based on an incremental construction of the abstraction for the original hybrid automaton, that is suitably driven by the property under consideration.
Kerstin Bauer, Raffaella Gentilini, Klaus Schneide
Added 25 May 2010
Updated 25 May 2010
Type Conference
Year 2009
Where WOLLIC
Authors Kerstin Bauer, Raffaella Gentilini, Klaus Schneider
Comments (0)