Logo del repository
  1. Home
 
Opzioni

Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties

Bozzelli L.
•
Peron A.
•
Sanchez C.
2022
  • conference object

Abstract
Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of these logics together with the extension S1S[E] of S1S with the equal-level predicate by obtaining an almost complete expressiveness picture. We also study the expressive power of these logics when interpreted on singleton sets of traces. We show that for two asynchronous extensions of HyperLTL, checking the existence of a singleton model is already undecidable, and for one of them, namely Context HyperLTL (HyperLTLC), we establish a characterization of the singleton models in terms of the extension of standard FO[<] over traces with addition. This last result generalizes the well-known equivalence between FO[<] and LTL. Finally, we identify new boundaries on the decidability of model checking HyperLTLC
DOI
10.4230/LIPIcs.CONCUR.2022.27
Archivio
https://hdl.handle.net/11368/3032701
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85138743075
https://drops.dagstuhl.de/opus/volltexte/2022/17090/
Diritti
open access
license:creative commons
license uri:http://creativecommons.org/licenses/by/4.0/
FVG url
https://arts.units.it/bitstream/11368/3032701/1/LIPIcs-CONCUR-2022-27.pdf
Soggetti
  • Asynchronous HyperLTL...

  • Expressiveness

google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback