Pith. sign in

REVIEW 2 major objections 5 minor 36 references

Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)

T0 review · 2 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Markov decision processes have four semantics generated by one classifier; the two new ones have threshold reachability problems that are undecidable and #P-hard respectively.

desk verdict The unified framework and algorithms are solid, but Theorem 25's finite-generation claim is unproved as written. read the letter →

arxiv 2506.10377 v2 pith:TSV7BAID submitted 2025-06-12 cs.FL

Yun Chen Tsai , Kittiphon Phalakarn , S. Akshay , Ichiro Hasuo This is my paper · ORCID
classification cs.FL
keywords Markovdecisionprocesseschance-massclassifierdistributiontransformersemanticsthresholdreachabilityantichainalgorithmtemplate-basedsynthesisprobabilisticfiniteautomatonemptinesssubmartingalecertificate
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

The paper claims that the many semantics of Markov decision processes are not separate formalisms but four points in a single taxonomy. The taxonomy classifies each source of randomness in an MDP—the scheduler's choices, the current configuration, and the transition probabilities—as either 'chance' (coin tosses) or 'mass' (splitting a fluid), and a single 'chance-mass classifier' converts any MDP plus scheduler into a Markov chain over probability distributions. Two of the four semantics are new. The paper shows that threshold reachability in one new semantics is undecidable and in the other is #P-hard, then gives sound algorithms that find reachability certificates despite those lower bounds.

What carries the argument

The chance-mass (CM) classifier $X_Q : D(D(D(Q))) \to D(D(Q))$ is the load-bearing object. It reads a pre-configuration $\delta_\sigma(p)$—a distribution over actions whose probabilities are weighted by the current configuration and then by transition probabilities—and outputs a distribution over next configurations. The classifier is assembled from three operators: suppression $\mu$ (merge two probability branchings into one), the Dirac operator $\eta$ (treat an object as a trivial one-point distribution), and the MC2CM operator $\lambda$ (swap the order of mass and chance branching). Fixing $X$ fixes the semantics, so the whole taxonomy is a choice of classifier.

What would settle it

In the paper's $[0,1]^Q$ setting, take $Q=\{1,2\}$ and $H=\{d : d_1 > 1/2\}$. The $\leq$-minimal elements of $H$ do not exist, so $H$ is not the upward closure of any finite set; checking this target inside the reduction for Theorem 25 would show that the advertised 'finitely generated monotone' restriction is not met by the proof's own target.

Watch

Extended reading notes

Core claim

Starting from an MDP and a scheduler, the paper builds a configuration Markov chain whose states are probability distributions over the MDP's states. The transition law is $X \circ \delta_\sigma$: the function $\delta_\sigma$ extracts a three-level distribution exposing scheduler, configuration, and transition probabilities, and the chance-mass classifier $X$ decides which levels are averaged away as mass and which remain as random chance branching. The four classifiers $X_{(CS,CT)}$, $X_{(MS,CT)}$, $X_{(CS,MT)}$, $X_{(MS,MT)}$ instantiate the classical semantics, the distribution-transformer semantics, and the two new mixtures. On the new semantics the paper establishes: $(CS,MT)$-reachability is undecidable even for finitely generated monotone target sets, by reduction from probabilistic finite automaton emptiness; and $(MS,CT)$-reachability is #P-hard even for a single action, by reduction from counting subset sum, and remains positivity-hard when the scheduler is fixed. It then gives a sound antichain-based backward reachability procedure for $(CS,MT)$ and a sound template-based $\gamma$-scaled submartingale synthesis procedure for $(MS,CT)$, both necessarily incomplete.

Load-bearing premise

The undecidability theorem for $(CS,MT)$ rests on treating the strict linear threshold target $H=\{d : \alpha^T d > \xi\}$ used in the PFA reduction as a finitely generated monotone set; the paper does not supply a finite generator set for this $H$, and without it the stronger finite-generation claim is unsupported.

Editorial extensions

