@todonotes@numberoftodonotes *[inlinelist,1]label=(),

# Sound and Complete Proof Rules for Probabilistic Termination

Rupak Majumdar  0000-0003-2136-0542 Max Planck Institute for Software Systems
(MPI-SWS)Paul-Ehrlich-Straße, Building G26Kaiserslautern67663Germany
<EMAIL_ADDRESS>and  V. R. Sathiyanarayana  0009-0006-5187-5415 Max Planck
Institute for Software Systems (MPI-SWS)Paul-Ehrlich-Straße, Building
G26Kaiserslautern67663Germany<EMAIL_ADDRESS>
###### Abstract.

Termination is a fundamental question in the analysis of probabilistic
imperative programs. We consider the _qualitative_ and _quantitative_
probabilistic termination problems for an imperative programming model with
discrete probabilistic choice and demonic bounded nondeterminism. The
qualitative question asks if the program terminates almost surely, no matter
how nondeterminism is resolved; the quantitative question asks for a bound on
the probability of termination. Despite a long and rich literature on the
topic, no sound and relatively complete proof systems were known for this
problem. We provide the first sound and relatively complete proof rules for
proving qualitative and quantitative termination in the assertion language of
arithmetic. Our proof rules use supermartingales as estimates of likelihood of
the prgroam’s evolution—the key insight is to use appropriately defined
finite-state sub-instances. Our completeness result shows how to construct a
suitable supermartingales from an almost-surely terminating program. We also
show that proofs of termination in many existing proof systems can be
transformed to proofs in our system, pointing to its applicability in
practice. As an application of our proof rule, we show a proof of almost sure
termination for the two-dimensional random walker.

##  1\. Introduction

Probabilistic programming languages extend the syntax of usual deterministic
computation with primitives for random choice. Thus, probabilistic programs
express randomized computation and have found applications in many domains
where randomization is essential.

We study the _termination problem_ for probabilistic programs with discrete
probabilistic and nondeterministic choice. Termination is a fundamental
property of programs and formal reasoning about (deterministic) program
termination goes back to Turing (Turing, 1937). Its extension to the
probabilistic setting can be either qualitative or quantitative. _Qualitative_
termination, or Almost-Sure Termination $(\mathsf{AST})$ asks if the program
terminates almost-surely, no matter how the nondeterminism is resolved.
_Quantitative_ termination, on the other hand, relates to finding upper and
lower bounds on the probability of termination that hold across all
resolutions of nondeterminism.

For finite-state probabilistic programs, both qualitative and quantitative
termination problems are well understood: there are sound and complete
_algorithmic_ procedures for termination that operate by analyzing the
underlying finite-state Markov decision processes. Intuitively, every run of
the system eventually arrives in an end component and thus, computing the
termination probabilities reduces to computing the reachability probabilities
for the appropriate end components (Hart et al., 1983; Vardi, 1985;
Courcoubetis and Yannakakis, 1995; Bianco and de Alfaro, 1995; de Alfaro et
al., 2007; de Alfaro and Henzinger, 2000).

The story is different for infinite state spaces. Existing techniques for
deducing termination typically take the form of _sound_ proof rules over a
program logic (Hart et al., 1983; de Alfaro et al., 2007; McIver and Morgan,
2005; Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2017; McIver et
al., 2018; Chatterjee et al., 2022). These rules ask for certificates
consisting of a variety of mathematical entities that satisfy locally-
checkable properties. None of them, however, are known to be complete; that
is, we do not know if certificates can always be found for terminating
programs. The search for relatively complete proof rules has been a long-
standing open problem. Note that, since the termination problem is
undecidable, one can only hope for completeness _relative_ to an underlying
logic.

In this paper, we describe the first sound and relatively complete proof rules
for qualitative and quantitative termination of probabilistic programs. We
present our rules in a simple proof system in the style of Floyd (1993) that
applies naturally to our program model. This proof system uses arithmetic as
its assertion language, interpreted over the standard model of rational
numbers. Soundness means that if our proof rule applies, then indeed the
system satisfies the (qualitative or quantitative) termination criterion.
Completeness of our rules is relative to the completeness of a proof system
for the underlying assertion language, i.e., arithmetic. Accordingly, we show
an effective reduction from the validity of our program logic to the validity
of a finite number of assertions in arithmetic. Whenever the original program
terminates (qualitatively or quantitatively), one can construct a proof in our
program logic in such a way that all relevant certificates can be expressed in
the assertion language. This is important: merely knowing that certain
semantic certificates exist may not be sufficient for a proof system, e.g., if
these certificates are provided non-constructively or require terms that
cannot be expressed in the assertion language.

Let us be more precise. We work in an imperative programming model with
variables ranging over rationals. Our model fixes a finite set of program
locations, and defines a guarded transition relation between the locations
representing computational steps. At marked locations, the model contains
primitives for probability distributions over available transitions. This
allows for the expression of _bounded_ nondeterministic and probabilistic
choice; we assume the nondeterminism is resolved demonically. We fix the
language of arithmetic as our expression and assertion language, and interpret
formulas over the standard model of the rational numbers.111 One can
generalize our result to _arithmetical_ structures (Harel et al., 2000), but
we stick to the simpler setting for clarity.  The semantics of our programming
language is given by a Markov decision process on countably many states, where
a demonic scheduler resolves the nondeterminism. Since the language has
bounded nondeterminism, we note that each state has a finite number of
immedicate successor states and so, for every scheduler, the number of states
reached in a bounded number of steps is finite.

Given a program and a terminal state, the _qualitative termination_ question
asks if the infimum over all schedulers resolving nondeterminism of the
probability of reaching the terminal state is one, that is, if the program
almost surely terminates under all possible schedulers. The _quantitative
termination_ question asks if the probability of reaching the terminal state
is bounded above or below by a given probability $p$.

For the special case of programs without probabilistic choice, sound and
relatively complete proof systems for termination are known (Manna and Pnueli,
1974; Harel, 1980; Apt, 1981): they involve finding a _variant_ function from
(reachable) program states to a well-founded domain that decreases on every
step of the program, and which maps the terminal state to a minimal element.

A natural generalization of variant functions is a _ranking supermartingale_ :
a function from states to reals that reduces in expectation by some amount on
each step of the program. Ranking supermartingales of various flavors are the
workhorse of existing proof rules for qualitative termination. Unfortunately,
an example from (Majumdar and Sathiyanarayana, 2024) shows that a proof rule
based only on a ranking supermartingale is incomplete: there may not exist a
ranking supermartingale that decreases in expectation on each step and one may
require transfinite ordinals in proofs.

#### Basic Ingredients

We take a different perspective. Instead of looking for a mapping that
represents the distance to a terminal state that goes down in each step, as in
previous approaches, we consider modeling the relative likelihood of the
program’s evolution instead. We provide two different proof rules. In the
first, we certify almost sure termination using a function that is unbounded
and non-increasing in expectation on _“most”_ states. In the second, we
certify almost sure termination using a family of functions, one for each
reachable state, each non-increasing in expectation. Both certificates track
the execution’s relative likelihood in subtly different ways, and both require
additional side conditions.

We prove an _unrolling lemma_ that is a central tool for our completeness
results. It states that if the infimum over all schedulers of the probability
of reaching a terminal state is at least $p$, then for every $\epsilon$, there
is a finite upper bound $k$ such that the infimum over all schedulers of the
probability mass of reaching the terminal state within $k$ steps is at least
$p-\epsilon$. In particular, the set of states reachable in $k$ steps defines
a finite state space. The unrolling lemma appears as a basic ingredient in
characterizing the complexity of almost sure termination (Kaminski et al.,
2019; Majumdar and Sathiyanarayana, 2023). We show that it provides a
surprisingly powerful tool in proving completeness of proof systems by
“carving out” finite state systems out of infinite-state termination problems.

#### Our Proof Rules for Qualitative Termination

I. Our first rule asks for a supermartingale (Doob, 1953) $V$ that is non-
increasing in expectation on all states except for some set containing the
terminal state. In addition, our rule asks for a variant function $U$ that
certifies that every reachable state has some finite path to the terminal
state. We also require a few compatibility conditions on $U$ from $V$ to let
us conclude the almost-sure escape from sets of states within which $V$ is
bounded.

We show the rule is sound by partitioning the collection of all runs and
strategically employing variant arguments and/or martingale theory within each
partition. The completeness of the rule uses the following observation. Fix an
enumeration of the reachable states $s_{1},s_{2},\ldots$ of an almost-surely
terminating program. Let $\Pr_{s}[\Diamond\mathbbm{1}_{>n}]$ denote the
probability that a run starting from state $s$ reaches some state in
$\\{s_{n},s_{n+1},\ldots\\}$ in the enumeration. For a fixed $s$, we first
show that $\Pr_{s}[\Diamond\mathbbm{1}_{>n}]$ goes to zero as
$n\rightarrow\infty$. Following a diagonal-like construction from the theory
of countable Markov chains (Mertens et al., 1978), we next define a sequence
$n_{1},n_{2},\ldots$ such that
$\Pr_{j}[\Diamond\mathbbm{1}_{s_{n_{k}}}]\leq\frac{1}{2^{k}}$ for all $j\leq
k$ (this is possible since the limit goes to zero and by the unrolling lemma).
This lets us define a supermartingale defined over the states $s$ as

$\sum_{k\in\mathbb{N}}\Pr{}_{s}[\Diamond\mathbbm{1}_{>n_{k}}]$

This supermartingale satisfies the requirements of our rule. Moreover, we show
that this supermartingale can be expressed in arithmetic, granting the rule
relative completeness.

II. We provide a second dual proof rule that takes a more local view. Our
first rule required certificates inferred from the global behaviour of the
program. Our second rule, by contrast, requires proofs of _near termination_ ,
i.e., termination with some non-zero probability, from _every_ reachable
state. If these proofs together indicate a non-zero lower bound of termination
across all states, a zero-one law indicates almost-sure termination.
Therefore, our rule asks for a proof of termination with probability at least
$1-\epsilon$, for some $\epsilon>0$.

How does our rule certify termination from a given state with probability
$1-\epsilon$? It incorporates a proof rule for quantitative termination by
Chatterjee et al. (2022) that builds finite supermartingales that take on non-
trivial values for only finitely many states. This rule employs _stochastic
invariants_ (Chatterjee et al., 2017): pairs $(\mathsf{SI},p)$ such that the
probability with which executions leave the set of states $\mathsf{SI}$ is
bounded above by $p$. Our proof rule needs a family of stochastic invariants,
one for each reachable state.

The completeness of this rule uses the unrolling lemma in a crucial way. The
unrolling lemma implies a finite state space around every state that
accumulates a termination probability mass of $1-\epsilon$. We use this fact
to show that the proof rule of Chatterjee et al. (2022) is complete for
finite-state systems. This completeness in turn induces the finite nature of
these supermartingales describing the stochastic invariants around each state.

#### Quantitative Termination

All our rules for quantitative termination again use the stochastic invariants
of Chatterjee et al. (2017). A stochastic invariant easily implies an upper
bound rule: if there is a stochastic invariant $(\mathsf{SI},p)$ that avoids
terminal states, the probability of termination is upper bounded by $p$. For
lower bounds, our starting point is the proof rule proposed by Chatterjee et
al. (2022) using stochastic invariants: if there is a stochastic invariant
$(\mathsf{SI},p)$ such that runs almost surely terminate within $\mathsf{SI}$
or leave $\mathsf{SI}$, then the probability of termination is at least $1-p$.
While they claimed soundness and completeness for their rule, there were two
issues. First, their rule was paramterized by a certificate for qualitative
termination. In the absence of a relatively complete proof rule for
qualitative termination, one could not achieve relative completeness. Second,
we show in Section 5.3 an explicit example where their rule cannot apply.

We show a sound and complete rule that is a modification of their rule: we
require that for each $n\in\mathbb{N}$, there is a stochastic invariant
$(\mathsf{SI}_{n},p+\frac{1}{n})$ such that all runs almost surely terminate
within $\mathsf{SI}_{n}$ or leave $\mathsf{SI}_{n}$. Sound and relatively
complete certificates for almost sure termination are now given using our
previous technique for qualitative termination.

In summary, we provide the first sound and relatively complete proof rules for
qualitative and quantitative termination, culminating the substantial body of
work on probabilistic termination in the last four decades.

#### Other Related Work

Our proof rules use supermartingales that are closely related to Lyapunov
functions in stability of dynamical systems. Lyapunov functions have been used
to characterize recurrence and transience in infinite-state Markov chains,
going back to the work of Foster (Foster, 1951, 1953). Completeness of
Lyapunov functions was shown in general by Mertens et al. (1978). Our proof of
soundness and completeness uses insights from Mertens et al. (1978), but we
have to overcome several technical issues. First, we have demonic
nondeterminism and therefore require the unrolling lemma to deal with infimums
over all schedulers. Second, we do not have irreducibility. Finally, whereas a
Markov chain is either recurrent or transient, we cannot assume that a program
that is not almost sure terminating has a strong transience property. Thus, we
have to prove these properties ab initio.

In the literature, there exist sound proof rules for $\mathsf{AST}$ that use
supermartingales. One rule by Huang et al. (2018) uses supermartingales that
exhibit a lower bound on their variation in each step. A much more closely
related work is the excellent $\mathsf{AST}$ proof rule by McIver et al.
(2018). Their work shows that a proof rule consisting of a supermartingale
function that also acts as a distance variant is sound for almost-sure
termination. While the former is believed to be incomplete (McIver et al.,
2018), it is not known if the latter rule is complete. Our work indicates that
one can achieve completeness by separating the roles of the distance variant
and the supermartingale into two functions.

The issue of an appropriate assertion language for proof rules for termination
have been mostly elided in the literature, and most rules are presented in an
informal language of “sufficiently expressive” mathematical constructs.
Important exceptions are the assertion languages of Batz et al. (2021) and den
Hartog and de Vink (2002). Their work shows that the language of arithmetic
extended with suprema and infima of functions over the state space is
relatively complete (in the sense of Cook (1978)) for weakest-preexpectation
style reasoning of probabilistic programs without nondeterminism. That is,
given a function $f$ definable in their language and a program $P$, they show
that their language is expressive enough to represent the weakest pre-
expectation of $f$ with respect to $P$. The need for suprema and infima is
motivated by demonstrating simple probabilistic programs whose termination
probabilities involve transcendental numbers. We note that arithmetic is
sufficient for relative completeness because suprema and infima arising in
probabilistic termination can be encoded (through quantifiers). We believe
that presenting the rules directly in the language of arithmetic allows
greater focus on the nature of the certificates required by the rules. Note
that for extensions of the programming model, such as with unbounded
nondeterministic choice, arithmetic is no longer sufficient for relative
completeness, and this holds already without probabilistic choice in the
language (Hitchcock and Park, 1972; Apt and Kozen, 1986; Apt and Plotkin,
1986).

While we focus on almost sure termination, there are related qualitative
termination problems: _positive_ almost sure termination ($\mathsf{PAST}$) and
_bounded_ almost sure termination $(\mathsf{BAST}$). These problems strengthen
almost sure termination by requiring that the expected time to termination is
finite. (Note that a program may be almost surely terminating but the expected
run time may be infinite: consider a one-dimensional symmetric random walk
where $0$ is an absorbing state.) The difference is that $\mathsf{PAST}$
allows the expected run time to depend on the scheduler that resolves
nondeterminism, and $\mathsf{BAST}$ requires a global bound that holds for
every scheduler. Sound and complete proof rules for $\mathsf{BAST}$ have been
studied extensively (Bournez and Garnier, 2005; Fioriti and Hermanns, 2015; Fu
and Chatterjee, 2019; Avanzini et al., 2020). More recently, a sound and
complete proof rule for $\mathsf{PAST}$ was given (Majumdar and
Sathiyanarayana, 2024). Completeness in these papers are semantic, and
relative completeness in the sense of Cook was not studied. Our techniques
would provide a relative completeness result for $\mathsf{BAST}$. In contrast,
Majumdar and Sathiyanarayana (2024) show that $\mathsf{PAST}$ is
$\Pi_{1}^{1}$-complete (AST and $\mathsf{BAST}$ are arithmetical, in
comparison); thus Peano arithmetic would be insufficient as a (relatively
complete) assertion language (see (Apt and Plotkin, 1986) for similar issues
and appropriate assertion languages for nondeterministic programs with
countable nondeterminism).

Our results apply to discrete probabilistic choice. While discrete choice and
computation captures many randomized algorithms, our proofs of completeness do
not apply to programs with, e.g., sampling from continuous probaility
distributions. The use of real values introduce measure-theoretic complexities
in the semantics (Takisaka et al., 2021). These can be overcome, but whether
there is a sound and relatively complete proof rule for an appropriate
assertion language remains open.

While we focus on the theoretical aspects here, there is a large body of work
on _synthesizing_ certificates automatically and tools for probabilistic
verification (Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2022;
McIver et al., 2018; Feng et al., 2023). We show a “compilation” of many
existing rules into our rules, thus, such tools continue to work in our proof
system.

##  2\. Probabilistic Programs

###  2.1. Syntax and Semantics

#### Syntax.

We work with _probabilistic control flow graphs_ , a program model used by
Chatterjee et al. (2022) to detail proof rules for quantitative termination.
Variables in this model range over the rationals. Assignment statements and
loop guards are terms and boolean combinations of atomic formulae expressible
in the language of arithmetic. This is standard in program logics (Apt, 1981),
and facilitates the use of the language of rational arithmetic with addition,
multiplication, and order to make assertions about desirable program
properties. For sake of conciseness, we augment this assertion language with
additional computable predicates as “syntactic sugar” in our proofs. We
interpret assertions over the standard model of rationals.

###### Definition 2.1 (Control Flow Graphs).

A Control Flow Graph ($\mathsf{CFG}$) $\mathcal{G}$ is a tuple
$(L,V,l_{init},\mathbf{x}_{init},\mathord{\mapsto},G,\mathsf{Pr},\mathsf{Upd})$,
where

  * •

$L$ is a finite set of program locations, partitioned into assignment,
nondeterministic, and probabilistic locations $L_{A}$, $L_{N}$, and $L_{P}$,
respectively.

  * •

$V=\\{x_{1},x_{2},\ldots x_{n}\\}$ is a finite set of program variables.

  * •

$l_{init}\in L$ is the initial program location, and
$\mathbf{x}_{init}\in\mathbb{Q}^{V}$ is the initial variable valuation.

  * •

$\mathord{\mapsto}\subseteq L\times L$ is a finite set of transitions. If
$\tau=(l,l^{\prime})\in\mathord{\mapsto}$, then $l$ and $l^{\prime}$ are
respectively referred to as the source and target locations of $\tau$.

  * •

$G$ is a function mapping each $\tau\in\mathord{\mapsto}$ to a Boolean
expression over $V\cup L$.

  * •

$\mathsf{Pr}$ is a function assigning each
$(l,l^{\prime})\in\mathord{\mapsto}$ with $l\in L_{P}$ a fractional expression
$p$ over the variables $V$ representing a rational probability value.

  * •

$\mathsf{Upd}$ is a map assigning each $(l,l^{\prime})\in\mathord{\mapsto}$
with $l\in L_{A}$ an update pair $(j,u)$ where $j\in\\{1,\ldots,|V|\\}$ is the
target variable index and $u$ is an arithmetic expression over the variables
$V$.

  * •

At assignment locations, there is at most one outgoing transition.

  * •

At probabilistic locations $l$, it must be that
$\mathsf{Pr}(l,\\_)[\mathbf{x}]>0$ and $\sum
G(l,\\_)[(l,\mathbf{x})]\times\mathsf{Pr}((l,\\_))[\mathbf{x}]=1$ over all
transitions $(l,\\_)\in\mathord{\mapsto}$ for all
$\mathbf{x}\in\mathbb{Q}^{V}$.

We use the boldface notation $\mathbf{x}$ for variable assignments and write
$\mathbf{0}$ for the assignment that maps every variable to zero.
$\mathsf{Pr}(l,l^{\prime})[\mathbf{x}]$, $G(l,l^{\prime})[\mathbf{x}]$, and
$\mathsf{Upd}(l,l^{\prime})[\mathbf{x}]$ refer to the output of the
expressions $\mathsf{Pr}(l,l^{\prime})$, $G(l,l^{\prime})$, and
$\mathsf{Upd}(l,l^{\prime})$ on the assignment $\mathbf{x}$. Note that the
finiteness of $L$ implies that the branching at both nondeterministic and
probabilistic locations is bounded. Without loss of generality, we assume
simple structural conditions that ensures that every state has a successor.
This follows similar assumptions made in prior work (Chatterjee et al., 2022).
Observe that, while the probabilistic choice is simple, it is sufficient to
model probabilistic Turing machines and some quite sophisticated probabilistic
phenomena (Flajolet et al., 2011). However, we explicitly forbid unbounded
nondeterministic choice or sampling from continuous distributions.

###### Remark 2.2.

While we use $\mathsf{CFG}$s as our formal model of programs, we could have
equivalently used probabilistic guarded command language ($\mathsf{pGCL}$).
$\mathsf{pGCL}$ is the probabilistic extension of the Guarded Command Language
of Dijkstra (1976), and is a convenient language for specifying probabilistic
computation. There is a large body of work (Kaminski et al., 2019; Feng et
al., 2023; Batz et al., 2021; McIver et al., 2018; McIver and Morgan, 2005)
that uses $\mathsf{pGCL}$ syntax. Our choice of $\mathsf{CFG}$s follows the
same choice made by Chatterjee et al. (2022) to describe quantitative
termination. It is standard to compile $\mathsf{pGCL}$ programs into
$\mathsf{CFG}$s and vice versa. For readability, we employ the syntax of
$\mathsf{pGCL}$ in some of our examples.

#### States, Runs, and Reachable States.

Fix a $\mathsf{CFG}$ $\mathcal{G}=(L,\allowbreak V,\allowbreak
l_{init},\allowbreak x_{init},\allowbreak\mathord{\mapsto},\allowbreak
G,\allowbreak\mathsf{Pr},\allowbreak\mathsf{Upd})$. A _state_ is a tuple
$(l,\mathbf{x})$, where $l\in L$ and $\mathbf{x}\in\mathbb{Q}^{V}$. A state
$(l,\mathbf{x})$ is termed _assignment_ (resp., _nondeterministic_ , or
_probabilistic_) if the location $l$ is assignment (resp., nondeterministic,
or probabilistic). We will refer to assignment locations $l$ where the updates
of all transitions sourced at $l$ don’t change the variable values as
_deterministic_ locations. Accordingly, states $(l,\mathbf{x})$ are termed
_deterministic_ when $l$ is deterministic. A transition
$(l,l^{\prime})\in\mathord{\mapsto}$ is _enabled_ at a state $(l,\mathbf{x})$
if the guard $G(l,l^{\prime})$ evaluates to true under $(l,\mathbf{x})$. The
vector $\mathbf{x}^{\prime}$ is the _result_ of the update pair $(j,u)$ from
the state $(l,\mathbf{x})$ if  1 for all $i\neq j$,
$\mathbf{x}^{\prime}[i]=\mathbf{x}[i]$, and  2
$\mathbf{x}^{\prime}[j]=u(\mathbf{x})$.  A state
$(l^{\prime},\mathbf{x}^{\prime})$ is a _successor_ to $(l,\mathbf{x})$ if the
transition $(l,l^{\prime})\in\mathord{\mapsto}$ is enabled at $(l,\mathbf{x})$
and $\mathbf{x}^{\prime}$ is the result of $\mathsf{Upd}(l,l^{\prime})$ on
$\mathbf{x}$. A _finite path_ is a sequence of states
$(l_{1},\mathbf{x}_{1}),(l_{2},\mathbf{x}_{2}),\ldots,(l_{n},\mathbf{x}_{n})$
with $(l_{k+1},\mathbf{x}_{k+1})$ being a successor to
$(l_{k},\mathbf{x}_{k})$. A _run_ (or _execution_) of $\mathcal{G}$ is a
sequence of states that  1 begins with the initial state
$(l_{init},\mathbf{x}_{init})$, and  2 only induces finite paths as prefixes.

