Pith. sign in

REVIEW 3 major objections 5 minor 30 references

Quantitative Strategy Templates

T0 review · 3 major / 5 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read A single strategy template can encode every winning strategy of an energy game and every finite-memory winning strategy of a mean-payoff game.

desk verdict The permissiveness theorems for QaSTels are the real contribution and appear sound, but the runtime-adaptability claim rests on a flawed proof that needs fixing before the paper is solid. read the letter →

arxiv 2504.16528 v1 pith:LSONGJ4K submitted 2025-04-23 cs.GT

Ashwani Anand , Satya Prakash Nayak , Ritam Raha , Irmak Sağlam , Anne-Kathrin Schmuck This is my paper · ORCID
classification cs.GT MSC 91A4391A50
keywords quantitativestrategytemplatesenergygamesmean-payoffpermissivestrategiesedge-basedvalueiterationsynthesismixedobjectivesreactive
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 establishes that a single data structure called a Quantitative Strategy Template (QaSTel) can represent, at once, all winning strategies of an energy game and all finite-memory winning strategies of a mean-payoff game. The template records, for each node and each current energy credit, every outgoing edge that can safely be taken, so a controller can switch between moves at runtime without losing the winning guarantee. The authors give an edge-based value iteration algorithm that computes an optimal template, prove that it is winning and permissive, and show how to combine it with qualitative strategy templates for mixed quantitative-qualitative objectives. They argue that this makes quantitative game solving more robust to disturbances and more amenable to incremental synthesis when new objectives arrive after the fact.

What carries the argument

