Supermartingale Certificates

Greg Neustroev

Dynamical systems are a useful language for many problems in AI: robots interacting with the world, learning-enabled controllers, optimization dynamics, epidemiological and economic simulators, and (more broadly) any process that evolves over time according to a known set of rules.

At the same time, even simple-looking dynamical systems can exhibit rich and unintuitive behavior—strong nonlinearities, high-dimensional coupling, sensitivity to initial conditions, and, in stochastic settings, irreducible randomness. This complexity makes direct reasoning about trajectories difficult. In many cases we cannot write the state \(x(t)\) in closed form, and even when we can simulate it numerically, simulation alone does not provide proofs.

A standard approach in dynamics and verification is therefore to distill the system into something more tractable: a certificate, that is, a scalar function of the state whose evolution can be bounded or controlled. Rather than predicting the full trajectory, a certificate supports global conclusions—such as stability, safety, or reachability—because it compresses the dynamics into a one-dimensional inequality.

This blog post begins a series about certificates for stochastic systems known as supermartingale certificates. These certificates yield quantitative probability bounds for events such as failure or reaching a goal. In this first post, you will learn:

• what Lyapunov functions and barrier functions are, and how to interpret them as deterministic certificates;
• how the same intuition extends to stochastic dynamics via supermartingales;
• how a running example (a double pendulum with friction) illustrates the certificate viewpoint: the angles are not available in closed form in general, but energy provides a certificate with a simple dissipation law.

The Running Example: A Pendulum#

To make the certificate viewpoint easier to follow, we will use a pendulum with viscous friction as a running example. The pendulum is nonlinear, but it is still simple enough that we can write down the dynamics in a few lines. This will let us focus on the main idea of the post: how a carefully chosen scalar function can support global conclusions without requiring a closed-form solution for the full trajectory.

Let \(\theta(t)\) denote the pendulum angle and \(\omega(t) = \dot{\theta}(t)\) its angular velocity. The state is

A standard viscous-friction damped pendulum model is

Even for this simple nonlinear system, obtaining an explicit closed-form expression for \(\theta(t)\) for arbitrary initial conditions is not generally the most useful way to reason about behavior. In verification, we typically want global statements—e.g., that the pendulum eventually comes to rest, or that it never exceeds a speed threshold—rather than an explicit formula for \(\theta(t)\).

The certificate viewpoint is that such global statements can often be obtained from inequalities satisfied by a scalar function of the state. For the damped pendulum, the relevant scalar will be the mechanical energy, which we introduce next.

Energy as a Certificate#

The central certificate for the damped pendulum is its mechanical energy,

This definition is standard: \(K\) is kinetic energy and \(U\) is gravitational potential energy (shifted so that \(U=0\) at the bottom equilibrium \(\theta=0\)). The key point is not the formula itself, but what it implies along trajectories.

Let’s differentiate \(E(\theta(t),\omega(t))\) along solutions of (1):

Integrating (3) gives an explicit balance law:

Equation (3) is the first example of what we mean by a certificate: even if we do not attempt to solve for \(\theta(t)\) explicitly, we can still prove a monotone property (\(E(t)\) is non-increasing) and extract global consequences.

Lyapunov Functions: Deterministic Stability Certificates#

A Lyapunov function is a scalar \(V(x)\) that is bounded below and decreases (or does not increase) along trajectories. It proves that the system’s dynamics approach an equilibrium point \(x = 0\). In continuous time, typical conditions are

Similarly, in discrete time

For the damped pendulum, \(V(\theta,\omega)=E(\theta,\omega)\) is a natural Lyapunov function.

These properties imply stability of the equilibrium \(x=0\) in the following sense: because \(V\) is positive definite and non-increasing along trajectories, initial conditions with small \(V(x(0))\) can never evolve into states with larger \(V(x(t))\). Concretely, for any threshold \(c>0\), the sublevel set

is what we call forward invariant; trajectories that start inside it remain inside it. Since \(V(x)\) is continuous and \(V(0)=0\), for every neighborhood of the equilibrium there exists a sufficiently small sublevel set contained in that neighborhood. Therefore, getting sufficiently close to the equilibrium \(x=0\) implies staying close to \(0\) for all future time.

Barrier Functions: Deterministic Safety Certificates#

Lyapunov functions are often introduced for stability, but certificates are equally useful for safety. A typical safety property is:

Starting from a safe set \(S\), the system remains in \(S\) for all future time.

Barrier methods formalize this through invariance. One common template is:

• Choose a scalar barrier \(B(x)\) and define \(S= L^-_\beta B\).
• Prove that solutions starting in \(S\) cannot cross the boundary \(B=\beta\).

For dissipative systems, a particularly simple family of invariant sets comes from energy. For any \(c\ge 0\), define the energy sublevel set

Because \(E(t)\) is non-increasing, we have:

This is an invariance statement—hence a safety guarantee—obtained without solving for \(\theta(t)\). In practice, \(c\) is chosen so that \(S_c\) excludes an unsafe set of interest (e.g., velocities above a hardware limit).

