Many industrial systems include components interacting with each other that evolve with possibly very different speeds. To deal with this situation many formalisms adopt the abstraction of ``zero-time transitions'', which do not consume time. These, however, have several drawbacks in terms of naturalness and logic consistency, as a system is modeled to be in different states at the same time. We introduce a metric temporal logic, called X-TRIO, that uses non-standard analysis to elegantly deal with zero-time transitions in an abstract, descriptive way. We study the decidability of the logic, and we introduce a decision procedure for a subset thereof. X-TRIO has been applied in companion works to the design and verification of industrial systems.

A Metric Temporal Logic for Dealing with Zero-Time Transitions

FERRUCCI, LUCA;
2012-01-01

Abstract

Many industrial systems include components interacting with each other that evolve with possibly very different speeds. To deal with this situation many formalisms adopt the abstraction of ``zero-time transitions'', which do not consume time. These, however, have several drawbacks in terms of naturalness and logic consistency, as a system is modeled to be in different states at the same time. We introduce a metric temporal logic, called X-TRIO, that uses non-standard analysis to elegantly deal with zero-time transitions in an abstract, descriptive way. We study the decidability of the logic, and we introduce a decision procedure for a subset thereof. X-TRIO has been applied in companion works to the design and verification of industrial systems.
2012
9781467326599
File in questo prodotto:
File Dimensione Formato  
A metric temporal logic.pdf

solo utenti autorizzati

Tipologia: Versione finale editoriale
Licenza: NON PUBBLICO - accesso privato/ristretto
Dimensione 237.63 kB
Formato Adobe PDF
237.63 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11568/1166191
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? ND
social impact