If this is right

  • If the undecidability result for $(CS,MT)$ holds, then that semantics has no complete reachability algorithm, so any practical tool must restrict the target shape or settle for an under-approximation.
  • If the #P-hardness result for $(MS,CT)$ holds, then exact threshold reachability is unlikely to be tractable, and certificate-based verification—searching for a $\gamma$-scaled submartingale—is the proposed route.
  • The four semantics are generated uniformly by one classifier, so complexity statements can be attached to a classifier choice rather than to an ad hoc model.
  • For finitely generated monotone targets, the paper's antichain algorithm is sound: every configuration it declares reachable really is reachable.
  • The template-based synthesis machinery, already used for distribution-transformer safety, now covers a mixed chance/mass semantics as well.

Reading between the lines

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

  • Beyond the paper, the other four of the eight combinatorial assignments of scheduler, configuration, and transition probabilities to chance or mass are left open; one could test whether they correspond to meaningful semantics or are ruled out by the requirement that config MC states be distributions.
  • If the finite-generation gap in Theorem 25 is real, a natural repair would be to replace the strict threshold target with a closed threshold or with an explicitly finitely generated monotone approximation; such a repair would preserve the undecidability of the underlying PFA reduction.
  • The prototype's success with low-degree templates suggests a testable hypothesis: for small MDPs, linear or low-degree $\gamma$-scaled submartingales may suffice as reachability certificates, even though the general problem is hard.
  • The CM-classifier framing is likely to transfer to quantum Markov chains and MDPs, as the paper itself suggests; the $\lambda$ operator's reordering of chance and mass resembles a commutation rule for probabilistic branching that quantum analogues may need to make explicit.
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

2 major / 5 minor

Summary. The paper introduces a unified semantical framework for Markov decision processes (MDPs), in which four semantics arise by classifying the probabilities coming from schedulers and transitions as either 'chance' (random events) or 'mass' (splitting of mass). The framework is built around a 'chance-mass classifier' that transforms pre-configurations into distributions over configurations. For the two new semantics, (CS,MT) and (MS,CT), the paper establishes complexity bounds — undecidability for threshold reachability under (CS,MT) and #P-hardness under (MS,CT) — and presents two sound algorithms: an antichain-based backward reachability algorithm for (CS,MT) and a template-based submartingale synthesis algorithm for (MS,CT). Prototype implementations are evaluated on small models, including the paper's motivating examples.

Significance. If the results hold, this is a valuable conceptual contribution: it provides a principled taxonomy of MDP semantics and identifies two new decision problems with practical motivation, together with first algorithmic approaches. The CM-classifier construction is elegant, and the #P-hardness reduction for (MS,CT) is clean and self-contained. The two algorithms are novel and supported by proof-of-concept implementations. The main reservation concerns the strengthened undecidability claim for (CS,MT), which is not established by the supplied proof; this affects the justification for the antichain algorithm's necessary incompleteness. The remainder of the framework and the algorithmic results appear sound and are likely to be of interest to the verification community.

major comments (2)
  1. [Theorem 25 and its proof in Appendix D] The reduction constructs the target set H = {d ∈ D(Q) | α^T d > ξ}. Under the paper's own definition (Section 2: 'an upward-closed set S⊆X is finitely generated if S=↑T for some finite set T'), this H is not finitely generated. For any d with α^T d > ξ, reducing a positive coordinate by a sufficiently small amount yields d' ≤ d with d' still in H, so H has no minimal elements; hence H cannot be the upward closure of a finite set. The proof never addresses finite generation, so the advertised strengthening 'even when the target set H is restricted to a finitely-generated monotone set' is not established as written. This also affects the claim in Section 5.2 that the antichain algorithm is 'necessarily incomplete', which is justified by this undecidability result. The bare undecidability for arbitrary upward-closed targets may survive, and the gap might be repairable by a different PFA encoding, but that repair is absent.
  2. [Sections 2 and 5.2, Theorem 27] The paper uses the phrase 'finitely-generated monotone set' without specifying the ambient poset in several places. The antichain algorithm operates on [0,1]^Q, while the undecidability proof in Theorem 25 defines H as a subset of D(Q). Under the componentwise order restricted to D(Q), any two comparable distributions are equal, so every subset of D(Q) is upward-closed and downward-closed, making the notion of finite generation either trivial or in need of an explicit ambient space. Please clarify whether finite generation is taken with respect to [0,1]^Q or D(Q), and state this consistently in Theorem 25, Theorem 27, and the algorithm.