A Safety Example: Speed Limit#

Suppose we wish to ensure \(|\omega(t)|\le \omega_{\max}\) for all \(t\). Since

the condition \(E(\theta,\omega)\le c\) implies

Thus, if we choose \(c=\tfrac12 I\omega_{\max}^2\), then invariance of \(S_c\) implies \(|\omega(t)|\le \omega_{\max}\) for all \(t\), regardless of how \(\theta(t)\) evolves.

This illustrates a general pattern: barrier-style guarantees often come from a certificate that bounds the system’s ability to enter dangerous regions.

From Deterministic to Stochastic Certificates#

In many AI settings, dynamics are stochastic:

• randomized policies and exploration,
• process noise,
• uncertain environments and disturbances,
• stochastic simulators.

Let \((X_t)_{t\ge 0}\) be a stochastic process representing the state over time, and let \(\mathcal{F}_t\) be the information about the process available up to time \(t\).

In stochastic settings, the Lyapunov condition \(\nabla_t V \le 0\) (or, in discrete time, \(V(X_{t+1}) \le V(X_t)\)) is typically too strong: random disturbances can increase \(V\) on a particular realization, even when the system exhibits an overall dissipative trend. The most direct relaxation is therefore to require decrease in conditional expectation, given the currently available information \(\mathcal{F}_t\) about the process.

For example, in the discrete-time case, \(V(x_{t+1})\le V(x_t)\) becomes

This is not merely an ad hoc modification: it is exactly the probabilistic analogue of “\(V\) does not increase along trajectories,” with the deterministic next state replaced by the conditional distribution of \(X_{t+1}\) given all of the information about the process up to time \(t\).

Supermartingales#

A stochastic process \((M_t)_{t \ge 0}\) is called a supermartingale if

Equation (8) is therefore a special case of (9): if we define \(M_t := V(X_t)\), then (8) is precisely the statement that \((M_t)_{t \ge 0}\) is a supermartingale. In other words, the function \(V\) serves as a “non-increasing certificate,” formulated in terms of conditional expectations. We call such functions \(V\) supermartingale certificates.

Many specifications in verification and safe AI are hitting-event statements:

• “avoid unsafe set \(U\)” (safety),
• “reach goal set \(G\)” (reachability),
• “reach \(G\) before \(U\)” (reach-avoid).

These are naturally expressed using stopping times.

A random time \(\tau\) is a stopping time if the event \(\{\tau\le t\}\) can be determined from information available up to time \(t\). Typical examples:

• first time the process enters an unsafe region or a goal region,
• deterministic deadlines (e.g., \(t=10\)).

Under standard technical conditions, supermartingales satisfy an optional stopping inequality:

Thus, one can think of supermartingale certificates as stochastic extensions of Lyapunov and barrier certificates. In the deterministic setting, a Lyapunov function enforces a one-step (or infinitesimal) decrease condition, which implies invariance of sublevel sets and hence stability-type guarantees. In the stochastic setting, the analogous requirement is not pointwise decrease—since noise can produce occasional increases—but negative drift in conditional expectation, i.e., the supermartingale condition. This preserves the same high-level role of the certificate (a scalar quantity that “tends not to increase”), while replacing deterministic monotonicity by its probabilistic counterpart.

The same connection applies to barrier reasoning: deterministic barrier certificates prove invariance of a safe set by preventing threshold crossing, while supermartingale certificates typically yield probabilistic barrier guarantees by bounding the probability of hitting the unsafe set. In both cases, the conceptual pattern is unchanged: design a scalar function whose evolution is constrained. At the same time, the conclusion becomes quantitative and probabilistic rather than absolute.

Example: Bounding Failure Probability#

Let \(U\) be an unsafe set and let \(\tau\) be the hitting time of \(U\). Suppose we design \(V\) such that:

1. \(V(x)\ge 0\) for all \(x\),
2. \(V(x)\ge 1\) for all \(x\in U\),
3. \(V(X_t)\) is a supermartingale outside of \(U\).

Assuming that \(X_0 = x_0\) is given, consider a process \((M_t)_{t\geq 0}\) that is given by

This process is a supermartingale. Therefore, by optional stopping (10),

At the same time, by Markov’s inequality

This provides a lower bound for the safety event \(\{\forall t\ge 0 : X_t\notin U\}\),

Equation (11) captures the central idea of supermartingale certificates in one line:

Local expected decrease yields lower probability bounds.

Summary#

This post introduced the certificate viewpoint in three stages.

1. Lyapunov functions (deterministic stability) certify energy dissipation and settling behavior.
2. Barrier functions (deterministic safety) provide safety envelopes via energy sublevel sets \(\{E\le c\}\) that are forward invariant.
3. Supermartingales (stochastic certificates) capture these properties in the presence of randomness, and stopping-time arguments yield quantitative probability bounds for hitting events.