Document Open Access Logo

A Probabilistic Higher-Order Fixpoint Logic

Authors Yo Mitani, Naoki Kobayashi , Takeshi Tsukada

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2020.19.pdf
  • Filesize: 0.57 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Probabilistic logics
  • higher-order fixpoint logic
  • model checking

Metrics

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

Abstract

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the μ^p-calculus. We show that PHFL is strictly more expressive than the μ^p-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the μ-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky’s μ-arithmetic to PHFL, which implies that PHFL model checking is Π^1₁-hard and Σ^1₁-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.

Cite As Get BibTex

Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada. A Probabilistic Higher-Order Fixpoint Logic. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.19

Author Details

Yo Mitani
  • The University of Tokyo, Japan
Naoki Kobayashi
  • The University of Tokyo, Japan
Takeshi Tsukada
  • The University of Tokyo, Japan

Funding

This work was supported by JSPS KAKENHI Grant Number JP15H05706 and 20H00577.

Acknowledgements

We would like to thank anonymous referees for useful comments.

References

  1. Roland Axelsson, Martin Lange, and Rafal Somla. The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science, 3(2), 2007. URL: https://doi.org/10.2168/LMCS-3(2:7)2007.
  2. Pablo F. Castro, Cecilia Kilmurray, and Nir Piterman. Tractable probabilistic mu-calculus that expresses probabilistic temporal logics. In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 211-223. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.211.
  3. Kousha Etessami and Mihalis Yannakakis. Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM, 56(1):1:1-1:66, 2009. URL: https://doi.org/10.1145/1462153.1462154.
  4. Nathanaël Fijalkow. Undecidability results for probabilistic automata. SIGLOG News, 4(4):10-17, 2017. URL: https://dl.acm.org/citation.cfm?id=3157833.
  5. Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi, and Youssouf Oualhadj. Deciding the value 1 problem for probabilistic leaktight automata. Logical Methods in Computer Science, 11(2), 2015. URL: https://doi.org/10.2168/LMCS-11(2:12)2015.
  6. Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 527-538. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_44.
  7. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Asp. Comput., 6(5):512-535, 1994. URL: https://doi.org/10.1007/BF01211866.
  8. David 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.
  9. Michael Huth and Marta Z. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 111-122. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614940.
  10. Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. On the termination problem for probabilistic higher-order recursive programs. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-14. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785679.
  11. Naoki Kobayashi, Étienne Lozes, and Florian Bruse. On the relationship between higher-order recursion schemes and higher-order fixpoint logic. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 246-259. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3009854.
  12. Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. Higher-order program verification via HFL model checking. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 711-738. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_25.
  13. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  14. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  15. Étienne Lozes. A type-directed negation elimination. In Ralph Matthes and Matteo Mio, editors, Proceedings Tenth International Workshop on Fixed Points in Computer Science, FICS 2015, Berlin, Germany, September 11-12, 2015, volume 191 of EPTCS, pages 132-142, 2015. URL: https://doi.org/10.4204/EPTCS.191.12.
  16. Robert S. Lubarsky. mu-definable sets of integers. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 343-352. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39189.
  17. Matteo Mio and Alex Simpson. Łukasiewicz mu-calculus. In David Baelde and Arnaud Carayol, editors, Proceedings Workshop on Fixed Points in Computer Science, FICS 2013, Turino, Italy, September 1st, 2013, volume 126 of EPTCS, pages 87-104, 2013. URL: https://doi.org/10.4204/EPTCS.126.7.
  18. Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada. A probabilistic higher-order fixpoint logic, 2020. A full version, available from URL: http://www.kb.is.s.u-tokyo.ac.jp/~mitaniyo/papers/fscd2020-long.pdf.
  19. Carroll Morgan and Annabelle McIver. A probabilistic temporal calculus based on expectations. In Proc. Formal Methods Pacific, pages 4-22. Springer, 1997. Google Scholar
  20. Azaria Paz. Introduction to probabilistic automata. Academic Press, 1971. Google Scholar
  21. Michael O Rabin. Probabilistic automata. Information and control, 6(3):230-245, 1963. Google Scholar
  22. Mahesh Viswanathan and Ramesh Viswanathan. A higher order modal fixed point logic. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 512-528. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_33.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact