The model-checking problem for hybrid systems is a well known challenge in the scientific community. Most of the existing approaches and tools are limited to safety properties only, or operates by transforming the hybrid system to be verified into a discrete one, thus loosing information on the continuous dynamics of the system. In this paper we present a logic for specifying complex properties of hybrid systems called HyLTL, and we show how it is possible to solve the model checking problem by translating the formula into an equivalent hybrid automaton. In this way the problem is reduced to a reachability problem on hybrid automata that can be solved by using existing tools.

HyLTL: a temporal logic for model checking hybrid systems / D. Bresolin. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - ELETTRONICO. - 124:(2013), pp. 73-84. (Intervento presentato al convegno 3rd International Workshop on Hybrid Autonomous Systems (HAS 2013) tenutosi a Roma nel 2013) [10.4204/EPTCS.124.8].

HyLTL: a temporal logic for model checking hybrid systems

BRESOLIN, DAVIDE
2013

Abstract

The model-checking problem for hybrid systems is a well known challenge in the scientific community. Most of the existing approaches and tools are limited to safety properties only, or operates by transforming the hybrid system to be verified into a discrete one, thus loosing information on the continuous dynamics of the system. In this paper we present a logic for specifying complex properties of hybrid systems called HyLTL, and we show how it is possible to solve the model checking problem by translating the formula into an equivalent hybrid automaton. In this way the problem is reduced to a reachability problem on hybrid automata that can be solved by using existing tools.
2013
3rd International Workshop on Hybrid Autonomous Systems (HAS 2013)
73
84
HyLTL: a temporal logic for model checking hybrid systems / D. Bresolin. - In: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. - ISSN 2075-2180. - ELETTRONICO. - 124:(2013), pp. 73-84. (Intervento presentato al convegno 3rd International Workshop on Hybrid Autonomous Systems (HAS 2013) tenutosi a Roma nel 2013) [10.4204/EPTCS.124.8].
D. Bresolin
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/371956
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

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