Document Open Access Logo

The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas

Authors Corto Mascle, Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.29.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Corto Mascle
  • ENS Paris-Saclay, Cachan, France
Martin Zimmermann
  • University of Liverpool, Liverpool, United Kingdom

Funding

Partially funded by EPSRC grant EP/S032207/1.

Cite As Get BibTex

Corto Mascle and Martin Zimmermann. The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.29

Abstract

HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border.
First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Hyperproperties
  • Linear Temporal Logic
  • Satisfiability

Metrics

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

Related Versions

References

  1. Shreya Agrawal and Borzoo Bonakdarpour. Runtime Verification of k-Safety Hyperproperties in HyperLTL. In CSF 2016, pages 239-252. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/CSF.2016.24.
  2. Borzoo Bonakdarpour and Bernd Finkbeiner. Runtime Verification for HyperLTL. In Yliès Falcone and César Sánchez, editors, RV 2016, volume 10012 of LNCS, pages 41-45. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46982-9_4.
  3. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal Logics for Hyperproperties. In Martín Abadi and Steve Kremer, editors, POST 2014, volume 8414 of LNCS, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  4. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  5. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In LICS 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785713.
  6. Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Isil Dillig and Serdar Tasiran, editors, CAV 2019, volume 11561 of LNCS, pages 121-139. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_7.
  7. Stéphane Demri and Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Inf. Comput., 174(1):84-103, 2002. URL: https://doi.org/10.1006/inco.2001.3094.
  8. Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. In Josée Desharnais and Radha Jagadeesan, editors, CONCUR 2016, volume 59 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  9. Bernd Finkbeiner, Christopher Hahn, and Tobias Hans. MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the ∃^*∀^* Fragment. In Shuvendu K. Lahiri and Chao Wang, editors, ATVA 2018, volume 11138 of LNCS, pages 521-527. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_31.
  10. Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesizing Reactive Systems from Hyperproperties. In Hana Chockler and Georg Weissenbacher, editors, CAV 2018 (Part I), volume 10981 of LNCS, pages 289-306. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_16.
  11. Bernd Finkbeiner, Christopher Hahn, and Marvin Stenger. EAHyper: Satisfiability, implication, and equivalence checking of hyperproperties. In Rupak Majumdar and Viktor Kuncak, editors, CAV 2017 (Part II), volume 10427 of LNCS, pages 564-570. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_29.
  12. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A runtime verification tool for temporal hyperproperties. In Dirk Beyer and Marieke Huisman, editors, TACAS 2018 (Part II), volume 10806 of LNCS, pages 194-200. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_11.
  13. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL^*. In Daniel Kroening and Corina S. Pasareanu, editors, CAV 2015 (Part I), volume 9206 of LNCS, pages 30-48. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_3.
  14. Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. In Heribert Vollmer and Brigitte Vallée, editors, STACS 2017, volume 66 of LIPIcs, pages 30:1-30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.30.
  15. Joseph A. Goguen and José Meseguer. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  16. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, and Victor Vianu. On the unusual effectiveness of logic in computer science. Bulletin of Symbolic Logic, 7(2):213-236, 2001. URL: https://doi.org/10.2307/2687775.
  17. Philip K. Hooper. The undecidability of the Turing machine immortality problem. J. Symb. Log., 31(2):219-234, 1966. URL: https://doi.org/10.2307/2269811.
  18. Robert P. Kurshan. Transfer of Model Checking to Industrial Practice. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking., pages 763-793. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_23.
  19. Daryl McCullough. Noninterference and the composability of security properties. In 1988 IEEE Symposium on Security and Privacy, pages 177-186. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SECPRI.1988.8110.
  20. Daryl McCullough. A Hookup Theorem for Multilevel Security. IEEE Trans. Software Eng., 16(6):563-568, 1990. URL: https://doi.org/10.1109/32.55085.
  21. John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 79-93. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/RISP.1994.296590.
  22. Jonathan K. Millen. Unwinding Forward Correctability. Journal of Computer Security, 3(1):35-54, 1995. URL: https://doi.org/10.3233/JCS-1994/1995-3104.
  23. Amir Pnueli. The Temporal Logic of Programs. In FOCS 1977, pages 46-57, 1977. Google Scholar
  24. Sylvain Schmitz. Complexity Hierarchies beyond Elementary. TOCT, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  25. A. Prasad Sistla and Edmund M. Clarke. The Complexity of Propositional Linear Temporal Logics. Journal of the ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  26. Larry J. Stockmeyer and Albert R. Meyer. Word Problems Requiring Exponential Time: Preliminary Report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, STOC 1973, pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
  27. Steve Zdancewic and Andrew C. Myers. Observational Determinism for Concurrent Program Security. In CSFW 2003, page 29. 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 About DROPS Imprint Privacy Contact