Many systems, both natural and artificial, exhibit a mixed discrete-continuous behavior that cannot be fully cap- tured by either continuous nor discrete models: they evolve in accordance to continuous laws, but these laws are controlled by a finite set of modes. Hybrid automata were proposed to represent such kind of behaviors and they have been used to model numerous natural phenomena in the last decades. Unfortunately, the Model Checking problem over them was proved undecidable and, because of that, many techniques were suggested so far to both approximate the original models and reduce the analysis complexity. This paper surveys some of such techniques and reports some open questions.

Model Checking on Hybrid Automata

CASAGRANDE, ALBERTO;
2012-01-01

Abstract

Many systems, both natural and artificial, exhibit a mixed discrete-continuous behavior that cannot be fully cap- tured by either continuous nor discrete models: they evolve in accordance to continuous laws, but these laws are controlled by a finite set of modes. Hybrid automata were proposed to represent such kind of behaviors and they have been used to model numerous natural phenomena in the last decades. Unfortunately, the Model Checking problem over them was proved undecidable and, because of that, many techniques were suggested so far to both approximate the original models and reduce the analysis complexity. This paper surveys some of such techniques and reports some open questions.
2012
978-1-4673-2498-4
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11368/2618036
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact