日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

Lexicographic Ranking Supermartingales with
Lazy Lower Bounds
Toru Takisaka, Libo Zhang, Changjiang Wang, Jiamou Liu
Lexicographic Ranking SuperMartingale (LexRSM) is a probabilistic extension of Lexicographic Ranking
Function (LexRF), which is a widely accepted technique for verifying program termination. In this paper,
we are the ﬁrst to propose sound probabilistic extensions of LexRF with a weaker non-negativity condition, called single-component (SC) non-negativity. It is known that such an extension, if it exists, will be
nontrivial due to the intricacies of the probabilistic circumstances. Toward the goal, we ﬁrst devise thenotion of ﬁxability, which oﬀers a systematic approach for analyzing the soundness of possibly negative
LexRSM. This notion yields a desired extension of LexRF that is sound for general stochastic processes.
We next propose another extension, called Lazy LexRSM, toward the application to automated veriﬁcation;
it is sound over probabilistic programs with linear arithmetics, while its subclass is amenable to automatedsynthesis via linear programming. We ﬁnally propose a LexRSM synthesis algorithm for this subclass, andperform experiments.

transitions is prohibited.

1 Introduction

The existence of sucha function implies termination of the underlying
Lexicographic RFs with

program, and therefore, one can automate veriﬁ-

diﬀerent non-negativity conditions. Ranking

cation of program termination by RF synthesis al-function (RF) is one of the most well-studied tools

gorithms.

Background 1:

for verifying program termination. An RF is typ-Improving the applicability of RF synthesis algo-

ically a real-valued function over program statesrithms, i.e., making them able to prove terminationthat satisﬁes: (a) the ranking condition, which re-of a wider variety of programs, is one of the core in-quires an RF to decrease its value by a constantterests in the study of RF. A lexicographic extension

through each transition; and (b) the non-negativityof RF (LexRF) [8,10] is known as a simple but eﬀec-

condition, which imposes a lower bound on thetive approach to the problem. Here, a LexRF is avalue of the RF so that its inﬁnite descent throughfunction to real-valued vectors instead of the reals,∗ ゆるやかな下限を持つ辞書式順序の超マルチンゲール

and its ranking condition is imposed with respect toThis is an unreferred paper, whose content has been
published in the proceedings of The 36th International Conference on Computer Aided Veriﬁcation(CAV 2024).
Toru Takisaka, Changjiang Wang, 電 子 科 技 大 学 計
算機科学・工学部, School of Computer Science andEngineering, University of Electronic Science andTechnology of China.
Libo Zhang, Jimou Liu, オークランド大学 計算機科学部, School of Computer Science, The University of
Auckland.

the lexicographic order. For example, the value of a
LexRF may change from (1, 1, 1) to (1, 0, 2) througha state transition; here, the value “lexicographicallydecreases by 1” through the transition, that is, it
decreases by 1 in some dimension while it is nonincreasing on the left to that dimension. LexRF isparticularly good at handling nested structures ofprograms, as vectors can measure the progress ofℓ1 : skip ;//η = (a1 , b1 , c1 )similar to RFs except that the ranking condition re-ℓ2 : x := 1 ;//η = (a2 , b2 , c2 )quires an RSM to decrease its value in expectation.

...
Non-negativity condition
Strong non-neg.
Leftward non-neg.
Single-component non-neg.

図1

The existence of an RSM typically implies almostη should be non-neg. at
a1 , b 1 , c1 , a 2 , b 2 , c 2
a1 , b 1 , a 2
b1 , a2

A demo of diﬀerent non-negativity

conditions for LexRFs. There, the ranking
dimensions of the LexRF η are indicated byunderlines, and the last column of the tableshows where each condition requires η to be
non-negative.

sure termination of the underlying program, i.e.,termination of the program with probability 1.
Such a probabilistic extension has been actively
studied, in fact: probabilistic programs are used
in e.g., stochastic network protocols [33], randomized algorithms [18,26], security [6,7,27], and planning [11]; and there is a rich body of studies in RSM
as a tool for automated veriﬁcation of probabilistic
programs (see §8). Similar to the RF case, a lexi-

diﬀerent “phases” of programs separately. LexRF

cographic extension of RSM (LexRSM, [2,15]) is an

is also used in top-performing termination provers

eﬀective approach to improve its applicability. In(e.g., [1]).

addition to its advantages over nested structures,

There are several known ways to impose non-

LexRSM can also witness almost-sure termination

negativity on LexRFs (see also Fig. 1): (a) Strongof certain probabilistic programs with inﬁnite ex-

non-negativity, which requires non-negativity in ev-

pected runtime [2, Fig. 2]; certifying such programs

ery dimension of the LexRF; (b) leftward non-is known as a major challenge for RSMs.

negativity, which requires non-negativity on theleft of the ranking dimension of each transition,i.e., the dimension where the value of the LexRF
should strictly decrease through the transition; and(c) single-component non-negativity, which requires
non-negativity only in the ranking dimensions. It
is known that any of these non-negativity conditions makes the resulting LexRF sound [8, 10], i.e.,a program indeed terminates whenever it admitsa LexRF with either of these non-negativity conditions. For better applicability, single-component
non-negativity is the most preferred, as it is theweakest constraint among the three.

Problem: Sound probabilistic extension of
LexRF with weaker non-negativity. strongly
non-negative LexRF soundly extends to LexRSM
in a canonical way [2], i.e., basically by changing
the clause “decrease by a constant” in the ranking condition of LexRF to “decrease by a constantin expectation”.

In contrast, the similar exten-

sion of leftward or single-component non-negative
LexRF yields an unsound LexRSM notion [15, 20].
To date, a sound LexRSM with the weakest nonnegativity in the literature is Generalized LexRSM(GLexRSM) [15], which demands leftward nonnegativity and an additional one, so-called expected

Background 2: Probabilistic programs andleftward non-negativity. Roughly speaking, the lat-

lexicographic RSMs. One can naturally think

ter requires LexRSMs to be non-negative in eachof a probabilistic counterpart of the above argu-

dimension (in expectation) upon “exiting” the left

ment. One can consider probabilistic programs thatof the ranking dimension. For example, in Fig. 1,

admit randomization in conditional branching andit requires b2 to be non-negative, as the second di-variable updates. The notion of RF is then general-mension of η “exits” the left of the ranking dimen-

ized to Ranking SuperMartingale (RSM), a function

sion upon the transition ℓ1 → ℓ2 . GLexRSM does

not generalize either leftward or single-component

thesis algorithms in [15] cannot witness its almost-

non-negative LexRF, in the sense that the former

sure termination); for example, the function η

is strictly more restrictive than the latter two whenranks every transition of the program, but violates

it is considered over non-probabilistic programs.

both leftward and expected leftward non-negativity

These results do not mean that leftward or single-

at the transition ℓ1 → ℓ2 (note η ranks this tran-

component non-negative LexRF can never be ex-sition in the third dimension; to check the viola-

tended to LexRSM, however. More concretely, thetion of expected leftward non-negativity, also notefollowing problem is valid (see the last paragraphη ranks ℓ2 → ℓ4 in the ﬁrst dimension). Here, theof §3 for a formal argument):

source of the problem is that the program has two

KEY PROBLEM: Find a sound LexRSM notion that instantiates†1 single-component non-variables whose progress must be measured (i.e.,

negative LexRF, i.e.,a LexRSM notion

in ℓ4 ), but one of their progress measures can bewhose condition is no stronger than that ofarbitrarily small during the program execution (ysingle-component non-negative LexRF in non-can be initialized with any value). Not only thatprobabilistic settings.

this structure is rather fundamental, it is also ex-increment y to 10 in ℓ3 ; and increment x to 5

We are motivated to study this problem for a couple

pected that our desired LexRSM could handle it, ifof reasons. First, it is a paraphrase of the follow-

it exists. Indeed, modify the probabilistic programing fundamental question: when do negative values

in Fig. 2 into a non-probabilistic one by changing

of (Lex)RSM cause trouble, say, to its soundness?

“Unif [1, 2]” to “1”; then the program admits η asThis question is a typical example in the study ofa single-component non-negative LexRF.

RSM where the question becomes challenging due

Contributions. In this paper, we are the ﬁrst toto its probabilistic nature. The question also ap-

introduce sound LexRSM notions that instantiate

pears in other topics in RSM; for example, it issingle-component non-negative LexRF. Our contri-

known that the classical variant rule of Floyd-Hoare

butions are threefold, as we state below.

logic does not extend to almost-sure termination• First, in response to the ﬁrst motivation weof probabilistic programs in a canonical way [24],stated above, we devise a novel notion of ﬁxa-

due to the complicated treatment of negativity inbility as a theoretical tool to analyze if negative

RSMs. To our knowledge, this question has only

values of a LexRSM “cause trouble”. Roughly

been considered in an ad-hoc manner through coun-speaking, we identify the source of the trouble

terexamples (e.g., [15, 20, 24]), and we do not yet

as “ill” exploitation of unbounded negativity of

have a systematic approach to answering it.

LexRSM; our ε-ﬁxing operation prohibits such

Second, relaxing the non-negativity condition of

exploitation by basically setting all the nega-

LexRSM is highly desirable if we wish to fully un-tive values of a LexRSM into the same negative

lock the beneﬁt of the lexicographic extension invalue −ε, and we say a LexRSM is ε-ﬁxable if

automated veriﬁcation. A motivating example isit retains the ranking condition through suchgiven in Fig. 2. The probabilistic program in Fig. 2

a transformation. We give more details about

terminates almost-surely, but it does not admit any

its concept and key ideas in §2.

linear GLexRSM (and hence, the GLexRSM syn-

The soundness of ε-ﬁxable LexRSM imme-†1 We use the term “instantiate” to emphasize that
we compare LexRSM and LexRF.

diately follows from that of strongly non-x := 0 ;ℓ1 : while x < 5 do

η = (15 − 2x, 12 − y, 1)[x < 7]ℓ2 :

η = (15 − 2x, 12 − y, 0)[x < 5]η = (15 − 2x, 11 − y, 2)[y < 10, x < 5]

η = (14 − 2x,0, 1)[y ≥ 10, x < 5]

η=(

0, 0)

[x ≥ 5]i f y < 10 theny := y + Unif [1, 2]

ℓ3 :

else
x := x + Unif [1, 2]

ℓ4 :
fi
od
ℓ5 :
図2

0,

A probabilistic modiﬁcation of speedDis1 [4], where Unif [a, b] is a uniform sampling from the(continuous) interval [a, b]. Inequalities on the right represent invariants. While η is not a
GLexRSM, it is an LLexRSM we propose; thus it witnesses almost-sure termination of the
program.

negative one [2] because any LexRSM becomes

ative in some dimension, it must stay nega-strongly non-negative through the ε-ﬁxing op-

tive until that dimension exits the left of theeration (after globally adding ε).

Fixableranking one. For example, η in Fig. 2 is an

LexRSM instantiates single-component non-

LLexRSM; indeed, ℓ2 → ℓ4 and ℓ1 → ℓ5 arenegative LexRF for general stochastic pro-the only transitions where η possibly changes

cesses (Thm. 4.3), while also serving as a tech-its value from negative to non-negative in somenical basis for proving the soundness of otherdimension (namely, the second one), which is

LexRSMs. Meanwhile, ﬁxable LexRSM cannot

although the right to the ranking dimension

be directly applied to automated veriﬁcation(the ﬁrst one).

algorithms due to the inherent non-linearity of

We prove linear LLexRSM is sound for prob-

ε-ﬁxing; this observation leads us to our second

abilistic programs over linear arithmetics (seecontribution.

Thm. 5.4 for the exact assumption). The proof• Second, in response to the second motiva-

is highly nontrivial, which is realized by subtle

tion we stated above, we introduce Lazyuse of a reﬁned variant of ﬁxability; we explain

LexRSM (LLexRSM) as another LexRSM no-its core idea in §2.

tion that instantiates single-component non-shows that expected leftward non-negativity innegative LexRF. LLexRSM does not in-

GLexRSM [15] is actually redundant under thevolve the ε-ﬁxing operation in its deﬁni-

assumption in Thm. 5.4. This is surprising,tion; thanks to this property, we have a

as expected leftward non-negativity has been

subclass of LLexRSM that is amenable toinvented to restore the soundness of leftward

automated synthesis via linear programming

non-negative LexRSM, which is generally un-(see §6).

sound.

The LLexRSM condition consists

Furthermore, Thm. 5.4of the single-component non-negative LexRSM• Third, we present a synthesis algorithm for thecondition and stability at negativity we propose

subclass of LLexRSM we mentioned above, and(Def. 5.1), which roughly requires the follow-

do experiments; there, our algorithms veriﬁed

ing: Once the value of a LexRSM gets neg-

almost-sure termination of various programs

that could not be handled by (a better proxy

ative value in the ranking domain R should beof) the GLexRSM-based one. The details canunderstood as the same state, namely the “bot-be found in §7.

tom” of the domain. Meanwhile, the ranking condition evaluates diﬀerent negative values diﬀerently;

2 Key Observations with Examples

a smaller negative value of ηk can contribute more

Here we demonstrate by examples how intricate

to satisfy the ranking condition, as one can see fromthe treatment of negative values of LexRSM is, andthe behavior of η2 in Fig. 3 at ℓ3 . The function η in

how we handle it by our proposed notion of ﬁxabil-Fig. 3 satisﬁes the ranking condition over a possibly

ity.

non-terminating program through “ill” exploitation

Blocking “ill” exploitation of unboundednegativity. Fig. 3 is a counterexample that shows
leftward non-negative LexRSM is generally unsound (conceptually the same as [15, Ex. 1]). The
probabilistic program in Fig. 3 does not terminate
almost-surely because the chance of entering ℓ4from ℓ3 quickly decreases as t increases. Meanwhile,η = (η1 , η2 , η3 ) in Fig. 3 is a leftward non-negative
LexRSM over a global invariant [0 ≤ x ≤ 1]; inparticular, observe η2 decreases by 1 in expectation from ℓ3 , whose successor location is either ℓ4
or ℓ1 .

of this inconsistency; as t becomes larger, the valueof η2 potentially drops more signiﬁcantly throughthe transition from ℓ3 , but with a smaller probability.
The ﬁrst variant of our ﬁxability notion, called
ε-ﬁxability, enables us to ensure that such exploitation is not happening. We simply set every negative value in a LexRSM η to a negative constant−ε, and say η is ε-ﬁxable if it retains the ranking
condition through the modiﬁcation†2 . For example, the ε-ﬁxing operation changes the value of η2
in Fig. 3 at ℓ4 from −2t to −ε, and η does not satisfy the ranking condition after that. Therefore,
η in Fig. 3 is not ε-ﬁxable for any ε > 0 (i.e.,

x := 0 ; t := 1 ;ℓ1 : while x = 0 do

η = (2 − x,0, 2)

we successfully reject this η through the ﬁxabil-ℓ2 :t := t + 1 ;

η=(

2,

0, 1)

ity check). Meanwhile, an ε-ﬁxable LexRSM wit-ℓ3 :i f prob(2−t )

η=(

2,

0, 0)

nesses almost-sure termination of the underlyingη=(2, −2 , 0)program; indeed, the ﬁxed LexRSM is a stronglyℓ4 :then x := 1tnon-negative LexRSM (by globally adding ε to thefiﬁxed η), which is known to be sound [2].

od
ℓ5 :
図3

η=(

0,

0, 0)

An example of “ill” exploitation.

The notion of ε-ﬁxability is operationally so simple that one might even feel it is a boring idea; nevertheless, its contribution to revealing the nature ofThis example reveals an inconsistency between
the ways how the single-component non-negativity
and ranking condition evaluate the value of a
LexRSM, say η = (η1 , . . . , ηn ).

The single-

possibly negative LexRSM is already signiﬁcant inour paper. Indeed, (a) ε-ﬁxable LexRSM instantiates single-component non-negative LexRF with
an appropriate ε (Thm. 4.3); (b) ε-ﬁxable LexRSM

component non-negativity claims η cannot ranka transition in a given dimension k whenever ηkis negative; intuitively, this means that any neg-

†2 To give the key ideas in a simpler way, the description here slightly diﬀers from the actual deﬁnitionin §4; referred results in §2 are derived from thelatter. See Rem. 4.1.

generalizes GLexRSM [15], and the proof oﬀers

ε-ﬁxability by allowing “harmless” unbounded neg-an alternative proof of soundness of GLexRSM

ative values of η.

that is signiﬁcantly simpler than the original one(Thm. 4.4); and (c) its reﬁned variant takes thex := 0 ; t := 1 ;crucial role in proving soundness of our secondℓ1 : while x = 0 do

η = (2 − x,

LexRSM variant, lazy LexRSM.

ℓ2 :

η=(

2,

t)

η=(

2,

4t + 2)η=(

2, −2t − 4)

η=(

0,

i f prob(0.5)ℓ3 :Allowing “harmless” unbounded negativ-

then t := 4tℓ4 :e l s e x := 1

ity. While ε-ﬁxable LexRSM already instantiatesfi

single-component non-negative LexRF, we go one
step further to obtain a LexRSM notion that is

t + 1)

od
ℓ5 :

0)

amenable to automated synthesis, in particular via
Linear Programming (LP). The major obstacle to

図4

An example of ”harmless” unboundednegativity.

this end is the case distinction introduced by εﬁxability, which makes the ﬁxed LexRSM nonlinear. Lazy LexRSM (LLexRSM), our second proposed LexRSM, resolves this problem while it also
instantiates single-component non-negative LexRF.
Linear LLexRSM is sound over probabilistic programs with linear arithmetics (Thm. 5.4). The key
to the proof is, informally, the following observation: Restrict our attention to probabilistic programs and functions η that are allowed in the LPbased synthesis. Then “ill” exploitation in Fig. 3
never occurs, and therefore, a weaker condition
than ε-ﬁxability (namely, the LLexRSM one) sufﬁces for witnessing program termination. In fact,
Fig. 3 involves (a) non-linear arithmetics in the program, (b) parametrized if-branch in the program(i.e., the grammar “ if prob(p) then P else Q ﬁ” with p being a variable), and (c) non-linearityof η. None of them are allowed in the LP-based
synthesis (at least, in the standard LP-based synthesis via Farkas’ Lemma [2, 12, 15]). Our informal
statement above is formalized as Thm. 5.3, whichroughly says: Under such a restriction to probabilistic programs and η, any LLexRSM is (ε, γ)ﬁxable. Here, (ε, γ)-ﬁxability is a reﬁned version of
ε-ﬁxability; while it also ensures that “ill” exploitation is not happening in η, it is less restrictive thanFig. 4 gives an example of such a harmless behavior of η rejected by ε-ﬁxability. It also shows
why we cannot simply use ε-ﬁxability to check an
LLexRSM does not do “ill” exploitation. The function η = (η1 , η2 ) in Fig. 4 is leftward non-negative
over the global invariant [0 ≤ x ≤ 1 ∧ t ≥ 1], so it isan LLexRSM for the probabilistic program there;
the program and η are also in the scope of LP-based
synthesis; but η is not ε-ﬁxable for any ε > 0. Indeed, the ε-ﬁxing operation changes the value of η2
at ℓ4 from −2t − 4 to −ε, and η does not satisfy
the ranking condition at ℓ2 after the change. Here
we notice that, however, the unbounded negativevalues of η2 are “harmless”; that is, the “ill-gotten
gains” by the unbounded negative values of η2 atℓ4 are only “wasted” to unnecessarily increase η2
at ℓ3 . In fact, η still satisﬁes the ranking condition
if we change the value of η2 at ℓ1 , ℓ2 , ℓ3 to 2, 1, and0, respectively.
We resolve this issue by partially waiving the
ranking condition of η after the ε-ﬁxing operation.
It is intuitively clear that the program in Fig. 4
almost-surely terminates, and the intuition here isthat the program essentially repeats an unbiased
coin tossing until the tail is observed (here, “observe the tail” corresponds to “observe prob(0.5) =false at ℓ2 ”). This example tells us that, to wit-las with atomic predicates of the form f ≤ g, where

ness the almost-sure termination of this program,f, g : valV → R and R is linearly ordered. Often,

we only need to guarantee the program (almost-

we are only interested in the value of a predicate

surely) visits either the terminal location ℓ5 or theφ over a certain subset X ⊆ valV , in which case,“coin-tossing location” ℓ2 from anywhere else. The

we call φ a predicate over X . We identify a predi-

ε-ﬁxed η in Fig. 4 does witness such a property

cate φ over X with a function φ̃ : X → {0, 1} suchof the program, as it ranks every transition exceptthat φ̃(x) = 1 if and only if φ(x) is true. The se-those that are from a coin-tossing location, namely

mantics of φ, i.e., the set {x ∈ X | φ(x) is true},ℓ2 .

is denoted by JφK.

The characteristic function

We generalize this idea as follows: Fix γ ∈ (0, 1),

1A : X → {0, 1} of a subset A of X is a function

and say a program state is a “coin-tossing state”

such that J1A = 1K = A. For a probability spacefor η = (η1 , . . . , ηn ) in the k-th dimension if ηk(Ω, F , P), we say φ over Ω is (F -)measurable whendrops from non-negative to negative (i.e., the rank-

JφK ∈ F . For such a φ, the satisfaction probability

ing is “done” in the k-th dimension) with the prob-of φ w.r.t. P, i.e., the value P(JφK), is also denoted

ability γ or higher. Then we say η is (ε, γ)-ﬁxableby P(φ); we say φ holds P-almost surely (P-a.s.) if(Def. 4.6) if the ε-ﬁxed η is a strongly non-negativeP(φ) = 1.

LexRSM (after adding ε) except that, at each cointossing state, we waive the ranking condition of ηin the corresponding dimension. For example, ηin Fig. 4 is (ε, γ)-ﬁxable for any γ ∈ (0, 0.5]. As

3. 1 Syntax and Semantics of Probabilistic Programs
Syntax. We deﬁne the syntax of Probabilistic

expected, (ε, γ)-ﬁxable LexRSM is sound for any

Programs (PPs) similarly to e.g., [2, 35].

ε > 0 and γ ∈ (0, 1) (Cor. 4.7).

concretely, PPs have the standard control struc-Moreture in imperative languages such as if-branches

3 Preliminaries

and while-loops, while the if-branching and vari-

We recall the technical preliminaries. Omitted

able assignments can also be done in either non-details are in [36].
Notations.

We assume the readers are famil-

iar with the basic notions of measure theory, seee.g. [5, 9]. The sets of non-negative integers andreals are denoted by N and R, respectively. The
collection of all Borel sets of a topological space
X is denoted by B(X ). The set of all probability
distributions over the measurable space (Ω, B(Ω))
is denoted by D(Ω). The value of a vector x at
the i-th index is denoted by x[i] or xi . A subset
D ⊆ R of the reals is bounded if D ⊆ [−x, x] forsome x > 0.
For a ﬁnite variable set V and the set valV of its
valuations, we form predicates as ﬁrst-order formu-

deterministic or probabilistic ways. Namely, ‘if ⋆’describes a nondeterministic branching; ‘ndet(D)’describes a nondeterministic assignment chosenfrom a bounded†3 domain D ⊆ B(R); ‘if prob(p)’with a constant p ∈ [0, 1] describes a probabilistic branching that executes the ‘then’ branch withprobability p, or the ‘else’ branch with probability 1 − p; and ‘sample(d)’ describes a probabilistic
assignment sampled from a distribution d ∈ D(R).
We consider PPs without conditioning, which arealso called randomized programs [35]; PPs with conditioning are considered in e.g. [32].

The exact

grammar is given in [36].
†3 This is also assumed in [15] to avoid a complication in possibly negative LexRSMs.

In this paper, we focus our attention on PPs with

R|V | → {0, 1} to each τ ∈ ∆.

linear arithmetics; we say a PP is linear if each

Below we ﬁx a pCFG C = (L, V, ∆, Up, G). A

arithmetic expression in it is linear, i.e., of the form∑b+ ni=1 ai · vi for constants a1 , . . . , an , b and pro-state of C is a tuple s = (ℓ, x) of location ℓ ∈ Lgram variables v1 , . . . , vn .

S to denote the state set L × R|V | . Slightly abus-

Semantics. We adopt probabilistic control ﬂow

ing the notation, for τ = (ℓ, δ), we identify the set

and variable assignment vector x ∈ R|V | . We write

graph (pCFG) as the semantics of PPs, which is

JG(τ )K ⊆ R|V | and the set {ℓ} × JG(τ )K ⊆ S; instandard in existing RSM works (e.g., [12, 15, 35]).

particular, we write s ∈ JG(τ )K when τ is enabled

Informally, it is a labeled directed graph whose ver-at s, i.e., s = (ℓ, x), τ = (ℓ, δ) and x ∈ JG(τ )K.

tices are program locations, and whose edges rep-

A pCFG C with its state set S can be understoodresent possible one-step executions in the program.

as a transition system over S with probabilistic

Edges are labeled with the necessary informationtransitions and nondeterminism (or, more specif-

so that one can reconstruct the PP represented by

ically, a Markov decision process with its states

the pCFG; for example, an edge e can be labeled

S). Standard notions such as successors of a statewith the assignment commands executed throughs ∈ S, ﬁnite paths, and (inﬁnite) runs of C are de-e (e.g., ‘x := x + 1’), the probability p ∈ [0, 1] thatﬁned as the ones over such a transition system. Thee will be chosen (through ‘if prob(p)’), the guard

set of all successors of s ∈ JG(τ )K via τ is denoted

condition, and so on. Below we give its formal deﬁ-

by succτ (s). The set of runs of C is denoted by ΠC .

nition for completeness; see [36] for how to translate

Schedulers resolve nondeterminism in pCFGs.

PPs into pCFGs.

Observe there are two types of nondeterminism:

Deﬁnition 3.1 (pCFG). A pCFG is a tuple(a) nondeterministic choice of τ ∈ ∆ at a given(L, V, ∆, Up, G), wherestate (corresponds to ‘if ⋆’), and (b) nondetermin-

1. L is a ﬁnite set of locations.

istic variable update in a nondeterministic transi-

2. V = {x1 , . . . , x|V | } is a ﬁnite set of programtion τ ∈ ∆n (corresponds to ‘xi :=ndet(D)’). We

variables.
3. ∆ is a ﬁnite set of (generalized) transitions†4 ,say a scheduler is ∆-deterministic if its choice is
non-probabilistic in Case (a).

i.e., tuples τ = (ℓ, δ) of a location ℓ ∈ L and a

We assume pCFGs are deadlock-free; we also as-

distribution δ ∈ D(L) over successor locations.

sume that there are designated locations ℓin and

4. Up is a function that receives a transition τ ∈ℓout that represent program initiation and termi-∆ and returns a tuple (i, u) of a target vari-nation, respectively. An initial state is a state ofable index i ∈ {1, . . . , |V |} and an update el-

the form (ℓin , x). We assume a transition from ℓout

ement u. Here, u is either (a) a Borel mea-

is unique, denoted by τout ; this transition does not

surable function u : R|V | → R, (b) a distribu-

update anything.

tion d ∈ D(R), or (c) a bounded measurable
set R ∈ B(R). In each case, we say τ is deterministic, probabilistic, and non-deterministic,

By ﬁxing a scheduler σ and an initial state sI ,the inﬁnite-horizon behavior of C is determined asa distribution PσsI over ΠC ; that is, for a measurable

respectively; the collections of these transitions
are denoted by ∆d , ∆p , and ∆n , respectively.
5. G is a guard function that assigns a G(τ ) :†4 Deﬁning these as edges might be more typical,
as in our informal explanation. We adopt thestyle of [2, 15] for convenience; it can handle‘if prob(p)’ by a single τ .

A ⊆ ΠC , the value PσsI (A) is the probability that

A level map Lv : ∆ → {0, . . . , n} designatesa run of C from sI is in A under σ. We call thethe ranking dimension of the associated LexRSM

probability space (ΠC , B(ΠC ), PσsI ) the dynamics ofη : S → Rn .

C under σ and sI . See [9] for the formal construc-only if τ = τout .

tion; a brief explanation is in [36].

transition τ in the dimension k (under Lv) when

We deﬁne the termination time of a pCFG C as
CTterm

We require Lv(τ ) = 0 if andWe say an MM η ranks ak = Lv(τ ). An invariant is a measurable predi-: ΠC → N ∪ {+∞} such thatcate I : S → {0, 1} such that JIK is closed underCTterm(s0 s1 . . .) = inf{t ∈ N | ∃x.st = (ℓout , x)}.

transitions and ℓin × R|V | ⊆ JIK. The set JIK over-Now we formalize our objective, i.e., almost-sureapproximates the reachable states in C.

the function

termination of pCFG, as follows.

Suppose an n-dimensional MM η and an associ-Deﬁnition 3.2 (AST of pCFG). A run ω ∈ ΠC

ated level map Lv are given. We say η satisﬁes theCterminates if Tterm(ω) < ∞. A pCFG C is a.s. ter-ranking condition (under Lv and I) if the follow-

minating (AST) under a scheduler σ and an initialing holds for each τ ̸= τout , s ∈ JI ∧ G(τ )K, andstate sI if a run of C terminates PσsI -a.s. We say C

k ∈ {1, . . . , Lv(τ )}:
η[k](s)if k < Lv(τ ),Xτ η[k](s) ≤
η[k](s) − 1 if k = Lv(τ ).
We also deﬁne the three diﬀerent non-negativity

is AST if it is AST for any σ and sI .
3. 2 Lexicographic Ranking Supermartingales

conditions in Fig. 1, i.e., STrong (ST), LeftWard

Here we recall mathematical preliminaries of the
LexRSM theory. A (Lex)RSM typically comes in(LW), and Single-Component (SC) non-negativity,
as follows:

two diﬀerent forms: one is a vector-valued function(ST non-neg.) ∀s ∈ JIK.∀k ∈ {1, . . . , n}.

η : S → R over states S of a pCFG C, and anotherη[k](s) ≥ 0,

is a stochastic process over the runs ΠC of C. We(LW non-neg.) ∀τ ̸= τout .∀s ∈ JI ∧ G(τ )K.

nrecall relevant notions in these formulations, which∀k ∈ {1, . . . , Lv(τ )}.

are frequently used in existing RSM works [12, 15].

η[k](s) ≥ 0,

We also recall the formal deﬁnition of LexRSMs(SC non-neg.) ∀τ =
̸ τout .∀s ∈ JI ∧ G(τ )K.
η[Lv(τ )](s) ≥ 0.

with three diﬀerent non-negativity conditions in
Fig. 1.

All the materials above are wrapped up in the fol-

LexRSM as a quantitative predicate.

Fix

a pCFG C. An (n-dimensional) measurable map(MM) is a Borel measurable function η : S → Rn .
For a given 1-dimensional MM η and a transition
τ , The (maximal) pre-expectation of η under τ is afunction that formalizes “the value of η after thetransition τ ”.

More concretely, it is a functionXτ η : JG(τ )K → R that returns, for a given state s,
the maximal expected value of η at the successor
state of s via τ . Here, the maximality refers to theset of all possible nondeterministic choices at s.

lowing deﬁnition.
Deﬁnition 3.3 ((ST/LW/SC)-LexRSM map). Fix
a pCFG C with an invariant I. Let η be an MM associated with a level map Lv. The MM η is called a
STrongly non-negative LexRSM map (ST-LexRSM
map) over C supported by I if it satisﬁes the ranking condition and the strong non-negativity under
Lv and I.

If it satisﬁes the leftward or single-

component non-negativity instead of the strong one,then we call it LW-LexRSM map or SC-LexRSM
map, respectively.
LexRSM as a stochastic process.

When itcomes to automated synthesis, a (Lex)RSM is usually a function η over program states, as deﬁnedω ∈ JLvt ̸= 0K, and k ∈ {1, . . . , Lvt (ω)}, we have:E[Xt+1 [k] | Ft ](ω) ≤ Xt [k](ω)− c · 1Jk=Lvt K (ω)

in Def. 3.3. Meanwhile, when we prove the proper-(P-a.s.) (1)ties of (Lex)RSMs themselves (e.g., soundness), it

Here, the function E[Xt+1 [k] | Ft ] denotes theis often necessary to inspect the behavior of η upon

conditional expectation of Xt+1 [k] given Ft , which

the program execution under given scheduler σ andtakes the role of pre-expectation. We mostly let

initial state sI . Such a behavior of η is formalized

c = 1 and simply call it the ranking condition; theas a sequence (Xt )∞t=0 of random variables over the

only result sensitive to c is Thm. 4.3.

dynamics of the underlying pCFG, which forms astochastic process.

We also deﬁne the three diﬀerent non-negativity
conditions for an instance as follows. Here we adopt

A (discrete-time) stochastic process in a probability space (Ω, F , P) is a sequence (Xt )∞t=0

a slightly general (but essentially the same) vari-of F -

ant of strong non-negativity instead, calling it uni-

measurable random variables Xt : Ω → Rn forform well-foundedness; we simply allow the uniformt ∈ N. In our context, it is typically associatedlower bound to be any constant ⊥ ∈ R instead ofwith another random variable T : Ω → N ∪ {+∞}

ﬁxing it to be zero. This makes the later argumentthat describes the termination time of ω ∈ Ω. We

simpler.

say T is AST (w.r.t. P) if P(T < ∞) = 1; observe(UN well-fnd.) ∃⊥ ∈ R.∀t ∈ N.

that, if (Ω, F , P) is the dynamics of a pCFG C under∀ω ∈ Ω.∀k ∈ {1, . . . , n}. Xt [k](ω) ≥ ⊥,σ and sI , then C is AST under σ and sI if and only

(LW non-neg.) ∀t ∈ N.∀ω ∈ JLvt ̸= 0K.

C
if Tterm
is AST w.r.t.

∀k ∈ {1, . . . , Lvt (ω)}. Xt [k](ω) ≥ 0,

P. As standard technical re-quirements, we assume there is a ﬁltration (Ft )∞t=0(SC non-neg.)∞in (Ω, F , P) such that (Xt )∞t=0 is adapted to (Ft )t=0 ,∀t ∈ N.∀ω ∈ JLvt ̸= 0K. Xt [Lvt (ω)](ω) ≥ 0.

T∞
is a stopping time w.r.t. (Ft )∞t=0 , and (Xt )t=0 is

stopped at T ; see [36] for their deﬁnitions.
For a stopping time T w.r.t. (Ft )∞t=0 , we de-Deﬁnition 3.4 ((UN/LW/SC)-LexRSM). Suppose the following are given: a probability space(Ω, F , P); a ﬁltration (Ft )∞t=0 on F ; and a stop-

ﬁne a level map (Lvt )∞t=0 as a sequence of Ft -ping time T w.r.t.

measurable functions Lvt : Ω → {0, . . . n} such that∞((Xt )∞
t=0 , (Lvt )t=0 )(Ft )∞
t=0 .

An instance I =is called a UNiformly well-

JLvt = 0K = JT ≤ tK for each t. We call a pair of afounded LexRSM (UN-LexRSM) for T with the bot-stochastic process and a level map an instance fortom ⊥ ∈ R and a constant c ∈ R if (a) (Xt )∞t=0

T ; just like we construct an MM η and a level map

is adapted to (Ft )∞t=0 ; (b) for each t ∈ N and

Lv as an AST certiﬁcate of a pCFG C, we construct

1 ≤ k ≤ n, the expectation of Xt [k] exists; (c) I

an instance for a stopping time T as its AST cer-satisﬁes the c-ranking condition; and (d) I is uni-∞
tiﬁcate. We say an instance ((Xt )∞t=0 , (Lvt )t=0 ) forformly well-founded with the bottom ⊥. We de-T ranks ω ∈ Ω in the dimension k at time t whenﬁne LW-LexRSM and SC-LexRSM by changing (d)T (ω) > t and k = Lvt (ω).

with LW and SC non-negativity, respectively.

∞
For c > 0, we say an instance ((Xt )∞t=0 , (Lvt )t=0 )We mostly assume c = 1 and omit to mention thesatisﬁes the c-ranking condition if, for each t ∈ N,

constant. UN-LexRSM is known to be sound [2];meanwhile, LW and SC-LexRSM are generally unsound [15, 20]. We still mention the latter two as
parts of sound LexRSMs.

From RSM maps to RSMs. Let η be an MM

ﬁxability.

over a pCFG C with a level map Lv. Together with

Remark 4.1. As in Footnote 2, our formal deﬁni-

a ∆-deterministic scheduler σ and initial state sI ,tions of ﬁxability in this section slightly diﬀer from∞an instance ((Xt )∞t=0 , (Lvt )t=0 ) over the

an informal explanation in §2. One diﬀerence isdynamics of C, by letting Xt (s0 s1 . . .) = η(st ); it

that the ε-ﬁxing in Def. 4.2 changes the value of a

describes the behavior of η and Lv through exe-

LexRSM at dimension k whenever it is negative or

cuting C from sI under σ. Properties of η such as

k is strictly on the right to the ranking dimension.

ranking condition or non-negativity are inherited

This modiﬁcation is necessary to prove Thm. 4.4.

to the induced instance (if the expectation of Xt [k]Another is that we deﬁne ﬁxability as the notion

exists for each t, k). For example, an instance in-for an instance I, rather than for an MM η. While

duced by an ST-LexRSM map is an UN-LexRSM

the latter can be also done in an obvious way (aswith ⊥ = 0.

informally done in §2), we do not formally do thatit induces

because it is not necessary for our technical develNon-probabilistic settings, and instantiation

opment. One can “ﬁx” the argument in §2 into theof SC-LexRF. The key question in this paper is

one over instances by translating “ﬁxability of η”

to ﬁnd a LexRSM notion that instantiates SC non-to “ﬁxability of an instance induced by η”.

negative LexRF (or SC-LexRF for short); that is,Deﬁnition 4.2 (ε-ﬁxing of an instance). Let I =we would like to ﬁnd a LexRSM notion whose con-∞((Xt )∞
t=0 ), (Lvt )t=0 ) be an instance for a stopping

ditions are satisﬁed by
SC-LexRSM†5 in the non-probabilistic setting,time T , and let ε > 0. The ε-ﬁxing of I is anotherwhich we formalize as follows. We say a pCFG isa (non-probabilistic) CFG if (a) δ is Dirac for each(ℓ, δ) ∈ ∆, and (b) ∆p = ∅; this roughly means thata CFG is a model of a PP without ‘if prob(p)’ and‘sample(d)’. We say a probability space (Ω, F , P)
is trivial if Ω is a singleton, say {ω}.

4 Fixable LexRSMs
In §4-6 we give our novel technical notions andresults. In this section, we will introduce the notion of ﬁxability and related results. Here we focus
on technical rigorousness and conciseness, see §2
for the underlying intuition. Proofs are given inappendices of [36].
We begin with the formal deﬁnition of ε-∞instance Ĩ =((X̃t )∞t=0 , (Lvt )t=0 ) for T , where−ε if Xt [k](ω) < 0 or k > Lvt (ω),
X̃t [k](ω) =Xt [k](ω) otherwise.
We say an SC-LexRSM I is ε-ﬁxable, or call itan ε-ﬁxable LexRSM, if its ε-ﬁxing Ĩ is an UNLexRSM with the bottom ⊥ = −ε.
Observe that the ε-ﬁxing of any instance is uniformly well-founded with the bottom ⊥ = −ε, sothe ε-ﬁxability only asks if the ranking condition ispreserved through ε-ﬁxing. Also, observe that thesoundness of ε-ﬁxable LexRSM immediately follows
from that of UN-LexRSM [2].
While we do not directly use ε-ﬁxability as a technical tool, the two theorems below show its conceptual value. The ﬁrst one answers our key problem:
ε-ﬁxable LexRSM instantiates SC-LexRF with sufﬁciently large ε.

†5 One would perhaps expect to see “SC-LexRF ”
here; such a change does not make a diﬀerence
under a canonical deﬁnition of SC-LexRF, so wedeﬁne the notion of instantiation in this way tosave space. See also [36, Appendix A].

Theorem

4.3(ﬁxable LexRSM instantiates∞
SC-LexRF). Suppose I = ((xt )∞t=0 , (Lvt )t=0 ) is an

SC-LexRSM for a stopping time T over the trivial
probability space with a constant c, and let ε ≥ c.

Then I is ε-ﬁxable.

an abstraction of the situation “we are at a coin-

The second theorem oﬀers a formal compari-

tossing state at time t in the k-th dimension”; andson between ε-ﬁxable LexRSM and the state-of-the condition (2) corresponds to the inﬁnite coin-

the-art LexRSM variant in the literature, namely

tossing argument (for a given k, if φt,k is satisﬁed

GLexRSM [15].

We show the former subsumes

at inﬁnitely many t, then the ranking in the k-th

the latter. In our terminology, GLexRSM is LW-

dimension is “done” inﬁnitely often, with probabil-

LexRSM that also satisﬁes the following expected

ity 1). Given these, Thm. 4.5 says that the rank-

leftward non-negativity:

ing condition of UN-LexRSM can be waived over∀t ∈ N.∀ω ∈ JLvt ̸= 0K.∀k ∈ {1, . . . , Lvt (ω)}.

JXt [k] > ⊥ ∧ φt,k K. In particular, the theorem

E[1Jk>Lvt+1 K · Xt+1 [k] | Ft ](ω) ≥ 0.

amounts to the soundness of UN-LexRSM when

We note that our result can be also seen as an al-

φt,k ≡ false for each t and k.

ternative proof of the soundness of GLexRSM [15,Based on Theorem 4.5, we introduce (ε, γ)-Thm. 1]. Our proof is also signiﬁcantly simpler

ﬁxability as follows. There, P[φ | F ′ ] := E[1JφK |than the original one, as the former utilizes theF ′ ] is the conditional probability of satisfying φsoundness of UN-LexRSM as a lemma, while thegiven F ′ .

latter does the proof “from scratch”.

Deﬁnition

Theorem∞((Xt )∞
t=0 , (Lvt )t=0 )4.4(ﬁxableLexRSM

generalizes

4.6((ε, γ)-ﬁxability). Let I=

be an instance for T , and let

GLexRSM). Suppose I is a GLexRSM for a stop-γ ∈ (0, 1). We call I a γ-relaxed UN-LexRSM forping time T . Then I is ε-ﬁxable for any ε > 0.

T if I satisﬁes the properties in Thm. 4.5, where

Now we move on to a reﬁned variant, (ε, γ)-φt,k is as follows:ﬁxability. Before its formal deﬁnition, we give aφt,k (ω) ≡ P[Xt+1 [k] = ⊥ | Ft ](ω) ≥ γ.

theorem that justiﬁes the partial waiving of theWe say I is (ε, γ)-ﬁxable if its ε-ﬁxing Ĩ is a γ-

ranking condition described in §2. Below, ∃ t.φtrelaxed UN-LexRSM.

∞

stands for ∀k ∈ N.∃t ∈ N.[t > k ∧ φt ].

(3)

The predicate φt,k (ω) in (3) is roughly read “theTheorem 4.5 (relaxation of the UN-LexRSM con-ranking by (Xt )∞t=0 is done at time t + 1 in dimen-

dition). Suppose the following are given: a prob-

sion k with probability γ or higher, given the infor-

ability space (Ω, F , P); a ﬁltration(Ft )∞
t=0

on F ;

mation about ω at t”. This predicate satisﬁes Con-Let I =

dition (2); hence we have the following corollary,∞((Xt )∞
t=0 , (Lvt )t=0 ) be an instance for T , and let

which is the key to the soundness of lazy LexRSM

and a stopping time T w.r.t.
⊥ ∈ R.

(Ft )∞t=0 .

For each k ∈ {1, . . . , n}, let (φt,k )∞t=0 be asequence of predicates over Ω such that

Corollary 4.7 (soundness of (ε, γ)-ﬁxable in-∞∃ t.φt,k (ω) ⇒∞in §5.
stances). Suppose there exists an instance I over(2)(Ω, F , P) for a stopping time T that is (ε, γ)-ﬁxable

Suppose I is an UN-LexRSM with the bottom ⊥ ex-

for any ε > 0 and γ ∈ (0, 1). Then T is AST w.r.t.

cept that, instead of the ranking condition, I satis-P.

∃ t.[Xt [k](ω) = ⊥ ∨ k > Lvt (ω)](P-a.s.)ﬁes the inequality (1) only for t ∈ N, k ∈ {1, . . . , n},

5 Lazy LexRSM and Its Soundnessand ω ∈ Jk ≤ Lvt ∧ ¬(Xt [k] > ⊥ ∧ φt,k )K (withHere we introduce another LexRSM variant, Lazyc = 1). Then T is AST w.r.t. P.

LexRSM (LLexRSM). We need this variant for

The correspondence between the argument in §2

our LexRSM synthesis algorithm; while ε-ﬁxable

and Thm. 4.5 is as follows. The predicate φt,k is

LexRSM theoretically answers our key question, it

is not amenable to LP-based synthesis algorithms

class of such distributions covers all distributions

because its case distinction makes the resulting con-with bounded supports and some distributions withstraint nonlinear.

unbounded supports such as the normal distribu-

We deﬁne LLexRSM map as follows; see Con-

tions [36, Prop. C.6].

tributions in §1 for its intuitive meaning with an

Possibly negative (Lex)RSM typically requires

example. The deﬁnition for an instance is in [36,some restriction on variable samplings of pCFG

Appendix C].

(e.g., the integrability in [15]) so that the pre-Deﬁnition 5.1 (LLexRSM map). Fix a pCFG C

expectation is well-deﬁned.

with an invariant I. Let η be an MM associated

The crucial part of the soundness proof is thewith a level map Lv. The MM η is called a Lazyfollowing theorem, where (ε, γ)-ﬁxability takes the

LexRSM map (LLexRSM map) over C supported

key role. Its full proof is given in [36, Appendix C].

by I if it is an SC-LexRSM map over C supported

Theorem 5.3. Let η : S → Rn be a linear

by I, and satisﬁes stability at negativity deﬁned as

LLexRSM map for a linear, well-behaved pCFG C.

follows:

Then for any ∆-deterministic scheduler σ and ini-∀τ ̸= τout .∀s ∈ JI ∧ G(τ )K.∀k ∈ {1, . . . , Lv(τ ) − 1}.
[′η[k](s) < 0 ⇒ ∀s ∈ succτ (s).
]η[k](s ) < 0 ∨ k > ′ ′max ′ Lv(τ ′ ) .
′τ :s ∈JG(τ )K

We ﬁrst observe LLexRSM also answers our key

tial state sI of C, the induced instance is (ε, γ)ﬁxable for some ε > 0 and γ ∈ (0, 1).
Proof (sketch). We can show that the ε-ﬁxing∞
Ĩ = ((X̃t )∞t=0 , (Lvt )t=0 ) of an induced instancequestion.

∞I = ((Xt )∞t=0 , (Lvt )t=0 ) almost-surely satisﬁes the

Theorem 5.2 (LLexRSM instantiates SC-LexRF).

inequality (1) of the ranking condition for each t,

Suppose ηis an SC-LexRSM over a non-ω, and k such that X̃t [k](ω) = −ε and 1 ≤ k ≤probabilistic CFG C supported by an invariant I,

Lvt (ω) [36, Prop. C.2]. Thus it suﬃces to show,with a level map Lv. Then η is stable at negativity

for each ω, k, and t such that X̃t [k](ω) ≥ 0 andunder I and Lv, and hence, η is an LLexRSM map

1 ≤ k ≤ Lvt (ω), either Ĩ satisﬁes the inequality (1)over C supported by I, with Lv.

or (1) as a requirement on Ĩ is waived due to the

Below we give the soundness result of LLexRSM
map.

We ﬁrst give the necessary assumptions

γ-relaxation.
Now take any such t, ω, and k, and suppose

on pCFGs and MMs, namely linearity and well-

the run ω reads the program line prog at time

behavedness. we say a pCFG is linear if the updatet. Then we can show the desired property by aelement of each τ ∈ ∆d is a linear function (thiscase distinction over prog as follows.

corresponds to the restriction on PPs to the linear

call ω is a sequence s0 s1 . . . st st+1 . . . of programones); and an MM η is linear if λx.η(ℓ, x) is lin-states; we deﬁned Xt by Xt [k](ω) = η[k](st ); andear for each ℓ ∈ L. We say a pCFG is well-behaved

E[Xt+1 [k] | Ft ](ω) is the expectation of η[k](s′ ),if its variable samplings are done via well-behaved

where s′ is the successor state of s0 . . . st under σdistributions, which roughly means that their tail(which is not necessarily st+1 ). Also observe theprobabilities vanish to zero toward inﬁnity quickly

requirement (1) on Ĩ is waived for given t, ω, andenough. Its formal deﬁnition is given in [36, Def.

k when the value of η[k](s′ ) is negative with theC.4], which is somewhat complex; an important

probability γ or higher.

fact from the application perspective is that the

1. Suppose prog is a non-probabilistic program

Here, re-line, e.g., ‘xi := f (x)’ or ‘while φ do’. Thenthe successor state s′ of st is unique. If η[k](s′ )subclass, and then introduce our algorithm.

is non-negative, then we have E[X̃t+1 [k] |Our algorithm is a variant of linear template-Ft ](ω) = E[Xt+1 [k] | Ft ](ω), so the inequal-

based synthesis. There, we ﬁx a linear MM η withity (1) is inherited from I to Ĩ; if negative,

unknown coeﬃcients (i.e., the linear template), andthen the requirement (1) on Ĩ is waived. The

consider an assertion “η is a certiﬁcate of AST”; forsame argument applies to ‘if ⋆ then’ (recall I

example, in the standard 1-dimensional RSM syn-is induced from a ∆-deterministic scheduler).

thesis, the assertion is “η is an RSM map”. We

2. Suppose prog ≡ ‘if prob(p) then’. By letting

then reduce this assertion into a set of linear con-′γ strictly smaller than p, we see either η[k](s )straints via Farkas’ Lemma [34]. These constraints

is never negative, or it is negative with a prob-

constitute an LP problem with an appropriate ob-ability more than γ. Thus we have the desired

jective function. A certiﬁcate is synthesized, if fea-

property for a similar reason to Case 1 (we notesible, by solving this LP problem. The reduction is

this argument requires p to be a constant).

standard, so we omit the details; see e.g. [35].

3. Suppose prog ≡ ‘xi := sample(d)’. We canshow the desired property by taking a suﬃciently small γ; roughly speaking, the requirement (1) on Ĩ is waived unless the chance of
η[k](s′ ) being negative is very small, in whichcase the room for “ill” exploitation is so smallthat the inequality (1) is inherited from I
to Ĩ. Almost the same argument applies to‘xi := ndet(D)’.
We note, by the ﬁniteness of program locations
L and transitions ∆, we can take γ ∈ (0, 1) thatsatisﬁes all requirements above simultaneously.
Now we have soundness of LLexRSM as the following theorem, which is almost an immediate consequence of Thm. 5.3 and Cor. 4.7.
Theorem 5.4 (soundness of linear LLexRSM map
over linear, well-behaved pCFG). Let C be a linear,well-behaved pCFG, and suppose there is a linear
LLexRSM map over C (supported by any invariant).
Then C is AST.

6 Automated Synthesis Algorithm of
LexRSM
In this section, we introduce a synthesis algorithm of LLexRSM for automated AST veriﬁcationof linear PPs. It synthesizes a linear MM in a certain subclass of LLexRSMs. We ﬁrst deﬁne theSubclass of LLexRSM for automated synthesis.

While LLexRSM resolves the major is-sue that ﬁxable LexRSM confronts toward its automated synthesis, we still need to tweak the notion
a bit more, as the stability at negativity condition
involves the value of an MM η in its antecedent
part (i.e., it says “whenever η[k] is negative forsome k...”); this makes the reduced constraints via
Farkas’ Lemma nonlinear. Therefore, we augment
the condition as follows.
Deﬁnition 6.1 (MCLC). Let η : S → Rn be an
MM supported by an invariant I, with a level map
Lv. We say η satisﬁes the multiple-choice leftward
condition (MCLC) if, for each k ∈ {1, . . . , n}, itsatisﬁes either (4) or (5) below:∀τ ∈ Jk < LvK.∀s ∈ JI ∧ G(τ )K.
η[k](s) ≥ 0,(4)

∀τ ∈ Jk < LvK.∀s ∈ JI ∧ G(τ )K.∀s′ ∈ succτ (s).
η[k](s′ ) ≤ η[k](s).

(5)

Condition (4) is nothing but the non-negativity
condition in dimension k. Condition (5) augments
the ranking condition in the strict leftward of the
ranking dimension (a.k.a. the unaﬀecting condition) so that the value of η[k] is non-increasing in
the worst-case. MCLC implies stability at negativity; hence, by Thm. 5.4, linear SC-LexRSM maps

with MCLC certify AST of linear, well-behaved

is 2U \ {∅}, the brute-force trial; the resulting algo-pCFGs. They also instantiate SC-LexRFs as fol-rithm does not terminate in polynomial time, but

lows.

ranks the maximal number of transitions (by trying

Theorem 6.2 (SC-LexRSM maps with MCLC

each T in the descending order w.r.t. |T |). Thisinstantiate SC-LexRFs). Suppose η is an SC-

property makes the algorithm complete. Another

LexRSM map over a non-probabilistic CFG C sup-choice is the singletons of U , i.e., {{τ } | τ ∈ U };ported by I, with Lv. Then η satisﬁes MCLC underwhile the resulting algorithm terminates in polyno-

I and Lv.

mial time, it lacks the maximality property. It is

The algorithm.

Our LexRSM synthesis algo-

our future work to verify if there is a polynomial

rithm mostly resembles the existing ones [2, 15], socomplete instance of our proposed algorithm. Still,

we are brief here; a line-to-line explanation with aany instance of it is complete over yet another classpseudocode is in [36, Appendix D].

of LLexRSMs, namely linear LW-LexRSMs. For a

The algorithm receives a pCFG C and an invari-formal statement and its proof, see [36, Thm. D.1].