minor comments (5)
  1. [Appendix D, proof of Theorem 16] The initial distribution is defined only as d0(n) = a_n / Σ a_i, leaving the other states' values unspecified; the subsequent argument requires d0(i) = a_i / Σ a_i for every i ∈ [n]. Please correct the definition.
  2. [Section 5.1, equation (10)] The constraint ΦInductive contains the term σ(q)(a); this should be σ(d)(a), consistent with the scheduler template defined one paragraph earlier.
  3. [Lemma 28] The statement of the lemma mixes notations: the first sentence defines the set as ⌊{y | M^T y ⪰ x}⌋, while the second sentence writes ⌊{y | My ⪰ x}⌋. Please unify the notation.
  4. [Section 3.1] The 'preview' passage before Definition 7 is quite long and may be better placed as a remark following Definition 7, since it interrupts the technical development.
  5. [Theorem 27] The statement says 'a finitely-generated upward-closed set H' but does not specify whether H is a subset of D(Q) or [0,1]^Q; given that the proof and the algorithm operate on the latter, this should be made explicit.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the framework is a definitional taxonomy, and the hardness and algorithmic results rest on external problems and independent certificate arguments, not on their own conclusions.

full rationale

The paper's derivation chain is not circular. The four-semantics taxonomy is a constructed framework: CM classifiers and config MCs are defined, and the semantics are derived from those definitions, so there is no input-to-output equivalence being disguised as a prediction. The load-bearing complexity results reduce from external problems: Theorem 16 reduces from counting subset sum (Papadimitriou [33]), Theorem 25 reduces from probabilistic finite automaton emptiness (Gimbert and Oualhadj [20]), and Theorem 18 reduces from the positivity-hardness result in [4]. These reductions do not assume the target hardness. The two algorithms are sound certificate procedures rather than fitted predictions: the template-based algorithm searches for a gamma-scaled submartingale satisfying R(d0) >= xi, and Theorem 21 proves such a witness implies reachability; the antichain algorithm computes an under-approximation of the least fixed point characterized in Theorem 27, with Lemmas 26 and 28 establishing the relevant upward-closed structure. Author self-citations to [6] and [35] supply prior template-synthesis and submartingale techniques, but these are independently published results with stated assumptions and do not include the target reachability conclusions, so they do not raise the circularity score. The possible gap in Theorem 25 regarding finite generation of the target set H is a proof-correctness concern, not a circularity: the reduction does not define reachability in terms of the claimed hardness. No step in the paper reduces by construction to its own inputs.

Assumptions & free parameters 3 free parameters · 6 assumptions · 0 invented entities

The central results rest on standard measure theory, known hardness results, and standard quantifier elimination theorems. The only hand-chosen numbers are algorithm hyperparameters, which affect completeness but not soundness. No physical or empirical entities are postulated.

free parameters (3)
  • antichain algorithm sampling bounds K and L = K=3 or 5, L=1 in experiments
    Chosen by hand to limit search; soundness holds for any K and L, completeness only in the limit, so these do not determine the central claim.
  • submartingale scaling factor gamma = 1 - 1e-5 in experiments
    Any gamma in (0,1) is allowed by Theorem 21; the specific value is an implementation choice.
  • Handelman semigroup degree bound = degree up to 4 in experiments
    The theoretical algorithm uses an unbounded semigroup; the implementation truncates it, affecting completeness but not soundness.
assumptions (6)
  • standard math Existence and uniqueness of the probability measure on infinite configuration paths of the config MC
    Relies on standard measure theory for countable Markov chains; cited [9,11].
  • domain assumption Undecidability of the emptiness problem for probabilistic finite automata
    External known result used as the source for the reduction in Theorem 25.
  • standard math #P-completeness of counting subset sum
    Used in the reduction for Theorem 16.
  • domain assumption Positivity-hardness of reachability for Markov chains as distribution transformers
    External result from [4], used to prove Theorem 18.
  • standard math Farkas's lemma and Handelman's theorem for quantifier elimination
    Used in the template-based synthesis algorithm; the strict-inequality handling is not fully detailed in the paper.
  • domain assumption Global actions suffice because local schedulers can be encoded by product actions
    Remark 4 is used throughout; it is standard and not likely to break the results.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)." pith.science (2026). https://pith.science/paper/TSV7BAID

