Bounded satisfiability for PCTL

DOI10.4230/LIPICS.CSL.2012.92zbMATH Open1252.68189arXiv1204.0469OpenAlexW2963957680MaRDI QIDQ4649540FDOQ4649540

Authors: Nathalie Bertrand, John Fearnley, Sven Schewe 

Publication date: 22 November 2012

Abstract: While model checking PCTL for Markov chains is decidable in polynomial-time, the decidability of PCTL satisfiability, as well as its finite model property, are long standing open problems. While general satisfiability is an intriguing challenge from a purely theoretical point of view, we argue that general solutions would not be of interest to practitioners: such solutions could be too big to be implementable or even infinite. Inspired by bounded synthesis techniques, we turn to the more applied problem of seeking models of a bounded size: we restrict our search to implementable -- and therefore reasonably simple -- models. We propose a procedure to decide whether or not a given PCTL formula has an implementable model by reducing it to an SMT problem. We have implemented our techniques and found that they can be applied to the practical problem of sanity checking -- a procedure that allows a system designer to check whether their formula has an unexpectedly small model.

Full work available at URL: https://arxiv.org/abs/1204.0469

Recommendations

• On the satisfiability of some simple probabilistic logics
• The satisfiability problem for unbounded fragments of probabilistic CTL
• Bounded model checking using satisfiability solving
• Bounded model checking for propositional projection temporal logic
• Verifying pCTL model checking

zbMATH Keywords

satisfiabilitytemporal logicprobabilistic logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cited In (6)

• Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
• The satisfiability problem for a quantitative fragment of PCTL
• The satisfiability problem for a quantitative fragment of PCTL
• Satisfiability of quantitative probabilistic CTL: rise to the challenge
• Title not available (Why is that?)
• Baire Category Quantifier in Monadic Second Order Logic

This page was built for publication: Bounded satisfiability for PCTL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649540)