{"id":"b8f51cf2-172c-4069-9b03-d47b4c46acac","arxiv_id":"2506.06959","paper_version":1,"verdict":"REJECT","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":1,"one_line_summary":"An RL algorithm that restricts policy updates to actions keeping a PCTL reachability probability above a threshold is proposed, with a claimed convergence to local optimality that is not rigorously established.","lead":"This paper proposes a reinforcement learning algorithm that maximizes reward while keeping a probabilistic logical constraint satisfied, using a modified policy improvement step that filters out actions which would lower the satisfaction probability below a threshold. It claims convergence to a locally optimal feasible policy, but the proof has a critical gap: the feasibility check is only local, so the final policy can violate the constraint.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The local Step 5 feasibility test uses the previous policy's satisfaction vector, so updated actions can jointly violate the PCTL constraint; Theorem 4.2's feasibility claim is unsupported, and a small counterexample MDP makes Algorithm 1 converge to an infeasible policy.","rationale":"I independently reconstructed the proof's gap and found an explicit finite MDP that demonstrates it. The reader's weakest_assumption identifies the same load-bearing premise: Step 5's per-action threshold test, evaluated with the previous policy's satisfaction vector, is not sufficient to guarantee that the globally updated policy satisfies the PCTL formula. My counterexample shows that the algorithm can terminate on an infeasible policy, so Theorem 4.2 is not established. This is an internal inconsistency in the central argument, not a disagreement with an external consensus. The reader's REJECT verdict is therefore appropriate, and my analysis does not change it.","tokens_in":15141,"tokens_out":11368,"duration_ms":133436,"concrete_test":"Implement Algorithm 1 with epsilon=0 on the 4-state MDP: states {S, A, T, L}, with T and L absorbing; S-actions b1 (to A with probability 1) and b2 (to A with probability 0.8, L with probability 0.2); A-actions a1 (to T with probability 0.9, L with probability 0.1) and a2 (to T with probability 0.5, L with probability 0.5); constraint P>=0.5(F T); and rewards satisfying R(L)>R(T) so that b2 and a2 improve utility, e.g. R(T)=10, R(L)=100, R(S)=R(A)=0. Run to convergence and check whether the returned policy satisfies x_S>=0.5. If the algorithm returns {S:b2, A:a2} with x_S=0.4, or any infeasible policy, Theorem 4.2's feasibility claim is refuted.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 4.2: with epsilon=0, Algorithm 1 terminates at a feasible local maximizer of (2). The proof's first item asserts that feasibility is preserved 'by construction' because Step 5 admits only actions with Y^{(t+1)}(s,a) = sum_{s'} T(s,a,s') x^{(t)}_{s'} >= lambda. This is load-bearing and false as stated. Step 5 tests each action against the satisfaction vector x^{(t)} of the previous policy. Once other states are updated in the same or later sweeps, those downstream probabilities change, so an action that passed the test can become violating, and the algorithm has no mechanism that forces a return to feasibility. Concrete failure with lambda=0.5 and target T: state A has current action a1 reaching T with probability 0.9 and alternative a2 reaching T with probability 0.5 (higher reward); state S has current action b1 going to A with probability 1 and alternative b2 going to A with probability 0.8 and to losing sink L with probability 0.2 (higher reward). Starting from pi0={S:b1, A:a1}, x_A=0.9. Step 5 admits b2 at S because 0.8*0.9=0.72>=0.5, and admits a2 at A because 0.5>=0.5. After both updates, the final policy has x_A=0.5 and x_S=0.8*0.5=0.4<0.5, violating P>=0.5(F T). In the next sweep b2 is no longer valid, but reverting to b1 decreases utility, so Step 7 performs no update and the algorithm terminates with an infeasible policy. Thus Theorem 4.2 fails exactly at the point the reader identifies: local per-action satisfaction does not imply global PCTL feasibility once the satisfaction vector changes.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Algorithm 1, a policy-improvement procedure for MDPs that must satisfy a PCTL constraint P≥λ(ΦUΨ), motivated by Expected Act Utilitarianism from stit logic. It claims (Theorem 4.2) that with ε=0 the algorithm converges to a feasible policy that is a local maximizer of the constrained utility maximization problem (2). The proof rests on four points: feasibility is preserved by a per-action reachability test in Step 5; value is non-decreasing; deterministic policy space is finite; and termination yields a Bellman-optimal policy within the feasible set. The paper also reports experiments on two small MDPs comparing the algorithm with brute-force global optima and studying ε-greedy exploration.","tokens_in":15499,"tokens_out":8543,"duration_ms":88804,"significance":"The problem—maximizing a scalar mission reward under a probabilistic temporal-logic constraint—is timely and the proposed local-search formulation is appealing. If Theorem 4.2 were correct, the algorithm would be a simple bridge between PCTL model checking and policy improvement, with no fitted parameters beyond the exploration rate. However, the central theorem is false: the feasibility test in Step 5 uses stale satisfaction probabilities and does not guarantee that the final policy satisfies the constraint. A concrete two-state counterexample yields an infeasible terminal policy. The claimed contribution therefore does not hold as stated.","major_comments":[{"comment":"The proof of Theorem 4.2 claims feasibility is preserved because Step 5 admits only actions with Y^{(t+1)}(s,a) ≥ λ. This test uses the satisfaction vector x^{(t)} of the policy at the time of the test. When downstream states are updated later, their satisfaction probabilities change, so an action that passed the test can become violating. Concretely, take λ=0.5 and target T, with state A having actions a1 (to T with probability 0.9) and a2 (to T with probability 0.5), and state S having actions b1 (to A with probability 1) and b2 (to A with probability 0.8, to losing sink with probability 0.2). Starting from π0={S:b1, A:a1}, x_A=0.9. If b2 is processed first and passes because 0.8·0.9=0.72≥0.5, and then a2 passes because 0.5≥0.5, the final policy has x_S=0.8·0.5=0.4<0.5. In the next sweep, b2 is invalid but b1 has lower utility, so the algorithm terminates with an infeasible policy. Hence Theorem 4.2's feasibility claim is false, and the algorithm does not solve (2).","section":"Theorem 4.2, proof item (1); Algorithm 1 Steps 4–7"},{"comment":"Step 3 defines x^{(t+1)}_s using x^{(t)}_{s'} on the right-hand side, which is a single Jacobi-like update rather than the solution of the reachability linear system described in the text. The vector x used in Step 4 is therefore not in general the actual satisfaction probability vector of the current policy, so the test Y^{(t+1)}(s,a) ≥ λ does not measure the candidate action's effect on the PCTL formula. This makes the feasibility guarantee in Theorem 4.2 even less supported: even within a single sweep, decisions are made on a stale or approximate x.","section":"Algorithm 1, Step 3"},{"comment":"The algorithm box says 'Set an initial feasible policy π0 arbitrarily', while Section 4.1 states that a feasible policy is first found by computing Pmax(φ). These are inconsistent. If π0 is arbitrary, it need not be feasible, and the proof's first sentence ('the initial policy π0 is feasible by construction') has no basis. If π0 is found by Pmax, the paper does not specify how the corresponding policy is obtained or whether it can be constructed for the general ΦUΨ fragment. The theorem therefore lacks a precise, correct initialization.","section":"Section 4.1 and Algorithm 1 initialization"}],"minor_comments":[{"comment":"There are several typos: 'Marov chain' should be 'Markov chain', 'unocnstrained' should be 'unconstrained', and 'endogeneous' should be 'endogenous'.","section":"Section 2, Section 4.1, Section 3.2"},{"comment":"The notation Y^{(t+1)}(s,a) uses x_{s'} without a superscript; the authors should specify whether x is x^{(t)} or x^{(t+1)}, since the distinction is critical for the correctness of the algorithm.","section":"Algorithm 1, Step 4"},{"comment":"The claim that 'If ε>0 then with probability 1, in the infinite iterations limit, the algorithm eventually visits a globally maximizing policy' is stated without proof. Since the paper explicitly calls this asymptotic result impractical, it should be either proved or removed.","section":"After Theorem 4.2"},{"comment":"The passage discussing the circularity between 'best' and 'maximal utility' is a significant conceptual caveat; it should be explicitly linked to the algorithm's guarantees or clearly declared out of scope for this paper.","section":"Section 3.2"}],"recommendation":"reject","confidential_remarks":"I agree with the reader's assessment: the counterexample is decisive and the central theorem is false. The algorithm would require a fundamentally different feasibility mechanism (e.g., recomputing satisfaction probabilities after each update and rolling back infeasible changes) before the claims could be reconsidered. The self-citations are confined to background and do not affect the outcome."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"What you should know: the main theorem is unsound as stated. Algorithm 1 filters actions by requiring Y(s,a) >= lambda, computed using the previous policy's satisfaction vector x. That local test does not survive later updates to downstream states. The stress-test counterexample is genuine: with lambda=0.5 and states S and A, updating S before A admits b2 because Y(S,b2)=0.8*0.9=0.72, then updating A sets x_A=0.5, pushing x_S to 0.4. The next sweep finds no improving feasible action, so the algorithm terminates at an infeasible policy. The proof's \"by construction\" step in Theorem 4.2 is simply false.\n\nWhat is new and good: the problem is real — enforcing PCTL constraints during policy improvement is a sensible middle ground between reward shaping and automata-based synthesis. The paper is clearly written, the algorithm is easy to understand, and it does not depend on the stit-logic framing, which the authors honestly label as motivation. They also correctly restrict the claim to local optimality. The experiments, though on toy MDPs, illustrate the algorithm's behavior and the exploration trade-off.\n\nWhere the soft spots are: the broken theorem is load-bearing, so the paper reduces to a heuristic plus anecdotal evidence. There is no code or data, and the 100-run counts are presented without error bars. The deontic logic section is long and unused in the main technical result. The novelty over standard action-masking in constrained MDPs is modest, but the PCTL-specific formulation is a fair extension.\n\nWho this is for: researchers in safe RL and formal methods who want a simple action-filtering method for PCTL reachability constraints. If the theorem could be repaired — say by recomputing the satisfaction vector after each single-state update and only committing when the whole vector stays above lambda, or by using a conservative threshold — the paper would be worth publishing. As it stands, I would not rely on the convergence guarantee.\n\nRecommendation: I would not desk-reject this. The topic is relevant and the counterexample is exactly the kind of thing referees should catch. But I would send it back with a clear requirement: fix Theorem 4.2 or revise the algorithm, and provide code and data. The current version should not be accepted.","headline":"Theorem 4.2 is unsound — the local action-filtering test does not guarantee global feasibility after later updates, so the paper's central guarantee is broken.","tokens_in":16046,"tokens_out":3064,"would_cite":false,"duration_ms":34343,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A PCTL-aware policy improvement algorithm provably converges to a feasible local maximizer of mission utility without leaving the allowed behavior set.","keywords":["deontic constraints","expected act utilitarianism","stit logic","PCTL","constrained policy improvement","reinforcement learning","Markov decision process"],"falsifier":"Construct a small MDP with an upstream state and a downstream state in which the utility-maximizing action at the upstream state changes the transition distribution into the downstream region, lowering the downstream satisfaction probability after a later update. Run Algorithm 1 with $\\varepsilon=0$ from a feasible initial policy and model-check the returned policy against $P_{\\ge\\lambda}(\\Phi U\\Psi)$: if the final policy violates the formula, the step that claims feasibility is preserved by construction has failed.","tokens_in":14912,"feed_emoji":"🤖","tokens_out":9830,"duration_ms":98364,"temperature":0.7,"pith_summary":"This paper tries to establish a practical way to keep a reinforcement-learning agent inside a normative constraint while it maximizes a separate mission reward. The constraint is written as a Probabilistic Computation Tree Logic (PCTL) formula of the form $P_{\\ge\\lambda}(\\Phi U\\Psi)$, and the authors treat it as the content of an Expected Act Utilitarianism obligation, a stit-logic notion in which duties come from expected-utility maximization. Their method is a constrained variant of policy improvement: at each state, only actions whose one-step satisfaction estimate stays above the threshold $\\lambda$ are allowed, and the policy is then improved within that restricted action set. The central claim is Theorem 4.2: with greedy updates ($\\varepsilon=0$) the procedure converges in finitely many steps to a feasible policy that locally maximizes the constrained utility. If true, this would let an agent optimize its mission without ever leaving the behavior class its deontic constraint permits, and without needing to encode the norm as a reward.","feed_headline":"Constrained policy improvement reaches feasible local optima","feed_subtitle":"A PCTL-based action filter provably keeps the agent's policy in the allowed set while greedy updates maximize mission utility.","key_machinery":"The carrying mechanism is the admissible-action filter $C^{(t+1)}(s)=\\{a\\in A(s)\\mid Y^{(t+1)}(s,a)\\ge\\lambda\\}$, where $Y^{(t+1)}(s,a)$ is the probability of satisfying the reachability or constrained-reachability path formula after taking action $a$, evaluated with the previous policy's satisfaction vector. This filter is what distinguishes the algorithm from ordinary policy improvement: it removes the constraint from the objective by removing constraint-violating actions from consideration at each state. The proof combines this filter with two standard ingredients: value-function evaluation and greedy improvement from reinforcement learning, and PCTL model-checking procedures (the $\\mathrm{Prob}_0$ and $\\mathrm{Prob}_1$ sets) used to compute the satisfaction vector.","core_discovery":"On the paper's own terms, the discovery is a policy-improvement step with a feasibility filter. At iteration $t+1$, the algorithm computes the satisfaction vector $x_s$ for the current policy $\\pi_t$, then for every state and action forms $Y^{(t+1)}(s,a)=\\sum_{s'} T(s,a,s')\\, x_{s'}$, the probability that the PCTL path formula will hold after taking action $a$. Only actions with $Y^{(t+1)}(s,a)\\ge\\lambda$ enter the candidate set $C^{(t+1)}(s)$, so every accepted update is claimed to preserve feasibility of the overall policy. With $\\varepsilon=0$, the paper proves that the value function never decreases, that termination follows from the finiteness of deterministic policy space, and that the terminal policy satisfies Bellman optimality restricted to the feasible action sets, hence is a local maximizer of the constrained problem. The same filter is also applied to general PCTL formulas through the standard recursive state-labeling method of PCTL model checking.","pith_inferences":["A natural testable extension is to re-evaluate the full satisfaction vector after each epoch instead of only per-action estimates; this would make the feasibility-preservation claim directly checkable when later updates change downstream satisfaction probabilities.","The same filtering scheme could be applied to other probability-thresholded properties such as bounded until or probabilistic safety, because the method already relies on the recursive PCTL state-labeling construction; whether the convergence proof extends to those classes is open.","The reported sensitivity to $\\varepsilon$ suggests a fixed exploration rate is a bottleneck; an annealed schedule that explores only while the policy is still changing would be a concrete alternative to benchmark.","Before deployment, a practitioner could verify the final policy with an independent PCTL model checker, since local optimality is proven with respect to the algorithm's own feasibility filter rather than the true satisfaction probability of the final policy."],"forward_implications":["With $\\varepsilon=0$, Algorithm 1 terminates after finitely many updates and returns a policy satisfying the Bellman optimality condition restricted to the feasible action sets, i.e., a local maximizer of the constrained utility.","Every intermediate policy is claimed to be feasible for $P_{\\ge\\lambda}(\\Phi U\\Psi)$, so an agent trained this way never acts outside its normative constraint during learning.","For reachability formulas $P_{\\ge\\lambda}(FB)$ and constrained reachability formulas $P_{\\ge\\lambda}(\\Phi U\\Psi)$, no product automaton and no reward encoding of the norm is needed; the constraint enters only through the per-state filter.","With $\\varepsilon>0$ the algorithm escaped local optima in the reported experiments, and in the infinite-iteration limit it would visit a global maximizer with probability 1, though the paper notes this limit is practically brute force."],"supporting_citations":[{"why":"Supplies the EAU/stit-logic semantics and the MDP-to-stit translation that makes PCTL formulas usable as deontic constraints.","marker":"[26]"},{"why":"Establishes the earlier translation of utility-maximizing RL systems into stit obligations that the present constrained-synthesis result extends.","marker":"[25]"},{"why":"Provides PCTL syntax, semantics, and the model-checking machinery (including Prob0/Prob1-style precomputation) used to compute satisfaction probabilities.","marker":"[6]"},{"why":"Supplies the standard policy improvement, value functions, and Bellman optimality framework that Algorithm 1 modifies.","marker":"[28]"},{"why":"Supplies MDP1, the small benchmark example, and the broader probabilistic-satisfaction policy synthesis setting.","marker":"[18]"},{"why":"Supplies MDP2, the grid-world benchmark with probabilistic movement and local-optima traps used in the experiments.","marker":"[17]"}],"fun_headline_variants":["PCTL filter keeps policies feasible while improving utility","Deontic logic meets RL: constrained policy improvement","Feasible policy updates: maximize mission, respect rules","Policy improvement with ethical constraints: local optima","Constrained RL: policy improvement within deontic bounds"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof assumes that checking each updated action against the previous policy's satisfaction probabilities is enough to keep the whole policy feasible, even though later updates at other states can change those same satisfaction probabilities and push the true satisfaction probability below the threshold.","fun_headline_variants_meta":{"raw":{"variants":["PCTL filter keeps policies feasible while improving utility","Deontic logic meets RL: constrained policy improvement","Feasible policy updates: maximize mission, respect rules","Policy improvement with ethical constraints: local optima","Constrained RL: policy improvement within deontic bounds"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000206,"raw_usage":{"total_tokens":1409,"prompt_tokens":970,"completion_tokens":439,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":586,"completion_tokens_details":{"reasoning_tokens":361}},"tokens_in":586,"tokens_out":439,"duration_ms":4707,"temperature":1.0,"reasoning_tokens":361,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:45:26.225353+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a small MDP with an upstream state and a downstream state in which the utility-maximizing action at the upstream state changes the transition distribution into the downstream region, lowering the downstream satisfaction probability after a later update. Run Algorithm 1 with $\\varepsilon=0$ from a feasible initial policy and model-check the returned policy against $P_{\\ge\\lambda}(\\Phi U\\Psi)$: if the final policy violates the formula, the step that claims feasibility is preserved by construction has failed.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the EAU/stit-logic semantics and the MDP-to-stit translation that makes PCTL formulas usable as deontic constraints."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the earlier translation of utility-maximizing RL systems into stit obligations that the present constrained-synthesis result extends."},{"cited_title":"Principles of model checking,","cited_arxiv_id":null,"evidence_quote":"Provides PCTL syntax, semantics, and the model-checking machinery (including Prob0/Prob1-style precomputation) used to compute satisfaction probabilities."},{"cited_title":"Reinforcement Learning: An Introduction,","cited_arxiv_id":null,"evidence_quote":"Supplies the standard policy improvement, value functions, and Bellman optimality framework that Algorithm 1 modifies."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies MDP1, the small benchmark example, and the broader probabilistic-satisfaction policy synthesis setting."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies MDP2, the grid-world benchmark with probabilistic movement and local-optima traps used in the experiments."}],"review_version":1}