Pith. sign in

REVIEW 3 major objections 6 minor 35 references

Omega-regular Verification and Control for Distributional Specifications in MDPs

T0 review · 3 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper introduces distributional certificates, a sound and complete proof rule for verifying and synthesizing strategies in Markov decision processes against omega-regular specifications on the sequence of probability distributions…

desk verdict A genuinely new framework for distributional omega-regular verification, but Theorem 9 is currently unsound as stated because the Büchi ranking conditions are vacuous when the NBA has missing transitions; the fix is straightforward. read the letter →

arxiv 2507.04286 v1 pith:7YQP6SIQ submitted 2025-07-06 cs.LO

S. Akshay (1) , Ouldouz Neysari (2 , 3) , {DJ}or{j̣e Žikelić (2) ((1) Dept of CSE , Indian Institute of Technology Bombay , (2) Singapore Management University , (3) University of Tehran) This is my paper
classification cs.LO MSC 68Q6068Q4503B70
keywords Markovdecisionprocessesdistributionalobjectivesomega-regularspecificationscertificatesverificationstrategysynthesistemplate-baseddistributiontransformers
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Markov decision processes can be viewed as transformers of probability distributions: an MDP under a strategy generates an infinite sequence of distributions over states. This paper tackles the problem of verifying and synthesizing strategies for properties of this sequence that are omega-regular, a far more expressive class than the reachability, safety, and reach-avoidance objectives handled by previous automated methods. The central claim is that a sound and complete proof rule exists: an MDP under a distributionally memoryless strategy satisfies a distributional omega-regular specification if and only if there is a distributional certificate, built from a Büchi ranking function and an invariant over a product transition system that tracks the automaton run alongside the distribution sequence. Based on this, the authors give the first fully automated template-based algorithms for distributional omega-regular verification and control, with soundness and relative completeness, running in PSPACE, and demonstrate them on benchmarks. If correct, this significantly extends the class of distributional objectives amenable to automated reasoning.

What carries the argument

The central objects are distributional certificates (C, I), defined over a product distributional transition system (PDTS) that synchronizes the MDP's distribution transformer Mπ with the Büchi automaton of the specification: each transition is guarded by the atomic propositions satisfied by the current distribution and applies the single-step distribution update. A certificate pairs a distributional Büchi ranking function C: Q × ∆(S) → R with a distributional invariant I that over-approximates reachable PDTS states; the ranking function decreases by at least 1 at non-accepting automaton states while staying non-negative and inside I, forcing infinitely many visits to accepting states along some path. For automation, the paper restricts to affine certificates and affine distributionally memoryless strategies and translates the certificate conditions, via Handelman's theorem (or Farkas' lemma in the memoryless-strategy case), into an existentially quantified system of polynomial constraints over real numbers, solved by an SMT backend.

What would settle it

Run the prototype on a small MDP and specification, then take the synthesized affine certificate and strategy and directly evaluate the conditions of Definition 8 over a dense grid of distributions in the simplex: a single point where an antecedent holds but the consequent fails for the returned certificate would refute soundness of the algorithm. A targeted version is to check whether the constraints after the Handelman translation are equisatisfiable with the original quantified constraints on the running example of Figures 1 and 2, where a mismatch would reveal the reduction's unsoundness or incompleteness.

Watch

Extended reading notes

Core claim

The paper's main theoretical result, Theorem 9, states that an MDP with a set of initial distributions Init under a distributionally memoryless strategy π satisfies a distributional ω-regular specification φ if and only if there exists a distributional certificate for M, Init, π, and φ. A distributional certificate consists of a distributional Büchi ranking function C, which is non-negative at initial states, stays non-negative along a chosen successor path, and decreases by at least 1 at every non-accepting NBA state until an accepting state is reached, together with a distributional invariant I that over-approximates the reachable states of the product distributional transition system that synchronizes the distribution sequence with a run of the automaton. This soundness-and-completeness result is the foundation for template-based algorithms that synthesize affine certificates and affine distributionally memoryless strategies by reducing the verification and synthesis problems to satisfiability in the existential theory of the reals, giving PSPACE procedures with relative completeness guarantees.

Load-bearing premise

The synthesis algorithms' soundness rests on Handelman's theorem applying to the polynomial constraints obtained after clearing denominators in the guard and strategy expressions, and the paper does not verify the required compactness and positivity hypotheses for the particular guard polytopes and the disjunction over NBA successors; if this reduction fails, the produced certificate need not actually prove satisfaction.

Editorial extensions

If this is right

  • For any satisfying instance, a distributional certificate exists, so certificate search is a complete proof method for distributional ω-regular satisfaction; restricting to affine templates gives relative completeness for the automated procedure.
  • The algorithms run in PSPACE in the size of the MDP, the NBA, the strategy description, and the invariant size parameter, making them the first automated methods for this specification class.
  • The approach covers both the universal setting, where the specification must hold from every initial distribution in Init, and the existential setting, where it must hold from at least one initial distribution.
  • The prototype handles benchmarks from gridworld robot swarms, PageRank Markov chains, pharmacokinetics, and prior distributional safety tasks, solving verification and synthesis for ω-regular specifications at runtimes comparable to earlier methods for simpler reachability and safety specifications.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The certificate rule is not tied to the template-based solver: any method that produces functions satisfying its conditions would also certify satisfaction, so the proof rule could serve as a verification layer for independently generated strategies.
  • Because the ranking function decreases by at least 1 at every non-accepting state, the certificate implicitly bounds the number of consecutive non-accepting visits, an invariant from which quantitative statements about how often acceptance occurs could be derived.
  • The completeness proof constructs a certificate from the existence of accepting paths, suggesting that every satisfying strategy admits some certificate; the practical question is whether affine templates suffice, so a natural stress test is to search for an MDP whose only certificates are non-affine.
  • The paper restricts attention to distributionally memoryless strategies, whose sufficiency is known for reachability and safety but is not established for ω-regular specifications; if sufficiency fails, the certificate rule would characterize only a subclass of satisfying strategies.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper studies MDPs viewed as distribution transformers and addresses strategy verification and synthesis for distributional ω-regular specifications. It introduces product distributional transition systems (PDTS) and a notion of distributional certificates (C,I) comprising a Büchi ranking function and an invariant over the PDTS. Theorem 9 claims that the certificate constitutes a sound and complete proof rule for satisfaction of a distributional ω-regular specification under a distributionally memoryless strategy. Building on this, the authors present template-based algorithms that synthesize affine certificates and affine distributionally memoryless strategies by encoding the certificate conditions as quantified real arithmetic constraints, then eliminating quantifiers via Handelman’s theorem or Farkas’ lemma. The resulting existential polynomial constraints are solved with an SMT solver, giving a PSPACE procedure with soundness and relative-completeness guarantees. The paper is evaluated on a prototype implementation over a range of benchmarks from the literature.

Significance. If the technical issues are fixed, this would be the first automated method for distributional ω-regular specifications, a substantial generalization of earlier distributional reachability, safety, and reach-avoidance methods. The certificate notion itself is a novel and potentially useful proof rule, and the completeness direction of Theorem 9 is a standard and plausible construction. The paper also contributes an implementation and experimental evaluation, which is valuable. However, the main theorem as stated is invalid due to a vacuity bug in the certificate definition, and the algorithm’s constraint reduction has an unresolved sign issue; the significance is therefore conditional on these corrections.

major comments (3)
  1. [Definition 8, Theorem 9] The Büchi ranking conditions (1) and (2) are vacuously satisfied when δ(q,σ)=∅, because the antecedent contains the disjunction over q′∈δ(q,σ) and an empty disjunction makes the implication true. This makes the soundness direction of Theorem 9 false. Concretely, consider a one-state Markov chain with P(s,s)=1, Init={δ_s}, AP={p: µ(s)≥0}, and an NBA with Q=F={q0} and δ(q0,{p})=∅. Then C(q0,µ)=0 and I=Q×Δ(S) satisfy the Initial condition and both Büchi conditions vacuously, yet the induced word {p}^ω is rejected by the NBA and the PDTS has no infinite path. The definition and theorem need an additional hypothesis: either a progress condition requiring δ(q,σ)≠∅ for the unique letter σ satisfied at every (q,µ)∈I with C(q,µ)≥0, or a requirement that the NBA be made complete by adding a rejecting sink. Please amend Definition 8 and re-prove Theorem 9 accordingly.
  2. [Definition 8, Eqs. (1)–(2); Section 5, Step 3] The formulas in the Büchi ranking condition are ill-scoped: q′ appears free in the consequent while being bound only inside the disjunction in the antecedent. The intended condition, as used in the soundness proof where the authors “repeatedly select successor states”, is an existential choice of successor: for every µ satisfying the guard, C(q,µ)≥0, and membership in I, there should exist some q′∈δ(q,σ) such that the consequent holds. As written, the condition is not a well-formed formula and, depending on interpretation, imposes either too strong or vacuous requirements. The same issue is repeated in the constraint encoding in Step 3 of Section 5. Please rewrite the condition as ∀µ. (A(µ) ⇒ ∃q′∈δ(q,σ). B(q′,µ)) and update the algorithm constraints to match the corrected certificate definition.
  3. [Section 5, Step 4] The reduction to polynomial constraints via multiplication by denominators is not sound as stated. In equation (5), π(s,a)(µ) is a quotient of affine expressions. Multiplying both sides of an inequality by the denominator preserves equivalence only if the denominator is nonzero and the inequality direction is handled according to the denominator’s sign. The paper neither adds constraints forcing the denominators to be positive nor proves that any solution with a negative denominator can be sign-normalized without changing the certificate conditions. Consequently, the claimed soundness of the algorithm (Theorem 12) is not established: a solution to the polynomial constraints may fail to satisfy the original rational certificate conditions. Please add explicit positivity constraints on the denominators (or provide a rigorous sign-normalization argument), and verify that Handelman’s theorem is applicable to the resulting polynomial constraints, including the required compactness and nonnegativity hypotheses.
minor comments (6)
  1. [Theorem 9, completeness proof] There are typos in the completeness argument: “Next(q,µ) = daccept(q,µ)− 1 ≥ 0” should read “C(Next(q,µ)) = daccept(q,µ)−1” or “daccept(Next(q,µ)) = daccept(q,µ)−1”, and “id q∈F” should be “if q∈F”.
  2. [Example 10] The invariant for q1 is written as “{(q1,µ)| µ(A)+0.25·µ(B)}” without a comparison operator; please provide the intended inequality.
  3. [Section 5, Step 3] In the two Büchi ranking constraint formulas, “Ik(Mπ(q′,µ))” should be “Ik(q′,Mπ(µ))” for consistency with the certificate definition; similarly, the displayed definition of Mπ(µ) should use “∑_{s∈S,a∈Act(s)}” rather than the current notation.
  4. [Definition 5] “V× = {µ1,...,µ|S|} is a finite state of real-valued variables” should be “a finite set of real-valued variables”.
  5. [Table 1] Several rows (e.g., the CAV23 [4] synthesis entries) appear to have misaligned columns, making the distinction between “SMT time” and “Total time” ambiguous; please reformat the table.
  6. [Throughout] There are minor typos: “startegy” in Theorem 12 and “Pharamakocinetics” in the benchmark description; please correct them.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity — the distributional certificate is a proof rule checked against externally provided Büchi automata; self-citations are contextual and not load-bearing.

full rationale

The paper's central theoretical claim (Theorem 9) is a sound-and-complete proof rule: a distributional certificate (C,I) is defined locally on the product distributional transition system, and the proof shows both directions. The completeness direction constructs C as distance to the next accepting state along a chosen accepting path; this is a normal completeness witness construction, not a fitted prediction. No parameter is fitted to a subset of data and then 'predicted' on a related quantity; the affine templates are searched symbolically to satisfy proof obligations. Self-citations [4,5] are used only to motivate the restriction to distributionally memoryless strategies and to position the work against prior automated methods; the paper explicitly notes the sufficiency result need not hold for ω-regular specifications, so the restriction is an assumption, not a derived consequence. The Büchi ranking function idea is attributed to [17] and extended; this is adaptation of a known technique, not smuggling an ansatz. The use of Handelman's theorem and Farkas' lemma is an external algebraic translation; any concern about unverified hypotheses is a soundness/completeness gap in the reduction, not a circularity. The skeptical objection about vacuous satisfaction when δ(q,σ)=∅ is a genuine soundness bug in Theorem 9 as stated, but it does not make the derivation circular: it shows the certificate conditions are too weak, not that satisfaction or certificates are defined in terms of each other.

Assumptions & free parameters 1 free parameters · 5 assumptions · 2 invented entities

The central claim is supported by external theorems and prior work rather than fitted constants; the only hand-set parameter is the invariant template size NI. The affine template restriction is the main domain assumption that bounds the scope.

free parameters (1)
  • invariant size NI = 1 in all reported experiments
    Number of affine inequalities in the invariant template; a user-chosen search parameter, not derived from data. Relative completeness only guarantees existence of some NI.
assumptions (5)
  • standard math Soundness of Handelman's theorem and Farkas' lemma for translating ∀µ constraints into ∃-polynomial constraints
    Used in Section 5, Step 4, to reduce certificate conditions to existential real arithmetic; the paper cites [7] for the reduction and [25] for Farkas' lemma.
  • domain assumption The NBA alphabet consists of affine predicates over the distribution simplex, and the PDTS guards are affine
    Certificates and strategies are restricted to affine forms; nonlinear atomic propositions or certificates fall outside the method (Section 5).
  • domain assumption Distributionally memoryless strategies are an adequate class for the considered specifications
    The paper restricts to this class, noting sufficiency is known only for reachability, safety, and reach-avoidance, not for omega-regular (Section 3).
  • domain assumption Finite MDP with finite action set and rational or evaluable transition probabilities
    The algorithms and prototype require finite state and action spaces and a concrete transition function (Sections 2 and 6).
  • standard math Decision procedure for existential theory of the reals is in PSPACE and implemented by SMT solvers
    The complexity claim and practical solving rely on this (Section 5).
invented entities (2)
  • Distributional certificate (C,I): Büchi ranking function plus invariant over the product distributional transition system
    purpose: Provide a sound and complete proof rule for distributional omega-regular satisfaction under a distributionally memoryless strategy
    It is an internal proof-theoretic construct whose correctness is established by Theorem 9, not by a falsifiable external prediction.
  • Product distributional transition system (PDTS)
    purpose: Synchronize the sequence of distributions generated by the MDP with a run in the NBA
    A bookkeeping automaton construction; its adequacy follows from Proposition 7 and the definitions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Omega-regular Verification and Control for Distributional Specifications in MDPs." pith.science (2026). https://pith.science/paper/7YQP6SIQ

@misc{pith2026250704286,
  author       = {Pith},
  title        = {Pith review of: Omega-regular Verification and Control for Distributional Specifications in MDPs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7YQP6SIQ}},
  note         = {Machine review of arXiv:2507.04286}
}
read the original abstract

A classical approach to studying Markov decision processes (MDPs) is to view them as state transformers. However, MDPs can also be viewed as distribution transformers, where an MDP under a strategy generates a sequence of probability distributions over MDP states. This view arises in several applications, even as the probabilistic model checking problem becomes much harder compared to the classical state transformer counterpart. It is known that even distributional reachability and safety problems become computationally intractable (Skolem- and positivity-hard). To address this challenge, recent works focused on sound but possibly incomplete methods for verification and control of MDPs under the distributional view. However, existing automated methods are applicable only to distributional reachability, safety and reach-avoidance specifications. In this work, we present the first automated method for verification and control of MDPs with respect to distributional omega-regular specifications. To achieve this, we propose a novel notion of distributional certificates, which are sound and complete proof rules for proving that an MDP under a distributionally memoryless strategy satisfies some distributional omega-regular specification. We then use our distributional certificates to design the first fully automated algorithms for verification and control of MDPs with respect to distributional omega-regular specifications. Our algorithms follow a template-based synthesis approach and provide soundness and relative completeness guarantees, while running in PSPACE. Our prototype implementation demonstrates practical applicability of our algorithms to challenging examples collected from the literature.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

35 extracted references · 19 canonical work pages

  1. [1]

    Stochastic omega-regular verification and control with supermartingales

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Stochastic omega-regular verification and control with supermartingales. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III , volume 14683 of Lecture Notes in Computer Science , ...

    doi:10.1007/978-3-031-65633-0 2024

  2. [2]

    Akshay, Blaise Genest, and P

    Manindra Agrawal, S. Akshay, Blaise Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of M arkov chains. J. ACM , 62(1):2:1--2:34, 2015. https://doi.org/10.1145/2629417 doi:10.1145/2629417

    doi:10.1145/2629417 2015

  3. [3]

    Akshay, Timos Antonopoulos, Jo \" e l Ouaknine, and James Worrell

    S. Akshay, Timos Antonopoulos, Jo \" e l Ouaknine, and James Worrell. Reachability problems for M arkov chains. Inf. Process. Lett. , 115(2):155--158, 2015. URL: https://doi.org/10.1016/j.ipl.2014.08.013, https://doi.org/10.1016/J.IPL.2014.08.013 doi:10.1016/J.IPL.2014.08.013

    work page doi:10.1016/j.ipl.2014.08.013 2015

  4. [4]

    Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic

    S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. MDP s as distribution transformers: Affine invariant synthesis for safety objectives. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III , volume 13966 of Lecture No...

    doi:10.1007/978-3-031-37709-9 2023

  5. [5]

    Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic

    S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. Certified policy verification and synthesis for MDP s under distributional reach-avoidance properties. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024 , pages 3--12. ijcai.org, 2024. URL: h...

    work page 2024

  6. [6]

    Akshay, Blaise Genest, and Nikhil Vyas

    S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for M arkov decision processes. In Anuj Dawar and Erich Gr \" a del, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018 , pages 36--45. ACM , 2018. https://doi.org/10.1145/3209108.3209185 doi:10.1145/320910...

    arXiv 2018

  7. [7]

    Polynomial reachability witnesses via stellens \" a tze

    Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. Polynomial reachability witnesses via stellens \" a tze. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021 , pages 772--787....

    arXiv 2021

  8. [8]

    Principles of model checking

    Christel Baier and Joost - Pieter Katoen. Principles of model checking . MIT Press, 2008

    2008

Show all 35 references
  1. [9]

    On the solvability of anonymous partial grids exploration by mobile robots

    Roberto Baldoni, Fran c ois Bonnet, Alessia Milani, and Michel Raynal. On the solvability of anonymous partial grids exploration by mobile robots. In Theodore P. Baker, Alain Bui, and S \' e bastien Tixeuil, editors, Principles of Distributed Systems, 12th International Confer...

    2008 doi

  2. [10]

    A logic of probability with decidable model checking

    Dani \` e le Beauquier, Alexander Moshe Rabinovich, and Anatol Slissenko. A logic of probability with decidable model checking. J. Log. Comput. , 16(4):461--487, 2006. https://doi.org/10.1093/logcom/exl004 doi:10.1093/logcom/exl004

    2006 doi

  3. [11]

    Model checking MDP s with a unique compact invariant set of distributions

    Rohit Chadha, Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Model checking MDP s with a unique compact invariant set of distributions. In Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 Septembe...

    2011 doi

  4. [12]

    Probabilistic program analysis with martingales

    Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings , vo...

    2013 doi

  5. [13]

    Termination analysis of probabilistic programs through positivstellensatz's

    Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through positivstellensatz's. In CAV (1) , volume 9779 of Lecture Notes in Computer Science , pages 3--22. Springer, 2016

    2016

  6. [14]

    Polynomial invariant generation for non-deterministic recursive programs

    Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. Polynomial invariant generation for non-deterministic recursive programs. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conferenc...

    2020

  7. [15]

    Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs

    Krishnendu Chatterjee, Hongfei Fu, Petr Novotn \' y , and Rouzbeh Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. TOPLAS , 40(2):7:1--7:45, 2018. https://doi.org/10.1145/3174800 doi:10.1145/3174800

    2018 doi

  8. [16]

    Polyqent: A polynomial quantified entailment solver, 2025

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and Đorđe Žikelić. Polyqent: A polynomial quantified entailment solver, 2025. URL: https://arxiv.org/abs/2408.03796, http://arxiv.org/abs/2408.03796 ...

    2025 arXiv

  9. [17]

    Sound and complete witnesses for template-based verification of LTL properties on polynomial programs

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, and Dorde Zikelic. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In Andr \' e Platzer, Kristin Yvonne Rozier, Matteo Pradella, ...

    2024

  10. [18]

    Sound and complete certificates for quantitative termination analysis of probabilistic programs

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. Sound and complete certificates for quantitative termination analysis of probabilistic programs. In CAV (1) , volume 13371 of Lecture Notes in Computer Science , pages 55--78. Springer, 2022

    2022

  11. [19]

    Stochastic invariants for probabilistic termination

    Krishnendu Chatterjee, Petr Novotn\' y , and or e Z ikeli\'c. Stochastic invariants for probabilistic termination. In POPL , pages 145--160, 2017. https://doi.org/10.1145/3009837.3009873 doi:10.1145/3009837.3009873

    2017

  12. [20]

    The MathSAT5 SMT Solver

    Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT Solver . In Nir Piterman and Scott Smolka, editors, Proceedings of TACAS , volume 7795 of LNCS . Springer, 2013

    2013

  13. [21]

    Linear invariant generation using non-linear constraint solving

    Michael Col \' o n, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In Warren A. Hunt Jr. and Fabio Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2...

    2003 doi

  14. [22]

    Synthesis of linear ranking functions

    Michael Col \' o n and Henny Sipma. Synthesis of linear ranking functions. In Tiziana Margaria and Wang Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Th...

    2001 doi

  15. [23]

    Leonardo Mendon c a de Moura and Nikolaj S. Bj rner. Z3: an efficient SMT solver. In TACAS , volume 4963 of Lecture Notes in Computer Science , pages 337--340. Springer, 2008

    2008

  16. [24]

    From spot 2.0 to spot 2.10: What’s new? In International Conference on Computer Aided Verification , pages 174--187

    Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, J \'e r \^o me Dubois, Cl \'e ment Gillard, et al. From spot 2.0 to spot 2.10: What’s new? In International Confere...

    2022

  17. [25]

    Theorie der einfachen ungleichungen

    Julius Farkas. Theorie der einfachen ungleichungen. Journal f \"u r die reine und angewandte Mathematik (Crelles Journal) , 1902(124):1--27, 1902

    1902

  18. [26]

    Distributional reachability for M arkov decision processes: Theory and applications

    Yulong Gao, Alessandro Abate, Lihua Xie, and Karl Henrik Johansson. Distributional reachability for M arkov decision processes: Theory and applications. IEEE Trans. Autom. Control. , 69(7):4598--4613, 2024. URL: https://doi.org/10.1109/tac.2023.3341282, https://doi.org/10.1109...

    2024

  19. [27]

    Representing polynomials by positive linear functions on compact convex polyhedra

    David Handelman. Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics , 132(1):35--62, 1988

    1988

  20. [28]

    Henzinger, Maria Mateescu, and Verena Wolf

    Thomas A. Henzinger, Maria Mateescu, and Verena Wolf. Sliding window abstraction for infinite M arkov chains. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings...

    2009 doi

  21. [29]

    Reasoning about MDP s as transformers of probability distributions

    Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Reasoning about MDP s as transformers of probability distributions. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September ...

    2010 doi

  22. [30]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV , volume 6806 of Lecture Notes in Computer Science , pages 585--591. Springer, 2011

    2011

  23. [31]

    YoungMin Kwon and Gul A. Agha. Verifying the evolution of probability distributions governed by a DTMC . IEEE Trans. Software Eng. , 37(1):126--141, 2011. https://doi.org/10.1109/TSE.2010.80 doi:10.1109/TSE.2010.80

    2011 doi

  24. [32]

    Decision problems for linear recurrence sequences

    Jo \" e l Ouaknine and James Worrell. Decision problems for linear recurrence sequences. In Alain Finkel, J \' e r \^ o me Leroux, and Igor Potapov, editors, Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings , vol...

    2012 doi

  25. [33]

    Stephen Prajna, Ali Jadbabaie, and George J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control. , 52(8):1415--1428, 2007. https://doi.org/10.1109/TAC.2007.902736 doi:10.1109/TAC.2007.902736

    2007

  26. [34]

    Ranking and repulsing supermartingales for reachability in randomized programs

    Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. , 43(2):5:1--5:46, 2021. https://doi.org/10.1145/3450967 doi:10.1145/3450967

    2021 doi

  27. [35]

    Henzinger, and Krishnendu Chatterjee

    Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligenc...

    2023

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.