@misc{pith2026250610377,
  author       = {Pith},
  title        = {Pith review of: Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TSV7BAID}},
  note         = {Machine review of arXiv:2506.10377}
}
read the original abstract

Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.

Figures

Figures reproduced from arXiv: 2506.10377 by the authors.

Figure 1
Figure 1. Casino MDP for (MS, CT) sem. (left); exam MDP for (CS,MT) sem. (right) Rj—and the probabilities pij are known. What is notable about the (MS, CT) semantics is that a mixed scheduler rkeepkeep + r1b1 + · · · + rnbn nicely models a gambler’s strategy to split the fund for different games (betting the r1 portion of the fund at Game 1, the r2 portion at Game 2, etc.). In contrast, the transition probabilities pij should… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 18 canonical work pages

  1. [1]

    Abramsky and A

    S. Abramsky and A. Jung. Domain theory. In S. Abramsky, Dov M. Gabbai, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science , volume 3, pages 1--168. Oxford Univ. Press, 1994

    work page 1994

  2. [2]

    Model checking markov chains as distribution transformers

    Rajab Aghamov, Christel Baier, Toghrul Karimov, Joris Nieuwveld, Jo \" e l Ouaknine, Jakob Piribauer, and Mihir Vahanwala. Model checking markov chains as distribution transformers. In Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mari \" e lle Stoelinga, and Matthias Volk, editors, Principles of Ve...

    work page 2024

  3. [3]

    Akshay, Blaise Genest, and P

    Manindra Agrawal, S. Akshay, Blaise Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of markov 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

  4. [4]

    Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell

    S. Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell. Reachability problems for markov chains. Information Processing Letters , 115(2):155--158, 2015. URL: https://www.sciencedirect.com/science/article/pii/S0020019014001781, https://doi.org/10.1016/j.ipl.2014.08.013 doi:10.1016/j.ipl.2014.08.013

    doi:10.1016/j.ipl.2014.08.013 2015

  5. [5]

    Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and or e Z ikeli\' c

    S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and or e Z ikeli\' c . Mdps as distribution transformers: Affine invariant synthesis for safety objectives. In Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III , page 86–112, Berlin, Heidelberg, 2023. Springer-Verlag. https://...

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

  6. [6]

    Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and or e Z ikeli\' c

    S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and or e Z ikeli\' c . Certified policy verification and synthesis for mdps under distributional reach-avoidance properties. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence , IJCAI '24, 2024. https://doi.org/10.24963/ijcai.2024/1 doi:10.24963/ijcai.2024/1

    work page doi:10.24963/ijcai.2024/1 2024

  7. [7]

    Akshay, Blaise Genest, and Nikhil Vyas

    S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for markov decision processes. In LICS , pages 36--45. ACM , 2018

    work page 2018

  8. [8]

    Computational Complexity - A Modern Approach

    Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach . Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264

    2009

