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;MANDRIOLI, DINO;MORZENTI, ANGELO CARLO;ROSSI, MATTEO GIOVANNI
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.File | Dimensione | Formato | |
---|---|---|---|
06311118.pdf
Accesso riservato
:
Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione
237.63 kB
Formato
Adobe PDF
|
237.63 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.