Yo Mitani ; Naoki Kobayashi ; Takeshi Tsukada - A Probabilistic Higher-order Fixpoint Logic

lmcs:6939 - Logical Methods in Computer Science, December 2, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:15)2021
A Probabilistic Higher-order Fixpoint LogicArticle

Authors: Yo Mitani ; Naoki Kobayashi ; Takeshi Tsukada

    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.


    Volume: Volume 17, Issue 4
    Published on: December 2, 2021
    Accepted on: October 4, 2021
    Submitted on: December 1, 2020
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1011 times.
    This article's PDF has been downloaded 232 times.