{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:12Z","timestamp":1753889772934,"version":"3.41.2"},"reference-count":34,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,26]],"date-time":"2012-06-26T00:00:00Z","timestamp":1340668800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["257005"],"award-info":[{"award-number":["257005"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The stochastic Boolean satisfiability (SSAT) problem has been introduced by\nPapadimitriou in 1985 when adding a probabilistic model of uncertainty to\npropositional satisfiability through randomized quantification. SSAT has many\napplications, among them probabilistic bounded model checking (PBMC) of\nsymbolically represented Markov decision processes. This article identifies a\nnotion of Craig interpolant for the SSAT framework and develops an algorithm\nfor computing such interpolants based on a resolution calculus for SSAT. As a\npotential application area of this novel concept of Craig interpolation, we\naddress the symbolic analysis of probabilistic systems. We first investigate\nthe use of interpolation in probabilistic state reachability analysis, turning\nthe falsification procedure employing PBMC into a verification technique for\nprobabilistic safety properties. We furthermore propose an interpolation-based\napproach to probabilistic region stability, being able to verify that the\nprobability of stabilizing within some region is sufficiently large.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:16)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":4,"title":["Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Tino","family":"Teige","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9138-8340","authenticated-orcid":false,"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,26]]},"reference":[{"key":"10.2168\/LMCS-8(2:16)2012_BiereEA:BMC","doi-asserted-by":"crossref","unstructured":"Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Rance Cleaveland, editor,Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS '99, volume 1579 ofLecture Notes in Computer Science, pages 193-207. Springer, 1999.","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"5","key":"10.2168\/LMCS-8(2:16)2012_Bellman:MDP","first-page":"679","volume":"6","author":"Richard Bellman","year":"1957","journal-title":"Journal of Mathematics and Mechanics"},{"issue":"1","key":"10.2168\/LMCS-8(2:16)2012_BaierHKH05","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"Christel Baier, Holger Hermanns, Joost-P","year":"2005","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-8(2:16)2012_HandbookOfSAT2009","unstructured":"Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors.Handbook of Satisfiability, volume 185 ofFrontiers in Artificial Intelligence and Applications. IOS Press, February 2009."},{"issue":"1","key":"10.2168\/LMCS-8(2:16)2012_BuningKF95","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"Hans Kleine B\u00fcning, Marek Karpinski, and","year":"1995","journal-title":"Inf. Comput."},{"key":"10.2168\/LMCS-8(2:16)2012_BalafoutisS06","doi-asserted-by":"crossref","unstructured":"Thanasis Balafoutis and Kostas Stergiou. Algorithms for stochastic CSPs. In Fr\u00e9d\u00e9ric Benhamou, editor,Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP 2006), volume 4204 ofLecture Notes in Computer Science, pages 44-58. Springer, 2006.","DOI":"10.1007\/11889205_6"},{"key":"10.2168\/LMCS-8(2:16)2012_BordeauxS07","doi-asserted-by":"crossref","unstructured":"Lucas Bordeaux and Horst Samulowitz. On the stochastic constraint satisfaction framework. InProceedings of the 2007 ACM Symposium on Applied Computing (SAC), pages 316-320. ACM, 2007.","DOI":"10.1145\/1244002.1244077"},{"key":"10.2168\/LMCS-8(2:16)2012_BSST09HBSAT","unstructured":"Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Biere et al. HandbookOfSAT2009, chapter 26, pages 825-885."},{"issue":"3","key":"10.2168\/LMCS-8(2:16)2012_Craig57","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"William Craig","year":"1957","journal-title":"J. Symb. Log."},{"issue":"7","key":"10.2168\/LMCS-8(2:16)2012_DavisEA:DPLL62","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"Martin Davis, George Logemann, and Donal","year":"1962","journal-title":"Commun. ACM"},{"issue":"3","key":"10.2168\/LMCS-8(2:16)2012_DavisPutnam","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"Martin Davis and Hilary Putnam","year":"1960","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(2:16)2012_FranzleHSCC2011","doi-asserted-by":"crossref","unstructured":"Martin Fr\u00e4nzle, Ernst Moritz Hahn, Holger Hermanns, Nicol\u00e1s Wolovick, and Lijun Zhang. Measurability and safety verification for stochastic hybrid systems. InProceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), pages 43-52, New York, NY, USA, 2011. ACM.","DOI":"10.1145\/1967701.1967710"},{"key":"10.2168\/LMCS-8(2:16)2012_FraHerTei08:SSMT","unstructured":"Martin Fr\u00e4nzle, Holger Hermanns, and Tino Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Magnus Egerstedt and Bud Mishra, editors,Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC 2008), volume 4981 ofLecture Notes in Computer Science, pages 172-186. Springer, 2008."},{"issue":"7","key":"10.2168\/LMCS-8(2:16)2012_FraTeiEgg:JLAP","first-page":"436","volume":"79","author":"Martin Fr\u00e4nzle, Tino Teige, and Andreas","year":"2010","journal-title":"Journal of Logic and Algebraic Programming 2010"},{"key":"10.2168\/LMCS-8(2:16)2012_prism4:cav2011","doi-asserted-by":"crossref","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. Prism 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors,Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), volume 6806 ofLecture Notes in Computer Science, pages 585-591. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"10.2168\/LMCS-8(2:16)2012_littman99initial","unstructured":"Michael L. Littman. Initial experiments in stochastic satisfiability. InProceedings of the 16th National Conference on Artificial Intelligence, pages 667-672, 1999."},{"issue":"3","key":"10.2168\/LMCS-8(2:16)2012_littman01stochastic","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1023\/A:1017584715408","volume":"27","author":"Michael L. Littman, Stephen M. Majercik,","year":"2001","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(2:16)2012_Majercik04Nonchronological","doi-asserted-by":"crossref","unstructured":"Stephen M. Majercik. Nonchronological backtracking in stochastic Boolean satisfiability. In16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2004), pages 498-507. IEEE Computer Society, 2004.","DOI":"10.1109\/ICTAI.2004.94"},{"key":"10.2168\/LMCS-8(2:16)2012_Maj09HBSAT","unstructured":"Stephen M. Majercik. Stochastic Boolean satisfiability. In Biere et al. HandbookOfSAT2009, chapter 27, pages 887-925."},{"key":"10.2168\/LMCS-8(2:16)2012_McMillan03","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. Interpolation and SAT-based model checking. In Warren A. Hunt Jr. and Fabio Somenzi, editors,Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003), volume 2725 ofLecture Notes in Computer Science, pages 1-13. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"10.2168\/LMCS-8(2:16)2012_McMillan:TACAS05","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. Applications of Craig interpolants in model checking. In Nicolas Halbwachs and Lenore D. Zuck, editors,Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 ofLecture Notes in Computer Science, pages 1-12. Springer, 2005.","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"10.2168\/LMCS-8(2:16)2012_majercik98maxplan","unstructured":"Stephen M. Majercik and Michael L. Littman. MAXPLAN: A new approach to probabilistic planning. InProceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, pages 86-93. AAAI, 1998."},{"issue":"1-2","key":"10.2168\/LMCS-8(2:16)2012_majercik03contingent","first-page":"119","volume":"147","author":"Stephen M. Majercik and Michael L. Littm","year":"2003","journal-title":"Artificial Intelligence Special Issue on Planning with Uncertainty and Incomplete Information"},{"issue":"2","key":"10.2168\/LMCS-8(2:16)2012_Papadimitriou85","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1016\/0022-0000(85)90045-5","volume":"31","author":"Christos H. Papadimitriou","year":"1985","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"10.2168\/LMCS-8(2:16)2012_Pudlak97","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"Pavel Pudl\u00e1k","year":"1997","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(2:16)2012_PodelskiW:FORMATS07","doi-asserted-by":"crossref","unstructured":"Andreas Podelski and Silke Wagner. Region stability proofs for hybrid systems. In Jean-Francois Raskin and P. S. Thiagarajan, editors,Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2007), volume 4763 ofLecture Notes in Computer Science, pages 320-335. Springer, 2007.","DOI":"10.1007\/978-3-540-75454-1_23"},{"key":"10.2168\/LMCS-8(2:16)2012_PodelskiW:HSCC07","doi-asserted-by":"crossref","unstructured":"Andreas Podelski and Silke Wagner. A sound and complete proof rule for region stability of hybrid systems. In Alberto Bemporad, Antonio Bicchi, and Giorgio C. Buttazzo, editors,Proceedings of the 10th International Workshop on Hybrid Systems: Computation and Control (HSCC 2007), volume 4416 ofLecture Notes in Computer Science, pages 750-753. Springer, 2007.","DOI":"10.1007\/978-3-540-71493-4_76"},{"issue":"1","key":"10.2168\/LMCS-8(2:16)2012_Robinson:Resolution65","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"John Alan Robinson","year":"1965","journal-title":"J. ACM"},{"issue":"2","key":"10.2168\/LMCS-8(2:16)2012_TeiEggFra:NAHS","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/j.nahs.2010.04.009","volume":"5","author":"Tino Teige, Andreas Eggers, and Martin F","year":"2011","journal-title":"Nonlinear Analysis: Hybrid Systems"},{"key":"10.2168\/LMCS-8(2:16)2012_TeiFra08:nonlinearSSMT","doi-asserted-by":"crossref","unstructured":"Tino Teige and Martin Fr\u00e4nzle. Stochastic satisfiability modulo theories for non-linear arithmetic. In Laurent Perron and Michael A. Trick, editors,Proceedings of the 5th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR 2008), volume 5015 ofLecture Notes in Computer Science, pages 248-262. Springer, 2008.","DOI":"10.1007\/978-3-540-68155-7_20"},{"key":"10.2168\/LMCS-8(2:16)2012_TeigeFraenzle09:ADHS","doi-asserted-by":"crossref","unstructured":"Tino Teige and Martin Fr\u00e4nzle. Constraint-based analysis of probabilistic hybrid systems. In Alessandro Giua, Cristian Mahulea, Manuel Silva, and Janan Zaytoon, editors,Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems, pages 162-167. IFAC, 2009.","DOI":"10.3182\/20090916-3-ES-3003.00029"},{"key":"10.2168\/LMCS-8(2:16)2012_TeiFrae:LPAR17","doi-asserted-by":"crossref","unstructured":"Tino Teige and Martin Fr\u00e4nzle. Resolution for stochastic Boolean satisfiability. In Christian G. Ferm\u00fcller and Andrei Voronkov, editors,Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), volume 6397 ofLecture Notes in Computer Science, pages 625-639. Springer, 2010.","DOI":"10.1007\/978-3-642-16242-8_44"},{"key":"10.2168\/LMCS-8(2:16)2012_walsh02stochastic","unstructured":"Toby Walsh. Stochastic constraint programming. In Frank van Harmelen, editor,Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002), pages 111-115. IOS Press, 2002."},{"key":"10.2168\/LMCS-8(2:16)2012_PHA:CAV10","doi-asserted-by":"crossref","unstructured":"Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. Safety verification for probabilistic hybrid systems. In Tayssir Touili, Byron Cook, and Paul Jackson, editors,Proceedings of the 22nd International Conference on Computer Aided Verification, CAV 2010, volume 6174 ofLecture Notes in Computer Science, pages 196-211. Springer, 2010.","DOI":"10.1007\/978-3-642-14295-6_21"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1031\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1031\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:01:42Z","timestamp":1681243302000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1031"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,26]]},"references-count":34,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:16)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1206.4444","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.4444","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1080\/23335777.2019.1624619","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,6,26]]},"article-number":"1031"}}