Yo Mitani

dblp:268/3672 · DBLP profile ↗
← Back
2ranked-venue papers
2as first author
1since 2021 · last 2021
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 2 · 2 first-author · 1 since 2021
YearPublicationVenuePosition
2021 A Probabilistic Higher-order Fixpoint Logic
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.
Yo Mitani, Naoki Kobayashi 0001, Takeshi Tsukada
Log. Methods Comput. Sci.1
2020 A Probabilistic Higher-Order Fixpoint Logic
Yo Mitani, Naoki Kobayashi 0001, Takeshi Tsukada
FSCD1