2026-08-17T03:43:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12341 2024-03-06T10:50:00Z ddc:004 open_access

A Probabilistic Higher-Order Fixpoint Logic Mitani, Yo Kobayashi, Naoki Tsukada, Takeshi Probabilistic logics higher-order fixpoint logic model checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yo Mitani and Naoki Kobayashi and Takeshi Tsukada 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.19 urn:nbn:de:0030-drops-123413 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.19 eng https://creativecommons.org/licenses/by/3.0/legalcode