References & Citations
Computer Science > Logic in Computer Science
Title: A Probabilistic Higher-order Fixpoint Logic
(Submitted on 29 Nov 2020 (v1), last revised 1 Dec 2021 (this version, v4))
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 $\mu^p$-calculus. We show that PHFL is strictly more expressive than the $\mu^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $\mu$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $\mu$-arithmetic to PHFL, which implies that PHFL model checking is $\Pi^1_1$-hard and $\Sigma^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.
Submission history
From: Naoki Kobayashi [view email] [via LOGICAL proxy][v1] Sun, 29 Nov 2020 07:31:00 GMT (113kb)
[v2] Wed, 16 Jun 2021 14:01:59 GMT (176kb,D)
[v3] Wed, 13 Oct 2021 10:11:59 GMT (176kb,D)
[v4] Wed, 1 Dec 2021 08:34:17 GMT (182kb,D)
Link back to: arXiv, form interface, contact.