A state $(l^{\prime},\mathbf{x}^{\prime})$ is said to be _reachable_ from a
state $(l,\mathbf{x})$ if there exists a finite path beginning at
$(l,\mathbf{x})$ and ending at $(l^{\prime},\mathbf{x}^{\prime})$. We write
$\mathsf{Reach}(\mathcal{G},(l,\mathbf{x}))$ for the set of states reachable
from $(l,\mathbf{x})$; we simply write $\mathsf{Reach}(\mathcal{G})$ when the
initial state is $(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$. An
$\mathsf{CFG}$ is said to be _finite state_ if the set of states reachable
from its initial state is finite.

#### Probability Theory

We now introduce some basic probability theoretic notions. The tuple
$(X,\mathcal{F},\mathbb{P})$ is called a _probability space_ where $X$ is the
sample space, $\mathcal{F}$ is a $\sigma$-algebra over $X$, and $\mathbb{P}$
is the probability measure over $\mathcal{F}$. The sequence
$(\mathcal{F}_{n})$, where $n$ ranges over $\mathbb{N}$, is a _filtration_ of
the probability space $(X,\mathcal{F},\mathbb{P})$ if each $\mathcal{F}_{n}$
is a sub $\sigma$-algebra of $\mathcal{F}$ and
$\mathcal{F}_{i}\subseteq\mathcal{F}_{j}$ for all $i\leq j$.

A _random variable_ is a measurable function from $X$ to $\mathbb{R}^{+}$, the
set of positive real numbers. The _expected value_ of the random variable $X$
is denoted by $\mathbb{E}[X]$. A _stochastic process_ over the filtered
probability space is a sequence of random variables $(X_{n})$ such that each
$X_{n}$ is measurable over $\mathcal{F}_{n}$. A _supermartingale_ is a
stochastic process $(X_{n})$ that does not increase in expectation, i.e.,
$\mathbb{E}[X_{n+1}]\leq\mathbb{E}[X_{n}]$ for each $n\in\mathbb{N}$. We will
abuse notation slightly and refer to any function over the state space of a
$\mathsf{CFG}$ that doesn’t increase in expectation at each execution step as
a _supermartingale function_.

We shall make use of the following version of Doob’s Martingale Convergence
Theorem.

###### Theorem 2.3 ((Doob, 1953)).

If a supermartingale $(X_{n})$ is bounded below, then there almost-surely
exists a random variable $X_{\infty}$ such that

$\mathbb{P}\left(X_{\infty}=\lim_{n\to\infty}X_{n}\right)=1\quad\text{and}\quad\mathbb{E}[X_{\infty}]\leq\mathbb{E}[X_{0}]$

#### Schedulers and Probabilistic Semantics.

Now, we introduce the operational semantics of our programs. These are
standard operational semantics that can be found in many other places (Baier
and Katoen, 2008; Chatterjee et al., 2022). A _scheduler_ is a mapping from
finite paths ending at nondeterministic states to successors from these
states. Note that, since the state space for any $\mathsf{CFG}$ is countable,
we do not require measurability conditions on the scheduler.

The semantics of $\mathcal{G}$ is understood through a probability space over
the runs of $\mathcal{G}$. Formally, let $\mathsf{Runs}_{\mathcal{G}}$ be the
collection of all executions of $\mathcal{G}$. Further, for a finite path
$\pi$, denote by $\mathsf{Cyl}_{\mathcal{G}}(\pi)$ the _cylinder set_
containing all runs $\rho\in\mathsf{Runs}_{\mathcal{G}}$ such that $\pi$ is a
prefix of $\rho$. Now, call $\mathcal{F}_{\mathcal{G}}$ the smallest
$\sigma$-algebra on $\mathsf{Runs}_{\mathcal{G}}$ containing all cylinder sets
of finite paths of $\mathcal{G}$.

A scheduler $\mathfrak{s}$ induces a probability space over the collection of
all runs of the $\mathsf{CFG}$ $\mathcal{G}$. A finite path (or run) $\pi$ is
said to be _consistent_ with $\mathfrak{s}$ if for every prefix $\pi^{\prime}$
of $\pi$ ending at a nondeterministic state, the finite path (or run) obtained
by appending the successor state $\mathfrak{s}(\pi^{\prime})$ to
$\pi^{\prime}$ is a prefix of $\pi$. A scheduler is said to induce a finite
path (or run) if the path (or run) is consistent with the scheduler. The
semantics of the $\mathsf{CFG}$ $\mathcal{G}$ under the scheduler
$\mathfrak{s}$ is captured by the probability space
$(\mathsf{Runs}_{\mathcal{G}},\allowbreak\mathcal{F}_{\mathcal{G}},\mathbb{P}_{\mathfrak{s}})$,
where for every consistent finite path
$\pi=((l_{1},\mathbf{x}_{1}),(l_{2},\mathbf{x}_{2}),\ldots(l_{n},\mathbf{x}_{n}))$
with probabilistic locations at indices $i_{1},i_{2},\ldots i_{n}$,

$\mathbb{P}{}_{\mathfrak{s}}(\pi)=\mathsf{Pr}(l_{i_{1}},l_{i_{1}+1})[\mathbf{x}_{i_{1}}]\times\cdots\mathsf{Pr}(l_{i_{n}},l_{i_{n}+1})[\mathbf{x}_{i_{n}}]$

We analogously define a probability space
$(\mathsf{Runs}_{\mathcal{G}(l,\mathbf{x})},\allowbreak\mathcal{F}_{\mathcal{G}(l,\mathbf{x})},\allowbreak\mathbb{P}_{\mathfrak{s}})$
to refer to the probability space induced by the scheduler $\mathfrak{s}$ on
the $\mathsf{CFG}$ obtained from $\mathcal{G}$ by setting the initial state to
$(l,\mathbf{x})$.

For a scheduler $\mathfrak{s}$, the _canonical filtration_ of $\mathcal{G}$ is
the sequence $(\mathcal{F}_{n})_{n\in\mathbb{N}}$ such that $\mathcal{F}_{n}$
is the smallest sub-$\sigma$-algebra of $\mathcal{F}_{\mathcal{G}(\sigma)}$
that contains the cylinder sets $\mathsf{Cyl}_{\mathcal{G}(\sigma)}(\pi_{\leq
n})$ of all finite paths $\pi_{\leq n}$ of length at most $n$. Under this
filtration, the semantics of $\mathcal{G}$ under $\mathfrak{s}$ can also be
viewed as a stochastic process $(X^{\mathfrak{s}}_{n})_{n\in\mathbb{N}}$
measurable against $(\mathcal{F}_{n})_{n\in\mathbb{N}}$ such that
$X^{\mathfrak{s}}_{n}$ takes on an encoding of the state of the execution
after $n$ steps. When convenient, we will use this view as well.

###  2.2. The Termination Problem

Fix an $\mathsf{CFG}$ $\mathcal{G}$ and a scheduler $\mathfrak{s}$. Let
$l_{\mathit{out}}$ be a distinguished location we refer to as _terminal_.
Denote by $\Diamond(l_{\mathit{out}},\mathbf{0})$ the set of all runs that
reach $(l_{\mathit{out}},\mathbf{0})$; we call these the _terminating runs_.
Observe that $\Diamond(l_{\mathit{out}},\mathbf{0})$ is measurable. The
$\mathsf{CFG}$ $\mathcal{G}$ is said to _terminate_ with probability $p$ under
the scheduler $\mathfrak{s}$ if
$\mathbb{P}_{\mathfrak{s}}[\Diamond(l_{\mathit{out}},\mathbf{0})]=p$.

###### Definition 2.4 (Termination Probability).

Let $\mathcal{G}$ be an $\mathsf{CFG}$ and for a scheduler $\mathfrak{s}$, let
$(\mathsf{Runs}_{\mathcal{G}},\mathcal{F}_{\mathcal{G}},\mathbb{P}_{\mathfrak{s}})$
be the probability space induced by $\mathfrak{s}$ on the executions of
$\mathcal{G}$. The termination probability of $\mathcal{G}$, denoted by
$\Pr_{\mathrm{term}}(\mathcal{G})$, is the infimum of
$\mathbb{P}_{\mathfrak{s}}[\Diamond(l_{\mathit{out}},\mathbf{0})]$ over all
schedulers $\mathfrak{s}$.

We also use the notation $\Pr_{\mathrm{term}}(\mathcal{G}(\sigma))$ to refer
to the termination probability of $\mathcal{G}$ if its initial state were
changed to $\sigma$.

An $\mathsf{CFG}$ is said to be _almost surely terminating_ ($\mathsf{AST}$)
if its termination probability is $1$. Our work is on sound and complete proof
rules for deciding, for an $\mathsf{CFG}$ $\mathcal{G}$,  1 the $\mathsf{AST}$
problem, i.e., whether $\mathcal{G}$ is almost surely terminating.  2 the
_Lower Bound_ problem, i.e., whether $\Pr_{\mathrm{term}}(\mathcal{G})$
exceeds some $p<1$,  3 the _Upper Bound_ problem, i.e., whether
$\Pr_{\mathrm{term}}(\mathcal{G})$ is bounded above by some $p>0$.  We remark
that, for the lower and upper bound problems, the proof rules we describe are
applicable to any number $p$ that is representable in our program logic. This
means that $p$ can take on irrational and transcendental values; this is
important, as termination probabilities can often take on such values (Batz et
al., 2021; Flajolet et al., 2011). We will elaborate in Section 2.4.

Note that, while we define termination for a specific state
$(l_{\mathit{out}},\mathbf{0})$, more general termination conditions can be
reduced to this case by a syntactic modification.

⬇

1x, y $\coloneqq$ 1, 1

2while (x $\neq$ 0 $\lor$ y $\neq$ 0):

3 { x $\coloneqq$ x + 1 $\oplus_{\frac{1}{2}}$ x $\coloneqq$ x - 1 }
$\oplus_{\frac{1}{2}}$

4 { y $\coloneqq$ y + 1 $\oplus_{\frac{1}{2}}$ y $\coloneqq$ y - 1 }

Prg. 1. The 2D symmetric random walker. The symbol $\oplus$ is a probabilistic
choice operator.

###### Example 2.5 (Symmetric Random Walk).

A $d$-dimensional _symmetric random walk_ has $d$ integer variables
$x_{1},\ldots,x_{d}$. Initially, all variables are $1$. In each step, the
program updates the variables to move to a “nearest neighbor” in the
$d$-dimensional lattice $\mathbb{Q}^{d}$; that is, the program picks uniformly
at random one of the variables and an element in $\\{-1,+1\\}$, and adds the
element to the chosen variable. Program 1 shows the code for $d=2$. It is well
known (Pólya, 1921) that the symmetric random walk is recurrent in dimension
$1$ and $2$, and transient otherwise. Thus, if we set any element in the
lattice, say $0$, to be an terminal state, then the program is almost surely
terminating in dimension $1$ and $2$ but not almost surely terminating when
$d\geq 3$. We shall refer to the $d=1$ and $d=2$ cases as 1DRW and 2DRW,
respectively. ∎

###  2.3. The Unrolling Lemma

Let $\mathcal{G}$ be an $\mathsf{CFG}$ such that
$\Pr_{\mathrm{term}}(\mathcal{G})\geq p$ for some rational $p>0$. Fix a
scheduler $\mathfrak{s}$. Let $(\pi_{1},\pi_{2},\ldots)$ be an ordering of the
terminating runs of $\mathcal{G}$ consistent with $\mathfrak{s}$ such that
$|\pi_{1}|\leq|\pi_{2}|\leq\cdots$. For some $\epsilon>0$, let $i_{n}$ be the
smallest number such that

$\mathbb{P}_{\mathfrak{s}}(\pi_{1})+\cdots+\mathbb{P}_{\mathfrak{s}}(\pi_{i_{n}})\geq
p-\epsilon$

where $\mathbb{P}_{\mathfrak{s}}$ is the probability measure induced by
$\mathfrak{s}$ over the set of all runs of $\mathcal{G}$.

We call $|\pi_{n}|$ the _required simulation time_ of $\mathcal{G}$ under
$\mathfrak{s}$ to assimilate a termination probability of $p-\epsilon$. The
required simulation time of $\mathfrak{s}$ is simply the length of the longest
terminating run that must be accounted for in the termination probability
series for it to cross $p-\epsilon$.

Define the simulation time of $\mathcal{G}$ w.r.t. $\epsilon$ as the supremum
over all schedulers $\mathfrak{s}$ of the required simulation time of
$\mathcal{G}$ under $\mathfrak{s}$ and $\epsilon$. The following lemma is at
the core of showing that the almost sure termination problem is
$\Pi^{0}_{2}$-complete (Majumdar and Sathiyanarayana, 2023).

###### Lemma 2.6 (Unrolling Lemma (Majumdar and Sathiyanarayana, 2023)).

Let $\mathcal{G}$ be an $\mathsf{CFG}$ such that
$\Pr_{\mathrm{term}}(\mathcal{G})\geq p$. For any $\epsilon$, the simulation
time of $\mathcal{G}$ w.r.t. $\epsilon$ is bounded above.

Lemma 2.6 is a generalization of Lemma B.3 of Majumdar and Sathiyanarayana
(2023). It holds for $\mathsf{CFG}$s because the branching at nondeterministic
locations is bounded. To prove the unrolling lemma, for each $m\in\mathbb{N}$,
we consider unrollings of $\mathcal{G}$ for $m$ steps, running under partial
schedules that resolve nondeterministic choices for up to $m$ steps. Partial
schedules are naturally ordered into a tree, where a partial schedule
$\mathfrak{s}$ is extended by $\mathfrak{s}^{\prime}$ if
$\mathfrak{s}^{\prime}$ agrees with $\mathfrak{s}$ when restricted to the
domain of $\mathfrak{s}$. An infinite path in this tree defines a scheduler.
For each scheduler $\mathfrak{s}$, we mark the $k$-th node in its path if $k$
is the minimum number such that the $k$-step unrolled program amasses
termination probability at least $p-\epsilon$. If two schedulers agree up to
$k$ steps, then they both mark the same node. The key observation is that,
since the nondeterminism is finite-branching, the scheduler tree is finite-
branching. Thus, if we cut off the tree at marked nodes and still have an
infinite number of incomparable marked nodes, there must be an infinite path
in the tree that is not marked. But this is a contradiction, because this
infinite path corresponds to a scheduler that never amasses $p-\epsilon$
probability mass for termination.

Corollary 2.7 follows directly, and is used multiple times in the proofs of
the soundness and completeness of our rules.

###### Corollary 2.7.

Let $\sigma$ be a state of an $\mathsf{CFG}$ $\mathcal{G}$. Suppose
$\Pr_{\mathrm{term}}(\mathcal{G}(\sigma\allowbreak))>0$. Then, varied across
schedulers, there is an upper bound on the length of the shortest consistent
terminal run from $\sigma$.

###### Proof.

For a scheduler $\mathfrak{s}$, let $\pi_{\mathfrak{s}}$ be the smallest
terminal run of $\mathcal{G}(\sigma)$ consistent with $\mathfrak{s}$. The
simulation time to assimilate a termination probability of $\epsilon$ for some
$0<\epsilon<\Pr_{\mathrm{term}}(\mathcal{G}(\sigma))$ under scheduler
$\mathfrak{s}$ is necessarily at least as large as $|\pi_{\mathfrak{s}}|$. If
the collection of lengths $|\pi_{\mathfrak{s}}|$ across schedulers
$\mathfrak{s}$ wasn’t bounded, then this simulation time is unbounded. This
contradicts the unrolling lemma. ∎

###  2.4. Assertion Language and Program Logic

Our language of choice for specifying assertions is the language of arithmetic
with addition, multiplication, and order interpreted over the domain of
rationals. We fix the interpretation model for our assertions as the standard
model of rationals. Refer to this interpretation by $\mathsf{I}_{\mathbb{Q}}$.
222 Instead of fixing $\mathsf{I}_{\mathbb{Q}}$, one can use any _arithmetical
structure_ (Harel et al., 2000) to specify and interpret assertions. All our
proof rules will remain sound and relatively complete with this change.  Let
$\mathsf{Th}(\mathbb{Q})$ denote the _theory of rationals_ , i.e., the
collection of assertions that are true in the standard model of rationals. The
evaluation of our assertions is tantamount to their implication by
$\mathsf{Th}(\mathbb{Q})$. All proof techniques we present in our work are
relative to complete proof systems for $\mathsf{Th}(\mathbb{Q})$.

Assertions are evaluated at program states. Fix a $\mathsf{CFG}$ $\mathcal{G}$
with transition relation $\mathord{\mapsto}_{\mathcal{G}}$. A state $\sigma$
of $\mathcal{G}$ _satisfies_ an assertion $\varphi$ if the interpretation
$\mathsf{I}_{\mathbb{Q}}$ augmented with the variable valuation encoded in
$\sigma$ models $\varphi$. We denote this by $\sigma\vDash\varphi$. An
assertion $\varphi$ is _valid_ if $\sigma\vDash\varphi$ for all states
$\sigma$. Valid assertions are contained in $\mathsf{Th}(\mathbb{Q})$.

We employ a program logic inspired by the seminal work of Floyd (1993).
Statements in our logic affix assertions as preconditions and postconditions
to transitions in $\mathcal{G}$. For example, the transition
$\tau\in\mathord{\mapsto}_{\mathcal{G}}$ could be affixed a precondition
$\varphi_{\tau}$ and postcondition $\psi_{\tau}$ to yield the sentence
$\\{\varphi_{\tau}\\}\tau\\{\psi_{\tau}\\}$. The precondition $\varphi_{\tau}$
is evaluated at the program state before taking $\tau$, and the postcondition
$\psi_{\tau}$ is evaluated at states reached immediately after $\tau$. The
sentence $\\{\varphi_{\tau}\\}\tau\\{\psi_{\tau}\\}$ is _true_ for
$\mathcal{G}$ if for every state $\sigma$ with $\sigma\vDash\varphi$, if
$\tau$ is enabled at $\sigma$ and $\sigma^{\prime}$ is a successor of $\sigma$
through $\tau$, then $\sigma^{\prime}\vDash\psi_{\tau}$.

We use the notion of _inductive invariants_ in our proof rules. An _inductive
invariant_ is an assertion with $n+1$ free variables, the first ranging over
$L$ and the others over $\mathbb{Q}$, that is closed under the successor
operation. That is, an assertion $\mathsf{Inv}$ is an inductive invariant if,
whenever $(l,\mathbf{x})$ satisfies $\mathsf{Inv}$, and
$(l^{\prime},\mathbf{x}^{\prime})$ is a successor to $(l,\mathbf{x})$, then
$(l^{\prime},\mathbf{x}^{\prime})$ satisfies $\mathsf{Inv}$. It follows that
if $(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$ satisfies $\mathsf{Inv}$,
then every reachable state satisfies $\mathsf{Inv}$.

Floyd (1993) specified axioms for a proof system over this program logic.
_Proof rules_ extend this system by enabling the deduction of complicated
program properties, such as termination. These rules are composed of
_antecedents_ and _consequents_. Antecedents are finite collections of
statements written in the program logic. Consequents detail properties of the
program at which the antecedents are evaluated. _Soundness_ of a proof rule
implies that if the antecedents are true for a program $\mathcal{G}$, then the
consequents hold for $\mathcal{G}$. _Completeness_ of a proof rule implies
that if the consequents are true for some $\mathcal{G}$, then one can come up
with proofs for the antecedents of the rule in the underlying proof system.

The completeness of all proof rules in this work is dependent on the existence
of a complete proof system for $\mathsf{Th}(\mathbb{Q})$. Such proof rules are
said to be complete _relative to a proof system for
$\mathsf{Th}(\mathbb{Q})$_. Relative completeness of this kind is standard in
program logics.

To show the relative completeness of our proof rules, we will need to be able
to encode _computable relations_ in our assertion language. A relation is
computable if its characteristic function is decidable. It is known that the
theory of arithmetic interpreted over natural numbers can encode all
computable relations. Let $\mathsf{I}_{\mathbb{N}}$ refer to the
interpretation model of the standard model of naturals. Denote by
$\mathsf{Th}(\mathbb{N})$ the collection of all true assertions under
$\mathsf{I}_{\mathbb{N}}$. $\mathsf{Th}(\mathbb{N})$ is generally referred to
as the theory of natural numbers. Thus, for each computable relation
$R(x_{1},x_{2},\ldots x_{n})$, there is an assertion
$\varphi_{R}(x_{1},x_{2},\ldots x_{n})$ that is true in
$\mathsf{Th}(\mathbb{N})$. To represent computable relations in
$\mathsf{Th}(\mathbb{Q})$, we use a result by Robinson (1949).

###### Theorem 2.8 (Robinson (1949)).

$\mathbb{N}$ is definable in $\mathsf{Th}(\mathbb{Q})$.

We refer to the assertion that encodes $\mathbb{N}$ by $\mathsf{Nat}$.
Therefore, $\mathsf{Nat}(x)$ is true in $\mathsf{I}_{\mathbb{Q}}$ _iff_
$x\in\mathbb{N}$. All computable relations can be encoded in our assertion
language through liberal usage of $\mathsf{Nat}$. An important implication is
that termination probabilities are expressible in our assertion language.

###### Lemma 2.9.

For a $\mathsf{CFG}$ $\mathcal{G}$ and a $p\in[0,1]$ with
$\Pr_{\mathrm{term}}(\mathcal{G})=p$, there is an assertion $\psi(x)$ with one
free variable $x$ such that
$\mathsf{Th}(\mathbb{Q})\vDash\psi(x)\Leftrightarrow x\leq p$.

###### Proof.

We know that $\Pr_{\mathrm{term}}(\mathcal{G})\geq p$ _iff_
$\Pr_{\mathrm{term}}(\mathcal{G})\geq p-\epsilon$ for all $\epsilon>0$. The
unrolling lemma implies that for all $\epsilon>0$, there is a $k\in\mathbb{N}$
such that the probability mass of the $k$-unrolled program is at least
$p-\epsilon$. Finite unrollings of $\mathcal{G}$ are, by definition,
computable, and checking the probability of termination amassed in this finite
unrolling is also computable; see Kaminski et al. (2019) for details. This
means that a relation $R(\epsilon,k)$ representing this relationship between
every rational $\epsilon$ and natural $k$. Such computable relations are
representable in $\mathsf{Th}(\mathbb{Q})$ through Theorem 2.8, completing the
proof. ∎

Notice that while the termination probabilities $p$ are real numbers, the
lower bounds verified by the assertion $\psi$ in the above lemma are entirely
rational. However, by representing the set of rational numbers under $p$,
$\psi$ has effectively captured the Dedekind cut of $p$. This expressibility
shows how irrational lower bounds on termination probabilities can be deduced
using our proof techniques.

##  3\. Almost-Sure Termination: Martingales

In all rules in this work, we fix a $\mathsf{CFG}$ $\mathcal{G}=(L,\allowbreak
V,\allowbreak
l_{init},\allowbreak\mathbf{x}_{init},\allowbreak\mathord{\mapsto},\allowbreak
G,\allowbreak\mathsf{Pr},\allowbreak\mathsf{Upd})$. We also abuse notation
slightly and use the inductive invariant $\mathsf{Inv}$ as a shorthand for all
states of $\mathcal{G}$ satisfying the predicate $\mathsf{Inv}$.

Our proof rules consist of sets and functions over the state spaces that
satisfy certain properties. Each of these entities must be representable in
our assertion language; therefore, they must be arithmetical expressions over
the program variables and program locations. Instead of specifying each
condition in our rules as formal statements in our program logic, we directly
describe the properties these entities must satisfy. We do so to emphasize
these entities themselves over the formalism surrounding them. It is
nevertheless possible to write each of the following proof rules as finite
sets of statements in the program logic.

Recall that a proof rule is _sound_ if, whenever we can find arithmetical
expressions in our assertion language that satisfy the conditions outlined in
the premise of a rule, the conclusion of the rule holds. A proof rule is
_relatively complete_ if, whenever the conclusion holds (e.g., a program
$\mathcal{G}$ is $\mathsf{AST}$), we can find certificates in the assertion
language that satisfy all the premises.

###  3.1. McIver and Morgan’s Variant Rule

We start with a well-known rule for almost-sure termination from (McIver and
Morgan, 2005). The rule is sound but complete only for finite-state programs
McIver and Morgan (2005, Lemma 7.6.1).

If there is (1) an inductive invariant $\mathsf{Inv}$ containing the initial
state $(l_{init},\mathbf{x}_{init})$, (2) a function
$U:\mathsf{Inv}\to\mathbb{Z}$, (3) bounds $\mathsf{Lo}$ and $\mathsf{Hi}$ such
that for all states $(l,\mathbf{x})\in\mathsf{Inv}$, $\mathsf{Lo}\leq
U(l,\mathbf{x})<\mathsf{Hi}$, and (4) an $\epsilon>0$, such that, for each
state $(l,\mathbf{x})\in\mathsf{Inv}$, (a) if $(l,\mathbf{x})$ is a terminal
state, $U(l,\mathbf{x})=0$. (b) if $(l,\mathbf{x})$ is an assignment, or
nondeterministic state, $U(l^{\prime},\mathbf{x}^{\prime})<U(l,\mathbf{x})$
for every successor $(l^{\prime},\mathbf{x}^{\prime})$. (c) if
$(l,\mathbf{x})$ is a probabilistic state,
$\sum\mathsf{Pr}(l,l^{\prime})[\mathbf{x}]>\epsilon$ over all successor states
$(l^{\prime},\mathbf{x}^{\prime})$ with
$U(l^{\prime},\mathbf{x}^{\prime})<U(l,\mathbf{x})$. Then, $\mathcal{G}$ is
$\mathsf{AST}$.

###### Lemma 3.1 (McIver and Morgan (2005)).

Section 3.1 is sound for all $\mathsf{AST}$ programs. It is relatively
complete for finite-state $\mathsf{AST}$ $\mathsf{CFG}$s.

While McIver and Morgan (2005) claim completeness and not relative
completeness, their proof trivially induces relative completeness. This rule
is not complete, however. This is because, if the rule is applicable, the
program is guaranteed a terminal run of length at most
$\mathsf{Hi}-\mathsf{Lo}$ from any state. But the 1D random walk (outlined in
Example 2.5) does not satisfy this property, even though it terminates almost-
surely.

Over the years, McIver and Morgan’s proof rule has been extended many times
(McIver et al., 2018; Huang et al., 2018). The most significant extension is
the proof rule of McIver et al. (2018), where they require the function $U$ to
additionally be a supermartingale. None of these extensions have managed to be
proven complete. Because we do not use ideas from these extensions, we do not
present them here.

###  3.2. Our Rule

We present a martingale-based proof rule for $\mathsf{AST}$ that exploits the
fact that $\mathsf{AST}$ programs, when repeatedly run, are recurrent.  If
there exists (1) an inductive invariant $\mathsf{Inv}$ containing the initial
state, (2) a set $A\subset\mathsf{Inv}$ containing the terminal state, (3) a
supermartingale function $V:\mathsf{Inv}\to\mathbb{R}$ that assigns $0$ to the
terminal state and at all states $(l,\mathbf{x})\in\mathsf{Inv}\setminus A$,
(a) $V(l,\mathbf{x})>0$, (b) $V(l,\mathbf{x})>V(l_{A},\mathbf{x}_{A})$ for
each $(l_{A},\mathbf{x}_{A})\in A$, (c) if $(l,\mathbf{x})$ is an assignment
or nondeterministic state, then $V(l,\mathbf{x})\geq
V(l^{\prime},\mathbf{x}^{\prime})$ for all possible successor states
$(l^{\prime},\mathbf{x}^{\prime})$, and (d) if $(l,\mathbf{x})$ is a
probabilistic state, then, over all successor states
$(l^{\prime},\mathbf{x}^{\prime})$,
$V(\sigma)\geq\sum\Pr(l,l^{\prime})\allowbreak
V(l^{\prime},\mathbf{x}^{\prime})$, (4) a variant function
$U:\mathsf{Inv}\to\mathbb{N}$ that (a) assigns $0$ to the terminal state, (b)
ensures that at nondeterministic and assignment states
$(l,\mathbf{x})\in\mathsf{Inv}$,
$U(l,\mathbf{x})>U(l^{\prime},\mathbf{x}^{\prime})$ for all possible successor
states $(l^{\prime},\mathbf{x}^{\prime})$, and (c) satisfies the following
compatibility criteria with the sublevel sets $V_{\leq
r}=\\{\sigma\in\mathsf{Inv}\mid V(\sigma)\leq r\\}$ for each $r\in\mathbb{R}$:
(i) the set $\\{u\in\mathbb{N}\mid\sigma\in V_{\leq r}\land u=U(\sigma)\\}$ is
bounded, and (ii) there exists an $\epsilon_{r}>0$ such that, for all
probabilistic states $(l,\mathbf{x})\in V_{\leq r}$, the sum
$\sum\mathsf{Pr}(l,l^{\prime})[\mathbf{x}]>\epsilon_{r}$ over all successor
states $(l^{\prime},\mathbf{x}^{\prime})$ with
$U(l^{\prime},\mathbf{x}^{\prime})<U(l,\mathbf{x})$. Under these conditions,
$\mathcal{G}$ is $\mathsf{AST}$.

In this rule, $U$ is meant to play the role of the variant function from
Section 3.1. $A$ is meant to form a “ball” around the terminal state; it is
useful in applications where the supermartingale properties of $V$ are
difficult to establish at all states. If the execution were to be restricted
within this ball $A$, the rule makes it easy to establish almost-sure
termination. This is because while $V$ must only be a supermartingale outside
of $A$, the variant $U$ must still decrease within $A$. Observe that $A$ must
be a strict subset of $\mathsf{Inv}$; this is to enforce an upper bound on the
collection of $V$-values of states in $A$. It’s easy to see that this rule
reduces to Section 3.1 if the supermartingale $V$ was bounded.

Intuitively, $V$ can be thought of as a measure of _relative likelihood_. The
probability that a transition increases $V$ by an amount $v$ reduces as $v$
increases. Unlikely transitions are associated with greater increments to $V$,
and (relatively) unlikely states have greater $V$ values. Separately, the
variant $U$ reprises its role from Section 3.1: it effectively measures the
shortest distance to a terminal state.

At a high level, Section 3.2 works for the following reasons. Suppose $V$ is
unbounded and executions begin at some initial state
$\sigma_{0}\in\mathsf{Inv}$. The supermartingale property of $V$ implies that
from $\sigma_{0}$, the probability of reaching a state $\sigma$ with
$V(\sigma)>V(\sigma_{0})$ approaches $0$ as $V(\sigma)$ grows to $+\infty$.
Now, fix an unlikely state $\sigma$ with $V(\sigma)\gg V(\sigma_{0})$. Let’s
now restrict our attention to the executions that remain in states
$\gamma\in\mathsf{Inv}$ with $V(\gamma)\leq V(\sigma)$. The compatibility
conditions satisfied by the variant $U$ with $V$ at the sublevel set $V_{\leq
V(\sigma)}$ implies the almost-sure termination of these executions. The
remaining executions must reach some unlikely state $\gamma^{\prime}$ with
$V(\gamma^{\prime})\geq V(\sigma)$.

Thus, as the probability of reaching unlikely states $\gamma^{\prime}$ reduces
the “further away” (from the perspective of $V$) they are, the probability of
terminating approaches $1$. Since $V$ is unbounded, the probability of
termination is $1$.

_Remark._ We note that our rule is quite similar to the $\mathsf{AST}$ rule of
McIver et al. (2018). Their rule consisted of a single supermartingale $V$
that, with the help of a few antitone functions, also exhibited the properties
of a distance variant. In other words, they combined the duties of the
functions $V$ and $U$ into a single function $V$. It is not known if their
rule is complete.

###### Lemma 3.2 (Soundness).

Section 3.2 is sound.

###### Proof.

Let us first dispense of the case where $V$ is bounded. If $V$ is bounded, the
compatibility criteria forces a bound on the variant function $U$. The
soundness of Section 3.1 implies $\mathcal{G}\in\mathsf{AST}$. Therefore, from
now on, $V$ is assumed to be unbounded.

Denote the initial state by $\sigma_{0}$. For each $n\in\mathbb{N}$, define
$\Pi_{n}$ to be the collection of runs from $\sigma_{0}$ that reach a maximum
$V$ value of $n$. This means that for each state $\sigma$ encountered in
executions in $\Pi_{n}$, $V(\sigma)\leq n$. Define $\Pi_{\infty}$ to be the
remaining collection of executions beginning at $\sigma_{0}$ that don’t have a
bound on the $V$ values that they reach. This means that for each execution
$\pi\in\Pi_{\infty}$ and each $n\in\mathbb{N}$, there are states
$\sigma\in\pi$ such that $V(\sigma)>n$. We have thus partitioned the
collection of executions of the $\mathsf{CFG}$ $\mathcal{G}$ to
$\Pi_{\infty}\cup(\bigcup_{i\in\mathbb{N}}\Pi_{i})$.

We will now argue that under every scheduler, the probability measure of all
non-terminating executions in each $\Pi_{n}$ is $0$. By definition, all
executions in $\Pi_{n}$ lie entirely within the sublevel set $V_{\leq n}$. The
compatibility of $U$ with $V_{\leq n}$ implies that the variant $U$ is bounded
across states in $\Pi_{n}$. Consider an $\mathsf{CFG}$ $\mathcal{G}_{\leq n}$
that mirrors $\mathcal{G}$ inside $V_{\leq n}$, but marks states in
$\mathcal{G}$ outside $V_{\leq n}$ as terminal. Applying Section 3.1 using the
now bounded variant $U$ allows us to deduce that $\mathcal{G}_{\leq n}$ is
almost-surely terminating. Observe now that the collection of non-terminating
runs of $\mathcal{G}_{\leq n}$ is precisely the collection of non-terminating
runs in $\Pi_{n}$. This immediately gives us what we need.

We now turn our attention to the final collection $\Pi_{\infty}$. Observe that
$\Pi_{\infty}$ must only contain non-terminal executions. Suppose that, under
some scheduler $\mathfrak{s}$, the probability measure of $\Pi_{\infty}$
wasn’t $0$. Let the probability space defining the semantics of $\mathcal{G}$
under $\mathfrak{s}$ (see Section 2.1) be
$(\mathsf{Runs}_{\mathcal{G}(\sigma)},\mathcal{F}_{\mathcal{G}(\sigma)},\mathbb{P}_{\mathfrak{s}})$,
and let its canonical filtration be $\\{\mathcal{F}_{n}\\}$. Define a
stochastic process $\\{X^{\mathfrak{s}}_{n}\\}$ over the aforementioned
probability space augmented with the filtration $\\{\mathcal{F}_{n}\\}$ that
tracks the current state of the execution of the program. Define another
stochastic process $\\{Y^{\mathfrak{s}}_{n}\\}$ as

$Y^{\mathfrak{s}}_{n}\triangleq\begin{cases}V(X^{\mathfrak{s}}_{n})&X^{\mathfrak{s}}_{n}\not\in
A\\\ 0&\text{otherwise}\end{cases}$

It’s easy to see that $Y^{\mathfrak{s}}_{n}$ is a non-negative
supermartingale. Since $Y^{\mathfrak{s}}_{n}$ is non-negative, Doob’s
Martingale Convergence Theorem (Doob, 1953) implies the almost-sure existence
of a random variable $Y^{\mathfrak{s}}_{\infty}$ that the process
$\\{Y^{\mathfrak{s}}_{n}\\}$ converges to. This means that
$\mathbb{E}[Y^{\mathfrak{s}}_{\infty}]\leq Y^{\mathfrak{s}}_{0}$.

Under the condition that $\Pi_{\infty}$ occurs,
$Y^{\mathfrak{s}}_{\infty}=+\infty$. Since the probability measure of these
non-terminal executions isn’t $0$, we have that
$\mathbb{E}[Y^{\mathfrak{s}}_{\infty}]=+\infty>Y^{\mathfrak{s}}_{0}=V(X^{\mathfrak{s}}_{0})$.
This raises a contradiction, completing the proof. ∎

To show completeness, we adapt a technique by Mertens et al. (1978) to build
the requisite supermartingale $V$. Suppose $\mathcal{G}$ is $\mathsf{AST}$.
Let $\mathsf{Reach}(\mathcal{G})$ be the set of its reachable states. Fix a
computable enumeration $\mathsf{Enum}$ of $\mathsf{Reach}(\mathcal{G})$ that
assigns $0$ to its terminal state. Intuitively, $\mathsf{Enum}$ is meant to
order states in a line so that the probability of reaching a state that’s far
to the right in this order is small. This is because the $\mathsf{AST}$ nature
of $\mathcal{G}$ forces executions to “lean left” toward the terminal state.
Note that we place no other requirements on $\mathsf{Enum}$; these intuitions
will work no matter how $\mathsf{Enum}$ orders the states. A state $\sigma$ is
said to be indexed $i$ if $\mathsf{Enum}(\sigma)=i$. From now on, we will
refer to the state indexed $i$ by $\sigma_{i}$.

A crucial part of our construction is the following function
$R:(\mathbb{N}\times\mathbb{N})\to[0,1]$. Intuitively, $R$ measures the
ability of executions beginning from a state to reach states that are far to
the right of it in the $\mathsf{Enum}$ order. Let $\mathcal{G}_{i}$ be the
$\mathsf{CFG}$ obtained from $\mathcal{G}$ by switching its initial state to
$\sigma_{i}$. Let the semantics of $\mathcal{G}_{i}$ under a scheduler
$\mathfrak{s}$ be the probability space
$(\mathsf{Runs}_{\mathcal{G}_{i}},\allowbreak\mathcal{F}_{\mathcal{G}_{i}},\allowbreak\mathbb{P}^{i}_{\mathfrak{s}})$.
Define $R(i,n)$ at indices $i$ and $n$ to be

(1)
$R(i,n)\triangleq\inf{}_{\mathfrak{s}}\mathbb{P}^{i}_{\mathfrak{s}}\left(\Diamond\left(\left\\{\sigma_{m}\in\mathsf{Reach}(\mathcal{G})\mid
m\geq n\right\\}\right)\right)$

Where $\Diamond(C)$ represents the event of eventually reaching the set $C$.
We will refer to the first argument $i$ as the source index and the second
argument $n$ as the minimum target index. Put simply, $R(i,n)$ measures the
infimum probability of reaching the target indices $\\{n,n+1,\ldots\\}$ from
the source $\sigma_{i}$.

###### Lemma 3.3.

$R(i,n)\to 0$ as $n\to\infty$ at every $i\in\mathbb{N}$, i.e., $\forall
i\in\mathbb{N}\cdot\lim_{n\to\infty}R(i,n)=0$.

###### Proof.

Denote by $E_{n}$ the event that executions beginning from $\sigma_{i}$ reach
states with index $\geq n$. Clearly, $R(i,n)$ measures the infimum probability
of $E_{n}$. Denote by $E_{\infty}$ the event that executions beginning from
$\sigma_{i}$ increase the maximum observed state index infinitely often. It’s
easy to see that, for every $n\in\mathbb{N}$, the event $E_{n}$ contains
$E_{\infty}$. Also, each execution outside $E_{\infty}$ must be inside some
$E_{n}\setminus E_{n+1}$, as it must yield a maximum state index contained in
it. Additionally, $E_{n+1}\subseteq E_{n}$ for all $n$. These three facts
imply

$E_{\infty}=\bigcap_{i\in\mathbb{N}}E_{n}=\lim_{n\to\infty}E_{n}$

Suppose that, $\lim_{n\to\infty}R(i,n)>0$ for some index $i$. Since
$R(i,n)=\inf{}_{\mathfrak{s}}\mathbb{P}^{i}_{\mathfrak{s}}[E_{n}]$, we have

$\inf{}_{\mathfrak{s}}\mathbb{P}^{i}_{\mathfrak{s}}[E_{\infty}]=\inf{}_{\mathfrak{s}}\left(\lim_{n\to\infty}\mathbb{P}^{i}_{\mathfrak{s}}[E_{n}]\right)=\lim_{n\to\infty}\inf{}_{\mathfrak{s}}\mathbb{P}^{i}_{\mathfrak{s}}[E_{n}]=\lim_{n\to\infty}R(i,n)>0$

As all executions in $E_{\infty}$ are non-terminating, this contradicts the
$\mathsf{AST}$ nature of $\mathcal{G}$. ∎

It turns out that, if we fix the minimum target index $n$, the function $R$
becomes a supermartingale. Define $V_{n}(\sigma)=R(\mathsf{Enum}(\sigma),n)$
for every $n\in\mathbb{N}$. It’s easy enough to see that $V_{n}$ is a
supermartingale; for assignment / non-deterministic states $\sigma$ with
possible successors $\sigma^{\prime}$, $V_{n}(\sigma)\geq
V_{n}(\sigma^{\prime})$, and for probabilistic $\sigma=(l,\mathbf{x})$,
$V_{n}(l,\mathbf{x})\geq\sum\mathsf{Pr}(l,l^{\prime})V_{n}(l^{\prime},\mathbf{x})$
across all successors $(l^{\prime},\mathbf{x})$. However, $V_{n}$ isn’t the
supermartingale we need, as we may not always be able to construct a
compatible $U$ for any $V_{n}$. This is because every $V_{n}$ is bounded above
(by $1$), whereas $U$ typically isn’t bounded above.

To construct an unbounded supermartingale, one could consider the sum $\sum
V_{n}$ varied across all $n\in\mathbb{N}$. However, this sum could be $\infty$
for certain states. To combat this, we carefully choose an infinite subset of
$\mathbb{N}$ to form the domain for $\sum V_{n}$. Consider the sequence
$(n_{j})_{j\in\mathbb{N}}$ such that $n_{j}$ is the smallest number so that
$R(i,n_{j})\leq 2^{-j}$ for all $i\leq j$. Each element in this sequence is
certain to exist due to the monotonically non-increasing nature of $R(i,n)$
for fixed $i$ and the limit result of Lemma 3.3. Furthermore, restricting the
domain of $\sum V_{n}$ to elements in $(n_{j})_{j\in\mathbb{N}}$ will mean
that no state is assigned $\infty$ by the sum. This is because for each
$\sigma$, the values of $V_{n_{j}}(\sigma)=R(\mathsf{Enum}(\sigma),n_{j})$
will certainly repeatedly halve after $j\geq\mathsf{Enum}(\sigma)$. Further
note that the supermartingale nature of the $V_{n}$ implies that this sum is
also a supermartingale. We thus have our required supermartingale

(2)
$V(\sigma)=\sum_{j\in\mathbb{N}}V_{n_{j}}(\sigma)=\sum_{j\in\mathbb{N}}R(\mathsf{Enum}(\sigma),n_{j})$

###### Lemma 3.4 (Completeness).

Section 3.2 is relatively complete.

###### Proof.

Take an $\mathsf{AST}$ $\mathsf{CFG}$ $\mathcal{G}$, and set $\mathsf{Inv}$
and $A$ to $\mathsf{Reach}(\mathcal{G})$ and the singleton set containing the
terminal state respectively. We first describe our choice for the variant
function $U$. Since $\mathcal{G}$ is $\mathsf{AST}$, for every
$\sigma\in\mathsf{Reach}(\mathcal{G})$, every scheduler must induce a finite
path to a terminal state. Corollary 2.7 implies an upper bound on the length
of the shortest terminal run from every $\sigma\in\mathsf{Inv}$. Set $U$ to
map each $\sigma\in\mathsf{Inv}$ to this upper bound.

If $U$ is bounded, setting $V(\sigma)=1$ for all $\sigma\in\mathsf{Inv}$
suffices. Otherwise, set $V$ to the supermartingale function defined in Eq. 2.
It is easy to observe that for every $r$, the sublevel set $V_{\leq
r}=\\{\sigma\mid V(\sigma)<r\\}$ is finite. This implies that $U$ is bounded
within every sublevel set, and is hence compatible with this $V$. This
completes the construction of the certificates required by the proof rule.

We now argue that the invariant $\mathsf{Inv}$, the set $A$, the
supermartingale $V$ and variant $U$ can each be represented in our assertion
language of arithmetic interpreted over the rationals. We do this by encoding
them first encoding them in the theory of natural numbers, and then using the
relation $\mathsf{Nat}$ from Theorem 2.8 to insert them into our assertion
language. Recall that all computable relations can be encoded in
$\mathsf{Th}(\mathbb{Q})$. We present techniques with which one can augment
computable relations with first-order quantifiers to represent these entities.
By doing so, we demonstrate that these sets are _arithmetical_ ; see the works
of Kozen (2006) and Rogers Jr. (1987) for detailed accounts on arithmetical
sets.

$A$ can trivially be represented in $\mathsf{Th}(\mathbb{Q})$. For
$\mathsf{Inv}$, consider the relation $I$ that contains tuples of the form
$(k,\sigma_{1},\sigma_{2})$ where $k\in\mathbb{N}$ and $\sigma_{1}$ and
$\sigma_{2}$ are states of $\mathcal{G}$. Require
$(k,\sigma_{1},\sigma_{2})\in I$ _iff_ there is a finite path of length $\leq
k$ from $\sigma_{1}$ to $\sigma_{2}$. Clearly, $I$ is a computable relation
and is thus representable in $\mathsf{Th}(\mathbb{Q})$. $\mathsf{Inv}(\sigma)$
can be represented from $I$ as $\exists k\cdot I(k,\sigma_{0},\sigma)$ where
$\sigma_{0}$ is the initial state of $\mathcal{G}$. Similarly, the output of
$U(\sigma)$ at every $\sigma$ can be represented using $I$ as
$U(\sigma)=k\allowbreak\Longleftrightarrow\allowbreak
I(\sigma,\sigma_{\bot},k)\allowbreak\land\left(\forall n<k\cdot\lnot
I\left(\sigma,\sigma_{\bot},n\right)\right)$, where $\sigma_{\bot}$ is the
terminal state. If $U$ were bounded, representing $V$ is trivial; we focus our
attention on representing $V$ when $U$ isn’t bounded.

Representations of $R$ (defined in Eq. 1 and used to derive $V$) and $V$ are
complicated slightly because they can output real numbers. Instead of
capturing the precise values of these functions, we capture their Dedekind
cuts instead. In other words, we show that the collections of rational numbers
$\leq V(\sigma)$, $\geq V(\sigma)$, $\leq\varphi_{i}(n)$ and
$\geq\varphi_{i}(n)$ are each representable for each $\sigma$, $i$, and $n$.

The unrolling lemma implies that if the probability of termination is $p$,
then for all $n\in\mathbb{N}$, assimilating a termination probability mass of
at least $p-1/n$ requires finitely many steps. It is simple to generalize this
to observe that assimilating a probability mass of at least $R(i,n)-1/n$ for
the event $\Diamond\left(\left\\{\sigma_{m}\in\mathsf{Inv}\mid m\geq
n\right\\}\right)$ when $\sigma_{i}$ is the initial state also requires
finitely many steps. Furthermore, computing the probability of the occurrence
of this event within $k$ steps is computable for every natural number $k$.
These two facts indicate that lower bounds on $R(i,n)$ can be represented in
$\mathsf{Th}(\mathbb{Q})$. Upper bounds on $R(i,n)$ can be represented by
simply negating this lower bound representation.

Using these, enable the representation of each member of the sequence
$(n_{j})_{j\in\mathbb{N}}$ that forms the domain of the sum that defines $V$.
This enables representations of lower bounds on $V(\sigma)$, which in turn
enables representations of upper bounds on $V(\sigma)$. Thus, the Dedekind cut
of $V(\sigma)$ is representable in $\mathsf{Th}(\mathbb{Q})$. This completes
the proof. ∎

###### Example 3.5 (Random Walks).

For the 1DRW example from Example 2.5, we take $\mathsf{Inv}$ to be all
program states, $A$ to be the set containing the single terminal state
$\\{x_{1}\coloneqq 0\\}$, and we set $V(x)=U(x)\coloneqq|x|$. It’s trivial to
observe that all conditions required in Section 3.2 are met, and therefore,
the 1DRW is $\mathsf{AST}$.

Let us now consider the 2-D Random Walker (2DRW). The $\mathsf{AST}$ nature of
this program has been notoriously hard to prove using prior rules. The
principal enabler of our rule on the 2DRW is its set $A$ that forms a circle
around the origin.

Begin by setting $\mathsf{Inv}$ to the set of all states. Declare the distance
variant $U$ to be the Manhattan distance $|x|+|y|$ of any state $(x,y)$ from
the origin. Clearly, $U$ has a $\geq 1/4$ probability of reducing in a single
step from every state. Now, define $V$ as

$V(x,y)\triangleq\sqrt{\ln\left(1+\sqrt{x^{2}+y^{2}}\right)}$

It is difficult to prove that $V$ is a supermartingale for all non-terminal
states. However, using Taylor series expansions, one can show that $V$ is a
supermartingale for “sufficiently large” values of $x^{2}+y^{2}$. Menshikov et
al. (2017) (see also Popov (2021, Section 2.3)) showed precisely this; their
proof showed that the error terms in the Taylor series expansion of $V(x,y)$
cease to matter when $x^{2}+y^{2}$ grow large. They prove that there must
exist a number $k$ such that the error terms in the Taylor expansion do not
affect the non-negativity conditions at states where $x^{2}+y^{2}>k$. We now
declare $A$ to be the set of states $(x,y)$ where $x^{2}+y^{2}\leq k$. Thus,
$V$ satisfies the supermartingale conditions of Section 3.2 outside of $A$.
Note that we don’t need to precisely decipher the value of $k$ for the
soundness of the proof rule to work; we just need $A$ to be smaller than the
invariant $\mathsf{Inv}$. The finiteness of $A$ satisfies this criterion.
Furthermore, since the sublevel set $V_{\leq r}$ is finite, $V$ is compatible
with $U$. Therefore, the 2DRW is $\mathsf{AST}$. ∎

##  4\. Almost-Sure Termination: Stochastic Invariants

Next, we give a different proof rule that takes a dual view. Instead of a
single unbounded supermartingale, we consider several bounded supermartingales
that each focus on different finite parts of the program’s state space. This
focus means that each of these supermartingales takes on non-trivial values
(i.e., between $0$ and $1$) at only finitely many states. They are thus
“local” supermartingales, i.e., they are only meaningful at particular parts
of the state space.

The key to our rule is the observation that a program is almost surely
terminating if, for every $\epsilon>0$, we can show that it terminates with
probability at least $\epsilon$. We characterize this “$\epsilon$-wiggle room”
using the stochastic invariants of Chatterjee et al. (2017).

###### Definition 4.1 (Stochastic Invariants (Chatterjee et al., 2017)).

Let $\mathcal{G}=(L,V,\allowbreak
l_{init},\mathbf{x}_{init},\mathord{\mapsto},G,\mathsf{Pr},\mathsf{Upd})$ be a
$\mathsf{CFG}$. Suppose $\mathbf{\Psi}$ is a subset of states and let $p$ be a
probability value. The tuple $(\mathbf{\Psi},p)$ is a _stochastic invariant_
(SI) if, under any scheduler $\mathfrak{s}$, the probability mass of the
collection of runs beginning from
$(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$ leaving $\mathbf{\Psi}$ is
bounded above by $p$, i.e.,

$\sup{}_{\mathfrak{s}}\mathbb{P}{}_{\mathfrak{s}}\left[\rho\in\mathsf{Runs}_{\mathcal{G}}\mid\exists
n\in\mathbb{N}\cdot\rho[n]\not\in\mathbf{\Psi}\right]\leq p$

Intuitively, stochastic invariants generalize the standard notion of
invariants to the probabilistic setting. Given a stochastic invariant
$(\mathbf{\Psi},p)$, the program execution is expected to hold $\mathbf{\Psi}$
(i.e., remain inside $\mathbf{\Psi}$) with probability $\geq 1-p$. As with
invariants, the collection of states in stochastic invariants is typically
captured by a predicate written in the assertion language of the program
logic. In this work however, we do not characterize stochastic invariants
directly; we instead use stochastic invariant indicators.

###### Definition 4.2 (Stochastic Invariant Indicator (Chatterjee et al.,
2022)).

Let $\mathcal{G}$ be the $\mathsf{CFG}$
$(L,V,l_{init},\allowbreak\mathbf{x}_{init},\mathord{\mapsto},G,\mathsf{Pr},\mathsf{Upd})$.
A tuple $(\mathsf{SI},p)$ is a _stochastic invariant indicator_ (SI-indicator)
if $p$ is a probability value and
$\mathsf{SI}:L\times\mathbb{Z}^{V}\to\mathbb{R}$ is a partial function such
that $\mathsf{SI}(l_{init},\mathbf{x}_{init})\leq p$, and for all states
$(l,\mathbf{x})$ reachable from
$(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$,

  1. (1)

$\mathsf{SI}(l,\mathbf{x})\geq 0$.

  2. (2)

if $(l,\mathbf{x})$ is an assignment or nondeterministic state, then
$\mathsf{SI}(l,\mathbf{x})\geq\mathsf{SI}(l^{\prime},\mathbf{x}^{\prime})$ for
every successor $(l^{\prime},\mathbf{x}^{\prime})$.

  3. (3)

if $(l,\mathbf{x})$ is a probabilistic state, then
$\mathsf{SI}(l,\mathbf{x})\geq\sum\mathsf{Pr}((l,l^{\prime}))[\mathbf{x}]\times\mathsf{SI}(l^{\prime},\mathbf{x}^{\prime})$
over all possible successor states $(l^{\prime},\mathbf{x}^{\prime})$.

Observe that functions $\mathsf{SI}$ in the SI-indicators are supermartingale
functions. These $\mathsf{SI}$ are typically most interesting at states
$\sigma$ where $\mathsf{SI}(\sigma)<1$; in fact, the collection of states
$\sigma$ with this property corresponds to an underlying stochastic invariant
with the same probability value as the SI-indicator. This was formally proven
by Chatterjee et al. (2022).

###### Lemma 4.3 ((Chatterjee et al., 2022)).

Let $\mathcal{G}$ be an $\mathsf{CFG}$. For each stochastic invariant
$(\mathbf{\Psi},p)$ of $\mathcal{G}$, there exists a stochastic invariant
indicator $(\mathsf{SI},p)$ of $\mathcal{G}$ such that
$\mathbf{\Psi}\supseteq\\{\gamma\in\Sigma_{\mathcal{G}}\mid\mathsf{SI}(\gamma)<1\\}$.
Furthermore, for each stochastic invariant indicator $(\mathsf{SI},p)$ of
$\mathcal{G}$, there is a stochastic invariant $(\mathbf{\Psi},p)$ such that
$\mathbf{\Psi}=\\{\gamma\in\Sigma_{\mathcal{G}}\mid\mathsf{SI}(\gamma)<1\\}$.

The SI-indicator $\mathsf{SI}$ corresponding to the stochastic invariant
$\mathbf{\Psi}$ maps each state $\sigma$ the probability with which runs
beginning from $\sigma$ exit $\mathbf{\Psi}$. Thus, the SI-indicator tracks
the probability of violating the stochastic invariant. Observe that
$\mathsf{SI}(\sigma)\geq 1$ for all states $\sigma\not\in\mathbf{\Psi}$.

We will use SI-indicators in our proof rules. Note that we cannot use a single
stochastic invariant: this is too weak to ensure soundness. Instead, we use a
family of stochastic invariants, one for each reachable state. Unlike
stochastic invariants, representing SI-indicators is more complicated. Because
SI-indicators map states to reals, we cannot always write them directly in our
assertion language. At all $\mathsf{AST}$ programs, we will nevertheless show
that one can always find expressions in our assertion language to effectively
represent the SI-indicators our proof rule needs.

$\mathsf{AST}$ is a property that holds when the initial state is changed to
any reachable state. If $\mathcal{G}$ is almost surely terminating, then
$\mathcal{G}$ is almost surely terminating from any state $\sigma$ reachable
from the initial state
$\sigma_{0}=(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$. Furthermore, if
from every reachable state $\sigma$, $\mathcal{G}$ is known to terminate with
some minimum probability $\epsilon>0$, then the program is $\mathsf{AST}$. We
exploit these facts in our rule.

If, for a fixed $0<p<1$, there exists (1) an inductive invariant
$\mathsf{Inv}$ containing the initial state, (2) a mapping $\mathsf{SI}$ from
each $\sigma\in\mathsf{Inv}$ to SI-indicator functions
$(\mathsf{SI}_{\sigma},p):\mathsf{Inv}\to\mathbb{R}$ such that
$\mathsf{SI}_{\sigma}(l,\mathbf{x})\leq p$ and, for all
$(l,\mathbf{x})\in\mathsf{Inv}$, (a) $\mathsf{SI}_{\sigma}(l,\mathbf{x})\geq
0$. (b) if $(l,\mathbf{x})$ is an assignment, or nondeterministic state, then
$\mathsf{SI}_{\sigma}(l,\mathbf{x})\geq\mathsf{SI}_{\sigma}(l^{\prime},\mathbf{x}^{\prime})$
for every successor $(l^{\prime},\mathbf{x}^{\prime})$. (c) if
$(l,\mathbf{x})$ is a probabilistic state, then
$\mathsf{SI}_{\sigma}(l,\mathbf{x})\geq\sum\mathsf{Pr}((l,l^{\prime}))[\mathbf{x}]\times\mathsf{SI}_{\sigma}(l^{\prime},\mathbf{x}^{\prime})$
over all possible successor states $(l^{\prime},\mathbf{x}^{\prime})$. (3) a
mapping $\mathcal{E}$ mapping states $\sigma\in\mathsf{Inv}$ to values
$\epsilon_{\sigma}\in(0,1]$, (4) a mapping $\mathcal{H}$ mapping states
$\sigma\in\mathsf{Inv}$ to values $H_{\sigma}\in\mathbb{N}$, (5) a mapping
$\mathcal{U}$ from each $\sigma\in\mathsf{Inv}$ to variants
$U_{\sigma}:\mathsf{Inv}\to\mathbb{N}$ that is bounded above by
$\mathcal{H}(\sigma)$, maps all states
$\\{\gamma\mid\mathsf{SI}_{\sigma}(\gamma)\geq 1\lor\gamma\text{ is
terminal}\\}$ to $0$ and, for other states $(l,\mathbf{x})\in\mathsf{Inv}$,
(a) if $(l,\mathbf{x})$ is an assignment, or nondeterministic state,
$U_{\sigma}(l^{\prime},\mathbf{x}^{\prime})<U_{\sigma}(l,\mathbf{x})$ for
every successor $(l^{\prime},\mathbf{x}^{\prime})$. (b) if $(l,\mathbf{x})$ is
a probabilistic state,
$\sum\mathsf{Pr}(l,l^{\prime})[\mathbf{x}]>\mathcal{E}(\sigma)$ over all
successor states $(l^{\prime},\mathbf{x}^{\prime})$ with
$U_{\sigma}(l^{\prime},\mathbf{x}^{\prime})<U_{\sigma}(l,\mathbf{x})$. Then,
$\mathcal{G}$ is $\mathsf{AST}$.

Intuitively, our rule requires SI-indicator functions $\mathsf{SI}_{\sigma}$
at each $\sigma\in\mathsf{Inv}$ that hold for executions beginning at $\sigma$
with probability $\geq 1-p$. Each of these imply stochastic invariants
$(\mathbf{\Psi}_{\sigma},p)$ centered around the state $\sigma$. The functions
$\mathcal{U}$, $\mathcal{H}$, and $\mathcal{E}$ combine together to form
variant functions $U_{\sigma}$ of the McIver-Morgan kind at each
$\sigma\in\mathsf{Inv}$. These $U_{\sigma}$ further imply that a terminal
state is contained within each $\mathbf{\Psi}_{\sigma}$, and induces paths
within each $\mathbf{\Psi}_{\sigma}$ to this terminal state. Feeding
$U_{\sigma}$, $\epsilon_{\sigma}$, and $H_{\sigma}$ into McIver and Morgan’s
variant Section 3.1 gives us a proof for the fact that, were the execution to
be restricted to $\mathbf{\Psi}_{\sigma}$, the probability of termination from
$\sigma$ is $1$. Therefore, the probability of termination from each $\sigma$
is $\geq 1-p$. Applying the zero-one law of probabilistic processes (McIver
and Morgan, 2005, Lemma 2.6.1) completes the proof of soundness of this rule.

Notice that we don’t mandate any locality conditions on the SI-indicators in
this rule. This is because they aren’t necessary to infer the soundness of the
rule. However, we show in our completeness proof that one can always find
“local” SI-indicators that only take on values $<1$ at finitely many states
for $\mathsf{AST}$ programs. This is because these SI-indicators are built
from appropriate finite stochastic invariants, the existence of which is a
consequence of the unrolling lemma.

###### Lemma 4.4 (Completeness).

Section 4 is relatively complete.

###### Proof (sketch).

Let $\mathcal{G}$ be an $\mathsf{AST}$ $\mathsf{CFG}$. Set
$\mathsf{Inv}=\mathsf{Reach}(\mathcal{G})$, the set of reachable states of
$\mathcal{G}$. Fix a $0<p<1$ and a $\sigma\in\mathsf{Reach}(\mathcal{G})$.
Since $\mathcal{G}$ is $\mathsf{AST}$,
$\Pr_{\mathrm{term}}(\mathcal{G}(\sigma))=1$. The unrolling lemma indicates a
$k\in\mathbb{N}$ such that the required simulation time to amass a termination
probability of $1-p$ in $\mathcal{G}(\sigma)$ is bounded above by $k$. Let
$\Sigma^{\sigma}_{k}$ be the collection of all states reachable from $\sigma$
by a finite path of length at most $k$. Observe that runs of
$\mathcal{G}(\sigma)$ 1 terminate inside $\Sigma^{\sigma}_{k}$ with a
probability of at least $1-p$, and  2 almost-surely terminate either inside
$\Sigma^{\sigma}_{k}$ or outside $\Sigma^{\sigma}_{k}$.
$(\Sigma^{\sigma}_{k},p)$ is thus the required stochastic invariant for
$\sigma$. Arguments by Chatterjee et al. (2022, Theorem 1) indicate the
existence of an SI-Indicator $(\mathsf{SI}_{\sigma},p)$ for the stochastic
invariant $(\Sigma^{\sigma}_{k},p)$. Furthermore, the finiteness of
$\Sigma^{\sigma}_{k}$ combined with the almost-sure property of either
termination inside or exit from $\Sigma^{\sigma}_{k}$ enables Corollary 2.7,
from which it is trivial to extract a suitable variant function $U_{\sigma}$
bounded above by some $H_{\sigma}$ exhibiting a minimum probability of
decrease of $\epsilon_{\sigma}>0$. This is can be done for all
$\sigma\in\mathsf{Inv}$.

Let us now show how we can represent these entities in our assertion language.
As in the proof of the completeness of the martingale Section 3.2, consider
the relation $I$ such that $(k,\sigma_{1},\sigma_{2})\in I$ _iff_ there is a
finite path of length $\leq k$ from $\sigma_{1}$ to $\sigma_{2}$ in
$\mathcal{G}$. Clearly, $I$ is a computable relation and is thus representable
in $\mathsf{Th}(\mathbb{Q})$. $\mathsf{Inv}$ and each $U_{\sigma}$ can easily
be represented in $\mathsf{Th}(\mathbb{Q})$ using this relation $I$ in exactly
the same way as with Section 3.2.

To represent each $\mathsf{SI}_{\sigma}$, we note that arguments from
Chatterjee et al. (2022) show that the output of $\mathsf{SI}_{\sigma}$ at a
state $\gamma$ is precisely the probability of leaving the stochastic
invariant $(\Sigma^{\sigma}_{k},p)$. Encoding lower bounds on this probability
in $\mathsf{Th}(\mathbb{Q})$ uses the unrolling lemma, and was essentially
shown by Majumdar and Sathiyanarayana (2023). The probability with which
executions escape $\Sigma^{\sigma}_{k}$ within $m$ steps lower bounds the
probability of leaving $\Sigma^{\sigma}_{k}$. The former probability is
computable, and the unrolling lemma ensures that in spite of non-determinism,
augmenting $m$ with a universal quantifier produces the precise lower bounds
over the latter. Hence, each $\mathsf{SI}_{\sigma}(\gamma)$ is representable
in $\mathsf{Th}(\mathbb{Q})$. This completes our proof of relative
completeness. ∎

##  5\. Quantitative Termination

We now extend our rules to reason about lower and upper bounds on the
probability of termination. This notion of termination is referred to in the
literature as _quantitative termination_. This is in contrast to _qualitative
termination_ , the nomenclature employed for $\mathsf{AST}$. As mentioned
earlier, the proof rules we specify in this section can be used to show
irrational bounds on the termination probability; this is a simple consequence
of the fact that all possible termination probabilities can be expressed in
our assertion language.

Our upper bound rule is immediate from an observation of the nature of
stochastic invariants.

If there exists (1) an inductive invariant $\mathsf{Inv}$ containing
$(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$, (2) a function
$\mathsf{SI}:\mathsf{Inv}\to\mathbb{R}$ such that
$\mathsf{SI}(l_{init},\mathbf{x}_{init})\leq p$ and for all
$(l,\mathbf{x})\in\mathsf{Inv}$, (a) $\mathsf{SI}(l,\mathbf{x})\geq 0$; (b) if
$(l,\mathbf{x})$ is an assignment, or nondeterministic state, then
$\mathsf{SI}(l,\mathbf{x})\geq\mathsf{SI}(l^{\prime},\mathbf{x}^{\prime})$ for
every successor $(l^{\prime},\mathbf{x}^{\prime})$; (c) if $(l,\mathbf{x})$ is
a probabilistic state, then
$\mathsf{SI}(l,\mathbf{x})\geq\allowbreak\sum\mathsf{Pr}((l,\allowbreak
l^{\prime}))[\mathbf{x}]\times\mathsf{SI}(l^{\prime},\mathbf{x}^{\prime})$
over all possible successor states $(l^{\prime},\mathbf{x}^{\prime})$. (d) if
$(l,\mathbf{x})$ is a terminal state, then $\mathsf{SI}(l,\mathbf{x})\geq 1$.
Then, $\Pr_{\mathrm{term}}(\mathcal{G})\leq p$.

This rule asks for an SI-indicator (and therefore a stochastic invariant) that
excludes the terminal state. Therefore, the probability of termination is the
probability of escaping the SI-indicator, which is included in the property of
the indicator. Notice that, because the SI-indicator is a supermartingale
function, the mere existence of a bounded supermartingale that assigns to the
terminal state a value $\geq 1$ is sufficient to extract an upper bound.

###### Lemma 5.1.

Section 5 is sound and relatively complete.

###### Proof.

Lemma 4.3 shows that the pair
$(\\{\gamma\in\mathsf{Inv}\mid\mathsf{SI}(\gamma)<1\\},p)$ is a stochastic
invariant of $\mathcal{G}$. Since $\mathsf{SI}(\gamma)\geq 1$ at the terminal
state, this stochastic invariant doesn’t contain the terminal state. Soundness
of the rule trivially follows from the fact that, in order to terminate, a run
must leave this invariant and this probability is bounded above by $p$.

For completeness, set $\mathsf{Inv}=\mathsf{Reach}(\mathcal{G})$ and let
$\sigma_{\bot}\in\mathsf{Inv}$ be the terminal state. Set
$\mathbf{\Psi}=\mathsf{Inv}\setminus\\{\sigma_{b}ot\\}$, and observe that the
collection of runs leaving $\mathbf{\Psi}$ is identical to the collection of
terminal runs. Therefore, $(\mathbf{\Psi},p)$ must be a stochastic invariant.
Lemma 4.3 indicates the existence of the SI-Invariant $\mathsf{SI}$ from
$\mathbf{\Psi}$. $\mathsf{SI}$ immediately satisfies the conditions of the
rule.

To represent $\mathsf{SI}$ in our assertion language, note again that
$\mathsf{SI}(\gamma)$ is precisely the probability of termination from
$\gamma$. The unrolling lemma indicates that this probability is lower bounded
by the probability of termination within $m$ steps from $\gamma$. The latter
probability is computable, and is hence representable in
$\mathsf{Th}(\mathbb{Q})$. Prepending an appropriate universal quantifier for
$m$ allows us to form lower bounds for $\mathsf{SI}$ in
$\mathsf{Th}(\mathbb{Q})$. Our upper bound rule is thus relatively complete. ∎

###  5.1. Towards a Lower Bound

For a lower bound on the probability of termination, we start with the
following rule from Chatterjee et al. (2022).

If there exists (1) an inductive invariant $\mathsf{Inv}$ containing
$(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})$, (2) a stochastic invariant
indicator $\mathsf{SI}:\mathsf{Inv}\to\mathbb{R}$ such that
$\mathsf{SI}(l_{\mathit{init}},\mathbf{x}_{\mathit{init}})\geq p$, and for all
$(l,\mathbf{x})\in\mathsf{Inv}$, (a) $\mathsf{SI}(l,\mathbf{x})\geq 0$. (b) if
$(l,\mathbf{x})$ is an assignment, or nondeterministic state, then
$\mathsf{SI}(l,\mathbf{x})\geq\mathsf{SI}(l^{\prime},\mathbf{x}^{\prime})$ for
every successor $(l^{\prime},\mathbf{x}^{\prime})$. (c) if $(l,\mathbf{x})$ is
a probabilistic state, then
$\mathsf{SI}(l,\mathbf{x})\geq\sum\mathsf{Pr}((l,\allowbreak
l^{\prime}))[\mathbf{x}]\allowbreak\times\mathsf{SI}(l^{\prime},\mathbf{x}^{\prime})$
over all possible successor states $(l^{\prime},\mathbf{x}^{\prime})$. (3) an
$\epsilon>0$, (4) a variant $U:\mathsf{Inv}\to\mathbb{N}$ that is bounded
above by some $H$, maps all states
$\\{\gamma\in\mathsf{Inv}\mid\mathsf{SI}(\gamma)\geq 1\lor\gamma\text{ is
terminal}\\}$ to $0$, and for other states $(l,\mathbf{x})\in\mathsf{Inv}$,
(a) if $(l,\mathbf{x})$ is an assignment, or nondeterministic state,
$U(l^{\prime},\mathbf{x}^{\prime})<U(l,\mathbf{x})$ for every successor
$(l^{\prime},\mathbf{x}^{\prime})$. (b) if $(l,\mathbf{x})$ is a probabilistic
state, $\sum\mathsf{Pr}(l,l^{\prime})[\mathbf{x}]>\epsilon$ over all successor
states $(l^{\prime},\mathbf{x}^{\prime})$ with
$U(l^{\prime},\mathbf{x}^{\prime})<U(l,\mathbf{x})$. Then,
$\Pr_{\mathrm{term}}(\mathcal{G})\geq 1-p$.

This rule demands a SI-indicator $(\mathsf{SI},p)$ and a bounded variant $U$
such that $\mathsf{SI}$ induces a stochastic invariant $(\mathbf{\Psi},p)$
that contains the terminal state. Intuitively, this rule works by splitting
the state space into terminating and possibly non-terminating segments. The
invariant $\mathbf{\Psi}$ represents the terminating section of the state
space. The application of McIver & Morgan’s Section 3.1 with the variant $U$
allows us to deduce that, were the execution be restricted to $\mathbf{\Psi}$,
the program almost-surely terminates. Observe that the variant $U$ effectively
considers all states outside $\mathbf{\Psi}$ to be terminal. Therefore,
$\mathcal{G}$ almost-surely either escapes $\mathbf{\Psi}$ or terminates
within $\mathbf{\Psi}$. Non-termination is thus subsumed by the event of
escaping the invariant, the probability of which is $p$. Hence, the
probability of termination is $\geq 1-p$.

Observe that, like our $\mathsf{AST}$ Section 3.2, this rule requires a
supermartingale and a variant function that work in tandem. However, unlike
Section 3.2, the supermartingale and the variant are entirely bounded.

This soundness argument was formally shown by Chatterjee et al. (2022). In
their original presentation, they do not specify an exact technique for
determining the almost-sure property of either termination within or escape
from the induced stochastic invariant $\mathbf{\Psi}$. We will explain our
choice of the bounded variant Section 3.1 of McIver and Morgan (2005) in a
moment. They additionally claimed the completeness of this rule, assuming the
usage of a complete rule for almost-sure termination. If their completeness
argument were true, it would indicate that all probabilistic programs induce
state spaces that can neatly be partitioned into terminating and non-
terminating sections. In Section 5.3, we show that this isn’t the case using a
counterexample where this split isn’t possible.

Nevertheless, this rule is complete for finite-state programs. This finite-
state completeness pairs well with the finite-state completeness of the
bounded variant Section 3.1 we use to certify the almost-sure property
contained in the rule.

$\sigma\in\Sigma_{good}$ Figure 1. If shortest runs of $\Sigma_{good}$ were
too long. This is a representation of the collection of executions beginning
at a good state $\sigma\in\Sigma_{good}$, according to the partitioning system
suggested in the proof of Lemma 5.2. The black nodes are the terminal states;
they all lead to the single terminal state. The blue states are identical to
each other; the same holds for the blue green states. The pathological
scheduler $\mathfrak{s}^{\prime}$ always takes the red back edges, rendering
no terminal runs from $\sigma$.

###### Lemma 5.2.

Section 5.1 is complete for finite state $\mathsf{CFG}$s.

###### Proof.

In this proof, we argue about the stochastic invariants directly. The SI-
indicator and variant functions can be derived from them using prior
techniques (Chatterjee et al., 2022; McIver and Morgan, 2005).

Let $\mathcal{G}$ be a finite state $\mathsf{CFG}$. Partition
$\mathsf{Reach}(\mathcal{G})$, the set of states reachable from the initial
state of $\mathcal{G}$, into  1 the singleton containing the terminal state
$\Sigma_{\bot}$,  2 the _bad_ states $\Sigma_{bad}$ with the property that no
finite paths ending on these states can be extended to a terminal run,  3 the
_good_ states $\Sigma_{good}$ such that if a scheduler $f$ induces a finite
path ending at a good state $\sigma$, $f$ induces at least one terminating run
passing through $\sigma$, and  4 the remaining _neutral_ states
$\Sigma_{neutral}$, with the property that each neutral state $\sigma$ is
associated with a pathological scheduler $\mathfrak{s}_{\sigma}$ that induces
runs that, if they pass through $\sigma$, do not terminate.  Notice that, as
long as $p<1$ (the case where $p=1$ is trivial, so we skip it), the initial
state of $\mathcal{G}$ is in $\Sigma_{good}$. We show that
$(\Sigma_{good}\cup\Sigma_{\bot},p)$ is the required stochastic invariant.

We begin by showing that runs that remain inside
$\Sigma_{good}\cup\Sigma_{\bot}$ almost-surely terminate. Fix a state
$\sigma\in\Sigma_{good}$. Map to every scheduler $\mathfrak{s}$ that induces
runs passing through $\sigma$ the shortest terminating consistent finite path
$\pi_{\mathfrak{s}}$ beginning from $\sigma$. Suppose, for some scheduler
$\mathfrak{s}$, $|\pi_{\mathfrak{s}}|>|\mathsf{Reach}(\mathcal{G})|$. Then,
$\pi_{\mathfrak{s}}$ must visit some
$\sigma^{\prime}\in\mathsf{Reach}(\mathcal{G})$ twice. This indicates a loop
from $\sigma^{\prime}\to\sigma^{\prime}$ in $\mathcal{G}$, and there must thus
exist a scheduler $\mathfrak{s}^{\prime}$ that extends $\pi_{\mathfrak{s}}$ by
repeating this loop infinitely often. Since $\pi_{\mathfrak{s}}$ is the
smallest terminating finite path beginning from $\sigma$, the same holds for
all terminating finite paths consistent with $\mathfrak{s}$ beginning from
$\sigma$. Thus, all terminating runs consistent with $\mathfrak{s}$ that pass
through $\sigma$ must contain a loop. There must exist a scheduler
$\mathfrak{s}^{\prime}$ which exploits these loops and yields no terminating
runs passing through $\sigma$. Fig. 1 depicts the operation of
$\mathfrak{s}^{\prime}$. Observe that the existence of $\mathfrak{s}^{\prime}$
contradicts $\sigma\in\Sigma_{good}$.

Therefore, from every state $\sigma\in\Sigma_{good}$, there is a terminating
run of length $\leq|\mathsf{Reach}(\mathcal{G})|$ no matter which scheduler is
used. Thus, the probability of leaving $\Sigma_{good}$ from $\sigma$ is
bounded below by $q^{|\mathsf{Reach}(\mathcal{G})|}$, where $q$ is the
smallest transition probability of $\mathcal{G}$ (note that $q$ only exists
because $\mathcal{G}$ is finite state). Further, $\Sigma_{good}$ only contains
non-terminal states. This enables the zero-one law of probabilistic processes
(McIver and Morgan, 2005, Lemma 2.6.1), allowing us to deduce the almost-
certain escape from $\Sigma_{good}$ to
$\Sigma_{\bot}\cup\Sigma_{bad}\cup\Sigma_{neutral}$. Hence, under all
schedulers, the probability of either terminating inside
$\Sigma_{good}\cup\Sigma_{\bot}$ or entering
$\Sigma_{bad}\cup\Sigma_{neutral}$ is $1$.

We now show that $(\Sigma_{good}\cup\Sigma_{bot},p)$ is a stochastic
invariant. It’s easy to see that if a run ever enters $\Sigma_{bad}$, it never
terminates. We know that if an execution enters some
$\sigma\in\Sigma_{neutral}$ under a pathological scheduler
$\mathfrak{s}_{\sigma}$, it never terminates. Let $\sigma_{1}$ and
$\sigma_{2}$ be neutral states and $\mathfrak{s}_{1}$ and $\mathfrak{s}_{2}$
be their corresponding pathological schedulers. Notice that $\mathfrak{s}_{1}$
may induce terminating executions that pass through $\sigma_{2}$. One can
build a scheduler $\mathfrak{s}_{3}$ that mimics $\mathfrak{s}_{1}$ until the
execution reaches $\sigma_{2}$, and once it does, mimics $\mathfrak{s}_{2}$.
Thus, $\mathfrak{s}_{3}$ would produce the pathological behaviour of both
$\mathfrak{s}_{1}$ and $\mathfrak{s}_{2}$. In this way, we compose the
pathological behavior of all neutral states to produce a scheduler
$\mathfrak{f}$ that induces runs that, if they enter a neutral state, never
terminate. Under $\mathfrak{f}$, leaving $\Sigma_{good}\cup\Sigma_{\bot}$ is
equivalent to non-termination, and all terminating runs are made up of good
states until their final states.

Take a scheduler $\mathfrak{s}$ that induces terminating runs that pass
through neutral states. Compose the scheduler $\mathfrak{s}^{\prime}$ that
mimics $\mathfrak{s}$ until the execution enters a neutral state and mimics
$\mathfrak{f}$ from then on. Let $T_{\mathfrak{s}}$ and
$T_{\mathfrak{s}^{\prime}}$ be the collection of terminating runs consistent
with $\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ respectively. Each run in
$T_{\mathfrak{s}^{\prime}}$ is made up of good and/or terminal states, and is
therefore consistent with $\mathfrak{s}$. Hence, $T_{\mathfrak{s}}\supset
T_{\mathfrak{s}^{\prime}}$ and, because $\mathfrak{s}$ and
$\mathfrak{s}^{\prime}$ agree on $T_{\mathfrak{s}^{\prime}}$, we have
$\mathbb{P}_{\mathfrak{s}}(T_{\mathfrak{s}})>\mathbb{P}_{\mathfrak{s}}(T_{\mathfrak{s}^{\prime}})$,
where $\mathbb{P}_{\mathfrak{s}}$ is the probability measures in the semantics
of $\mathcal{G}$ induced by $\mathfrak{s}$.

Leaving $\Sigma_{good}\cup\Sigma_{\bot}$ is equivalent to entering
$\Sigma_{neutral}\cup\Sigma_{\bot}$. Observe that the probability of never
leaving $\Sigma_{good}\cup\Sigma_{\bot}$ under $\mathfrak{s}$ is the same as
the probability of never leaving $\Sigma_{good}\cup\Sigma_{\bot}$ under
$\mathfrak{s}^{\prime}$, as $\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ agree
until then. Furthermore, the probability measure of never leaving
$\Sigma_{good}\cup\Sigma_{\bot}$ is just
$\Pr_{\mathfrak{s}}(T_{\mathfrak{s}^{\prime}})=\Pr_{\mathfrak{s}^{\prime}}(T_{\mathfrak{s}^{\prime}})$.
Add $\Pr_{\mathrm{term}}(\mathcal{G})\geq 1-p\implies
p_{\mathfrak{s}^{\prime}}(T_{\mathfrak{s}^{\prime}})\geq 1-p$, and we get
that, under $\mathfrak{s}$, the probability of leaving
$\Sigma_{good}\cup\Sigma_{\bot}$ is upper bounded by $p$. Since this is true
for any $\mathfrak{s}$, the lemma is proved. ∎

We do not show the relative completeness of this rule; nevertheless, this is
easy to show using techniques discussed in prior rules.

###  5.2. Our Rule

We now show a sound and complete rule for lower bounds that fixes the prior
Section 5.1. This rule is implicitly contained in the details of the erroneous
proof of (Chatterjee et al., 2022). It is principally similar to Section 4, in
that it identifies finite sub-instances where prior rules can apply. It then
combines the proofs of these sub-instances to deduce the desired lower bound.

If for all $n\in\mathbb{N}$, there are functions $SI_{n}$ and $U_{n}$ that
enable the application of Section 5.1 to deduce
$\Pr_{\mathrm{term}}(\mathcal{G})\geq 1-(p+\frac{1}{n})$, then
$\Pr_{\mathrm{term}}(\mathcal{G})\geq 1-p$.

Soundness of this rule follows trivially from the soundness of the prior
Section 5.1. The completeness of this rule is derived from the unrolling
lemma; to reach a termination probability of $p$, the program must be able to
amass a termination probability of $p-\frac{1}{n}$ within a finite subspace.
Lemma 5.2 shows that finiteness can always be captured by the prior Section
5.1.

###### Lemma 5.3.

Section 5.2 is relatively complete.

###### Proof.

Let $\mathcal{G}$ be $\mathsf{CFG}$ such that
$\Pr_{\mathrm{term}}(\mathcal{G})\geq 1-p$ for some $p>0$. Fix some
$n\in\mathbb{N}$. Let $k_{n}$ be the upper bound over the required simulation
times across all schedulers to amass a termination probability of $p-1/n$.
Denote by $\Sigma_{n}$ the set of states $\sigma$ such that there is a finite
path of length at most $k_{n}$ beginning at $(l_{init},\mathbf{x}_{init})$ and
ending at $\sigma$. Clearly, $\Sigma_{n}$ must be finite and, for a fixed
scheduler $\mathfrak{s}$, the probability measure of the collection of
terminating runs made up of states in $\Sigma_{n}$ consistent with
$\mathfrak{s}$ must be $\geq p-1/n$. Additionally, observe that runs of
$\mathcal{G}$ either terminate inside $\Sigma_{n}$ or leave $\Sigma_{n}$. By
the soundness of Section 5.1, the termination probability of
$\mathcal{G}_{\varphi_{n}}$ must be $\geq p-1/n$.

Each stochastic invariant $(\Sigma_{n},p+1/n)$ can be transformed into SI-
Indicators $(\mathsf{SI}_{n},p+1/n)$ using prior techniques (Chatterjee et
al., 2022). Representing each $SI_{n}$ and $U_{n}$ in
$\mathsf{Th}(\mathbb{Q})$ can be done using techniques described in the proof
of Lemma 4.4. Hence, this rule is relatively complete. ∎

###  5.3. Counterexample to Completeness for Section 5.1

(Chatterjee et al., 2022) claimed that their Section 5.1 is complete for all
programs. As promised, we now demonstrate a counterexample to their claim of
completeness.

$\sigma\in\Sigma_{good}$
$l_{1}$$l_{2}$$l_{3}$$x_{1}/x_{2}$$\begin{matrix}x_{1}\coloneqq x_{2}\\\
x_{2}\coloneqq x_{2}+x_{3}\\\ x_{3}\coloneqq
x_{3}/2\end{matrix}$$1-(x_{1}/x_{2})$ Figure 2. Counterexample to the SI-rule
for lower bounds. With an initial state of $(l_{1},(1,2,1/4))$, the
termination probability of this program is $1/2$. However, there is no SI that
shows this.

Section 5.1 for lower bounds can be applied onto any $\mathsf{CFG}$ that
induces a set of states $\mathbf{\Psi}$ with the property that executions
remain within $\mathbf{\Psi}$ with exactly the probability of termination. As
mentioned previously, not all programs are so well behaved. Consider the
program $\mathcal{K}$ defined in Fig. 2.

The initial location of $\mathcal{K}$ is $l_{1}$, and the values of the
variables $(x_{1},x_{2},x_{3})$ are $(1,2,1/4)$. $l_{1}$ is a probabilistic
location, $l_{3}$ is an assignment location, and $l_{2}$ is a terminal
location. It isn’t difficult to prove that the probability of termination of
$\mathcal{K}$ is $1/2$; we leave the details to the diligent reader. The SI-
rule for lower bounds requires a stochastic invariant
$(\mathbf{\Psi}_{\mathcal{K}},1/2)$ such that executions almost-surely either
terminate or exit $\mathbf{\Psi}_{\mathcal{K}}$.

###### Lemma 5.4.

There is no stochastic invariant $(\mathbf{\Psi}_{\mathcal{K}},1/2)$ of
$\mathcal{K}$ such that runs almost-surely either terminate or leave
$\mathbf{\Psi}_{\mathcal{K}}$.

###### Proof.

Suppose there does exist a stochastic invariant
$(\mathbf{\Psi}_{\mathcal{K}},1/2)$ that satisfies these properties.
Therefore, the probability measure of the union of the collection of runs
$\mathsf{Leave}_{\mathbf{\Psi}}$ that leave $\mathbf{\Psi}_{\mathcal{K}}$ and
the runs $\mathsf{Term}_{\mathbf{\Psi}}$ that terminate inside
$\mathbf{\Psi}_{\mathcal{K}}$ is $1$. However, because
$\mathbf{\Psi}_{\mathcal{K}}$ is a stochastic invariant, the probability
measure of $\mathsf{Leave}_{\mathbf{\Psi}}$ is bounded above by $1/2$. This
means that the measure of $\mathsf{Term}_{\mathbf{\Psi}}$ is bounded below by
$1/2$. But, the termination probability of $\mathcal{K}$ is $1/2$.
Consequently, the measure of $\mathsf{Term}_{\mathbf{\Psi}}$ must be exactly
$1/2$. This means $\mathsf{Term}_{\mathbf{\Psi}}$ contains all terminating
runs of $\mathcal{K}$.

It is easy to see that from any state $(l,\mathbf{x})$ reachable from the
initial state, there is a finite path of length at most $2$ that leads it to a
terminal state. Therefore, all reachable states $(l,\mathbf{x})$ are a part of
some terminating run; meaning that the set of states that make up the runs in
$\mathsf{Term}_{\mathbf{\Psi}}$ must be the set of reachable states. This is
only possible when $\mathbf{\Psi}_{\mathcal{K}}$ is the set of reachable
states. This means no runs leave $\mathbf{\Psi}_{\mathcal{K}}$, and therefore,
the measure of $\mathsf{Term}_{\mathbf{\Psi}}$ is $1$. This contradicts the
fact that the termination probability of $\mathcal{K}$ is $1/2$. ∎

_A note on syntax._ The $\mathsf{CFG}$ of Chatterjee et al. (2022) over which
the claim of completeness of Section 5.1 was made do not feature fractional
expressions guiding probabilistic branching. Nevertheless, they can be
simulated with small programs that only use the basic coin flip (Flajolet et
al., 2011). Therefore, Fig. 2 is a valid counterexample to their claim.

##  6\. Traveling Between Proof Systems

A new proof rule, ultimately, is interesting only if one can actually prove
the termination of many programs. In order to show that our proof rules, in
addition to their theoretical properties, are also applicable in a variety of
situations, we demonstrate that proofs in many existing proof systems can be
compiled into our proof rules.

#### From McIver and Morgan (2005)

The variant functions from Section 3.1 immediately form the variant functions
required in Section 3.2. Take $A$ to simply be the singleton containing the
terminal state, and set $V$ to $0$ at the terminal state and $1$ everywhere
else. This gives all we need to apply Section 3.2.

#### From McIver et al. (2018)

The $\mathsf{AST}$ proof rule proposed by McIver et al. (2018) has been
applied onto a variety of programs, and has been shown to be theoretically
applicable over the 2D random walker. Applications of their rule effectively
requires the construction of a distance variant that is also a
supermartingale. We note that their variants can be reused in Section 3.2 with
little alterations as both the supermartingale and variant functions. This
means proofs in their rule can be easily translated to proofs that use Section
3.2.

#### From Section 3.2 to Section 4

Hidden in the proof of the soundness of Section 3.2 are the stochastic
invariants that form the basis of Section 4. Fix a $p$, and take the set
$\mathbf{\Psi}_{\sigma}=\\{\gamma\in\mathsf{Inv}\mid V(\gamma)\leq
v_{\mathrel{\shortuparrow}}\\}$ for a sufficiently high value of
$v_{\mathrel{\shortuparrow}}$ to yield an upper bound of $p$ on the
probability of exiting $\mathbf{\Psi}_{\sigma}$. Then, expand
$\mathbf{\Psi}_{\sigma}$ with the states necessary to keep all shortest
consistent terminal runs across schedulers from states in
$\mathbf{\Psi}_{\sigma}$ entirely within $\mathbf{\Psi}_{\sigma}$. In spite of
these extensions, the value of $V$ will be entirely bounded when restricted to
states in $\mathbf{\Psi}_{\sigma}$. It is then trivial to build the indicator
functions from each stochastic invariant $(\mathbf{\Psi}_{\sigma},p)$ and the
variant functions from $U$, completing a translation from Section 3.2 to
Section 4. Note that using this technique, one can translate proofs from
McIver et al. (2018) and McIver and Morgan (2005) to Section 4 as well.

#### Using Guard Strengthening (Feng et al., 2023)

Feng et al. (2023) have demonstrated Guard Strengthening as a technique for
proving lower bounds on, amongst others, the termination of deterministic
probabilistic programs. In principle, their technique can be translated to
apply over $\mathsf{CFG}$s as follows: strengthen each transition guard by a
suitable predicate $\varphi$ and add self loops at all locations guarded by
$\lnot\varphi$. We observe that guards can succinctly overapproximate the set
of states forming finite-state stochastic invariants: simply take the highest
and lowest values each variable can take while remaining in the invariant, and
form a predicate that limits each variable within these bounds. Thus, guards
serve as convenience mechanisms for the application of Section 5.2.
Additionally, observe that when proving lower bounds on termination
probabilities, relevant finite state stochastic invariants
$\mathbf{\Psi}_{\sigma}$ for each reachable state $\sigma$ are guaranteed to
exist. Therefore, each stochastic invariant in Section 5.2 can be more
succinctly represented using guards.

#### Using Stochastic Invariants (Chatterjee et al., 2022)

Separately, Chatterjee et al. (2022) have shown the applicability of Section
5.1 to demonstrate lower bounds on the termination probabilities for a variety
of programs, and have also presented template-based synthesis techniques for
achieving limited completeness. These proofs are also valid for Section 5.2,
by setting the same stochastic invariant for each $n$.

##  7\. Conclusion

We have presented the first sound and relatively complete proof rules for
qualitative and quantitative termination of probabilistic programs with
bounded probabilistic and nondeterministic choice. Our proof rules combine the
familiar ingredients of supermartingales and variant functions in novel ways
to reach completeness. We have demonstrated relative completeness of our rules
in the assertion language of arithmetic. Our rules are able to accommodate
existing proof techniques in the literature with minimal effort, thus
demonstrating their applicability.

pages main.pages.ctrpages pages0 pages

## References

  * (1)
  * Apt (1981) Krzysztof R. Apt. 1981\.  Ten Years of Hoare’s Logic: A Survey - Part 1.  _ACM Trans. Program. Lang. Syst._ 3, 4 (1981), 431–483.  https://doi.org/10.1145/357146.357150
  * Apt and Kozen (1986) Krzysztof R. Apt and Dexter Kozen. 1986.  Limits for Automatic Verification of Finite-State Concurrent Systems.  _Inf. Process. Lett._ 22, 6 (1986), 307–309.  https://doi.org/10.1016/0020-0190(86)90071-2
  * Apt and Plotkin (1986) Krzysztof R. Apt and Gordon D. Plotkin. 1986.  Countable nondeterminism and random assignment.  _J. ACM_ 33, 4 (1986), 724–767.  https://doi.org/10.1145/6490.6494
  * Avanzini et al. (2020) Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. 2020\.  On probabilistic term rewriting.  _Sci. Comput. Program._ 185 (2020).  https://doi.org/10.1016/j.scico.2019.102338
  * Baier and Katoen (2008) Christel Baier and Joost-Pieter Katoen. 2008.  _Principles of model checking_.  MIT Press.
  * Batz et al. (2021) Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021\.  Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.  _Proc. ACM Program. Lang._ 5, POPL (2021), 1–30.  https://doi.org/10.1145/3434320
  * Bianco and de Alfaro (1995) Andrea Bianco and Luca de Alfaro. 1995.  Model Checking of Probabalistic and Nondeterministic Systems. In _Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Bangalore, India, December 18-20, 1995, Proceedings_ _(Lecture Notes in Computer Science, Vol. 1026)_ , P. S. Thiagarajan (Ed.). Springer, 499–513.  https://doi.org/10.1007/3-540-60692-0_70
  * Bournez and Garnier (2005) Olivier Bournez and Florent Garnier. 2005.  Proving Positive Almost-Sure Termination. In _Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings_ _(Lecture Notes in Computer Science, Vol. 3467)_ , Jürgen Giesl (Ed.). Springer, 323–337.  https://doi.org/10.1007/978-3-540-32033-3_24
  * Chakarov and Sankaranarayanan (2013) Aleksandar Chakarov and Sriram Sankaranarayanan. 2013.  Probabilistic Program Analysis with Martingales. In _Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings_ _(Lecture Notes in Computer Science, Vol. 8044)_ , Natasha Sharygina and Helmut Veith (Eds.). Springer, 511–526.  https://doi.org/10.1007/978-3-642-39799-8_34
  * Chatterjee et al. (2022) Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. 2022\.  Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. In _Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I_ _(Lecture Notes in Computer Science, Vol. 13371)_ , Sharon Shoham and Yakir Vizel (Eds.). Springer, 55–78.  https://doi.org/10.1007/978-3-031-13185-1_4
  * Chatterjee et al. (2017) Krishnendu Chatterjee, Petr Novotný, and Dorde Zikelic. 2017\.  Stochastic invariants for probabilistic termination. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017_ , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 145–160.  https://doi.org/10.1145/3009837.3009873
  * Cook (1978) Stephen A. Cook. 1978\.  Soundness and Completeness of an Axiom System for Program Verification.  _SIAM J. Comput._ 7, 1 (1978), 70–90.  https://doi.org/10.1137/0207005
  * Courcoubetis and Yannakakis (1995) Costas Courcoubetis and Mihalis Yannakakis. 1995.  The Complexity of Probabilistic Verification.  _J. ACM_ 42, 4 (1995), 857–907.  https://doi.org/10.1145/210332.210339
  * de Alfaro and Henzinger (2000) Luca de Alfaro and Thomas A. Henzinger. 2000.  Concurrent Omega-Regular Games. In _15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000_. IEEE Computer Society, 141–154.  https://doi.org/10.1109/LICS.2000.855763
  * de Alfaro et al. (2007) Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. 2007\.  Concurrent reachability games.  _Theor. Comput. Sci._ 386, 3 (2007), 188–217.  https://doi.org/10.1016/J.TCS.2007.07.008
  * den Hartog and de Vink (2002) Jerry den Hartog and Erik P. de Vink. 2002.  Verifying Probabilistic Programs Using a Hoare Like Logic.  _Int. J. Found. Comput. Sci._ 13, 3 (2002), 315–340.  https://doi.org/10.1142/S012905410200114X
  * Dijkstra (1976) Edsger W. Dijkstra. 1976\.  _A Discipline of Programming_.  Prentice-Hall.  https://www.worldcat.org/oclc/01958445
  * Doob (1953) J. L. Doob. 1953\.  _Stochastic processes_.  John Wiley & Sons, New York. viii+654 pages.  MR 15,445b. Zbl 0053.26802..
  * Feng et al. (2023) Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Naijun Zhan. 2023.  Lower Bounds for Possibly Divergent Probabilistic Programs.  _Proc. ACM Program. Lang._ 7, OOPSLA1 (2023), 696–726.  https://doi.org/10.1145/3586051
  * Fioriti and Hermanns (2015) Luis María Ferrer Fioriti and Holger Hermanns. 2015.  Probabilistic Termination: Soundness, Completeness, and Compositionality. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015_ , Sriram K. Rajamani and David Walker (Eds.). ACM, 489–501.  https://doi.org/10.1145/2676726.2677001
  * Flajolet et al. (2011) Philippe Flajolet, Maryse Pelletier, and Michèle Soria. 2011\.  On Buffon Machines and Numbers. In _Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2011, San Francisco, California, USA, January 23-25, 2011_ , Dana Randall (Ed.). SIAM, 172–183.  https://doi.org/10.1137/1.9781611973082.15
  * Floyd (1993) Robert W. Floyd. 1993\.  _Assigning Meanings to Programs_.  Springer Netherlands, Dordrecht, 65–81.  https://doi.org/10.1007/978-94-011-1793-7_4
  * Foster (1951) F.G. Foster. 1951\.  Markov chains with an enumerable number of states and a class of cascade processes.  _Math. Proc. Cambridge Philos. Soc._ 47 (1951), 77–85.
  * Foster (1953) F.G. Foster. 1953\.  On the stochastic matrices associated with certain queuing processes.  _Ann. Math. Statistics_ 24 (1953), 355–360.
  * Fu and Chatterjee (2019) Hongfei Fu and Krishnendu Chatterjee. 2019.  Termination of Nondeterministic Probabilistic Programs. In _Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings_ _(Lecture Notes in Computer Science, Vol. 11388)_ , Constantin Enea and Ruzica Piskac (Eds.). Springer, 468–490.  https://doi.org/10.1007/978-3-030-11245-5_22
  * Harel (1980) David Harel. 1980\.  Proving the Correctness of Regular Deterministic Programs: A Unifying Survey Using Dynamic Logic.  _Theor. Comput. Sci._ 12 (1980), 61–81.  https://doi.org/10.1016/0304-3975(80)90005-5
  * Harel et al. (2000) David Harel, Dexter Kozen, and Jerzy Tiuryn. 2000\.  _Dynamic Logic_.  MIT Press.
  * Hart et al. (1983) Sergiu Hart, Micha Sharir, and Amir Pnueli. 1983\.  Termination of Probabilistic Concurrent Program.  _ACM Trans. Program. Lang. Syst._ 5, 3 (1983), 356–380.  https://doi.org/10.1145/2166.357214
  * Hitchcock and Park (1972) Peter Hitchcock and David Michael Ritchie Park. 1972\.  Induction Rules and Termination Proofs. In _Automata, Languages and Programming, Colloquium, Paris, France, July 3-7, 1972_ , Maurice Nivat (Ed.). North-Holland, Amsterdam, 225–251.
  * Huang et al. (2018) Mingzhang Huang, Hongfei Fu, and Krishnendu Chatterjee. 2018\.  New Approaches for Almost-Sure Termination of Probabilistic Programs. In _Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings_ _(Lecture Notes in Computer Science, Vol. 11275)_ , Sukyoung Ryu (Ed.). Springer, 181–201.  https://doi.org/10.1007/978-3-030-02768-1_11
  * Kaminski et al. (2019) Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2019.  On the hardness of analyzing probabilistic programs.  _Acta Informatica_ 56, 3 (2019), 255–285.  https://doi.org/10.1007/s00236-018-0321-1
  * Kozen (2006) Dexter Kozen. 2006\.  _Theory of Computation_.  Springer.  https://doi.org/10.1007/1-84628-477-5
  * Majumdar and Sathiyanarayana (2023) Rupak Majumdar and V. R. Sathiyanarayana. 2023.  Positive Almost-Sure Termination - Complexity and Proof Rules.  _CoRR_ abs/2310.16145 (2023).  https://doi.org/10.48550/ARXIV.2310.16145 arXiv:2310.16145
  * Majumdar and Sathiyanarayana (2024) Rupak Majumdar and V. R. Sathiyanarayana. 2024.  Positive Almost-Sure Termination: Complexity and Proof Rules.  _Proc. ACM Program. Lang._ 8, POPL (2024), 1089–1117.  https://doi.org/10.1145/3632879
  * Manna and Pnueli (1974) Zohar Manna and Amir Pnueli. 1974.  Axiomatic Approach to Total Correctness of Programs.  _Acta Informatica_ 3 (1974), 243–263.  https://doi.org/10.1007/BF00288637
  * McIver and Morgan (2005) Annabelle McIver and Carroll Morgan. 2005.  _Abstraction, Refinement and Proof for Probabilistic Systems_.  Springer.  https://doi.org/10.1007/B138392
  * McIver et al. (2018) Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018.  A new proof rule for almost-sure termination.  _Proc. ACM Program. Lang._ 2, POPL (2018), 33:1–33:28.  https://doi.org/10.1145/3158121
  * Menshikov et al. (2017) Mikhail Menshikov, Serguei Popov, and Andrew Wade. 2017\.  _Non-homogeneous random walks: Lyapunov function methods for near critical stochastic systems_.  Cambridge University Press.
  * Mertens et al. (1978) Jean-François Mertens, Ester Samuel-Cahn, and Shmuel Zamir. 1978\.  Necessary and Sufficient Conditions for Recurrence and Transience of Markov Chains, in Terms of Inequalities.  _Journal of Applied Probability_ 15, 4 (1978), 848–851.  http://www.jstor.org/stable/3213440
  * Pólya (1921) George Pólya. 1921\.  Über eine aufgabe betreffend die irrfahrt im strassennetz.  _Math. Ann._ 84 (1921), 149–160.
  * Popov (2021) Serguei Popov. 2021\.  _Two-Dimensional Random Walk: From Path Counting to Random Interlacements_.  Cambridge University Press.  https://doi.org/10.1017/9781108680134
  * Robinson (1949) Julia Robinson. 1949\.  Definability and Decision Problems in Arithmetic.  _J. Symb. Log._ 14, 2 (1949), 98–114.  https://doi.org/10.2307/2266510
  * Rogers Jr. (1987) Hartley Rogers Jr. 1987\.  _Theory of recursive functions and effective computability (Reprint from 1967)_.  MIT Press.  https://mitpress.mit.edu/9780262680523/theory-of-recursive-functions-and-effective-computability/
  * Takisaka et al. (2021) Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. 2021.  Ranking and Repulsing Supermartingales for Reachability in Randomized Programs.  _ACM Trans. Program. Lang. Syst._ 43, 2 (2021), 5:1–5:46.  https://doi.org/10.1145/3450967
  * Turing (1937) Alan M. Turing. 1937\.  On computable numbers, with an application to the Entscheidungsproblem.  _Proc. London Math. Soc._ s2-42, 1 (1937), 230–265.  https://doi.org/10.1112/PLMS/S2-42.1.230
  * Vardi (1985) Moshe Y. Vardi. 1985\.  Automatic Verification of Probabilistic Concurrent Finite-State Programs. In _26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21-23 October 1985_. IEEE Computer Society, 327–338.  https://doi.org/10.1109/SFCS.1985.12

pagesbib main.pagesbib.ctrpagesbib pagesbib0 pagesbib

todos main.todos.ctrtodos todos0 todos

pagestotal main.pagestotal.ctrpagestotal pagestotal0 pagestotal