Tino Teige ; Martin Fränzle - Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability

lmcs:1031 - Logical Methods in Computer Science, June 26, 2012, Volume 8, Issue 2 - https://doi.org/10.2168/LMCS-8(2:16)2012
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region StabilityArticle

Authors: Tino Teige ; Martin Fränzle ORCID

    The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpolation, we address the symbolic analysis of probabilistic systems. We first investigate the use of interpolation in probabilistic state reachability analysis, turning the falsification procedure employing PBMC into a verification technique for probabilistic safety properties. We furthermore propose an interpolation-based approach to probabilistic region stability, being able to verify that the probability of stabilizing within some region is sufficiently large.


    Volume: Volume 8, Issue 2
    Published on: June 26, 2012
    Imported on: October 12, 2011
    Keywords: Computer Science - Logic in Computer Science,D.2.4,F.3.1,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Modeling, verification and control of complex systems: From foundations to power network applications; Funder: European Commission; Code: 257005

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1503 times.
    This article's PDF has been downloaded 483 times.