A Probabilistic Higher-order Fixpoint Logic

TL;DR

This paper introduces PHFL, a probabilistic higher-order fixpoint logic, demonstrating its greater expressiveness over existing logics and analyzing the complexity and decidability of its model-checking problems.

Contribution

The paper presents PHFL as a new probabilistic higher-order logic, proves its increased expressiveness, and characterizes a decidable fragment with a novel type system.

Findings

PHFL is strictly more expressive than the $0$-p calculus.

Model-checking PHFL on finite Markov chains is undecidable for certain fragments.

A decidable fragment of PHFL is characterized using a new type system.

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.