@InProceedings{ mahdi2014b,
title = {Generalized Craig Interpolation for Stochastic
Satisfiability Modulo Theory problems},
author = {Ahmed Mahdi and Martin Fr{\"a}nzle},
booktitle = {Proceedings of the 8th International Workshop on
Reachability Problems, RP 2014},
year = {2014},
editor = {Joel Ouaknine and James Worrell},
pages = {203-215},
publisher = {Springer International Publishing Switzerland},
series = {Lecture Notes in Computer Science},
volume = {8762},
abstract = {Craig interpolation is widely used in solving reachability
and model-checking problems by SAT or SMT techniques, as it
permits the computation of invariants as well as discovery
of meaningful predicates in CEGAR loops based on predicate
abstraction. Extending such algorithms from the qualitative
to the quantitative setting of probabilistic models seems
desirable. In 2012, [Teige et al.] succeeded to define an
adequate notion of generalized, stochastic interpolants and
to expose an algorithm for efficiently computing them for
stochastic Boolean satisfiability problems, i.e., SSAT. In
this work we present a notion of Generalized Craig
Interpolant for the stochastic SAT modulo theories
framework, i.e., SSMT, and introduce a mechanism to compute
such stochastic interpolants for non-polynomial SSMT
problems based on a sound and, w.r.t. the arithmetic
reasoner, relatively complete resolution calculus. The
algorithm computes interpolants in SAT, SMT, SSAT, and SSMT
problems. As this extends the scope of SSMT-based
model-checking of probabilistic hybrid automata from the
bounded to the unbounded case, we demonstrate our
interpolation principle on an unbounded probabilistic
reachability problem in a probabilistic hybrid automaton.
},
access = {open},
bibtex = {mahdi.RP2014b.bib},
category = {other},
conference-long={International Workshop on Reachability Problems},
conference-short={RP},
cross-site = { },
pdf = {mahdi.RP2014b.pdf},
language = {English},
subproject = {H4}
}