{"id":"10149769-e909-49dc-be04-a7c844233a8e","arxiv_id":"2501.16291","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"Proposes non-dominated almost-sure winning strategies for stochastic games with incomplete LTLf preferences, via a rank-based algorithm, and claims these form Nash equilibria.","lead":"This paper presents an automata-based method for synthesizing strategies in two-player stochastic games when players have incomplete and opposite preferences over temporal goals, formalized in linear temporal logic on finite traces. Its value would be to give robots and autonomous systems formal guarantees about preferred outcomes under adversarial behavior, but the main correctness proof appears flawed.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 3 is false for incomplete preferences, so the Nash-equilibrium theorem is unsupported: a four-state adversarial preorder gives non-constant rank sums.","rationale":"The reader's broad diagnosis—that the rank construction does not faithfully support the dominance/Nash reasoning for incomplete preferences—is confirmed. I do not rely on the reader's specific claim that Lemma 2 reverses the strict-preference direction; the clearer and more decisive failure is a concrete false combinatorial lemma. Lemma 3 is used exactly to relate P1's and P2's minimax ranks, and the counterexample above is expressible with the paper's unrestricted preorder model. Since the paper's advertised scope is incomplete preferences, a repair would need either a new invariant or a restriction to total/weak-order preferences, which would narrow the contribution substantially. Thus the present version should not be accepted.","tokens_in":13643,"tokens_out":27648,"duration_ms":263191,"concrete_test":"Check Lemma 3 by brute force on the four-state preorder: set V={v1,v2,v3,v4}, E1 generated by v1≻v2≻v4 and v3≻v4 with v1∥v3 and v2∥v3, and E2 defined by u⪰E2 v iff v⪰E1 u. Compute rank1 and rank2 exactly as in Definition 9 by iterated Max removal. Reproducing sums 2,2,1,2 refutes Lemma 3; any implementation of Definition 9 will return this output, proving the theorem's proof invalid.","verdict_should_be":"REJECT","load_bearing_attack":"Even under the intended reading of Definition 9 (iterated removal of maximal elements), Lemma 3 is false. Lemma 3 asserts that for every state v, rank1(v)+rank2(v)=kmax1=kmax2 when E2 is the adversarial inverse of E1. This fails for the very incomparability the paper advertises. Let V={v1,v2,v3,v4}, with E1 satisfying v1≻v2≻v4, v3≻v4, and v1∥v3, v2∥v3. Definition 9 gives rank1(v1)=rank1(v3)=0, rank1(v2)=1, rank1(v4)=2. The inverse relation E2 satisfies v4≻v2≻v1 and v4≻v3, so rank2(v4)=0, rank2(v2)=rank2(v3)=1, rank2(v1)=2. The sums rank1+rank2 are 2,2,1,2, not constant. This is not a corner case: v3 is an incomparable branch of exactly the kind used in the drone example, and no restriction in the paper rules it out. Consequently, Lemma 4 and the claimed Nash-equilibrium proof collapse. The central claim that ND-ASWin profiles are Nash equilibria is therefore not established as stated.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies two-player stochastic games on graphs in which players have adversarial and possibly incomplete preferences over LTLf temporal goals. It introduces a solution concept, non-dominated almost-sure winning (ND-ASWin), together with a scalar 'rank' metric derived from a preference automaton, and an algorithm that computes an ND-ASWin strategy by successively solving almost-sure reachability games. The main theoretical claims are that the algorithm's output is ND-ASWin (Theorem 2) and that any profile of ND-ASWin strategies is a Nash equilibrium under a risk-averse qualitative interpretation (Theorem 3). The paper also includes a drone-delivery experiment illustrating the rank computation. The central proofs rely on Lemma 2, connecting rank minimization to undominance, and Lemma 3, asserting that the ranks of the two adversarial players sum to a constant.","tokens_in":13901,"tokens_out":9892,"duration_ms":83571,"significance":"If the results were correct, the paper would provide a practically appealing synthesis method: polynomial-time computation of preference-aligned, robust strategies in stochastic games with incomplete preferences, plus a Nash-equilibrium guarantee. The problem formulation is meaningful, the automata-theoretic reduction is natural, and the drone example is a useful concrete illustration. The paper is also commendable for not fitting parameters and for defining the rank from the preference automaton rather than reverse-engineering it. However, the central correctness arguments contain load-bearing errors. Lemma 3 is false, and the proof of Lemma 2 reverses the direction of strict dominance given by Definition 6. Because these lemmas underpin Theorems 1–3, the paper's main claims are not established.","major_comments":[{"comment":"Lemma 3 is false. Consider V={v1,v2,v3,v4} with E1 defined by v1≻v2≻v4, v3≻v4, v1∥v3, and v2∥v3. Under Definition 9 with the standard meaning of maximal elements, rank1(v1)=rank1(v3)=0, rank1(v2)=1, and rank1(v4)=2. The adversarial inverse E2 satisfies v4≻v2≻v1 and v4≻v3, with v1∥v3 and v2∥v3, giving rank2(v4)=0, rank2(v2)=rank2(v3)=1, and rank2(v1)=2. Then rank1(v1)+rank2(v1)=2 while rank1(v3)+rank2(v3)=1, contradicting the asserted constancy. This is not a corner case: v3 is an incomparable branch of exactly the kind the paper's incomplete-preference model is meant to accommodate. Since Lemma 4 and Theorem 3 rely on the constancy of rank1+rank2, the Nash-equilibrium theorem is unsupported.","section":"Qualitative Nash Equilibrium, Lemma 3"},{"comment":"The proof of Lemma 2 reverses the preference direction given by Definition 6. If (π1′,π2) strictly dominates (π1,π2), condition 2 of Definition 6 yields ρ∈Min(Ω(π1′,π2)) and ρ′∈Min(Ω(π1,π2)) such that L(ρ)≻1L(ρ′). The proof instead asserts the existence of v′∈Min(Ω(π1′,π2)) with v′≻1v for some v∈Min(Ω(π1,π2)), which is the opposite orientation. With the direction corrected, the purported contradiction does not follow: a strict improvement among some minimal outcomes does not imply a decrease in the maximum rank over the whole outcome set, because minimal outcomes need not realize the maximum rank. Consequently, Theorem 1 and the correctness of Algorithm 1 are not established.","section":"Synthesis of Non-dominated Almost-sure Winning Strategy, Lemma 2"},{"comment":"The rank metric is not shown to be a faithful proxy for the dominance order used in Definition 6. Proposition 2 gives only one-way implications, and the authors explicitly acknowledge in Example 1 that the converses fail; in particular, a lower rank does not imply weak preference. Lemma 1 only asserts that maximum-rank states are minimal, which is one direction. The central claim that minimizing MaxRank is equivalent to being non-dominated is not proven by any valid argument, since Lemma 2 is the only bridge and its proof is invalid. Thus the assertion in the Ranks subsection that rank is 'sufficient to synthesize ND-ASWin strategies' is unsupported.","section":"Ranks: A Measure of Quality of Outcome, Definition 9 and Proposition 2"}],"minor_comments":[{"comment":"The definitions of maximal and minimal elements appear reversed relative to standard usage: 'u is maximal if there is no v∈U such that u⪰v' describes a least-preferred element, not a maximal one. This ambiguity propagates into Definition 9 and Lemma 1 and should be corrected.","section":"Preliminaries, maximal and minimal elements"},{"comment":"In the proof of Lemma 3, the sentence 'Since v was a minimal element in V under E2' is not consistent with the construction: v is chosen from the last rank class under E1, so it is maximal under E1 and minimal under E2 only under the intended standard reading. The phrasing needs to be made precise.","section":"Proof of Lemma 3"},{"comment":"Strategies were defined as functions π:S+→D(A), but Definition 2 writes π:S+→A, which is the signature of a deterministic strategy. The definition should clarify whether properness applies to randomized strategies and, if so, how 'undefined' interacts with probability distributions.","section":"Definition 2 (Proper Strategy)"},{"comment":"In the proof of Theorem 2, the expression 'v′∈max{rank1(v) | v∈Ω(...)}' uses 'max' ambiguously to denote both a numerical maximum and a set of states attaining it; this should be rewritten for clarity.","section":"Theorem 2 proof"},{"comment":"Example 1 contains a typo: 'the rank of v3 is smaller than that of v3' should presumably compare the rank of v3 with the rank of v2.","section":"Example 1"},{"comment":"The paper relies on the preference-automaton theorem of Rahmani, Kulkarni, and Fu (2024) for Proposition 1. Since this is a nonstandard imported result, the dependency should be stated more prominently, and ideally a proof sketch or self-contained statement should be included.","section":"Proposition 1 dependency"}],"recommendation":"reject","confidential_remarks":"The central results are not established: Lemma 3 is false, and the proof of Lemma 2 reverses the dominance direction. These errors are load-bearing for Theorems 1–3. The counterexample to Lemma 3 uses exactly the incomparability that motivates the paper, so the failure is not a technical edge case. I see no straightforward repair within the paper's current framework: rank additivity does not hold for iterated maximal-element ranks on partial orders, and the equivalence between rank minimization and undominance is not demonstrated. The heavy reliance on self-cited prior work for the preference-automaton construction is a separate concern but would not by itself justify rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me give you the short version: the paper is worth reading for its problem statement, but the main theorems don't hold as written. The novel piece is the combination of incomplete LTLf preferences with two-player stochastic games, and the ND-ASWin solution concept is a sensible extension of almost-sure winning. The automata-based reduction is a natural follow-on to the MDP work, and the drone example does illustrate the intent.\n\nThe soft spots are at the core. First, the definitions of maximal and minimal elements in the preliminaries are swapped relative to the standard ordering—they say maximal is 'no v such that u ⪰ v' and minimal is 'no v such that v ⪰ u'. That's backwards. Their own Example 1 uses the ordinary reading (v1, v3, v5 get rank 0 as the best states), so the formal definitions don't match the usage. Every lemma that mentions Max or Min inherits this ambiguity.\n\nSecond, Lemma 3 is false for incomplete preferences. Take V with v1≻v2≻v4, v3≻v4, and v1∥v3, v2∥v3. Under the intended rank definition, ranks for E1 are (0,1,0,2). The adversarial inverse E2 gives ranks (2,1,1,0). The sums are 2,2,1,2—not constant. That kills Lemma 4 and the Nash equilibrium argument. This isn't a corner case; the incomparability is exactly what the paper advertises.\n\nThird, Lemma 2's proof has a gap. The reader's claim that the strict-preference direction is reversed doesn't survive a close read of Definition 6—condition 2 does put the dominator's minimal outcome above the dominated's. But the proof then jumps from v'≻v to a contradiction with MaxRank minimization. That doesn't follow: a dominating profile could have a better minimal outcome while still having a higher maximum rank elsewhere. Theorem 2 inherits the gap.\n\nSo the central claims are not established. The paper would be a good starting point for a next attempt, and the problem deserves serious attention, but this version isn't close. If you are the editor, I'd send it to referees anyway because the topic is timely and the flaws are concrete enough to be fixable—but the referee report would be heavy.\n\nRecommendation: reject in current form; invite major revision.","headline":"Important problem, but the core correctness argument collapses: Lemma 3 is false under the intended reading and the order-theoretic definitions are inconsistent.","tokens_in":14435,"tokens_out":11306,"would_cite":false,"duration_ms":92058,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper introduces non-dominated almost-sure winning, a solution concept for two-player stochastic games with adversarial, incomplete preferences over temporal goals, and proves that strategies synthesized by its rank-based algorithm…","keywords":["stochastic games","incomplete preferences","linear temporal logic on finite traces","almost-sure winning","Nash equilibrium","strategy synthesis","preference automata","rank"],"falsifier":"Enumerate all small stochastic games with incomplete preorders on a few outcomes, run Algorithm 1, and check Definition 6 directly by enumerating all opponent strategies; the central claim is false if any returned strategy is strictly dominated. A more targeted search looks for a game where a strategy minimizes the maximum rank but an alternative strategy makes the least-preferred outcome strictly better in the preference order without increasing that maximum.","tokens_in":13393,"feed_emoji":"🎯","tokens_out":10693,"duration_ms":88581,"temperature":0.7,"pith_summary":"The paper addresses a gap in strategic decision-making: how to synthesize a strategy for an AI agent when its preferences over temporal goals are incomplete—some outcomes are incomparable—and an adversary with opposite preferences acts in a stochastic environment. It introduces non-dominated almost-sure winning (ND-ASWin), which guarantees the agent the most-preferred worst-case outcome regardless of the opponent's strategy. The authors prove that every strategy returned by their algorithm is ND-ASWin, and that a profile of ND-ASWin strategies for both players is a Nash equilibrium under a risk-averse, worst-case reading of the game. If correct, this gives a tractable way to compute stable, preference-aligned behavior in stochastic adversarial settings without forcing preferences to be complete.","feed_headline":"Rank-based strategies win games with incomplete preferences","feed_subtitle":"A scalar 'rank' turns incomplete preference orders into almost-sure winning strategies that form Nash equilibria.","key_machinery":"The central object is the product game H formed from the original stochastic game and each player's preference automaton, a deterministic finite automaton whose states carry a preorder lifted from the LTLf preference relation. The load-bearing device is the state rank: repeatedly remove the maximal elements of the preorder, and assign to each state the layer in which it is removed. A scalar rank of 0 is most preferred, and higher ranks are worse. Algorithm 1 iterates k = 0, 1, ... and checks whether the initial state lies in the almost-sure winning region for the set of states of rank at most k; the first such k yields an ND-ASWin strategy. The Nash-equilibrium result rests on Lemma 3, which shows that for adversarial preferences the ranks of the two players on any state sum to a constant, so that minimizing one's own worst-case rank is automatically a best response to the opponent doing the same.","core_discovery":"The central claim is that incomplete preferences over LTLf (linear temporal logic over finite traces) objectives can be handled in two-player stochastic games by compressing each player's preference preorder into a scalar rank on the states of a product game, and then treating the best worst-case outcome as minimizing the maximum rank the player can be forced into. Theorem 2 states that every P1 strategy returned by Algorithm 1 is ND-ASWin: no alternative strategy can strictly improve the least-preferred outcome that P1 can be held to against any P2 strategy. Theorem 3 states that any strategy profile made of ND-ASWin strategies for both players is a Nash equilibrium, under the paper's worst-case interpretation of equilibrium. The rank is computed by iteratively peeling off maximal elements of the preference preorder, and the synthesis algorithm solves an almost-sure reachability game for each rank threshold, so the whole procedure runs in polynomial time.","pith_inferences":["Because rank collapses incomparability into equal or ordered scalars, a natural extension would test how sensitive the synthesized strategies are to different tie-breaking conventions among incomparable outcomes.","The constant-rank-sum lemma suggests a structural duality: in adversarial incomplete-preference games there is a rank value, and ND-ASWin strategies are rank-minimax strategies; this could connect to classical min-max and multi-objective game results.","A testable extension would replace the scalar rank with a lexicographic sequence of layer counts, preserving more information about incomparability at the cost of solving harder multi-objective games; the paper's own complexity discussion indicates this trade-off.","A broader empirical sweep over random small games could check how often rank-minimization is exactly equivalent to undominance of worst-case outcomes, beyond the drone gridworld demonstration."],"forward_implications":["Any pair of ND-ASWin strategies is a Nash equilibrium, so in the risk-averse sense preference-aligned play is stable against unilateral deviations.","The synthesis procedure is polynomial-time, quadratic in the size of the game and linear in the maximum rank, making it feasible on finite-state models.","Incomparability among goals need not be resolved in advance; the rank-based method synthesizes a guaranteed best worst-case outcome without a utility representation.","Because incomplete preferences subsume complete and lexicographic preferences, ND-ASWin generalizes earlier almost-sure winning with a single temporal goal.","The drone delivery experiment shows the framework can also guide game design, for instance by identifying which starting cell an agent should choose to guarantee its best possible outcome under adversarial obstruction."],"supporting_citations":[{"why":"Supplies the almost-sure winning algorithm and its complexity, which Algorithm 1 calls as a subroutine.","marker":"De Alfaro, Henzinger, and Kupferman 2007"},{"why":"Defines LTLf and its translation to finite automata, giving the temporal-goal specification formalism.","marker":"De Giacomo and Vardi 2013"},{"why":"Provides the preference-automaton construction and Theorem 1 linking preference between words to preference between automaton states, used in Proposition 1.","marker":"Rahmani, Kulkarni, and Fu 2024"},{"why":"Supplies the undominance principle and maximization viewpoint on which the rank metric is based.","marker":"Sen 1997"},{"why":"Makes the computational-hardness case for multi-objective stochastic games, motivating the scalar rank in place of multi-utility representations.","marker":"Chen et al. 2013b"},{"why":"Gives the prior treatment of Nash equilibrium with incomplete preferences that the paper extends to sequential stochastic games.","marker":"Bade 2005"}],"fun_headline_variants":["Rank compresses incomplete preferences into winning strategies","Non-dominated almost-sure winning gives Nash equilibrium","Stochastic games: rank-based synthesis from partial preferences","Incomplete preferences? Rank them and win almost surely","Preference rank turns adversarial games into stable wins"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument assumes that minimizing the maximum rank over all reachable outcomes is exactly the same as ensuring that no other strategy can produce a strictly preferred worst-case outcome; if rank order misrepresents the preference preorder for incomparable outcomes, this equivalence fails.","fun_headline_variants_meta":{"raw":{"variants":["Rank compresses incomplete preferences into winning strategies","Non-dominated almost-sure winning gives Nash equilibrium","Stochastic games: rank-based synthesis from partial preferences","Incomplete preferences? Rank them and win almost surely","Preference rank turns adversarial games into stable wins"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000242,"raw_usage":{"total_tokens":1521,"prompt_tokens":937,"completion_tokens":584,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":553,"completion_tokens_details":{"reasoning_tokens":512}},"tokens_in":553,"tokens_out":584,"duration_ms":6103,"temperature":1.0,"reasoning_tokens":512,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T13:36:56.986689+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate all small stochastic games with incomplete preorders on a few outcomes, run Algorithm 1, and check Definition 6 directly by enumerating all opponent strategies; the central claim is false if any returned strategy is strictly dominated. A more targeted search looks for a game where a strategy minimizes the maximum rank but an alternative strategy makes the least-preferred outcome strictly better in the preference order without increasing that maximum.","supporting_citations":[{"cited_title":"A.; and Kupferman, O","cited_arxiv_id":null,"evidence_quote":"Supplies the almost-sure winning algorithm and its complexity, which Algorithm 1 calls as a subroutine."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines LTLf and its translation to finite automata, giving the temporal-goal specification formalism."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the undominance principle and maximization viewpoint on which the rank metric is based."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the prior treatment of Nash equilibrium with incomplete preferences that the paper extends to sequential stochastic games."}],"review_version":1}