Show all 36 references
  1. [9]

    Ash and Catherine A

    Robert B. Ash and Catherine A. Dol\' e ans-Dade. Probability and Measure Theory . Academic Press, 1999

    1999

  2. [10]

    Category Theory

    Steve Awodey. Category Theory . Oxford Logic Guides. Oxford Univ. Press, 2006

    2006

  3. [11]

    Principles of model checking

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

    2008

  4. [12]

    Pyomo-optimization modeling in python , volume 67

    Michael L Bynum, Gabriel A Hackebeil, William E Hart, Carl D Laird, Bethany L Nicholson, John D Siirola, Jean-Paul Watson, David L Woodruff, et al. Pyomo-optimization modeling in python , volume 67. Springer, 2021

    2021

  5. [13]

    Model checking mdps with a unique compact invariant set of distributions

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

    2011 doi

  6. [14]

    Polyqent: A polynomial quantified entailment solver

    Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and or e Z ikeli \'c . Polyqent: A polynomial quantified entailment solver. arXiv preprint arXiv:2408.03796 , 2024

    2024 arXiv

  7. [15]

    Z3: An efficient smt solver

    Leonardo de Moura and Nikolaj Bj rner. Z3: An efficient smt solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems , pages 337--340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg

    2008

  8. [16]

    Limit synchronization in markov decision processes

    Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Limit synchronization in markov decision processes. In FoSSaCS , volume 8412 of Lecture Notes in Computer Science , pages 58--72. Springer, 2014

    2014

  9. [17]

    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

  10. [18]

    Antichains and compositional algorithms for ltl synthesis

    Emmanuel Filiot, Naiyong Jin, and Jean-Fran c ois Raskin. Antichains and compositional algorithms for ltl synthesis. Form. Methods Syst. Des. , 39(3):261–296, December 2011. https://doi.org/10.1007/s10703-011-0115-3 doi:10.1007/s10703-011-0115-3

    2011 doi

  11. [19]

    Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms

    Marco Gario and Andrea Micheli. Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In SMT Workshop 2015 , 2015

    2015

  12. [20]

    Probabilistic automata on finite words: Decidable and undecidable problems

    Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th Internat...

    2010 doi

  13. [21]

    Measurement-based verification of quantum markov chains

    Ji Guan, Yuan Feng, Andrea Turrini, and Mingsheng Ying. Measurement-based verification of quantum markov chains. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedi...

    2024 doi

  14. [22]

    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

  15. [23]

    Generic trace semantics via coinduction

    Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Comp. Sci. , 3(4:11), 2007

    2007

  16. [24]

    The probabilistic model checker storm

    Christian Hensel, Sebastian Junges, Joost - Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. , 24(4):589--610, 2022. URL: https://doi.org/10.1007/s10009-021-00633-z, https://doi.org/10.1007/S10009-021-...

    2022 doi

  17. [25]

    Introduction to Coalgebra: Towards Mathematics of States and Observation , volume 59 of Cambridge Tracts in Theoretical Computer Science

    Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation , volume 59 of Cambridge Tracts in Theoretical Computer Science . Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781316823187 doi:10.1017/CBO9781316823187

    2016 doi

  18. [26]

    Reasoning about mdps as transformers of probability distributions

    Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Reasoning about mdps as transformers of probability distributions. In QEST , pages 199--208. IEEE Computer Society, 2010

    2010

  19. [27]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. The PRISM benchmark suite. In Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, September 17-20, 2012 , pages 203--204. IEEE Computer Society, 2012. https://doi.org/10...

    2012 doi

  20. [28]

    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

  21. [29]

    Mac Lane

    S. Mac Lane . Categories for the Working Mathematician . Springer, Berlin, 2nd edition, 1998

    1998

  22. [30]

    Glpk (gnu linear programming kit)

    Andrew Makhorin. Glpk (gnu linear programming kit). http://www. gnu. org/s/glpk/glpk. html , 2008

    2008

  23. [31]

    Decision problems for linear recurrence sequences

    Jo \" e l Ouaknine and James Worrell. Decision problems for linear recurrence sequences. In RP , volume 7550 of Lecture Notes in Computer Science , pages 21--28. Springer, 2012

    2012

  24. [32]

    On linear recurrence sequences and loop termination

    Jo \" e l Ouaknine and James Worrell. On linear recurrence sequences and loop termination. ACM SIGLOG News , 2(2):4--13, 2015. https://doi.org/10.1145/2766189.2766191 doi:10.1145/2766189.2766191

    2015

  25. [33]

    Papadimitriou

    Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994

    1994

  26. [34]

    Puterman

    Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming . Wiley Series in Probability and Statistics. Wiley, 1994. https://doi.org/10.1002/9780470316887 doi:10.1002/9780470316887

    1994 doi

  27. [35]

    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), June 2021. https://doi.org/10.1145/3450967 doi:10.1145/3450967

    2021 doi

  28. [36]

    Optimal policies for quantum markov decision processes

    Mingsheng Ying, Yuan Feng, and Shenggang Ying. Optimal policies for quantum markov decision processes. Int. J. Autom. Comput. , 18(3):410--421, 2021. URL: https://doi.org/10.1007/s11633-021-1278-z, https://doi.org/10.1007/S11633-021-1278-Z doi:10.1007/S11633-021-1278-Z

    2021 doi

Pith tools

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