Document Open Access Logo

Propositional Dynamic Logic for Hyperproperties

Authors Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.50.pdf
  • Filesize: 0.62 MB
  • 22 pages

Document Identifiers

Author Details

Jens Oliver Gutsfeld
  • Institut für Informatik, Westfälische Wilhelms-Universität Münster, Germany
Markus Müller-Olm
  • Institut für Informatik, Westfälische Wilhelms-Universität Münster, Germany
Christoph Ohrem
  • Institut für Informatik, Westfälische Wilhelms-Universität Münster, Germany

Funding

This work was partially funded by DFG project Model-Checking of Navigation Logics (MoNaLog) (MU 1508/3).

Acknowledgements

We thank the reviewers for their helpful comments.

Cite As Get BibTex

Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Propositional Dynamic Logic for Hyperproperties. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 50:1-50:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.50

Abstract

Information security properties of reactive systems like non-interference often require relating different executions of the system to each other and following them simultaneously. Such hyperproperties can also be useful in other contexts, e.g., when analysing properties of distributed systems like linearizability. Since common logics like LTL, CTL, or the modal μ-calculus cannot express hyperproperties, the hyperlogics HyperLTL and HyperCTL^* were developed to cure this defect. However, these logics are not able to express arbitrary ω-regular properties. In this paper, we introduce HyperPDL-Δ, an adaptation of the Propositional Dynamic Logic of Fischer and Ladner for hyperproperties, in order to remove this limitation. Using an elegant automata-theoretic framework, we show that HyperPDL-Δ model checking is asymptotically not more expensive than HyperCTL^* model checking, despite its vastly increased expressive power. We further investigate fragments of HyperPDL-Δ with regard to satisfiability checking.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
Keywords
  • Hyperlogics
  • Hyperproperties
  • Model Checking
  • Automata

Metrics

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

Related Versions

References

  1. Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, et al. The ForSpec temporal logic: A new temporal property-specification language. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 296-311. Springer, 2002. URL: https://doi.org/10.1007/3-540-46002-0_21.
  2. Borzoo Bonakdarpour, Cesar Sanchez, and Gerardo Schneider. Monitoring hyperproperties by combining static analysis and runtime verification. In International Symposium on Leveraging Applications of Formal Methods, pages 8-27. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03421-4_2.
  3. Borzoo Bonakdarpour and Sarai Sheinvald. Automata for hyperlanguages, 2020. URL: http://arxiv.org/abs/2002.09877.
  4. Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In FoSSaCS, volume 9034 of Lecture Notes in Computer Science, pages 167-182. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_11.
  5. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In POST 2014, pages 265-284, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  6. 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.
  7. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13, 2019. URL: https://doi.org/10.1109/LICS.2019.8785713.
  8. Giuseppe De Giacomo and Moshe Y Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Twenty-Third International Joint Conference on Artificial Intelligence, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  9. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781139236119.
  10. Peter Faymonville and Martin Zimmermann. Parametric linear dynamic logic. Information and Computation, 253:237-256, 2017. GandALF 2014. URL: https://doi.org/10.1016/j.ic.2016.07.009.
  11. Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In CONCUR 2016, pages 13:1-13:14, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.13.
  12. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking HyperLTL and HyperCTL^*. In CAV 2015, pages 30-48, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_3.
  13. Michael J. Fischer and Richard 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.
  14. Joseph Y. Halpern, Ron van der Meyden, and Moshe Y. Vardi. Complete axiomatizations for reasoning about knowledge and time. SIAM J. Comput., 33(3):674-703, 2004. URL: https://doi.org/10.1137/S0097539797320906.
  15. Yonit Kesten and Amir Pnueli. Complete proof system for QPTL. J. Log. Comput., 12(5):701-745, 2002. URL: https://doi.org/10.1093/logcom/12.5.701.
  16. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. Extended temporal logic revisited. In CONCUR 2001, pages 519-535, 2001. URL: https://doi.org/10.1007/3-540-44685-0_35.
  17. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Logic, 2(3):408-429, July 2001. URL: https://doi.org/10.1145/377978.377993.
  18. Martin Lange. Model checking propositional dynamic logic with all extras. J. Applied Logic, 4(1):39-49, 2006. URL: https://doi.org/10.1016/j.jal.2005.08.002.
  19. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on omega-words. Theoretical Computer Science, 32(3):321-330, 1984. URL: https://doi.org/10.1016/0304-3975(84)90049-5.
  20. Markus N. Rabe. A temporal logic approach to Information-flow control. PhD thesis, Saarland University, 2016. URL: https://doi.org/10.22028/D291-26650.
  21. Kristin Y. Rozier and Moshe Y. Vardi. LTL satisfiability checking. In SPIN 2007, pages 149-167, 2007. URL: https://doi.org/10.1007/978-3-540-73370-6_11.
  22. Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1/2):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
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