Document Open Access Logo

Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties

Authors Laura Bozzelli, Adriano Peron, César Sánchez

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.27.pdf
  • Filesize: 0.82 MB
  • 16 pages

Document Identifiers

Author Details

Laura Bozzelli
  • University of Napoli "Federico II", Italy
Adriano Peron
  • University of Napoli "Federico II", Italy
César Sánchez
  • IMDEA Software Institute, Madrid, Spain

Funding

  • Sánchez, César: funded in part by the Madrid Regional Government under project "S2018/TCS-4339 (BLOQUES-CM)" and by a research grant from Nomadic Labs and the Tezos Foundation.

Cite AsGet BibTex

Laura Bozzelli, Adriano Peron, and César Sánchez. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.27

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 (HyperLTL_C), 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 HyperLTL_C.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Hyperproperties
  • Asynchronous hyperproperties
  • Temporal logics for hyperproperties
  • Expressiveness
  • Decidability
  • Model checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. E. Bartocci, T. Ferrère, T.A. Henzinger, D. Nickovic, and A.O. da Costa. Flavors of Sequential Information Flow. In Proc. 23rd VMCAI, volume 13182 of LNCS, pages 1-19. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-94583-1_1.
  2. J. Baumeister, N. Coenen, B. Bonakdarpour, B. Finkbeiner, and C. Sánchez. A Temporal Logic for Asynchronous Hyperproperties. In Proc. 33rd CAV, LNCS 12759, pages 694-717. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_33.
  3. R. Beutner and B. Finkbeiner. A Logic for Hyperproperties in Multi-Agent Systems. CoRR, abs/2203.07283, 2022. URL: https://doi.org/10.48550/arXiv.2203.07283.
  4. B. Bonakdarpour, C. Sánchez, and G. Schneider. Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. In Proc. 8th ISoLA, LNCS 11245, pages 8-27. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03421-4_2.
  5. L. Bozzelli, B. Maubert, and S. Pinchinat. Unifying Hyper and Epistemic Temporal Logics. In Proc. 18th FoSSaCS, LNCS 9034, pages 167-182. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_11.
  6. L. Bozzelli, A. Peron, and C. Sánchez. Asynchronous Extensions of HyperLTL. In Proc. 36th LICS, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470583.
  7. L. Bozzelli, A. Peron, and C. Sánchez. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. CoRR, abs/2207.02956, 2022. URL: https://doi.org/10.48550/arXiv.2207.02956.
  8. M.R. Clarkson, B. Finkbeiner, M. Koleini, K.K. Micinski, M.N. Rabe, and C. Sánchez. Temporal Logics for Hyperproperties. In Proc. 3rd POST, LNCS 8414, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  9. M.R. Clarkson and F.B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  10. N. Coenen, B. Finkbeiner, C. Hahn, and J. Hofmann. The hierarchy of hyperlogics. In Proc. 34th LICS, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785713.
  11. R. Dimitrova, B. Finkbeiner, M. Kovács, M.N. Rabe, and H. Seidl. Model Checking Information Flow in Reactive Systems. In Proc. 13th VMCAI, LNCS 7148, pages 169-185. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27940-9_12.
  12. E.A. Emerson and J.Y. Halpern. "Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  13. B. Finkbeiner and C. Hahn. Deciding Hyperproperties. In Proc. 27th CONCUR, LIPIcs 59, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  14. B. Finkbeiner, C. Hahn, P. Lukert, M. Stenger, and L. Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137-163, 2020. URL: https://doi.org/10.1007/s00236-019-00358-2.
  15. B. Finkbeiner, M.N. Rabe, and C. Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL*. In Proc. 27th CAV Part I, LNCS 9206, pages 30-48. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_3.
  16. B. Finkbeiner and M. Zimmermann. The first-order logic of hyperproperties. In Proc. 34th STACS, LIPIcs 66, pages 30:1-30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.30.
  17. M.J. Fischer and R.E. Ladner. Propositional Dynamic Logic of Regular Programs. J. Comput. Syst. Sci., 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  18. J.A. Goguen and J. Meseguer. Security Policies and Security Models. In IEEE Symposium on Security and Privacy, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  19. J.O. Gutsfeld, A. Meier, C. Ohrem, and J. Virtema. Temporal Team Semantics Revisited. CoRR, abs/2110.12699, 2021. URL: https://doi.org/10.48550/arXiv.2110.12699.
  20. J.O. Gutsfeld, M. Müller-Olm, and C. Ohrem. Deciding Asynchronous Hyperproperties for Recursive Programs. CoRR, abs/2201.12859, 2022. URL: https://doi.org/10.48550/arXiv.2201.12859.
  21. J.Oliver. Gutsfeld, M. Müller-Olm, and C. Ohrem. Propositional dynamic logic for hyperproperties. In Proc. 31st CONCUR, LIPIcs 171, pages 50:1-50:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.50.
  22. J.Oliver. Gutsfeld, M. Müller-Olm, and C. Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 4(POPL), 2021. URL: https://doi.org/10.1145/3434319.
  23. D. Harel. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM, 33(1):224-248, 1986. URL: https://doi.org/10.1145/4904.4993.
  24. A. Krebs, A. Meier, J. Virtema, and M. Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In Proc. 43rd MFCS, LIPIcs 117, pages 10:1-10:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.10.
  25. M. Lück. On the complexity of linear temporal logic with team semantics. Theor. Comput. Sci., 837:1-25, 2020. URL: https://doi.org/10.1016/j.tcs.2020.04.019.
  26. J. McLean. A General Theory of Composition for a Class of "Possibilistic" Properties. IEEE Trans. Software Eng., 22(1):53-67, 1996. URL: https://doi.org/10.1109/32.481534.
  27. A. Pnueli. The Temporal Logic of Programs. In Proc. 18th FOCS, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  28. M.N. Rabe. A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016. Google Scholar
  29. A.P. Sistla, M.Y. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49:217-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90008-9.
  30. M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. URL: https://doi.org/10.1006/inco.1994.1092.
  31. J. Virtema, J. Hofmann, B. Finkbeiner, J. Kontinen, and F. Yang. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In Proc. 41st IARCS FSTTCS, LIPIcs 213, pages 52:1-52:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.52.
  32. S. Zdancewic and A.C. Myers. Observational Determinism for Concurrent Program Security. In Proc. 16th IEEE CSFW-16, pages 29-43. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/CSFW.2003.1212703.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact