Time-Bounded Termination Analysis for Probabilistic Programs with Delays
Ming Xu and Yuxin Deng
This paper investigates the model of probabilistic program with delays (PPD) that
consists of a few program blocks. Performing each block has an additional
time-consumption--waiting to be executed--besides the running time. We interpret
the operational semantics of PPD by Markov automata with a cost structure on transitions.
Our goal is to measure those individual execution paths of a PPD that terminates within
a given time bound, and to compute the minimum termination probability, i. e. the
termination probability under a demonic scheduler that resolves the nondeterminism
inherited from probabilistic programs. When running time plus waiting time is bounded,
the demonic scheduler can be determined by comparison between a class of well-formed
real numbers. The method is extended to parametric PPDs. When only the running time
is bounded, the demonic scheduler can be determined by real root isolation over a class
of well-formed real functions under Schanuel's conjecture. Finally we give the complexity
upper bounds of the proposed methods.