{"id":"7c15e331-5be4-4daf-bf6c-9339afa872ce","arxiv_id":"2412.15135","paper_version":3,"verdict":"REJECT","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper introduces oPSL, an extension of Probabilistic Strategy Logic with observability and degree-of-observability operators, and claims a decidable model checking problem with 3EXPSPACE complexity.","lead":"This paper defines a new logic called oPSL that extends Probabilistic Strategy Logic with operators for measuring how observable a property is to an agent, and it claims that checking formulas in this logic is decidable. If the proof is correct, it would give a formal tool for reasoning about information transparency and potential data leakage in stochastic multi-agent systems.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The real-arithmetic encoding of Dβ,i(Φ) violates the zero-denominator convention: with Pβ(Φ)=0 it sets rD=1, so comparisons like D=1 become true where semantics is false; Theorem 1's proof fails as written.","rationale":"I read the paper as extending Probabilistic Strategy Logic with observability and degree-of-observability operators, with the central claim being decidability of model checking for memoryless strategies. The proof is a reduction to the first-order theory of the reals. Many components of the reduction are standard: the use of Rabin/Streett automata, the product Markov chain construction, and the reachability/linear-equation encoding are all plausible. However, the reduction's correctness rests on the exact equivalence between oPSL satisfaction and the truth of the generated real-arithmetic formula. That equivalence is broken by the explicit clause in Appendix A that sets rDβ,i(Φ) ≈ 1 when rPβ(Φ) ≈ 0, because Definition 7's zero-denominator convention makes every comparison involving such a Dβ,i(Φ) term false. This is not a subtle philosophical disagreement or a matter of external consensus; it is an internal mismatch between the semantics and the encoding. The bug is easy to demonstrate with an unsatisfiable Φ, and it invalidates the proof of Theorem 1 as written. The reader's weakest-assumption analysis identified exactly this issue, and I agree with that assessment. I therefore recommend keeping the reader's REJECT verdict. A corrected encoding that guards the whole inequality against zero denominators could plausibly salvage the result, but that is not the paper as written.","tokens_in":23396,"tokens_out":7560,"duration_ms":69704,"concrete_test":"Apply the Appendix's translation to a one-agent, one-state POMAS with formula φ = ∃x.(D_{[1↦x],1}(p∧¬p) = 1), where β(1)=x and Φ=p∧¬p. Semantics: Pβ(Φ)=0 for every strategy, so by the zero-denominator convention φ is false. Run the reduction; because Eqn D sets rD≈1 when rP≈0, the generated real-arithmetic sentence is satisfiable, so the algorithm would report 'true'. If it does, Lemma A.1 (aφ,s iff s⊩φ) is disproved. Then patch the encoding by replacing the zero-denominator clause with a guard that makes the whole inequality false, and re-run; a correct reduction should report 'false'.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing point is the correctness of the reduction from oPSL to real arithmetic, specifically the handling of Dβ,i(Φ) when its denominator is zero. In Definition 7 the authors state a convention: for every formula τ ▷◁ τ′ containing a subterm Dβ,i(Φ) whose denominator evaluates to 0, the formula is false by default. The Appendix's encoding does not implement this. Its Eqn Dβ,i(Φ),s is satisfiable with rDβ,i(Φ) ≈ 1 when rPβ(Φ) ≈ 0. Consequently the inequality Dβ,i(Φ) = 1 is encoded as true under any valuation making Pβ(Φ)=0, even though the oPSL semantics declares it false. Concretely, take a one-agent POMAS and the sentence ∃x. (D_{[1↦x],1}(p∧¬p) = 1); since every path has Φ-probability 0, the semantic value is undefined and the sentence is false by the convention, but the real-arithmetic translation is satisfiable. Thus the claimed equivalence aφ,s iff s ⊩ φ, which is the core of the proof of Theorem 1, fails. The decidability theorem is therefore not established by the paper's argument; Theorem 2 inherits the gap. This is an internal inconsistency, not a matter of disagreeing with a consensus, and it is localized and fixable, but a corrected proof is required.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces oPSL, an extension of Probabilistic Strategy Logic with an observability operator ⊙iΦ and a degree-of-observability term Dβ,i(Φ), interpreted over partially observable stochastic multi-agent systems (POMASs). The semantics defines Dβ,i(Φ) as the conditional probability that a Φ-path is not observationally equivalent, for agent i, to a ¬Φ-path, and adopts the convention that any comparison containing a zero-denominator D-term or inverse term is false by default. The main results are Theorem 1, stating that model checking oPSL sentences under memoryless strategies is decidable, and Theorem 2, giving 3EXPSPACE complexity in the sentence and 2EXPSPACE in the system. The decidability proof works by translating oPSL satisfaction into the first-order theory of real arithmetic, with a detailed Appendix that encodes strategies, Büchi/Rabin/Streett automata, Safra determinization, product Markov chains, and reachability probabilities inside the arithmetic formula.","tokens_in":23689,"tokens_out":7960,"duration_ms":73540,"significance":"The intended contribution is significant: opacity-style hyperproperties have not previously been integrated with probabilistic strategy logic, and a decidable fragment with memoryless strategies would be a useful tool for reasoning about information transparency, privacy, and security in multi-agent systems. The real-arithmetic reduction is a natural and potentially robust approach, and the paper contains an unusually detailed automata-theoretic construction, including an explicit Safra determinization encoded inside the arithmetic formula. The critical flaw identified below is localized to a single equation in the encoding of Dβ,i(Φ); it invalidates the proof of Theorem 1 as written, but it appears repairable, so I see this as a major-revision issue rather than a ground for outright rejection.","major_comments":[{"comment":"Definition 7 states that any comparison τ ▷◁ τ′ containing a subterm Dβ,i(Φ) whose denominator evaluates to 0 is false by default. The real-arithmetic encoding, however, contains the conjunct rPβ(Φ) ≈ 0 → rDβ,i(Φ) ≈ 1. Thus, when Pβ(Φ) = 0, the encoding makes Dβ,i(Φ) = 1 true, whereas the oPSL semantics declares every comparison involving that D-term false. Concretely, in a one-agent POMAS, the sentence ∃x. (D_{[1↦x],1}(p∧¬p) = 1) is false by the zero-denominator convention, but the arithmetic translation is satisfiable because Eqn_{Dβ,i(Φ),s} sets rD to 1. This breaks the claimed equivalence aφ,s iff s ⊩ φ, which is the core of the proof of Theorem 1. The fix is not simply to set rD to 0 in the zero-denominator case; the encoding must make the enclosing inequality/equality formula false whenever the denominator vanishes, for example by introducing a definedness predicate that guards every comparison involving Dβ,i(Φ).","section":"Appendix A, 'Degree of observability terms' (Eqn_{Dβ,i(Φ),s})"},{"comment":"The proof sketch of Theorem 2 states that the number of quantifiers in the real-arithmetic formula is 'easily verified to be single exponential w.r.t. the sentence size', while Appendix B states that the number of quantifiers is double exponential, since there is a quantifier for each Safra tree. These claims are contradictory, and the proof of the exact 3EXPSPACE bound depends on which count is correct. The appendix's own count (one quantifier per Safra tree, with the number of Safra trees double exponential in the formula) does yield the stated triple-exponential bound, so this appears to be a local error, but the main text must be corrected to agree with the detailed construction.","section":"Section 5.2 vs. Appendix B"}],"minor_comments":[{"comment":"The grammar for arithmetic terms, τ ::= c | |τ −1 | |τ ⊕ τ | |Pβ(Φ) | |Dβ,i(Φ), contains a doubled separator after c; this is likely a typographical error and should be cleaned up.","section":"Section 4, Definition 6"},{"comment":"The equation rτ × rτ^{-1} ≈ 1 makes Eqn_{τ^{-1},s} unsatisfiable when rτ = 0, which matches the false-by-default convention, but this behavior is not stated. It would be helpful to note explicitly that this is the intended encoding of the zero-denominator rule for inverses.","section":"Appendix A, Eqn_{τ^{-1},s}"},{"comment":"The Safra determinization construction is attributed in a footnote to Roggenbach (2002), but that reference is not listed in the bibliography. Add the full citation.","section":"Section 2 and bibliography"},{"comment":"The abstract announces decidability without mentioning that this holds only under memoryless strategies, although the paper later makes clear that the general problem is undecidable. The abstract should state this restriction to avoid overstating the scope.","section":"Abstract and Section 1"},{"comment":"The phrase 'logarithmic w.r.t. the size of the quantifier-free part' is based on the real-arithmetic decision procedure, but the citation style differs between the main text ([21,5]) and the appendix (Basu, Pollack and Roy). Unify the references and state the exact complexity theorem being cited.","section":"Section 5.2"}],"recommendation":"major_revision","confidential_remarks":"The reader's report correctly identifies the zero-denominator flaw in the encoding of Dβ,i(Φ), and that flaw is real: it invalidates the proof of Theorem 1 as written. I nevertheless recommend major revision rather than rejection, because the flaw is localized to one equation and a definedness-guarded encoding should repair it without changing the overall architecture of the reduction. The other parts of the construction, especially the Safra-based automata encoding, are detailed and generally consistent, so the paper is likely salvageable after a careful revision of the D-term encoding and the complexity discussion."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth your time. It extends Probabilistic Strategy Logic with observability operators (⊙iΦ) and a degree-of-observability term Dβ,i(Φ), and it claims model checking is decidable under memoryless strategies. The logic itself is a real contribution: it gives a way to quantify information transparency in stochastic MAS, which is genuinely missing from the PSL literature. The technical apparatus is also serious — the appendix works through determinization, Safra trees, and real-arithmetic encodings in unusual detail for a conference paper. I believe the authors put real work into this.\n\nThe main theorem, however, does not go through as written. The issue is exactly what the stress-test note flags. Definition 7 says that any formula containing a D term whose denominator evaluates to zero is false by default. But the real-arithmetic encoding in the appendix, Eqn_D, has the clause rPβ(Φ) ≈ 0 → rDβ,i(Φ) ≈ 1. That makes D equal to 1 when the denominator is zero, so a comparison like D = 1 becomes true where the semantics says the formula is false. The concrete counterexample — one agent, Φ = p ∧ ¬p, with Pβ(Φ) = 0 — works. The claimed equivalence aφ,s iff s ⊨ φ fails for such formulas, and Theorem 1 is not proven. Theorem 2 inherits the gap.\n\nThe rest of the construction looks standard: the automata-based translations for Pβ(Φ) and the observability operator follow the usual PCTL* and PSL playbook. The bug is localized and fixable — one could, for instance, add a flag that forces the whole inequality to false when the denominator is zero, or restrict the encoding to the nonzero case and handle zero explicitly. But as it stands, the paper proves decidability of a different logic than the one it defines.\n\nWho is this for? People working in formal verification of multi-agent systems, especially on opacity and information flow, will find the framework and examples useful even with the current flaw. It deserves a serious referee — this is not a desk-reject-level paper. My recommendation is to send it to review, but with a clear request for a corrected zero-denominator encoding and a reworked proof of Theorem 1. If the fix is straightforward, this becomes a solid paper.","headline":"A genuinely new logic and a serious technical effort, but the central decidability proof has a concrete, localized bug in the zero-denominator encoding that needs fixing before the main theorem is established.","tokens_in":24225,"tokens_out":1489,"would_cite":false,"duration_ms":16033,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper introduces observability operators for probabilistic strategy logic and proves model checking remains decidable under memoryless strategies.","keywords":["probabilistic strategy logic","opacity","observability","model checking","multi-agent systems","real arithmetic","partially observable systems","information transparency"],"falsifier":"Take a system and a formula where the probability of $\\Phi$ is zero, and ask whether $D_{\\beta,i}(\\Phi)=1$ holds. The paper's semantics says the comparison is false (the denominator is zero), while the appendix's encoding sets the degree to 1, making the comparison true; a model checker built from the encoding would return 'true' where the semantics says 'false'.","tokens_in":23182,"feed_emoji":"🔍","tokens_out":9886,"duration_ms":77426,"temperature":0.7,"pith_summary":"Information transparency — how much one agent can observe of another's behavior — lies outside the expressive power of Probabilistic Strategy Logic (PSL). This paper introduces Opacity Probabilistic Strategy Logic (oPSL), which adds to PSL a boolean observability operator $\\odot_i\\Phi$ and a real-valued degree-of-observability term $D_{\\beta,i}(\\Phi)$. The central claim is that model checking oPSL sentences under memoryless strategies is decidable, even though full PSL model checking is undecidable. The proof translates every oPSL sentence into a formula in the first-order theory of real arithmetic, whose truth mirrors the sentence's truth, and then appeals to the decidability of that theory. If the translation is correct, quantitative transparency and opacity requirements on stochastic multi-agent systems become algorithmically verifiable.","feed_headline":"Observability-aware strategy logic is decidable","feed_subtitle":"Probabilistic strategy logic gains degree-of-observability operators and a 3EXPSPACE model-checking bound.","key_machinery":"The load-bearing mechanism is a reduction of oPSL model checking to the first-order theory of real arithmetic. Each state formula is replaced by a real-arithmetic formula over variables that encode the agents' strategy distributions and the probabilities of path properties. For the degree-of-observability term, the reduction constructs a deterministic automaton accepting the $\\Phi$-paths, another automaton accepting paths observationally equivalent to $\\neg\\Phi$-paths (built by nondeterministically guessing the equivalent path and then determinizing the resulting automaton), complements the second, forms their product, and then expresses the acceptance probability of the resulting Markov chain as a system of linear equations. The whole construction is written inside the real-arithmetic formula, so decidability of real arithmetic yields the model checking algorithm.","core_discovery":"The paper claims that adding observability operators to Probabilistic Strategy Logic does not destroy decidability, provided strategies are restricted to memoryless ones. The new operators are interpreted over partially observable stochastic multi-agent systems, where each agent sees states and joint actions through an observation function. The full observability operator $\\odot_i\\Phi$ holds when every $\\Phi$-path and every $\\neg\\Phi$-path disagree in agent $i$'s observations; the degree term $D_{\\beta,i}(\\Phi)$ is the conditional probability that a $\\Phi$-path is not observationally equivalent to any $\\neg\\Phi$-path, given that a $\\Phi$-path occurs. The decidability proof works by reducing oPSL model checking to the first-order theory of real arithmetic: each sentence and system state is mapped to a real-arithmetic formula that is satisfiable exactly when the sentence holds at that state. The overall space complexity is triple exponential in the sentence and double exponential in the system.","pith_inferences":["The degree term $D_{\\beta,i}(\\Phi)$ is effectively a per-agent conditional probability of non-opacity, so the logic could serve as a specification language for quantitative information-flow bounds in security and privacy settings.","The encoding technique appears to generalize: any observability equivalence that can be recognized by a nondeterministic automaton could be plugged into the same real-arithmetic reduction, yielding decidability for richer observation models.","The complexity gap between system and formula suggests that, in practice, one should look for fragments of oPSL or classes of systems where the deterministic-automaton blowup can be avoided, e.g., state-only observability."],"forward_implications":["oPSL can express both boolean and quantitative observability properties, such as 'agent 1 has a strategy making $\\Phi$ observable to her against all strategies of the other agents' and 'the degree of observability of $\\Psi$ from agent 1's perspective is at most 0.1, provided $\\Psi$ holds with probability at least 0.9.'","Model checking any oPSL sentence under memoryless strategies terminates with the correct answer, so transparency and opacity requirements can be verified automatically on finite stochastic multi-agent systems.","The decision procedure runs in space triple exponential in the sentence and double exponential in the system, giving an explicit, if high, complexity bound.","Because the proof reduces to real arithmetic, the same approach applies to any extension whose semantics can be encoded by automata and linear equations."],"supporting_citations":[{"why":"Defines Probabilistic Strategy Logic, the base logic whose syntax, semantics, and model-checking reduction oPSL extends.","marker":"[3]"},{"why":"Introduces the opacity framework used to define observability of behaviours.","marker":"[11]"},{"why":"Defines Strategy Logic, the non-probabilistic predecessor that supplies the strategy-quantification mechanism.","marker":"[12]"},{"why":"Treats strategy logic with imperfect information, motivating uniform, observation-based strategies.","marker":"[8]"},{"why":"Proves decidability of the first-order theory of the reals, the target of the model-checking reduction.","marker":"[21]"},{"why":"Provides the real-algebraic-geometry complexity bounds used in the 3EXPSPACE estimate.","marker":"[5]"}],"fun_headline_variants":["Observability degrees added to strategy logic, still decidable","Strategy logic with observability degrees remains decidable","Probabilistic strategy logic gains observability operators, stays decidable","Observability-aware strategy logic is decidable with tight bound"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof assumes that the algebraically encoded degree-of-observability term computes exactly the conditional probability defined by the semantics, including the rule that a comparison whose denominator is zero is false.","fun_headline_variants_meta":{"raw":{"variants":["Observability degrees added to strategy logic, still decidable","Strategy logic with observability degrees remains decidable","Probabilistic strategy logic gains observability operators, stays decidable","Observability-aware strategy logic is decidable with tight bound"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000316,"raw_usage":{"total_tokens":1738,"prompt_tokens":843,"completion_tokens":895,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":459,"completion_tokens_details":{"reasoning_tokens":828}},"tokens_in":459,"tokens_out":895,"duration_ms":5230,"temperature":1.0,"reasoning_tokens":828,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T11:36:19.225449+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a system and a formula where the probability of $\\Phi$ is zero, and ask whether $D_{\\beta,i}(\\Phi)=1$ holds. The paper's semantics says the comparison is false (the denominator is zero), while the appendix's encoding sets the degree to 1, making the comparison true; a model checker built from the encoding would return 'true' where the semantics says 'false'.","supporting_citations":[{"cited_title":"In: IJCAI","cited_arxiv_id":null,"evidence_quote":"Defines Probabilistic Strategy Logic, the base logic whose syntax, semantics, and model-checking reduction oPSL extends."},{"cited_title":"In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S.A","cited_arxiv_id":null,"evidence_quote":"Introduces the opacity framework used to define observability of behaviours."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines Strategy Logic, the non-probabilistic predecessor that supplies the strategy-quantification mechanism."},{"cited_title":"ACM Trans","cited_arxiv_id":null,"evidence_quote":"Treats strategy logic with imperfect information, motivating uniform, observation-based strategies."},{"cited_title":"preliminaries","cited_arxiv_id":null,"evidence_quote":"Proves decidability of the first-order theory of the reals, the target of the model-checking reduction."}],"review_version":1}