REVIEW 4 major objections 4 minor 22 references
Dealing with imperfect information in Strategy Logic
T0 review · 4 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read This paper builds Branching-time Strategy Logic (BSL), proves BSL and SL equiexpressive via linear translations, and obtains Epistemic Strategy Logic (ESL), where uniform, de re, de dicto, and memoryless strategies are expressed in the…
desk verdict Solid perfect-information core (BSL equiexpressive with SL), but the ESL encodings that are supposed to subsume uniform-strategy semantics never constrain complement agents' strategies, so the central subsumption claim fails as stated. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The paper's mechanism has two layers. In BSL, the load-bearing additions are the path quantifier $E$, which ranges over the outcome set $\mathrm{Out}(s,\chi)$ of a partial assignment and so lets a formula inspect several plays generated by the same strategy, and the unbinding operator $(a,?)$, which deletes agent $a$ from the assignment so that all outcomes of that agent's strategy can be compared; the mutual translation $\mathrm{tr}$/$\mathrm{tr}'_A$ shows these additions are syntactic sugar in the perfect-information setting. In ESL, the extra machinery is the set of action propositions $p^a_c$ (one for each agent-action pair, attached to states in the unfolded game), the distributed knowledge operator $D_A$ whose semantics quantify over initial paths equivalent under the intersection of the agents' indistinguishability relations, and the weak-uniformity formula $a\text{-wUniform}$, which at every reachable point of every outcome asserts that agent $a$ knows a single action is being played along all related outcomes. That formula, combined with unbinding and with knowledge operators placed before or after strategy quantifiers, carries the encodings of uniform, de re, de dicto, and memoryless strategies.
What would settle it
Search a small two-agent ICGS for an ESL sentence of the form $\langle x\rangle (a,x)(a\text{-wUniform} \wedge AG\,K_a(a\text{-wUniform} \wedge AFp))$ and an assignment on which it holds even though the chosen strategy is not globally uniform, because some indistinguishable history outside its own outcome receives a different action, while no globally uniform strategy satisfies the sentence. One such example settles the Section 4.3 sufficiency step.
Extended reading notes
Core claim
The central claim is that the strategic side-conditions of imperfect-information games can be internalized in the logic. Theorem 1 states that SL and BSL are equiexpressive: the translation $\mathrm{tr}$ replaces SL's temporal operators by $E$-quantified BSL operators, and the reverse translation $\mathrm{tr}'_A$ simulates every $E$ by existentially quantifying fresh strategies and binding every currently unbound agent, with the parameter $A$ remembering which agents are unbound. On top of BSL, ESL evaluates formulas on initial paths, uses action propositions $p^a_c$ to make chosen actions observable, and interprets $D_A$ via the relation $\sim_A=\bigcap_{a\in A}\sim_a$. The paper proves that a strategy $\sigma$ is weakly uniform for agent $a$ in $\rho$ exactly when the formula $a\text{-wUniform}$, which unbinds all other agents and asserts $AG(\bigvee_{c\in Ac} K_a A X p^a_c)$, holds; de re, de dicto, and memoryless variants are then obtained by placing strategy quantifiers and $D_A$ in different orders around this formula. The upshot is that uniform, de re, de dicto, and memoryless requirements no longer need to be hardwired into the semantics of the strategic quantifier.
Load-bearing premise
The encoding assumes that weak uniformity, which checks only the outcomes of the strategy being evaluated, can be extended to genuine global uniformity for simple objectives, and that repeating the weak-uniformity formula after each knowledge operator handles harder objectives; the paper argues this informally in Section 4.3 and gives no proof.
Editorial extensions
If this is right
- BSL inherits SL's complexity profile: its model-checking problem is nonelementary decidable and its satisfiability problem is $\Sigma^1_1$-hard, so the new operators are free in expressivity and worst-case cost.
- A single ESL formula family replaces the semantic variants of ATL-style logics: the uniform, de dicto, and de re readings of 'coalition $A$ can force $Fp$' differ only in where the quantifiers and knowledge operators sit.
- The paper's encoding of memorylessness via an artificial agent related by 'same last state' gives a template for expressing other strategy restrictions in the language instead of in the model.
- The authors state that model checking ESL is certainly undecidable with perfect-recall relations and several agents, so the generality of ESL comes with a worst-case price in the imperfect-information setting.
Reading between the lines
- A formal proof of the Section 4.3 sufficiency claim would let one define a syntactic fragment of ESL in which one uniformity conjunct per knowledge operator guarantees full uniformity; without it, the subsumption claim rests on an informal argument.
- The BSL/SL equivalence suggests that path quantifiers and unbinding are safe additions in perfect information, so the real payoff of the design is as scaffolding for epistemic extensions; a similar operator pair might lift other first-class-object logics to imperfect information.
- The action-proposition technique could likely be turned into a direct translation from a wide range of epistemic ATL variants into ESL, making the 'subsumes most logics' statement checkable formula by formula.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes an extension of Strategy Logic (SL) designed to handle imperfect information. It first introduces BSL, a branching-time version of SL with a path quantifier and an unbinding operator, and claims that BSL is equiexpressive with SL via linear translations. It then adds action propositions and distributed-knowledge operators to obtain ESL, and argues that ESL can express properties of strategies that are usually hardwired into the semantics, such as uniformity, de re and de dicto strategy quantifiers, and memorylessness. The paper therefore claims that ESL subsumes most existing epistemic strategic logics with imperfect information.
Significance. If the claims are correct, the paper offers a genuinely useful conceptual contribution: instead of fixing uniformity or other strategy constraints in the semantics, one can state them in the object language, which would unify several existing logics. The BSL-versus-SL equiexpressivity result, with translations in both directions, is also interesting and potentially reusable. The paper also gives concrete formulas for de re and de dicto readings of an ATL-style formula, which makes the proposal falsifiable. However, the manuscript as written has several load-bearing gaps: a type error in the definition of weak uniformity, an encoding of the basic ATL semantics that omits uniformity requirements for complement agents, and multiple central results stated without proof.
major comments (4)
- [§4.2, Definition 3] Definition 3 is ill-typed. It says that for an initial path ρ, a strategy σ is weakly uniform if, for all initial paths ρ′ ∈ Out(ρ, [a ↦ σ]) and ρ′′ ∈ Paths∗ with ρ′ ∼a ρ′′, σ(ρ′) = σ(ρ′′). But Out(ρ, [a ↦ σ]) is defined as the set of infinite paths extending ρ, so its elements are not initial paths and are not in the domain of a strategy σ. The relation ∼a is also defined only on finite sequences of valuations. This type error affects Propositions 3 and 4, which are precisely the results establishing that a-wUniform and a-wUniform-aux express weak uniformity. The intended meaning is presumably that ρ′ ranges over finite prefixes of outcomes, e.g. ρ′ ∈ Pref(Out(ρ, [a ↦ σ])), but this must be stated and the subsequent propositions re-verified with the corrected definition.
- [§4.3, translation of basic ⟨⟨A⟩⟩Fp] The proposed translation of the basic ATL semantics is not equivalent to the standard semantics from [15]. The displayed formula only quantifies existentially over strategies for agents in A, binds them, and adds ai-wUniform for those agents. The complement Ag \ A remains unbound, so the path quantifier A in AFp ranges over all completions of the complement agents' strategies, including non-uniform ones. In the standard semantics, all agents' strategies, including those of the complement, are required to be uniform. Concretely, consider agents a and b where a has only action 0, b cannot distinguish any histories, and the transition structure is: from s0, b chooses L to sL or R to sR; from sL, b chooses L to win(p) or R to lose; from sR, b chooses R to win(p) or L to lose. Every uniform b-strategy (always L or always R) leads to a state satisfying p, so standard ⟨⟨{a}⟩⟩Fp holds. But the paper's translation evaluates AFp under an assignment that leaves b unbound, and the non-uniform b-strategy 'L at s0, R at sL' produces a losing path, so the translation returns false. A faithful encoding would need to universally quantify over complement strategies and add the uniformity condition for each complement agent as well. This flaw directly undermines the paper's claim to subsume prior ATL-based logics with imperfect information.
- [§3.3 and §4.3, Lemma 1 and Propositions 3 and 4] Lemma 1 in Section 3.3 and Propositions 3 and 4 in Section 4.3 are stated without proof, but they are load-bearing. Lemma 1 is needed for Proposition 2 and hence for the reverse direction of Theorem 1, the main equiexpressivity result. Propositions 3 and 4 are what connect the syntactic formula a-wUniform with the semantic notion of weak uniformity, and they underwrite all the translations in Section 4.3. The note that some proofs are omitted by lack of space is not sufficient for these central claims; the full proofs should be supplied or the claims should be clearly marked as conjectural.
- [Abstract and Conclusion] The paper claims that ESL 'subsumes most, if not all, the variants of epistemic strategic logics with imperfect information that we know about,' but the evidence provided is only the translation of a single ATL-style formula, not a general embedding of any of those logics. Moreover, the paragraph after the de re translation acknowledges that weak uniformity may not be sufficient for objectives involving knowledge, and informally suggests repeating the uniformity formula after knowledge operators, but no formal statement or proof is given. Either a rigorous embedding theorem should be supplied, or the scope of the subsumption claim should be substantially narrowed.
minor comments (4)
- [§3.3, Theorem 1] Theorem 1 says the translations are 'linear in both directions,' but the translation in Definition 2 has complexity O(2^{|Ag|}|φ|). This is linear in the formula size only when the agent set is fixed; the statement should be qualified accordingly to avoid confusion.
- [§2.1] The notation Dc = AcAg is ambiguous; it should be written as Ac^{Ag}, the set of functions from Ag to Ac.
- [Abstract and Introduction] There are several typographical errors, such as 'c an' in the abstract and 'F or' in Section 3.3; a careful proofreading pass is needed.
- [§4.2, semantics of D_A] The relation ∼A is defined on sequences of extended valuations, but the last paragraph of Definition 3 and the semantics of D_A would be clearer if the paper explicitly stated whether the related initial paths must have the same length or may have different lengths; this affects the reading of the knowledge operator.
Circularity Check
No circularity: the BSL/SL equivalence is proved by explicit translations, and the ESL uniformity formulas are direct encodings, not fitted predictions.
full rationale
The main technical result, Theorem 1, is self-contained: Definition 1 gives a syntactic translation from SL to BSL, and Proposition 1 proves it semantics-preserving; Definition 2 gives the inverse translation parameterized by the set of unbound agents, with Lemma 1 and Proposition 2 establishing correctness. Neither translation assumes the target equivalence; each is verified against the independently defined semantics of the source and target logics. The expressibility claims for ESL in Section 4.3 are of the standard 'property P can be encoded by formula φ' form: Definition 3 states the semantic notion of weak uniformity, Definition 4 introduces a formula that mirrors that notion using the knowledge operators, and Propositions 3-4 verify the equivalence. This is an encoding, not a fitted parameter renamed as a prediction; no data or parameter is fitted, and no result is imported from a self-citation. The paper explicitly notes that some proofs are omitted and that the sufficiency of weak uniformity for complex objectives is argued informally; that is a proof gap or correctness risk, not circularity. Since no load-bearing step reduces by construction or by self-citation to its own input, the circularity score is 0.
Assumptions & free parameters
assumptions (4)
- standard math Known complexity results for SL: model checking is nonelementary decidable and satisfiability is Sigma_1^1-hard (Mogavero et al., cited as [18]).
- domain assumption Every CGS can be unfolded so each non-initial state has a unique incoming transition, allowing action propositions p^a_c to label the action just played.
- domain assumption Indistinguishability relations can be arbitrary equivalence relations on finite sequences of valuations, and distributed knowledge is their intersection.
- ad hoc to paper Weak uniformity on the outcomes of a strategy is enough to represent standard global uniformity for simple objectives such as AFp, and repeated uniformity checks after knowledge operators handle harder cases.
Cite this review
Pith. "Pith review of Dealing with imperfect information in Strategy Logic." pith.science (2026). https://pith.science/paper/RCTMFQ5L
@misc{pith2026190802488,
author = {Pith},
title = {Pith review of: Dealing with imperfect information in Strategy Logic},
year = {2026},
howpublished = {\url{https://pith.science/paper/RCTMFQ5L}},
note = {Machine review of arXiv:1908.02488}
}
read the original abstract
We propose an extension of Strategy Logic (SL), in which one can both reason about strategizing under imperfect information and about players' knowledge. One original aspect of our approach is that we do not force strategies to be uniform, i.e. consistent with the players' information, at the semantic level; instead, one can express in the logic itself that a strategy should be uniform. To do so, we first develop a "branching-time" version of SL with perfect information, that we call BSL, in which one can quantify over the different outcomes defined by a partial assignment of strategies to the players; this contrasts with SL, where temporal operators are allowed only when all strategies are fixed, leaving only one possible play. Next, we further extend BSL by adding distributed knowledge operators, the semantics of which rely on equivalence relations on partial plays. The logic we obtain subsumes most strategic logics with imperfect information, epistemic or not.
Reference graph
Works this paper leans on
-
[15]
Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003) , pp
Wojtek Jamroga (2003): Some remarks on alternating temporal epistemic logic . Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003) , pp. 133–140
work page 2003
-
[1]
Henzinger & Orna Kupferman (2002) : Alternating-time tem- poral logic
Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002) : Alternating-time tem- poral logic . J. ACM 49(5), pp. 672–713, doi:10.1145/585265.585270. Availabl e at http://doi.acm.org/10.1145/585265.585270
arXiv 2002
-
[2]
Francesco Belardinelli (2014): Reasoning about Knowledge and Strategies: Epistemic Strat egy Logic. In: SR, pp. 27–33. Available at http://dx.doi.org/10.4204/EPTCS.146.4
-
[3]
Francesco Belardinelli (2015): A Logic of Knowledge and Strategies with Imperfect Informat ion. In: Private communication
work page 2015
-
[4]
Bulletin of Economic Research 53(4), pp
Johan van Benthem (2001): Games in Dynamic-Epistemic Logic . Bulletin of Economic Research 53(4), pp. 219–248, doi:10.1111/1467-8586.00133
arXiv 2001
-
[5]
Johan van Benthem (2011): Logical dynamics of information and interaction . Cambridge University Press
work page 2011
-
[6]
In: Proceedings of SR 2014, pp
Dietmar Berwanger & Anup Basil Mathew (2014): Games with recurring certainty . In: Proceedings of SR 2014, pp. 91–96, doi:10.4204/EPTCS.146.12
-
[7]
Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics
R. Bozianu, C. Dima & C. Enea (2013): Model Checking an Epistemic mu-calculus with Synchronous a nd Perfect Recall Semantics. In: TARK’2013. Available at http://arxiv.org/abs/1310.6434
work page Pith review arXiv 2013
Show all 22 references
-
[8]
In: CA V, pp
Petr Cerm´ ak, Alessio Lomuscio, Fabio Mogavero & Aniell o Murano (2014): MCMAS-SLK: A Model Checker for the V erification of Strategy Logic Specification s. In: CA V, pp. 525–532. Available at http://dx.doi.org/10.1007/978-3-319-08867-9_34
2014 doi
-
[9]
Henzinger & Nir Piterm an (2010): Strategy logic
Krishnendu Chatterjee, Thomas A. Henzinger & Nir Piterm an (2010): Strategy logic. Inf. Comput. 208(6), pp. 677–693, doi:10.1016/j.ic.2009.07.004. Avai lable at http://dx.doi.org/10.1016/j.ic.2009.07.004
2010 doi
-
[10]
Halpern, Y oram Moses & Moshe Y
Ronald Fagin, Joseph Y . Halpern, Y oram Moses & Moshe Y . Vardi (1995): Reasoning about knowledge . 4, MIT press Cambridge
1995
-
[11]
Halpern, Ron van der Meyden & Moshe Y
Joseph Y . Halpern, Ron van der Meyden & Moshe Y . V ardi (20 04): Complete Axiomatizations for Reasoning about Knowledge and Time . SIAM J. Comput. 33(3), pp. 674–703. Available at http://dx.doi.org/10.1137/S0097539797320906
-
[12]
van der Hoek & M
W . van der Hoek & M. Wooldridge (2003): Cooperation, knowledge, and time: Alternating-time Tempo ral Epistemic Logic and its applications . Studia Logica 75(1), pp. 125–157, doi:10.1023/A:1026185103185
2003 doi
-
[13]
Jamroga & T
W . Jamroga & T. ˚Agotnes (2006): What agents can achieve under incomplete information . In: Proceedings of the fifth international joint conference on Autonomous ag ents and multiagent systems, ACM, pp. 232–234
2006
-
[14]
Wojciech Jamroga & Wiebe van der Hoek (2004): Agents that Know How to Play . Fundam. Inform. 63(2-3), pp. 185–219. Available at http://iospress.metapress.com/content/xh738axb47d8rchf/
2004
-
[16]
In: Proceedings Fourth International Symposium on Games, Automata, Logics and Formal V erification, GandALF 2013, Borca di Cadore, Dolomites, Italy, 29-31th August 2013
Franc ¸ois Laroussinie & Nicolas Markey (2013): Satisfiability of ATL with strategy contexts . In: Proceedings Fourth International Symposium on Games, Automata, Logics and Formal V erification, GandALF 2013, Borca di Cadore, Dolomites, Italy, 29-31th August 2013. , pp. 208–223,...
2013 doi
-
[17]
V ardi (2012):What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic
Fabio Mogavero, Aniello Murano, Giuseppe Perelli & Mos he Y . V ardi (2012):What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic . In: CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, Septembe r 4-7, 2012. Pro...
2012 doi
-
[18]
V ardi (2014):Reasoning About Strategies: On the Model-Checking Problem
Fabio Mogavero, Aniello Murano, Giuseppe Perelli & Mos he Y . V ardi (2014):Reasoning About Strategies: On the Model-Checking Problem . ACM Trans. Comput. Log. 15(4), pp. 34:1–34:47, doi:10.1145/2631917. Available at http://doi.acm.org/10.1145/2631917. 12 Dealing with imperfec...
2014 doi
-
[19]
V ardi (2010): Reasoning About Strategies
Fabio Mogavero, Aniello Murano & Moshe Y . V ardi (2010): Reasoning About Strategies . In: IARCS An- nual Conference on Foundations of Software Technology and T heoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India , pp. 133–144, doi:10.4230/LIPIcs.FST...
2010 doi
-
[20]
Pnueli & R
A. Pnueli & R. Rosner (1989): On the Synthesis of a Reactive Module . In: POPL’89, pp. 179–190, doi:10.1145/75277.75293. Available at http://doi.acm.org/10.1145/75277.75293
1989
-
[21]
Reif (1984): The complexity of two-player games of incomplete informati on
John H. Reif (1984): The complexity of two-player games of incomplete informati on. Journal of computer and system sciences 29(2), pp. 274–301, doi:10.1016/0022-0000(84)90034-5
1984 doi
-
[22]
Electronic Notes in Theoretical Computer Science 85(2), pp
Pierre-Yves Schobbens (2004): Alternating-time logic with imperfect recall . Electronic Notes in Theoretical Computer Science 85(2), pp. 82–93
2004
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.