This paper surveys hybrid automata and bisimulation relations. We formally introduce both notions and briefly present the model checking problem over hybrid automata. We show how, in some cases, bisimulations can be used to quotient infinite state systems to finite ones and, hence, we reduce the model checking over hybrid automata to model checking over finite models. Finally, we review some classes of hybrid automata which admit finite bisimulation quotients.

Hybrid Automata and Bisimulation

CASAGRANDE, ALBERTO
2010-01-01

Abstract

This paper surveys hybrid automata and bisimulation relations. We formally introduce both notions and briefly present the model checking problem over hybrid automata. We show how, in some cases, bisimulations can be used to quotient infinite state systems to finite ones and, hence, we reduce the model checking over hybrid automata to model checking over finite models. Finally, we review some classes of hybrid automata which admit finite bisimulation quotients.
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/2337246
 Avviso

Registrazione in corso di verifica.
La registrazione di questo prodotto non è ancora stata validata in ArTS.

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact