Complete Supermartingale Certificates for $\omega$-Regular Properties

Alessandro Abate; Diptarko Roy; Mirco Giacobbe; Sergey Ichtchenko

arxiv: 2605.21134 · v1 · pith:UKYN33HPnew · submitted 2026-05-20 · 💻 cs.LO

Complete Supermartingale Certificates for ω-Regular Properties

Alessandro Abate , Mirco Giacobbe , Sergey Ichtchenko , Diptarko Roy This is my paper

Pith reviewed 2026-05-21 01:40 UTC · model grok-4.3

classification 💻 cs.LO

keywords supermartingalesreactivity propertiesω-regular propertiesMarkov chainsalmost-sure terminationproof rulestemporal logicverification

0 comments

The pith

Reactivity properties on Markov chains decompose into almost-sure termination obligations to absorbing regions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that every reactivity property, which captures ω-regular properties and subsumes linear temporal logic, admits a decomposition into multiple almost-sure termination obligations directed at absorbing regions. It proves that suitable absorbing regions exist for any time-homogeneous Markov chain, even with general state spaces. This reduction converts any complete proof rule for almost-sure termination into a complete rule for reactivity in the almost-sure case and an ε-complete rule in the quantitative case. A sympathetic reader would care because the result lets existing termination certificates, such as supermartingales, now certify full temporal behaviors on countably infinite state spaces.

Core claim

Every reactivity property admits decomposition into multiple obligations of almost-sure termination into absorbing regions, and appropriate absorbing regions always exist on general state spaces. This enables the extension of every complete proof rule for almost-sure termination into a proof rule for reactivity that is complete in the almost-sure case, and complete up to an arbitrarily small ε-approximation in the quantitative case. Applied to supermartingales, the approach produces the first sound and complete supermartingale certificates for almost-sure ω-regular properties and the first sound and ε-complete supermartingale certificates for quantitative ω-regular properties on time-homog

What carries the argument

the decomposition of reactivity properties into almost-sure termination obligations into absorbing regions

If this is right

Every complete proof rule for almost-sure termination extends to a complete proof rule for reactivity.
Supermartingale certificates for almost-sure termination become sound and complete certificates for almost-sure ω-regular properties on countably infinite state spaces.
Quantitative supermartingales become sound and ε-complete certificates for quantitative ω-regular properties.
Standard quantitative safety results extend to quantitative reactivity via the same construction.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same decomposition technique could be tested on non-countable or uncountable state spaces to check whether the existence of absorbing regions remains guaranteed.
One could explore whether the number of required absorbing regions can be bounded for common reactivity patterns such as fairness or persistence.
The approach suggests a route to lift other termination certificates, such as ranking functions, to full ω-regular verification without new machinery.

Load-bearing premise

For any reactivity property on a time-homogeneous Markov chain with general state space, appropriate absorbing regions exist that allow decomposition into almost-sure termination obligations.

What would settle it

A concrete reactivity property together with a time-homogeneous Markov chain on which no absorbing regions exist that permit the required decomposition into almost-sure termination obligations.

read the original abstract

We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneous Markov chains with general state spaces. Reactivity captures $\omega$-regular properties and subsumes linear temporal logic. Our core technical result establishes that every reactivity property admits decomposition into multiple obligations of almost-sure termination into absorbing regions, and that appropriate absorbing regions always exist on general state spaces. This enables the extension of every complete proof rule for almost-sure termination into a proof rule for reactivity that is complete in the almost-sure case, and complete up to an arbitrarily small $\varepsilon$-approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale certificates for almost-sure termination in the special case of countably infinite state spaces, alongside standard results on quantitative safety. As a result, we obtain the first sound and complete supermartingale certificates for almost-sure $\omega$-regular properties and the first sound and $\varepsilon$-complete supermartingale certificates for quantitative $\omega$-regular properties on time-homogeneous Markov chains with countably infinite state spaces.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper lifts complete supermartingale termination certificates to ω-regular properties via a decomposition into absorbing regions, but the claimed generality on arbitrary state spaces rests on an existence result whose measurability details are not obvious from the abstract.

read the letter

The core contribution is a decomposition that turns any reactivity property into a finite set of almost-sure termination obligations to absorbing regions, plus the claim that such regions always exist on general state spaces. This lets the authors reuse recent complete supermartingale rules for termination and obtain the first sound-and-complete certificates for almost-sure ω-regular properties, and sound-plus-ε-complete ones for the quantitative case, on countably infinite chains. That extension is the actual new piece; the rest follows by plugging in prior termination results and standard quantitative safety facts. The write-up is direct about what is being reused and what is being added, which makes the logic easy to follow. The countable-state application looks workable on the surface. The soft spot is the existence claim for absorbing regions. The abstract states that appropriate regions always exist, yet it does not list the measure-theoretic or topological conditions needed to keep the regions measurable, the subprocesses Markov, and the supermartingales well-defined. If the construction relies on arbitrary choice of sets that fail these requirements, the completeness argument does not go through for truly general spaces. The stress-test note correctly flags this gap; without the full derivations it is impossible to see whether the paper supplies the missing regularity assumptions or works only under implicit standard-Borel restrictions. The quantitative ε-completeness part also needs explicit error-bound tracking that is only sketched. This work is aimed at people who already use supermartingales or ranking functions for probabilistic verification of infinite-state systems. A reader who wants a general way to move from termination certificates to full LTL-style properties will find the decomposition technique useful even if the generality claim needs tightening. I would send it to peer review because the claimed advance is substantial and the method is modular enough that referees can check the critical existence step without starting from scratch.

Referee Report

1 major / 2 minor

Summary. The paper introduces a general methodology for sound and complete supermartingale certificates for almost-sure and quantitative acceptance of reactivity (ω-regular) properties on time-homogeneous Markov chains with general state spaces. The core technical result asserts that every reactivity property decomposes into finitely many almost-sure termination obligations into absorbing regions, which are shown to always exist; this allows every complete termination certificate to be lifted to a complete (or ε-complete) certificate for reactivity. The approach is instantiated on recent supermartingale results for countable state spaces, yielding the first such certificates for almost-sure and quantitative ω-regular properties.

Significance. If the central decomposition and existence claims hold, the work provides a reusable bridge from termination analysis to full ω-regular verification, with explicit completeness guarantees. The decomposition into absorbing-region termination obligations is a clean technical contribution that preserves soundness and completeness (up to ε in the quantitative case). The application to countable spaces produces novel certificates that were previously unavailable.

major comments (1)

[Core technical result / existence theorem] Core technical result (abstract and the existence theorem): the claim that 'appropriate absorbing regions always exist on general state spaces' is load-bearing for completeness, yet the construction does not explicitly verify that the chosen regions are measurable with respect to the underlying σ-algebra. Without this, the induced subprocesses may fail to remain Markovian and the almost-sure termination obligations cannot be expressed via supermartingales in the required sense. A concrete counter-example construction or an additional regularity assumption (e.g., standard Borel) is needed to close the gap.

minor comments (2)

[Introduction] The distinction between the fully general state-space theorem and the countable-space instantiation is not always sharp in the introduction; a short paragraph clarifying which results require only countability would improve readability.
[Preliminaries] Notation for reactivity properties and absorbing regions is introduced gradually; a single consolidated table or definition block early in the paper would help readers track the decomposition.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the importance of measurability in the core construction. We address the single major comment below and will incorporate a clarification to strengthen the presentation.

read point-by-point responses

Referee: Core technical result (abstract and the existence theorem): the claim that 'appropriate absorbing regions always exist on general state spaces' is load-bearing for completeness, yet the construction does not explicitly verify that the chosen regions are measurable with respect to the underlying σ-algebra. Without this, the induced subprocesses may fail to remain Markovian and the almost-sure termination obligations cannot be expressed via supermartingales in the required sense. A concrete counter-example construction or an additional regularity assumption (e.g., standard Borel) is needed to close the gap.

Authors: We appreciate the referee drawing attention to this point. The absorbing regions in our decomposition are constructed as the sets of states from which there exists a scheduler ensuring that the ω-regular reactivity condition is satisfied by reaching designated absorbing components. Because the reactivity property is expressed via a measurable acceptance set on path space and the transition kernel is measurable, these regions arise as the greatest fixed points of measurable set-valued operators and are therefore measurable with respect to the given σ-algebra. Consequently the restricted subprocesses remain time-homogeneous Markov chains. We will add an explicit lemma (and its proof) in the revised manuscript that verifies this measurability directly from the construction, thereby confirming that the almost-sure termination obligations are well-defined and that the supermartingale certificates apply without change. No additional regularity assumption such as standard Borel spaces is required, and we do not believe a counter-example exists under the stated hypotheses. revision: yes

Circularity Check

0 steps flagged

No circularity: core existence result and decomposition are independent of the termination certificates being extended

full rationale

The paper's central technical result asserts that every reactivity property decomposes into almost-sure termination obligations into absorbing regions that always exist on general state spaces. This is presented as a new contribution that then enables extension of prior complete termination proof rules (applied to recent supermartingale results for countably infinite spaces). No equation or definition in the provided abstract reduces the existence claim or completeness to a self-referential fit, renaming, or load-bearing self-citation chain; the termination results are treated as independent inputs whose completeness is presupposed rather than redefined. The derivation chain therefore remains self-contained against external benchmarks for termination.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the existence of suitable absorbing regions for every reactivity property and on the prior soundness and completeness of termination certificates; these are domain assumptions rather than new free parameters or invented entities.

axioms (1)

domain assumption Time-homogeneous Markov chains admit absorbing regions for any reactivity property such that the property decomposes into almost-sure termination obligations.
Invoked as the core technical result enabling the extension of termination rules to reactivity.

pith-pipeline@v0.9.0 · 5740 in / 1393 out tokens · 29872 ms · 2026-05-21T01:40:06.817058+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

69 extracted references · 69 canonical work pages

[1]

1968 , publisher=

An introduction to probability theory and its applications, Volume 1 , author=. 1968 , publisher=

work page 1968
[2]

Rick Durrett , title =

work page
[3]

2023 , publisher=

Esparza, Javier and Blondin, Michael , title=. 2023 , publisher=

work page 2023
[4]

Meyn, Sean and Tweedie, Richard L. , year=. Markov Chains and Stochastic Stability , publisher=

work page
[5]

Meyn and R

Sean P. Meyn and R. L. Tweedie , journal =. Stability of Markovian Processes I: Criteria for Discrete-Time Chains , urldate =

work page
[6]

2018 , publisher=

Markov Chains , author=. 2018 , publisher=

work page 2018
[7]

1968 , publisher=

Lecture Notes on Limit Theorems for Markov Chain Transition Probability Functions , author=. 1968 , publisher=

work page 1968
[8]

A User's Guide to Measure Theoretic Probability , publisher=

Pollard, David , year=. A User's Guide to Measure Theoretic Probability , publisher=

work page
[9]

Amir Pnueli , title =

work page
[10]

Rabinizer 4: From

Jan Kret. Rabinizer 4: From

work page
[11]

Principles of model checking , publisher =

Christel Baier and Joost. Principles of model checking , publisher =

work page
[12]

From Spot 2.0 to Spot 2.10: What's New? , booktitle =

Alexandre Duret. From Spot 2.0 to Spot 2.10: What's New? , booktitle =

work page
[13]

Automata, Logics, and Infinite Games:

work page
[14]

Rupak Majumdar and V. R. Sathiyanarayana , title =. Proc

work page
[15]

A new proof rule for almost-sure termination , journal =

Annabelle McIver and Carroll Morgan and Benjamin Lucien Kaminski and Joost. A new proof rule for almost-sure termination , journal =

work page
[16]

Alessandro Abate and Mirco Giacobbe and Diptarko Roy , title =

work page
[17]

Henzinger and Kaushik Mallik and Pouya Sadeghi and

Thomas A. Henzinger and Kaushik Mallik and Pouya Sadeghi and. Supermartingale Certificates for Quantitative Omega-Regular Verification and Control , booktitle =

work page
[18]

Shmuel Safra , title =

work page
[19]

Zohar Manna and Amir Pnueli , title =

work page
[20]

, title =

Doblin, W. , title =. Annales scientifiques de l'\'Ecole Normale Sup\'erieure , pages =. 1940 , publisher =. doi:10.24033/asens.883 , zbl =

work page doi:10.24033/asens.883 1940
[21]

Necessary and Sufficient Conditions for Recurrence and Transience of Markov Chains, in Terms of Inequalities , urldate =

Jean-François Mertens and Ester Samuel-Cahn and Shmuel Zamir , journal =. Necessary and Sufficient Conditions for Recurrence and Transience of Markov Chains, in Terms of Inequalities , urldate =

work page
[22]

CoRR , volume =

Satoshi Kura and Hiroshi Unno , title =. CoRR , volume =

work page
[23]

A. G. Pakes , journal =. Some Conditions for Ergodicity and Recurrence of Markov Chains , urldate =

work page
[24]

Stefan Kiefer and Richard Mayr and Mahsa Shirmohammadi and Patrick Totzke , title =

work page
[25]

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains , booktitle =

Hannah Mertens and Joost. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains , booktitle =

work page
[26]

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving , journal =

Peixin Wang and Tengshun Yang and Hongfei Fu and Guanyan Li and C. Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving , journal =

work page
[27]

Henzinger and Mathias Lechner and

Matin Ansaripour and Krishnendu Chatterjee and Thomas A. Henzinger and Mathias Lechner and. Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems , booktitle =

work page
[28]

F. G. Foster , title =. The Annals of Mathematical Statistics , number =. 1953 , doi =

work page 1953
[29]

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning , journal =

Kevin Batz and Benjamin Lucien Kaminski and Joost. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning , journal =

work page
[30]

Deductive Proofs of Almost Sure Persistence and Recurrence Properties , booktitle =

Aleksandar Chakarov and Yuen. Deductive Proofs of Almost Sure Persistence and Recurrence Properties , booktitle =

work page
[31]

Toru Takisaka and Yuichiro Oyabu and Natsuki Urabe and Ichiro Hasuo , title =

work page
[32]

Krishnendu Chatterjee and Hongfei Fu and Amir Kafshdar Goharshady , title =

work page
[33]

Aleksandar Chakarov and Sriram Sankaranarayanan , title =

work page
[34]

Pappas , title =

Stephen Prajna and Ali Jadbabaie and George J. Pappas , title =

work page
[35]

Stochastic invariants for probabilistic termination , booktitle =

Krishnendu Chatterjee and Petr Novotn. Stochastic invariants for probabilistic termination , booktitle =

work page
[36]

Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees , booktitle =

work page
[37]

1967 , publisher=

Stochastic Stability and Control , author=. 1967 , publisher=

work page 1967
[38]

This is the moment for probabilistic loops , journal =

Marcel Moosbrugger and Miroslav Stankovic and Ezio Bartocci and Laura Kov. This is the moment for probabilistic loops , journal =

work page
[39]

2019 , publisher=

Measure, Integration & Real Analysis , author=. 2019 , publisher=

work page 2019
[40]

The Probabilistic Termination Tool Amber

Moosbrugger, Marcel and Bartocci, Ezio and Katoen, Joost-Pieter and Kov \'a cs, Laura. The Probabilistic Termination Tool Amber. Formal Methods. 2021

work page 2021
[41]

Automated Termination Analysis of Polynomial Probabilistic Programs , booktitle =

Marcel Moosbrugger and Ezio Bartocci and Joost. Automated Termination Analysis of Polynomial Probabilistic Programs , booktitle =

work page
[42]

ThanhVu Nguyen and Deepak Kapur and Westley Weimer and Stephanie Forrest , title =

work page
[43]

Sipma and Zohar Manna , title =

Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna , title =

work page
[44]

Ernst and Jeff H

Michael D. Ernst and Jeff H. Perkins and Philip J. Guo and Stephen McCamant and Carlos Pacheco and Matthew S. Tschantz and Chen Xiao , title =. Sci. Comput. Program. , volume =

work page
[45]

Practical Methods for Proving Program Termination , booktitle =

Michael Col. Practical Methods for Proving Program Termination , booktitle =

work page
[46]

Linear Invariant Generation Using Non-linear Constraint Solving , booktitle =

Michael Col. Linear Invariant Generation Using Non-linear Constraint Solving , booktitle =

work page
[47]

Parrilo , title =

Stephen Prajna and Antonis Papachristodoulou and Pablo A. Parrilo , title =

work page
[48]

Antonis Papachristodoulou and Stephen Prajna , title =

work page
[49]

Sutton and Andrew G

Richard S. Sutton and Andrew G. Barto , title =

work page
[50]

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs , journal =

Krishnendu Chatterjee and Hongfei Fu and Petr Novotn. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs , journal =

work page
[51]

Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs , journal =

Sheshansh Agrawal and Krishnendu Chatterjee and Petr Novotn. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs , journal =

work page
[52]

Synthesis of Linear Ranking Functions , booktitle =

Michael Col. Synthesis of Linear Ranking Functions , booktitle =

work page
[53]

Motwani and Maximilian Seeliger and

Krishnendu Chatterjee and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and Harshit J. Motwani and Maximilian Seeliger and. Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization , booktitle =

work page
[54]

Ali Asadi and Krishnendu Chatterjee and Hongfei Fu and Amir Kafshdar Goharshady and Mohammad Mahdavi , title =

work page
[55]

Krishnendu Chatterjee and Amir Kafshdar Goharshady and Tobias Meggendorfer and Dorde Zikelic , title =

work page
[56]

Sound and Complete Witnesses for Template-Based Verification of

Krishnendu Chatterjee and Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and. Sound and Complete Witnesses for Template-Based Verification of

work page
[57]

2013 , journal =

Sankaranarayanan, Sriram and Chen, Xin and. 2013 , journal =

work page 2013
[58]

She, Zhikun and Li, Haoyang and Xue, Bai and Zheng, Zhiming and Xia, Bican , year =

work page
[59]

Representing polynomials by positive linear functions on compact convex polyhedra , volume =

Handelman, David , year =. Representing polynomials by positive linear functions on compact convex polyhedra , volume =

work page
[60]

Equivalence and Similarity Refutation for Probabilistic Programs , journal =

Krishnendu Chatterjee and Ehsan Kafshdar Goharshady and Petr Novotn. Equivalence and Similarity Refutation for Probabilistic Programs , journal =

work page
[61]

Differential cost analysis with simultaneous potentials and anti-potentials , booktitle =

work page
[62]

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants , booktitle =

Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants , booktitle =

work page
[63]

Stability Verification in Stochastic Control Systems via Neural Network Supermartingales , booktitle =

Mathias Lechner and. Stability Verification in Stochastic Control Systems via Neural Network Supermartingales , booktitle =

work page
[64]

2025 , booktitle =

Grigory Neustroev and Mirco Giacobbe and Anna Lukina , title =. 2025 , booktitle =

work page 2025
[65]

Henzinger and Mathias Lechner and

Krishnendu Chatterjee and Thomas A. Henzinger and Mathias Lechner and. A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems , booktitle =

work page
[66]

Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees , booktitle =

work page
[67]

Daniele Ahmed and Andrea Peruffo and Alessandro Abate , title =

work page
[68]

NeurIPS , year =

Mirco Giacobbe and Daniel Kroening and Abhinandan Pal and Michael Tautschnig , title =. NeurIPS , year =

work page
[69]

Alessandro Abate and Alec Edwards and Mirco Giacobbe and Hashan Punchihewa and Diptarko Roy , title =. Log. Methods Comput. Sci. , volume =

work page

[1] [1]

1968 , publisher=

An introduction to probability theory and its applications, Volume 1 , author=. 1968 , publisher=

work page 1968

[2] [2]

Rick Durrett , title =

work page

[3] [3]

2023 , publisher=

Esparza, Javier and Blondin, Michael , title=. 2023 , publisher=

work page 2023

[4] [4]

Meyn, Sean and Tweedie, Richard L. , year=. Markov Chains and Stochastic Stability , publisher=

work page

[5] [5]

Meyn and R

Sean P. Meyn and R. L. Tweedie , journal =. Stability of Markovian Processes I: Criteria for Discrete-Time Chains , urldate =

work page

[6] [6]

2018 , publisher=

Markov Chains , author=. 2018 , publisher=

work page 2018

[7] [7]

1968 , publisher=

Lecture Notes on Limit Theorems for Markov Chain Transition Probability Functions , author=. 1968 , publisher=

work page 1968

[8] [8]

A User's Guide to Measure Theoretic Probability , publisher=

Pollard, David , year=. A User's Guide to Measure Theoretic Probability , publisher=

work page

[9] [9]

Amir Pnueli , title =

work page

[10] [10]

Rabinizer 4: From

Jan Kret. Rabinizer 4: From

work page

[11] [11]

Principles of model checking , publisher =

Christel Baier and Joost. Principles of model checking , publisher =

work page

[12] [12]

From Spot 2.0 to Spot 2.10: What's New? , booktitle =

Alexandre Duret. From Spot 2.0 to Spot 2.10: What's New? , booktitle =

work page

[13] [13]

Automata, Logics, and Infinite Games:

work page

[14] [14]

Rupak Majumdar and V. R. Sathiyanarayana , title =. Proc

work page

[15] [15]

A new proof rule for almost-sure termination , journal =

Annabelle McIver and Carroll Morgan and Benjamin Lucien Kaminski and Joost. A new proof rule for almost-sure termination , journal =

work page

[16] [16]

Alessandro Abate and Mirco Giacobbe and Diptarko Roy , title =

work page

[17] [17]

Henzinger and Kaushik Mallik and Pouya Sadeghi and

Thomas A. Henzinger and Kaushik Mallik and Pouya Sadeghi and. Supermartingale Certificates for Quantitative Omega-Regular Verification and Control , booktitle =

work page

[18] [18]

Shmuel Safra , title =

work page

[19] [19]

Zohar Manna and Amir Pnueli , title =

work page

[20] [20]

, title =

Doblin, W. , title =. Annales scientifiques de l'\'Ecole Normale Sup\'erieure , pages =. 1940 , publisher =. doi:10.24033/asens.883 , zbl =

work page doi:10.24033/asens.883 1940

[21] [21]

Necessary and Sufficient Conditions for Recurrence and Transience of Markov Chains, in Terms of Inequalities , urldate =

Jean-François Mertens and Ester Samuel-Cahn and Shmuel Zamir , journal =. Necessary and Sufficient Conditions for Recurrence and Transience of Markov Chains, in Terms of Inequalities , urldate =

work page

[22] [22]

CoRR , volume =

Satoshi Kura and Hiroshi Unno , title =. CoRR , volume =

work page

[23] [23]

A. G. Pakes , journal =. Some Conditions for Ergodicity and Recurrence of Markov Chains , urldate =

work page

[24] [24]

Stefan Kiefer and Richard Mayr and Mahsa Shirmohammadi and Patrick Totzke , title =

work page

[25] [25]

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains , booktitle =

Hannah Mertens and Joost. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains , booktitle =

work page

[26] [26]

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving , journal =

Peixin Wang and Tengshun Yang and Hongfei Fu and Guanyan Li and C. Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving , journal =

work page

[27] [27]

Henzinger and Mathias Lechner and

Matin Ansaripour and Krishnendu Chatterjee and Thomas A. Henzinger and Mathias Lechner and. Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems , booktitle =

work page

[28] [28]

F. G. Foster , title =. The Annals of Mathematical Statistics , number =. 1953 , doi =

work page 1953

[29] [29]

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning , journal =

Kevin Batz and Benjamin Lucien Kaminski and Joost. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning , journal =

work page

[30] [30]

Deductive Proofs of Almost Sure Persistence and Recurrence Properties , booktitle =

Aleksandar Chakarov and Yuen. Deductive Proofs of Almost Sure Persistence and Recurrence Properties , booktitle =

work page

[31] [31]

Toru Takisaka and Yuichiro Oyabu and Natsuki Urabe and Ichiro Hasuo , title =

work page

[32] [32]

Krishnendu Chatterjee and Hongfei Fu and Amir Kafshdar Goharshady , title =

work page

[33] [33]

Aleksandar Chakarov and Sriram Sankaranarayanan , title =

work page

[34] [34]

Pappas , title =

Stephen Prajna and Ali Jadbabaie and George J. Pappas , title =

work page

[35] [35]

Stochastic invariants for probabilistic termination , booktitle =

Krishnendu Chatterjee and Petr Novotn. Stochastic invariants for probabilistic termination , booktitle =

work page

[36] [36]

Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees , booktitle =

work page

[37] [37]

1967 , publisher=

Stochastic Stability and Control , author=. 1967 , publisher=

work page 1967

[38] [38]

This is the moment for probabilistic loops , journal =

Marcel Moosbrugger and Miroslav Stankovic and Ezio Bartocci and Laura Kov. This is the moment for probabilistic loops , journal =

work page

[39] [39]

2019 , publisher=

Measure, Integration & Real Analysis , author=. 2019 , publisher=

work page 2019

[40] [40]

The Probabilistic Termination Tool Amber

Moosbrugger, Marcel and Bartocci, Ezio and Katoen, Joost-Pieter and Kov \'a cs, Laura. The Probabilistic Termination Tool Amber. Formal Methods. 2021

work page 2021

[41] [41]

Automated Termination Analysis of Polynomial Probabilistic Programs , booktitle =

Marcel Moosbrugger and Ezio Bartocci and Joost. Automated Termination Analysis of Polynomial Probabilistic Programs , booktitle =

work page

[42] [42]

ThanhVu Nguyen and Deepak Kapur and Westley Weimer and Stephanie Forrest , title =

work page

[43] [43]

Sipma and Zohar Manna , title =

Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna , title =

work page

[44] [44]

Ernst and Jeff H

Michael D. Ernst and Jeff H. Perkins and Philip J. Guo and Stephen McCamant and Carlos Pacheco and Matthew S. Tschantz and Chen Xiao , title =. Sci. Comput. Program. , volume =

work page

[45] [45]

Practical Methods for Proving Program Termination , booktitle =

Michael Col. Practical Methods for Proving Program Termination , booktitle =

work page

[46] [46]

Linear Invariant Generation Using Non-linear Constraint Solving , booktitle =

Michael Col. Linear Invariant Generation Using Non-linear Constraint Solving , booktitle =

work page

[47] [47]

Parrilo , title =

Stephen Prajna and Antonis Papachristodoulou and Pablo A. Parrilo , title =

work page

[48] [48]

Antonis Papachristodoulou and Stephen Prajna , title =

work page

[49] [49]

Sutton and Andrew G

Richard S. Sutton and Andrew G. Barto , title =

work page

[50] [50]

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs , journal =

Krishnendu Chatterjee and Hongfei Fu and Petr Novotn. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs , journal =

work page

[51] [51]

Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs , journal =

Sheshansh Agrawal and Krishnendu Chatterjee and Petr Novotn. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs , journal =

work page

[52] [52]

Synthesis of Linear Ranking Functions , booktitle =

Michael Col. Synthesis of Linear Ranking Functions , booktitle =

work page

[53] [53]

Motwani and Maximilian Seeliger and

Krishnendu Chatterjee and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and Harshit J. Motwani and Maximilian Seeliger and. Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization , booktitle =

work page

[54] [54]

Ali Asadi and Krishnendu Chatterjee and Hongfei Fu and Amir Kafshdar Goharshady and Mohammad Mahdavi , title =

work page

[55] [55]

Krishnendu Chatterjee and Amir Kafshdar Goharshady and Tobias Meggendorfer and Dorde Zikelic , title =

work page

[56] [56]

Sound and Complete Witnesses for Template-Based Verification of

Krishnendu Chatterjee and Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and. Sound and Complete Witnesses for Template-Based Verification of

work page

[57] [57]

2013 , journal =

Sankaranarayanan, Sriram and Chen, Xin and. 2013 , journal =

work page 2013

[58] [58]

She, Zhikun and Li, Haoyang and Xue, Bai and Zheng, Zhiming and Xia, Bican , year =

work page

[59] [59]

Representing polynomials by positive linear functions on compact convex polyhedra , volume =

Handelman, David , year =. Representing polynomials by positive linear functions on compact convex polyhedra , volume =

work page

[60] [60]

Equivalence and Similarity Refutation for Probabilistic Programs , journal =

Krishnendu Chatterjee and Ehsan Kafshdar Goharshady and Petr Novotn. Equivalence and Similarity Refutation for Probabilistic Programs , journal =

work page

[61] [61]

Differential cost analysis with simultaneous potentials and anti-potentials , booktitle =

work page

[62] [62]

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants , booktitle =

Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants , booktitle =

work page

[63] [63]

Stability Verification in Stochastic Control Systems via Neural Network Supermartingales , booktitle =

Mathias Lechner and. Stability Verification in Stochastic Control Systems via Neural Network Supermartingales , booktitle =

work page

[64] [64]

2025 , booktitle =

Grigory Neustroev and Mirco Giacobbe and Anna Lukina , title =. 2025 , booktitle =

work page 2025

[65] [65]

Henzinger and Mathias Lechner and

Krishnendu Chatterjee and Thomas A. Henzinger and Mathias Lechner and. A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems , booktitle =

work page

[66] [66]

Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees , booktitle =

work page

[67] [67]

Daniele Ahmed and Andrea Peruffo and Alessandro Abate , title =

work page

[68] [68]

NeurIPS , year =

Mirco Giacobbe and Daniel Kroening and Abhinandan Pal and Michael Tautschnig , title =. NeurIPS , year =

work page

[69] [69]

Alessandro Abate and Alec Edwards and Mirco Giacobbe and Hashan Punchihewa and Diptarko Roy , title =. Log. Methods Comput. Sci. , volume =

work page