  The extension of classical imperative programs with real-valued random
variables and random branching gives rise to probabilistic programs. The
termination problem is one of the most fundamental liveness properties for such
programs. The qualitative (aka almost-sure) termination problem asks whether a
given program terminates with probability 1. Ranking functions provide a sound
and complete approach for termination of non-probabilistic programs, and their
extension to probabilistic programs is achieved via ranking supermartingales
(RSMs). RSMs have been extended to lexicographic RSMs to handle programs with
involved control-flow structure, as well as for compositional approach. There
are two key limitations of the existing RSM-based approaches: First, the
lexicographic RSM-based approach requires a strong nonnegativity assumption,
which need not always be satisfied. The second key limitation of the existing
RSM-based algorithmic approaches is that they rely on pre-computed invariants.
The main drawback of relying on pre-computed invariants is the
insufficiency-inefficiency trade-off: weak invariants might be insufficient for
RSMs to prove termination, while using strong invariants leads to inefficiency
in computing them. Our contributions are twofold: First, we show how to relax
the strong nonnegativity condition and still provide soundness guarantee for
almost-sure termination. Second, we present an incremental approach where the
process of computing lexicographic RSMs proceeds by iterative pruning of parts
of the program that were already shown to be terminating, in cooperation with a
safety prover. In particular, our technique does not rely on strong
pre-computed invariants. We present experimental results to show the
applicability of our approach to examples of probabilistic programs from the
literature.
