Hyperproperties are a modern specification paradigm that extends trace properties to express properties of sets of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this paper, we introduce two asynchronous and orthogonal extensions of HyperLTL, namely Stuttering HyperLTL (HyperLTLS) and Con HyperLTL (HyperLTLC). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTLS fragment, coincides with that of the strictly less expressive logic HyperLTL.

Asynchronous Extensions of HyperLTL / Bozzelli, L.; Peron, A.; Sanchez, C.. - 2021-:(2021), pp. 1-13. (Intervento presentato al convegno 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 tenutosi a Roma nel june 29 - july 2 2021) [10.1109/LICS52264.2021.9470583].

Asynchronous Extensions of HyperLTL

Bozzelli L.;Peron A.;
2021

Abstract

Hyperproperties are a modern specification paradigm that extends trace properties to express properties of sets of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this paper, we introduce two asynchronous and orthogonal extensions of HyperLTL, namely Stuttering HyperLTL (HyperLTLS) and Con HyperLTL (HyperLTLC). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTLS fragment, coincides with that of the strictly less expressive logic HyperLTL.
2021
978-1-6654-4895-6
Asynchronous Extensions of HyperLTL / Bozzelli, L.; Peron, A.; Sanchez, C.. - 2021-:(2021), pp. 1-13. (Intervento presentato al convegno 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 tenutosi a Roma nel june 29 - july 2 2021) [10.1109/LICS52264.2021.9470583].
File in questo prodotto:
File Dimensione Formato  
Asynchronous_Extensions_of_HyperLTL.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Versione Editoriale (PDF)
Licenza: Accesso privato/ristretto
Dimensione 1.74 MB
Formato Adobe PDF
1.74 MB 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/11588/858072
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 7
social impact