ant I, and attempts to construct a SC-LexRSM
with MCLC over C supported by I. The construc-

7 Experimentstion is iterative; at the k-th iteration, the algorithm

We performed experiments to evaluate the per-attempts to construct a one-dimensional MM ηkformance of our proposed algorithm. The implementation is publicly available†6 .

that ranks transitions of C that are not ranked by
the current construction η = (η1 , . . . , ηk−1 ), while

Our evaluation criteria are twofold:

one isrespecting MCLC. If the algorithm ﬁnds ηk that

how the relaxed non-negativity condition ofranks at least one new transition, then it appends

our LexRSM—SC non-negativity and MCLC—ηk to η and goes to the next iteration; otherwise,

improves the applicability of the algorithm, com-it reports a failure. Once η ranks all transitions,pared to other existing non-negativity conditions.

the algorithm reports a success, returning η as an

To this end, we consider two baseline algorithms.

AST certiﬁcate of C.

(a) The algorithm STR: This is the one proposed

Our algorithm attempts to construct ηk in two

in [2], which synthesizes an ST-LexRSM. We

ways, by adopting either (4) or (5) as the leftward

use the implementation provided by the au-

condition at the dimension k. The attempt withthors [3].

the condition (4) is done in the same manner as ex-(b) The algorithm LWN : This synthesizes an LW-

isting algorithms [2, 15]; we require ηk to rank the

LexRSM. LWN is realized as an instance of

unranked transitions as many as possible. The at-our algorithm with Class(U ) = ∅.

tempt with the condition (5) is slightly nontrivial;

LWN as a proxy of the synthesis algorithm of

the algorithm demands a user-deﬁned parameter

GLexRSM [16, Alg. 2], whose implementation

Class(U ) ⊆ 2U for each U ⊆ ∆ \ {τout }. The pa-

does not seem to exist. We note [16, Alg. 2]

rameter Class(U ) speciﬁes which set of transitions

synthesizes an LW-LexRSM with some addi-

the algorithm should try to rank, given the set oftional conditions; therefore, it is no less restric-

current unranked transitions U ; that is, for eachtive than LWN.

T ∈ Class(U ), the algorithm attempts to ﬁnd ηk

We useAnother criterion is how the choice of Class(U ) af-

that exactly ranks transitions in T .
There are two canonical choices of Class(U ). One†6 https://doi.org/10.5281/zenodo.10937558

fects the performance of our algorithm. To thiswhenever STR does; the same relation is observed

end, we consider two instances of it: (a) Single-

between SMC vs. LWN and EMC vs. SMC. In

ton Multiple Choice (SMC), given by Class(U ) ={{τ } | τ ∈ U }; and (b) Exhaustive Multiple Choice

most cases, STR, LWN, and SMC return an output within a second†7 , while EMC suﬀers from an(EMC), given by Class(U ) = 2U \ ∅. SMC runs in

exponential blowup when it attempts to rank tran-

PTIME, but we do not know if it is complete; EMC

sitions with Condition (5) in Def. 6.1. The full

does not run in PTIME, but is complete.

results are in [36, Appendix E].

We use benchmarks from [2], which consist of

On the ﬁrst evaluation criterion, the advantage of

non-probabilistic programs collected in [4] andthe relaxed non-negativity is evident: SMC/EMC

their probabilistic modiﬁcations.

The modiﬁca-

have unique successes vs. STR on 21 programstion is done in two diﬀerent ways: (a) while loops(21/135 = 15.6% higher success rate) from 16 diﬀer-“while φ do P od” are replaced with probabilis-

ent models; SMC/EMC also have unique successes

tic ones “while φ do (if prob(0.5) then P elsevs. LWN in 14 programs (14/135 = 10.4% higher

skip ﬁ) od”; (b) in addition to (a), variablesuccess rate) from 12 models. This result shows

assignments “x := f (x) + a” are replaced withthat the program structure we observed in Fig. 2“x := f (x) + Unif [a − 1, a + 1]”.

appears in various programs in the real world.

We include

non-probabilistic programs in our benchmark set

On the second criterion, EMC does not have any

because the “problematic program structure” thatunique success compared to SMC. This result sug-

hinders automated LexRSM synthesis already ex-gests that SMC can be the ﬁrst choice as a concrete

ists in non-probabilistic programs (cf. our explana-

instance of our proposed algorithm. Indeed, we sus-tion to Fig. 2). We also tried two PPs from [15, Fig.

pect that SMC is actually complete—verifying its

1], which we call counterexStr1 and counterexStr2.

(in)completeness is a future work. For some pro-We implemented our algorithm upon [2], whichgrams, EMC found a LexRSM with a smaller di-is available at [3]. Similar to [2], our implementa-

mension than SMC.

tion works as follows: (1) it receives a linear PP as

Interestingly, LWN fails to ﬁnd a LexRSM for

an input, and translates it into a pCFG C; (2) itcounterexStr2, despite it being given in [15] as a

generates an invariant for C; (3) via our algorithm,

PP for which a GLexRSM (and hence, an LW non-it synthesizes an SC-LexRSM map with MCLC. In-

negative LexRSM) exists. This happens because

variants are generated by ASPIC [19], and all LP

the implementation in [3] translates the PP into a

problems are solved by CPLEX [25].

pCFG with a diﬀerent shape than the one in [15]Results. In 135 benchmarks from 55 models, STR
succeeds in 98 cases, LWN succeeds in 105 cases
while SMC and EMC succeed in 119 cases (we did
not run STR for counterexStr1 because it involves asampling from an unbounded support distribution,
which is not supported by STR). Table 1 summarizes the cases where we observe diﬀerences in the(for the latter, a GLexRSM indeed exists); the former possesses a similar structure as in Fig. 2 because diﬀerent locations are assigned for the while
loop and if branch.

This demonstrates the ad-vantage of our algorithm from another point ofview, i.e., robustness against diﬀerent translationsof PPs.

feasibility of algorithms. As theoretically anticipated, LWN always succeeds in ﬁnding a LexRSM†7 There was a single example for which more time
was spent, due to a larger size.

Benchmark spec.
Modelcomplexcomplexcomplexcousot9
cousot9loops
nestedLoop
realheapsort
RHS step1
RHS step1
realshellsort

p.l.
√
√

p.a.
√

√
√

√

√
√

√
√

Synthesis result
Baselines
Our algs.
STR
LWN
SMC
EMC
×
×
7
5
×
×
7
5
×
×
3
3
×
3
3
3
×
×
4
4
×
×
4
3
×
×
4
3
×
3
3
3
×
3
3
3
×
3
3
3
×
2
2
2

Benchmark spec.
Modelserpent
speedDis1
speedDis2
spdSimMul
spdSimMulDep
spdSglSgl2
speedpldi3
speedpldi3
counterexStr1
counterexStr2

p.l.
√

p.a.
√

√

√
√

-

Synthesis result
Baselines
Our algs.
STR
LWN
SMC
EMC
×
×
3
3
×
×
4
4
×
×
4
4
×
×
4
4
×
×
4
4
×
×
5
5
×
3
3
3
×
×
4
4
N/A
3
3
3
×
×
4
4

表 1 The list of benchmarks in which a feasibility diﬀerence is observed between baselines andproposed algorithms. Ticks in “p.l.” and “p.a.” indicate the benchmark has a probabilistic loop
and assignment, respectively. Numbers in the result indicate that the algorithm found a LexRSM
with that dimension; the crosses indicate failures; “N/A” means we did not run the experiment.

structure shown in Fig. 2, where the value of our

8 Related WorkLexRSM can be arbitrarily small upon the loop en-

There is a rich body of studies in 1-dimensional

trance (at some dimension; see η2 at ℓ1 in Fig. 2).

RSM [12–14, 17, 20–23, 28–30], while lexicographic

The work [29] extends the applicability of stan-

RSM is relatively new [2, 15]. Our paper gener-

dard RSM on a diﬀerent aspect from LexRSM. The

alizes the latest work [15] on LexRSM as follows:main feature of their RSM is that it can verify AST(a) Soundness of LexRSM as a stochastic process:of the symmetric random walk. While our LexRSM

soundness of ε-ﬁxable LexRSMs (Def. 4.2) general-cannot verify AST of this process, the RSM by [29]izes [15, Thm. 1] in the sense that every GLexRSM

is a 1-dimensional one, which typically struggles

is ε-ﬁxable for any ε > 0 (Thm. 4.4); (b) Sound-on PPs with nested structures. Such a diﬀerence

ness of LexRSM as a function on program states:

can be observed from the experiment result in [31]our result (Thm. 5.4) generalizes [15, Thm.

(compare [31, Table 2] and nested loops, sequen-2]

under the linearity and well-behavedness assump-

tial loops in [31, Table 1]).

tions; (c) Soundness and completeness of LexRSM
synthesis algorithms: our result generalizes the re-

参 考 文 献sults for one of two algorithms in [15] that assumes[ 1 ] : Ultimate Automizer,.
[ 2 ] Agrawal, S., Chatterjee, K., and Novotný, P.:
Lexicographic ranking supermartingales: an efﬁcient approach to termination of probabilistic
programs, Proc. ACM Program. Lang., Vol. 2,
No. POPL(2018), pp. 34:1–34:32.
[ 3 ] Agrawal, S., Chatterjee, K., and Novotný, P.:
Lexicographic ranking supermartingales: an eﬃcient approach to termination of probabilistic programs: Implementation, 2018.
[ 4 ] Alias, C., Darte, A., Feautrier, P., and Gonnord,
L.: Multi-dimensional rankings, program termination, and complexity bounds of ﬂowchart programs,
Static Analysis: 17th International Symposium,
SAS 2010, Perpignan, France, September 14-16,
2010. Proceedings 17, Springer, 2010, pp. 117–133.
[ 5 ] Ash, R. and Doléans-Dade, C.: Probability andMeasure Theory, Harcourt/Academic Press, 2000.

boundedness assumption on assignment distribution [15, Thm. 3].
The work [24] also considers a relaxed nonnegativity of RSMs. Their descent supermartingale,which acts on while loops, requires well-foundedness
only at every entry into the loop body. A majordiﬀerence from our LexRSM is that they only consider 1-dimensional RSMs; therefore, the problem
of relaxing the LW non-negativity does not appear
in their setting. Compared with their RSM, our
LexRSM has an advantage in verifying PPs with a[ 6 ] Barthe, G., Gaboardi, M., Grégoire, B., Hsu, J.,
and Strub, P.-Y.: Proving diﬀerential privacy via
probabilistic couplings, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer
Science, 2016, pp. 749–758.
[ 7 ] Barthe, G., Gaboardi, M., Hsu, J., and Pierce,
B.: Programming language techniques for differential privacy, ACM SIGLOG News, Vol. 3,
No. 1(2016), pp. 34–53.
[ 8 ] Ben-Amram, A. M. and Genaim, S.: Complexity of Bradley-Manna-Sipma Lexicographic Ranking
Functions, Computer Aided Veriﬁcation - 27th International Conference, CAV 2015, San Francisco,
CA, USA, July 18-24, 2015, Proceedings, Part II,
Kroening, D. and Pasareanu, C. S.(eds.), Lecture
Notes in Computer Science, Vol. 9207, Springer,
2015, pp. 304–321.
[ 9 ] Bertsekas, D. P. and Shreve, S. E.: Stochastic
Optimal Control: The Discrete-Time Case, Athena
Scientiﬁc, 2007.
[10] Bradley, A. R., Manna, Z., and Sipma,
H. B.: Linear Ranking with Reachability, Computer Aided Veriﬁcation, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July
6-10, 2005, Proceedings, Etessami, K. and Rajamani, S. K.(eds.), Lecture Notes in Computer Science, Vol. 3576, Springer, 2005, pp. 491–504.
[11] Canal, G., Cashmore, M., Krivić, S., Alenyà,G., Magazzeni, D., and Torras, C.: Probabilisticplanning for robotics with ROSPlan, Towards Autonomous Robotic Systems: 20th Annual Conference, TAROS 2019, London, UK, July 3–5, 2019,
Proceedings, Part I 20, Springer, 2019, pp. 236–
250.
[12] Chakarov, A. and Sankaranarayanan, S.: Probabilistic program analysis with martingales, Computer Aided Veriﬁcation: 25th International Conference, CAV 2013, Saint Petersburg, Russia,
July 13-19, 2013. Proceedings 25, Springer, 2013,
pp. 511–526.
[13] Chatterjee, K., Fu, H., and Goharshady, A. K.:
Termination analysis of probabilistic programs
through Positivstellensatz s, Computer Aided Veriﬁcation: 28th International Conference, CAV 2016,
Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I 28, Springer, 2016, pp. 3–22.
[14] Chatterjee, K., Fu, H., Novotnỳ, P., andHasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems foraﬃne probabilistic programs, Proceedings of the
43rd Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, 2016,
pp. 327–342.
[15] Chatterjee, K., Goharshady, E. K., Novotný,P., Zárevúcky, J., and Zikelic, D.: On Lexicographic Proof Rules for Probabilistic Termination,
Formal Methods - 24th International Symposium,
FM 2021, Virtual Event, November 20-26, 2021,

Proceedings, Huisman, M., Pasareanu, C. S., andZhan, N.(eds.), Lecture Notes in Computer Science,Vol. 13047, Springer, 2021, pp. 619–639.
[16] Chatterjee, K., Goharshady, E. K., Novotný, P.,
Zárevúcky, J., and Zikelic, D.: On Lexicographic
Proof Rules for Probabilistic Termination, CoRR,
Vol. abs/2108.02188(2021).
[17] Chatterjee, K., Novotnỳ, P., and Zikelic, D.:
Stochastic invariants for probabilistic termination,
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages,
2017, pp. 145–160.
[18] Dubhashi, D. P. and Panconesi, A.: Concentration of measure for the analysis of randomized algorithms, Cambridge University Press, 2009.
[19] Feautrier, P. and Gonnord, L.: Accelerated invariant generation for C programs with Aspic andC2fsm, Electronic Notes in Theoretical Computer
Science, Vol. 267, No. 2(2010), pp. 3–13.
[20] Ferrer Fioriti, L. M. and Hermanns, H.: Probabilistic termination: Soundness, completeness, andcompositionality, Proceedings of the 42nd Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015, pp. 489–501.
[21] Fu, H. and Chatterjee, K.: Termination of nondeterministic probabilistic programs, Veriﬁcation,
Model Checking, and Abstract Interpretation: 20th
International Conference, VMCAI 2019, Cascais,
Portugal, January 13–15, 2019, Proceedings 20,
Springer, 2019, pp. 468–490.
[22] Giesl, J., Giesl, P., and Hark, M.: Computing expected runtimes for constant probability programs, Automated Deduction–CADE 27: 27th International Conference on Automated Deduction,
Natal, Brazil, August 27–30, 2019, Proceedings 27,
Springer, 2019, pp. 269–286.
[23] Huang, M., Fu, H., and Chatterjee, K.: New
approaches for almost-sure termination of probabilistic programs, Programming Languages andSystems: 16th Asian Symposium, APLAS 2018,
Wellington, New Zealand, December 2–6, 2018,
Proceedings 16, Springer, 2018, pp. 181–201.
[24] Huang, M., Fu, H., Chatterjee, K., and Goharshady, A. K.: Modular veriﬁcation for almostsure termination of probabilistic programs, Proc.
ACM Program. Lang., Vol. 3, No. OOPSLA(2019),
pp. 129:1–129:29.
[25] IBM: IBM ILOG CPLEX 12.7 User’s Manual(IBM ILOG CPLEX Division, Incline Village, NV),(2017).
[26] Karp, R. M.: An introduction to randomized algorithms, Discrete Applied Mathematics, Vol. 34,
No. 1-3(1991), pp. 165–201.
[27] Lobo-Vesga, E., Russo, A., and Gaboardi, M.: A
programming language for data privacy with accuracy estimations, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 43,
No. 2(2021), pp. 1–42.

[28] McIver, A. and Morgan, C.: A new rule foralmost-certain termination of probabilistic-and demonic programs, arXiv preprint arXiv:1612.01091,(2016).
[29] McIver, A., Morgan, C., Kaminski, B. L., andKatoen, J.-P.: A new proof rule for almost-sure termination, Proceedings of the ACM on Programming
Languages, Vol. 2, No. POPL(2017), pp. 1–28.
[30] Moosbrugger, M., Bartocci, E., Katoen, J.-P.,
and Kovács, L.: Automated termination analysisof polynomial probabilistic programs, Programming
Languages and Systems: 30th European Symposiumon Programming, ESOP 2021, Held as Part of theEuropean Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City,
Luxembourg, March 27–April 1, 2021, Proceedings 30, Springer International Publishing, 2021,
pp. 491–518.
[31] Moosbrugger, M., Bartocci, E., Katoen, J., andKovács, L.: The Probabilistic Termination Tool
Amber, Formal Methods - 24th International Sym-

posium, FM 2021, Virtual Event, November 20-26,
2021, Proceedings, Huisman, M., Pasareanu, C. S.,
and Zhan, N.(eds.), Lecture Notes in Computer Science, Vol. 13047, Springer, 2021, pp. 667–675.
[32] Olmedo, F., Gretz, F., Jansen, N., Kaminski,
B. L., Katoen, J., and McIver, A.: Conditioning in
Probabilistic Programming, ACM Trans. Program.
Lang. Syst., Vol. 40, No. 1(2018), pp. 4:1–4:50.
[33] Parker, D.: Veriﬁcation of probabilistic realtime systems, Proc. 2013 Real-time Systems Summer School (ETR’13), (2013).
[34] Schrijver, A.: Theory of linear and integer programming, John Wiley & Sons, 1998.
[35] Takisaka, T., Oyabu, Y., Urabe, N., and Hasuo, I.: Ranking and Repulsing Supermartingales
for Reachability in Randomized Programs, ACM
Trans. Program. Lang. Syst., Vol. 43, No. 2(2021),
pp. 5:1–5:46.
[36] Takisaka, T., Zhang, L., Wang, C., and Liu, J.:
Lexicographic Ranking Supermartingales with Lazy
Lower Bounds, CoRR, Vol. abs/2304.11363(2024).