In this paper, we present a three-valued property driven model checking algorithm for the logic CTL on hybrid automata. The technique of multi-valued 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 above problem, 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.

Property Driven Three-Valued Model Checking on Hybrid Automata

GENTILINI, Raffaella;
2009

Abstract

In this paper, we present a three-valued property driven model checking algorithm for the logic CTL on hybrid automata. The technique of multi-valued 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 above problem, 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.
2009
9783642022609
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11391/174221
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact