Hybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance. We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.

HRELTL: A temporal logic for hybrid systems / Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 245:(2015), pp. 54-71. [http://dx.doi.org/10.1016/j.ic.2015.06.006]

HRELTL: A temporal logic for hybrid systems

Cimatti Alessandro;Roveri Marco;Tonetta Stefano
2015-01-01

Abstract

Hybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance. We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.
2015
Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano
HRELTL: A temporal logic for hybrid systems / Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 245:(2015), pp. 54-71. [http://dx.doi.org/10.1016/j.ic.2015.06.006]
File in questo prodotto:
File Dimensione Formato  
HRELTL-A-temporal-logic-for-hybrid-systems2015Information-and-Computation.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 565.64 kB
Formato Adobe PDF
565.64 kB Adobe PDF   Visualizza/Apri

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/11572/258655
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 16
social impact