A Probabilistic Higher-order Fixpoint Logic

11/29/2020
by   Yo Mitani, et al.
0

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_1-hard and Σ^1_1-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset