Pith. sign in

REVIEW

On the Hardness of PCTL Satisfiability

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1506.02483 v3 pith:YNHKPVXN submitted 2015-06-08 cs.LO

Souymodip Chakraborty , Joost-Pieter Katoen This is my paper · ORCID
classification cs.LO
keywords pctlsatisfiabilityproblemfragmentalgorithmboundedestablishexponential-time
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
abstract

This paper shows that the satisfiability problem for probabilistic CTL (PCTL, for short) is undecidable. By a reduction from $1\frac{1}{2}$-player games with PCTL winning objectives, we establish that the PCTL satisfiability problem is ${\Sigma}_1^1$-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.

Discussion (0). Continue with ORCID to comment.

Pith tools