Usually, systems properties are defined in terms of the infinite executions which satisfy it. In this work we explore what happens if we allow finite executions in properties de-nitions. In particular, we give a topological interpretation of the safety/liveness classification in the do-mains of: only finite, only infinite and mixed executions. Then we extend our reasoning to hyperproperties, namely sets of sets of executions (or sets of properties). Also in this case we give a topological interpretation of the hypersafety/hyperliveness classification in the three domains.
On topologies for (hyper)properties
Pasqua, M.
;Mastroeni, I.
2017-01-01
Abstract
Usually, systems properties are defined in terms of the infinite executions which satisfy it. In this work we explore what happens if we allow finite executions in properties de-nitions. In particular, we give a topological interpretation of the safety/liveness classification in the do-mains of: only finite, only infinite and mixed executions. Then we extend our reasoning to hyperproperties, namely sets of sets of executions (or sets of properties). Also in this case we give a topological interpretation of the hypersafety/hyperliveness classification in the three domains.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
main.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Pre-print
Licenza:
Dominio pubblico
Dimensione
341.82 kB
Formato
Adobe PDF
|
341.82 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