The load-bearing mechanism is edge-based value iteration. The standard vertex value iteration operator is extended from functions over nodes to functions over edges: for $e=(u,v)$, the operator takes the minimum or maximum over successor edges of $\mu(e')\ominus w(e)$, depending on which player controls $v$. Its least fixed point is the edge-optimal value function $\mathrm{opt}_E$, from which the optimal QaSTel is read off by activating exactly the edges with value at most the current credit. The same fixed point yields the winning region, and its monotonicity is what makes hot-starting template recomputation possible after edge deletions.

What would settle it

A concrete counterexample to Proposition 3 would settle the issue: take a small weighted game, delete a set of Player-0 edges that leaves at least one minimum-activation edge at every node, and recompute the edge-optimal value function from scratch; if any value changes, the hot-starting guarantee and the runtime-adaptability claim fail for that instance.

Watch

Extended reading notes

Core claim

The central discovery is that the optimal initial credit of a node can be refined into an edge-optimal value function $\mathrm{opt}_E(e)$, the least credit needed to take edge $e$ and still win from its source. The QaSTel defined by $\Pi(u,c)=\{e\in E(u)\mid c\ge \mathrm{opt}_E(e)\}$ is winning, and it is maximally permissive for energy games (every winning strategy follows it) and $f$-maximally permissive for mean-payoff games (every finite-memory winning strategy follows it). The proof works because any play that follows the template keeps the credit nonnegative, while any winning strategy can only use edges whose edge-optimal value is no larger than the current credit.

Load-bearing premise

The runtime-adaptability claim rests on Proposition 3, which says the original template remains optimal after deleting edges as long as every node keeps at least one minimum-activation edge; the proposition is stated without proof in the appendix and its written condition is tautological, so this is the point where the practical robustness story could collapse.

Editorial extensions

If this is right

  • An optimal QaSTel for an energy or mean-payoff game is computable in $O(|V||E|W)$ time, matching the complexity of standard value iteration while delivering many viable strategies rather than a single one.
  • Any runtime choice of an active edge, for example driven by dynamic preferences such as obstacle avoidance or actuator failures, preserves the winning guarantee as long as every node retains at least one minimum-activation edge, per Proposition 3.
  • For several mean-payoff objectives, the algorithm CombineQaSTel returns a single winning strategy for their conjunction in $O(k|V||E|W)$ time, supporting incremental arrival of quantitative objectives.
  • For mixed games with a quantitative objective and a qualitative objective such as mean-payoff co-Büchi, computeMiSTel iteratively resolves conflicts between the QaSTel and a bounded PeSTel, and on the paper's benchmarks it recovers the full winning region for over 90% of the instances.

Reading between the lines

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

  • If the runtime-adaptability guarantee holds, the template itself becomes a compact robustness certificate: the fraction of minimum-activation edges that can be deleted before a recomputation is forced gives a quantitative measure of how fault-tolerant a synthesized controller is.
  • The same edge-activation scheme should transfer to other quantitative objectives that admit a value iteration algorithm, such as discounted-sum or shortest-path-like objectives, provided an analogous edge-optimal value function can be defined.
  • Because the mixed-template construction under-approximates the winning region in general, a practitioner should run a completeness check before relying on a MiSTel; the paper's experiments suggest incompleteness appears mainly after several conflict-resolution rounds.
  • A directly testable extension is to run the online preference strategy on a physical robot with a battery constraint and measure how often blocked edges force a template recomputation, comparing the measured frequency with the paper's simulated deletion rates.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper introduces Quantitative Strategy Templates (QaSTels), which are local edge-activation annotations that succinctly represent families of winning strategies in two-player energy and mean-payoff games. The main theoretical results are that an optimal QaSTel, computed by an edge-based value iteration, is winning and maximally permissive for energy games (Theorem 3) and f-maximally permissive for mean-payoff games (Theorem 4). The paper also proposes a combination of QaSTels with bounded PeSTels into MiSTels for mixed quantitative/qualitative objectives, an incremental synthesis algorithm (Algorithm 2), and a prototype implementation evaluated on benchmarks derived from SYNTCOMP. The central permissiveness theorems have detailed appendix proofs, while the runtime-adaptability and MiSTel-soundness claims are shown to rest on Proposition 3, whose proof is incomplete.

Significance. If the results are fully established, the paper makes a useful contribution by transferring permissive strategy templates from qualitative parity games to quantitative energy and mean-payoff games, with a permissiveness guarantee that goes beyond single winning strategies. The edge-based value iteration and the extraction of the optimal QaSTel are cleanly defined, and Theorems 2--4 appear substantially correct. The empirical section is a strength: it builds a new benchmark suite, implements the state-of-the-art MPCoBuechi algorithm as a baseline, and reports quantitative comparisons for incremental synthesis. The paper does not provide machine-checked proofs or a code/data release, but the detailed appendix proofs and prototype experiments are valuable. The main unaddressed issue is the missing or incorrect proof of Proposition 3, which underpins both the runtime-adaptability claim and the soundness of MiSTel synthesis; until that is fixed, the applied claims are not fully supported.

major comments (3)
  1. [Sec. 5.1 and App. A.7] Proposition 3 is load-bearing for the runtime-adaptability claim (Eq. (6)) and for the soundness of Algorithm 2 via Theorem 6, but its proof is not supplied. The appendix proof of Corollary 2 first states the desired inequality optE(e) <= optE'(e), then derives the opposite inequality optE(e) >= optE'(e) from winning strategies in G', and it never shows that optE is a fixed point of the edge operator O'_E of G'. Consequently, the Knaster-Tarski step does not apply, and the claim that computeQaSTel(G',w,act_Π) equals computeQaSTel(G',w,µ0) is unsubstantiated. The intended argument should be a Bellman-equation induction showing that if every Player-0 node retains at least one minimal-activation edge, then the least fixed point of O'_E equals optE on the surviving edges; that argument is absent and must be supplied or the later claims must be weakened.
  2. [Thm. 5 and App. A.6] The complexity claim O(k·|V|·|E|·W) for CombineQaSTel is not proved. The proof in Appendix A.6 ends with 'the time complexity of the algorithm is O(k·|V|·|E|)', omitting the W factor, and the theorem's W factor is never justified. Moreover, each outer iteration hot-starts computeQaSTel from the previous activation function, and the proof does not bound the accumulated cost of these hot-started value iterations over up to |V| outer iterations. Please provide a per-iteration bound that accounts for W and the number of value-iteration rounds, or revise the claimed complexity accordingly.
  3. [Sec. 5.1, Proposition 3] The statement of Proposition 3 is tautological as written: it asserts that Π = computeQaSTel(G',w,µ0) is the optimal QaSTel for G'\E*_t, but Π is already defined as exactly that object by the right-hand side. The intended content — namely, that the original activation function act_Π, restricted to the remaining edges, still coincides with the optimal edge values in the modified game — is not actually stated. The proposition and its surrounding text should be reformulated so that the condition under which the original template remains optimal is explicit and testable.
minor comments (5)
  1. [Sec. 1, p. 2] The sentence 'n the context of the previously discussed robot example' contains a typo and should read 'In the context'.
  2. [Alg. 1, line 5] The set 'W'×(W\W')' denotes node pairs, not necessarily edges; please write {e∈E | src(e)∈W', tgt(e)∈W\W'} and justify why all such edges are Player-0 edges.
  3. [Sec. 7, Fig. 3a] The x-axis is labeled 'Player 0 edges deleted (in %)' while the text describes the average number of deletions needed to remove a minimal-activation edge; please align the axis label with the reported quantity.
  4. [Sec. 6.3, footnote 2] The footnote marker after 'T' appears malformed in the provided text, and the sentence around it is awkward; please repair the citation and the sentence structure.
  5. [App. A.4, Lemma 1] The proof should explicitly justify why a reachable simple cycle of negative weight in Gπ yields a π-play with negative limit average weight; the current sentence 'has a negative limit average weight' is a conclusion without the intervening argument.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the permissiveness theorems are derived from the definition of optE and standard value iteration, and the Proposition 3 gap is a proof incompleteness rather than a circular reduction.

full rationale

The central claims are self-contained against external benchmarks. Theorem 3 proves maximal permissiveness by applying the definition of optE: for a winning π-play, each suffix after edge e_i is winning with credit c_{i+1}, so c_i = c_{i+1} - w(e_i) >= optE(e_i) = actΠ(e_i), placing e_i in Π(u_i,c_i). Theorem 2 proves winningness by showing that a (Π,c)-play can never leave Π: if it did, the last active edge would give a winning strategy for the successor with enough credit to reactivate an edge, contradicting the empty activation set; otherwise all credits stay nonnegative. Lemma 1 bounds prefix weights by 2|V'|W using nonnegative cycles in the finite-memory product graph, and Theorem 4 merely instantiates c = max{W|V|, Bπ} before applying Theorem 3. These arguments use only standard external facts (energy/mean-payoff equivalence and value iteration) and do not reduce to the authors' earlier PeSTel results, which are cited only for motivation and for the bounded-PeSTel subroutine. The one substantive weakness is Proposition 3 / Corollary 2: the appendix proof derives optE(e) >= optE'(e) where the hot-start claim needs the opposite inequality, and no Knaster-Tarski step supplies the missing least-fixed-point property. That is an unproven lemma and a correctness risk for the runtime-adaptability and MiSTel soundness claims, but it is not a circularity, because the claim is not obtained by assuming the conclusion or by renaming a fitted input.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters are fitted to data; the central algorithms have no tunable constants. The paper introduces new mathematical objects (QaSTels, MiSTels) but these are formal definitions with proofs, not speculative entities. The main axioms are standard results in energy and mean-payoff games, plus the newly proved Lemma 1.

assumptions (4)
  • domain assumption Mean-payoff games and energy games with unknown initial credit have the same winning region (equivalence result from [9]).
    Used in Lemma 3 and Theorem 4 to transfer permissiveness from energy to mean-payoff games.
  • standard math The standard value iteration algorithm (Eq. 1) correctly computes the optimal credit function opt for energy games.
    The edge-based variant in Eq. (2) inherits correctness via Remark 1.
  • standard math The optimal initial credit is bounded by W·|V| (standard result for energy games).
    Used to define the credit threshold c ≥ W·|V| for mean-payoff games in Def. 2.
  • domain assumption Every finite-memory winning strategy in a mean-payoff game has a uniform lower bound on the credit (Lemma 1, proved in A.4).
    Used to prove f-maximal permissiveness (Theorem 4).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Quantitative Strategy Templates." pith.science (2026). https://pith.science/paper/LSONGJ4K

@misc{pith2026250416528,
  author       = {Pith},
  title        = {Pith review of: Quantitative Strategy Templates},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LSONGJ4K}},
  note         = {Machine review of arXiv:2504.16528}
}
abstract

This paper presents (permissive) \emph{Quantitative Strategy Templates} (QaSTels) to succinctly represent infinitely many winning strategies in two-player energy and mean-payoff games. This transfers the recently introduced concept of \emph{Permissive (qualitative) Strategy Templates} (PeSTels) for $\omega$-regular games to games with quantitative objectives. We provide the theoretical and algorithmic foundations of (i) QaSTel synthesis, and (ii) their (incremental) combination with PeSTels for games with mixed quantitative and qualitative objectives. Using a prototype implementation of our synthesis algorithms, we demonstrate empirically that QaSTels extend the advantageous properties of strategy templates over single winning strategies -- known from PeSTels -- to games with (additional) quantitative objectives. This includes (i) the enhanced robustness of strategies due to their runtime-adaptability, and (ii) the compositionality of templates w.r.t. incrementally arriving objectives. We use control-inspired examples to illustrate these superior properties of QaSTels for CPS design.

Figures

Figures reproduced from arXiv: 2504.16528 by the authors.

Figure 1
Figure 1. Example of an energy game (right top) with the computation for the [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Mean-payoff co-Büchi game with co-Buchi ¨ ({a, c}) . We note that the state-of-the-art al￾gorithm by Chatterjee et al. [11] is in￾stead complete. Our experimental results presented in Section 7 however show that the winning region computed by computeMiSTel coincides with the full winning region computed by MPCoBuechi for more then 90% of the considered benchmark instances. 7 Empirical Evaluations This section aims t… view at source ↗
Figure 3
Figure 3. Plots summarizing the experimental evaluations. Bigger figures can be [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Plots summarizing the experimental evaluations. [PITH_FULL_IMAGE:figures/full_fig_p029_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 13 canonical work pages

  1. [1]

    In: Tools and Algorithms for the Construction and Analysis of Systems (2023)

    Anand, A., Mallik, K., Nayak, S.P., Schmuck, A.K.: Computing adequately per- missive assumptions for synthesis. In: Tools and Algorithms for the Construction and Analysis of Systems (2023)

    work page 2023

  2. [2]

    In: Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I

    Anand, A., Nayak, S.P., Schmuck, A.K.: Synthesizing permissive winning strategy templates for parity games. In: Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. Lec- ture Notes in Computer Science (2023). https://doi.org/10.1007/978-3-031-37706- 8\_22

    doi:10.1007/978-3-031-37706- 2023

  3. [3]

    In: ATVA

    Anand, A., Nayak, S.P., Schmuck, A.: Strategy templates - robust certified inter- faces for interacting systems. In: ATVA. Lecture Notes in Computer Science, vol. 15054, pp. 22–41. Springer (2024)

    work page 2024

  4. [4]

    In: Proceedings of the 27th ACM International Con- ference on Hybrid Systems: Computation and Control

    Anand, A., Schmuck, A.K., Prakash Nayak, S.: Contract-Based Distributed Log- ical Controller Synthesis. In: Proceedings of the 27th ACM International Con- ference on Hybrid Systems: Computation and Control. HSCC ’24 (May 2024). https://doi.org/10.1145/3641513.3650123

    arXiv 2024

  5. [5]

    Theoretical Computer Science 807, 42–55 (2020)

    Avni, G., Henzinger, T.A., Kupferman, O.: Dynamic resource al- location games. Theoretical Computer Science 807, 42–55 (2020). https://doi.org/https://doi.org/10.1016/j.tcs.2019.06.031, in memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part II

    work page doi:10.1016/j.tcs.2019.06.031 2020

  6. [6]

    RAIRO Theor

    Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. RAIRO Theor. Informatics Appl. 36(3), 261–275 (2002). https://doi.org/10.1051/ita:2002013

    doi:10.1051/ita:2002013 2002

  7. [7]

    In: Cassez, F., Jard, C

    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems, 6th Interna- tional Conference, FORMATS 2008, Saint Malo, France, September 15-17,

    work page 2008

  8. [8]

    In: Bultan, T., Hsi- ung, P

    Bouyer, P., Markey, N., Olschewski, J., Ummels, M.: Measuring permissive- ness in parity games: Mean-payoff parity games revisited. In: Bultan, T., Hsi- ung, P. (eds.) Automated Technology for Verification and Analysis, 9th Interna- tional Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceed- ings. Lecture Notes in Computer Science, vol. 699...

    doi:10.1007/978-3-642-24372-1 2011

Show all 30 references
  1. [9]

    Formal Methods Syst

    Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.: Faster al- gorithms for mean-payoff games. Formal Methods Syst. Des. 38(2), 97–118 (2011). https://doi.org/10.1007/S10703-010-0105-X, https://doi.org/10.1007/ s10703-010-0105-x

    2011 doi

  2. [10]

    In: Alur, R., Lee, I

    Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource in- terfaces. In: Alur, R., Lee, I. (eds.) Embedded Software, Third Interna- tional Conference, EMSOFT 2003, Philadelphia, PA, USA, October 13-15, 2003, Proceedings. Lecture Notes in Computer Science, vol...

    2003

  3. [11]

    In: Larsen, K.G., Bodlaender, H.L., Raskin, J

    Chatterjee, K., Henzinger, M., Svozil, A.: Faster algorithms for mean- payoff parity games. In: Larsen, K.G., Bodlaender, H.L., Raskin, J. (eds.) 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark. LIP...

    2017 doi

  4. [12]

    In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings

    Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings. pp. 178–187. IEEE Computer Society (2005). https://doi.org/10.1109/LICS.2005.26, https:/...

    2005 doi

  5. [13]

    In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015

    De Giacomo, G., Vardi, M.Y., et al.: Synthesis for ltl and ldl on finite traces. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015. pp. 1558–1564. AAAI Press (2015)

    2015

  6. [14]

    CoRR abs/2305.10546 (2023)

    Fijalkow, N., Bertrand, N., Bouyer-Decitre, P., Brenguier, R., Carayol, A., Fearnley, J., Gimbert, H., Horn, F., Ibsen-Jensen, R., Markey, N., Mon- mege, B., Novotný, P., Randour, M., Sankur, O., Schmitz, S., Serre, O., Skomra, M.: Games on graphs. CoRR abs/2305.10546 (2023). ...

    2023 doi arXiv

  7. [15]

    Fijalkow, N., Bertrand, N., Bouyer-Decitre, P., Brenguier, R., Carayol, A., Fearn- ley,J.,Gimbert,H.,Horn,F.,Ibsen-Jensen,R.,Markey,N.,Monmege,B.,Novotný, P., Randour, M., Sankur, O., Schmitz, S., Serre, O., Skomra, M.: Games on graphs (2023), https://arxiv.org/abs/2305.10546

    2023 arXiv

  8. [16]

    Automatica 127, 109543 (2021)

    Girard, A., Eqtami, A.: Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications. Automatica 127, 109543 (2021). https://doi.org/https://doi.org/10.1016/j.automatica.2021.109543, https://www. sciencedirect.com/science/article/pii/S...

    2021

  9. [17]

    In: CAV (2)

    Gittis, A., Vin, E., Fremont, D.J.: Randomized synthesis for diversity and cost constraints with control improvisation. In: CAV (2). Lecture Notes in Computer Science, vol. 13372, pp. 526–546. Springer (2022)

    2022

  10. [18]

    In: 2017 IEEE/RSJ International Con- ference on Intelligent Robots and Systems (IROS)

    He, K., Lahijanian, M., Kavraki, L.E., Vardi, M.Y.: Reactive synthesis for fi- nite tasks under resource constraints. In: 2017 IEEE/RSJ International Con- ference on Intelligent Robots and Systems (IROS). pp. 5326–5332 (2017). https://doi.org/10.1109/IROS.2017.8206426

    2017

  11. [19]

    https://doi.org/10.5281/zenodo.8112518

    Jacobs, S., Perez, G., Schlehuber-Caissier, P.: Data, scripts, and results from synt- comp 2023 (2023). https://doi.org/10.5281/zenodo.8112518

    2023 doi

  12. [20]

    Acta Informatica 52(4-5), 443–482 (2015)

    Klein, J., Baier, C., Klüppelholz, S.: Compositional construction of most general controllers. Acta Informatica 52(4-5), 443–482 (2015). https://doi.org/10.1007/s00236-015-0239-9 Quantitative Strategy Templates 21

    2015 doi

  13. [21]

    In: Artho, C., Legay, A., Peled, D

    Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the gpu. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis. pp. 262–267. Springer International Publishing, Cham (2016)

    2016

  14. [22]

    In: 2023 IEEE/RSJ International Con- ference on Intelligent Robots and Systems (IROS)

    Muvvala, K., Lahijanian, M.: Efficient symbolic approaches for quantitative reactive synthesis with finite tasks. In: 2023 IEEE/RSJ International Con- ference on Intelligent Robots and Systems (IROS). pp. 8666–8672 (2023). https://doi.org/10.1109/IROS55552.2023.10342496

    2023

  15. [23]

    IEEE Open Journal of Control Systems 2, 277–296 (2023)

    Nayak,S.P.,Egidio,L.N.,DellaRossa,M.,Schmuck,A.K.,Jungers,R.M.:Context- triggered abstraction-based control design. IEEE Open Journal of Control Systems 2, 277–296 (2023). https://doi.org/10.1109/OJCSYS.2023.3305835

    2023

  16. [24]

    In: Finkbeiner, B., Kovács, L

    Nayak,S.P.,Schmuck,A.:Mostgeneralwinningsecureequilibriasynthesisingraph games. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construc- tion and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences...

    2024 doi

  17. [25]

    Neider, D., Rabinovich, R., Zimmermann, M.: Down the borel hierarchy: Solv- ing muller games via safety games. Theor. Comput. Sci. 560, 219–234 (2014). https://doi.org/10.1016/j.tcs.2014.01.017

    2014 doi

  18. [26]

    In: Robotics: Science and Systems (2021)

    Vazquez-Chanlatte, M., Junges, S., Fremont, D.J., Seshia, S.: Entropy-guided con- trol improvisation. In: Robotics: Science and Systems (2021)

    2021

  19. [27]

    Information and Computation 241, 177–196 (2015)

    Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A., Raskin, J.F.: The complexity of multi-mean-payoff and multi- energy games. Information and Computation 241, 177–196 (2015). https://doi.org/https://doi.org/10.1016/j.ic.2015.03.001, https://www. sciencedir...

    2015 doi

  20. [28]

    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1&2), 343–359 (1996). https://doi.org/10.1016/0304- 3975(95)00188-3, https://doi.org/10.1016/0304-3975(95)00188-3 22 A. Anand et al. A Missing Proofs A.1 Proof of Proposition 1 Prop...

    1996 doi

  21. [133]

    https://doi.org/10.1007/978-3-540-45212-6\_9, https:// doi.org/10.1007/978-3-540-45212-6\_9

    Springer (2003). https://doi.org/10.1007/978-3-540-45212-6\_9, https:// doi.org/10.1007/978-3-540-45212-6\_9

    2003 doi

  22. [2008]

    Lecture Notes in Computer Science, vol

    Proceedings. Lecture Notes in Computer Science, vol. 5215, pp. 33–47. Springer (2008). https://doi.org/10.1007/978-3-540-85778-5\_4, https://doi. org/10.1007/978-3-540-85778-5\_4

    2008 doi

Pith tools

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