The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
Jan K\v{r}et\'insk\'y, Alexej Rotar
TL;DR
This paper explores the decidability of the satisfiability problem for unbounded fragments of probabilistic CTL, identifying decidable cases and highlighting challenges in more complex fragments.
Contribution
It establishes decidability results for certain unbounded PCTL fragments and discusses open problems in more complex cases.
Findings
Decidability established for specific PCTL fragments with quantitative operators.
Identification of complexities preventing decidability in certain fragments.
Open problems highlighted for future research.
Abstract
We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establish decidability for several fragments containing quantitative operators and pinpoint the difficulties arising in more complex fragments where the decidability remains open.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.