On the Hardness of PCTL Satisfiability
Logic in Computer Science
2015-12-01 v3
Abstract
This paper shows that the satisfiability problem for probabilistic CTL (PCTL, for short) is undecidable. By a reduction from -player games with PCTL winning objectives, we establish that the PCTL satisfiability problem is -hard. We present an exponential-time algorithm for the satisfiability of a bounded, negation-closed fragment of PCTL, and show that the satisfiability problem for this fragment is EXPTIME-hard.
Cite
@article{arxiv.1506.02483,
title = {On the Hardness of PCTL Satisfiability},
author = {Souymodip Chakraborty and Joost-Pieter Katoen},
journal= {arXiv preprint arXiv:1506.02483},
year = {2015}
}
Comments
This paper has been withdrawn by the author due to a crucial error in Theorem 2