Name
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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.46298/LMCS-17(4:15)2021 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
Probabilistic logics, higher-order fixpoint logic, model checking | Journal | 17 |
Issue | ISSN | Citations |
4 | 1860-5974 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yo Mitani | 1 | 0 | 0.34 |
| Naoki Kobayashi | 2 | 1172 | 75.17 |
| Takeshi Tsukada | 3 | 0 | 2.03 |