Probabilistic Strategy Logic with Degrees of Observability

Brian Logan; Chunyan Mu; Natasha Alechina; Nima Motamed

REVIEW 2 major objections 5 minor 41 references

Probabilistic Strategy Logic with Degrees of Observability

T0 review · 2 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read The paper introduces observability operators for probabilistic strategy logic and proves model checking remains decidable under memoryless strategies.

desk verdict 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. read the letter →

arxiv 2412.15135 v3 pith:CXW2V5GF submitted 2024-12-19 cs.AI cs.LO

Chunyan Mu , Nima Motamed , Natasha Alechina , Brian Logan This is my paper · ORCID

classification cs.AIcs.LO MSC 03B7068Q60

keywords probabilisticstrategylogicopacityobservabilitymodelcheckingmulti-agentsystemsrealarithmeticpartiallyobservableinformationtransparency

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

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.

What carries the argument

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.

What would settle it

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'.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

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

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.

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.

Desk Editor's Note

read the 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.

The 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.

The 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.

Who 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.

Referee Report

2 major / 5 minor

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.

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 (2)

[Appendix A, 'Degree of observability terms' (Eqn_{Dβ,i(Φ),s})] 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 5.2 vs. Appendix B] 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.

minor comments (5)

[Section 4, Definition 6] 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.
[Appendix A, Eqn_{τ^{-1},s}] 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 2 and bibliography] 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.
[Abstract and Section 1] 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 5.2] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the oPSL logic, semantics, and real-arithmetic reduction are defined from scratch; the only self-citation (Mu and Pang) is background, not load-bearing. The zero-denominator mismatch in Appendix A is a correctness issue, not circularity.

full rationale

The central derivation is self-contained. The paper introduces the syntax and semantics of oPSL from first principles, including the new observability operator and degree-of-observability term, and then gives an inductive translation into real arithmetic. The decidability argument rests on standard external results: Büchi/Rabin/Streett automata constructions, Safra determinization, PCTL* product-Markov-chain reasoning, and Renegar/Basu decidability of the first-order theory of the reals. The proof claims aφ,s holds iff s ⊩ φ, and this equivalence is constructed directly from the semantics rather than imported from the authors' prior work. The only self-citation is [20] (Mu and Pang), which appears in the related-work section to contrast an earlier PATL opacity framework with the proposed PSL-based one; it is not used to justify Theorem 1 or Theorem 2. The skeptical issue about the encoding of Dβ,i(Φ) is real but is an internal correctness bug, not circularity: Definition 7 states that comparisons involving Dβ,i(Φ) are false by default when the denominator evaluates to 0, whereas the Appendix's Eqn Dβ,i(Φ),s sets rDβ,i(Φ) ≈ 1 when rPβ(Φ) ≈ 0, potentially making Dβ,i(Φ)=1 satisfiable in real arithmetic when the oPSL semantics declares it false. That would break the claimed equivalence and hence the proof of Theorem 1 as written, but the flaw is a mismatch between a stipulated semantic convention and its encoding, not a round-trip in which the conclusion is assumed in the premise. No fitted parameter is renamed as a prediction, no uniqueness theorem from the authors is invoked, and no ansatz is smuggled in via self-citation. The paper's central contribution remains independently derived content, so the circularity score is low despite the technical gap.

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

The paper introduces no fitted parameters and no invented entities. Its central claim rests on standard results in real algebraic geometry and automata theory, plus one domain-specific semantic convention. The main weakness is that the encoding of the division-by-zero convention for the degree operator is inconsistent with the semantics.

assumptions (5)

standard math The first-order theory of real arithmetic is decidable in exponential space with respect to the number of quantifiers.
Used in Section 5.1 and Appendix B to conclude decidability of the constructed real arithmetic formulas.
standard math Every LTL formula can be translated to a nondeterministic Büchi automaton and to a deterministic Rabin or Streett automaton.
Used throughout Section 5 and Appendix A for the automata constructions.
standard math Safra's determinization construction converts a nondeterministic Büchi automaton into a deterministic Rabin automaton.
Used in the B-construction in Appendix A to determinize the NBA for observational equivalence.
standard math In a finite Markov chain, a random walk reaches a terminal strongly connected component with probability 1, and acceptance probabilities can be computed by solving linear reachability equations.
Used in the product Markov chain construction for Pβ(Φ) and Dβ,i(Φ) in Appendix A.
domain assumption Formulas containing an undefined arithmetic term (such as division by zero) are false by convention.
Inherited from PSL and stated in Section 4; this convention is load-bearing for the semantics of D terms when the denominator is zero, but the encoding in Appendix A does not respect it.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Probabilistic Strategy Logic with Degrees of Observability." pith.science (2026). https://pith.science/paper/CXW2V5GF

@misc{pith2026241215135,
  author       = {Pith},
  title        = {Pith review of: Probabilistic Strategy Logic with Degrees of Observability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CXW2V5GF}},
  note         = {Machine review of arXiv:2412.15135}
}

read the original abstract

There has been considerable work on reasoning about the strategic ability of agents under imperfect information. However, existing logics such as Probabilistic Strategy Logic are unable to express properties relating to information transparency. Information transparency concerns the extent to which agents' actions and behaviours are observable by other agents. Reasoning about information transparency is useful in many domains including security, privacy, and decision-making. In this paper, we present a formal framework for reasoning about information transparency properties in stochastic multi-agent systems. We extend Probabilistic Strategy Logic with new observability operators that capture the degree of observability of temporal properties by agents. We show that the model checking problem for the resulting logic is decidable.

Figures

Figures reproduced from arXiv: 2412.15135 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

41 extracted references · 40 canonical work pages

[1]

˚Agotnes, T.: Action and knowledge in alternating-time temporal logic. Synth. 149(2), 375–407 (2006)

work page 2006
[2]

Information Security and Cryp- tography, Springer (2020)

Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: The Science of Quantitative Information Flow. Information Security and Cryp- tography, Springer (2020)

work page 2020
[3]

In: IJCAI

Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., Rubin, S.: Probabilistic strategy logic. In: IJCAI. pp. 32–38 (2019) 16 C. Mu, N. Motamed, N. Alechina, B. Logan

work page 2019
[4]

In: Dastani, M., Sichman, J.S., Alechina, N., Dignum, V

Ballot, G., Malvone, V., Leneutre, J., Laarouchi, Y.: Strategic reasoning under capacity-constrained agents. In: Dastani, M., Sichman, J.S., Alechina, N., Dignum, V. (eds.) Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024. pp. 123–131. International Foundation for Autonomous Agents and Multiagent Sys...

work page 2024
[5]

CoRR abs/1409.1534 (2014), http://arxiv.org/abs/1409.1534

Basu, S.: Algorithms in real algebraic geometry: A survey. CoRR abs/1409.1534 (2014), http://arxiv.org/abs/1409.1534

arXiv 2014
[6]

In: AAMAS

Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with imperfect information and public actions. In: AAMAS. pp. 1268–

work page
[7]

Artificial Intelligence 285, 103302 (2020)

Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with public actions against strategy logic. Artificial Intelligence 285, 103302 (2020)

work page 2020
[8]

ACM Trans

Berthon, R., Maubert, B., Murano, A., Rubin, S., Vardi, M.Y.: Strategy logic with imperfect information. ACM Trans. Comput. Log. 22(1), 5:1–5:51 (2021)

work page 2021

Show all 41 references

[9]

In: Sankaranarayanan, S., Sharygina, N

Beutner, R., Finkbeiner, B.: Autohyper: Explicit-state model checking for hyper- ltl. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Join...

2023
[10]

In: LICS

Br´ azdil, T., Brozek, V., Forejt, V., Kucera, A.: Stochastic games with branching- time winning objectives. In: LICS. pp. 349–358. IEEE Computer Society (2006)

2006
[11]

In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S.A

Bryans, J.W., Koutny, M., Mazar´ e, L., Ryan, P.Y.A.: Opacity generalised to tran- sition systems. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S.A. (eds.) Formal Aspects in Security and Trust, Third International Workshop, F AST 2005, Newcastle upon Tyne, UK, ...

2005
[12]

Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677–693 (2010)

2010
[13]

In: Lei, J

Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: Lei, J. (ed.) Fourth International Conference on Fuzzy Systems and Knowledge Discovery, FSKD 2007, 24-27 August 2007, Haikou, Hainan, China, Proceedings, Volume 2. pp. 35–39. IEEE...

2007
[14]

In: AAMAS

Ferrando, A., Malvone, V.: Towards the verification of strategic properties in multi- agent systems with imperfect information. In: AAMAS. pp. 793–801. ACM (2023)

2023
[15]

Goranko, V., Jamroga, W.: Comparing semantics of logics for multi-agent systems. Synth. 139(2), 241–280 (2004)

2004
[16]

In: AAAI

Huang, X., Su, K., Zhang, C.: Probabilistic alternating-time temporal logic of incomplete information and synchronous perfect recall. In: AAAI. AAAI Press (2012)

2012
[17]

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based proba- bilistic model checking for concurrent stochastic games. In: FM. Lecture Notes in Computer Science, vol. 11800, pp. 298–315. Springer-Verlag (2019)

2019
[18]

International Journal on Software Tools for Technology Transfer 19(1), 9–30 (2017)

Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer 19(1), 9–30 (2017)

2017
[19]

In: Larson, K., Winikoff, M., Das, S., Durfee, E.H

Malvone, V., Murano, A., Sorrentino, L.: Hiding actions in multi-player games. In: Larson, K., Winikoff, M., Das, S., Durfee, E.H. (eds.) Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017. pp. 1205–1213. ACM (2017) Probabilistic Strateg...

2017
[20]

In: ECAI

Mu, C., Pang, J.: On observability analysis in multiagent systems. In: ECAI. Fron- tiers in Artificial Intelligence and Applications, vol. 372, pp. 1755–1762 (2023)

2023
[21]

preliminaries

Renegar, J.: On the computational complexity and geometry of the first-order the- ory of the reals, part I: introduction. preliminaries. the geometry of semi-algebraic sets. the decision problem for the existential theory of the reals. J. Symb. Comput. 13(3), 255–300 (1992)

1992
[22]

In: van der Hoek, W., Lomuscio, A., de Vink, E.P., Wooldridge, M.J

Schobbens, P.: Alternating-time logic with imperfect recall. In: van der Hoek, W., Lomuscio, A., de Vink, E.P., Wooldridge, M.J. (eds.) 1st International Workshop on Logic and Communication in Multi-Agent Systems, LCMAS 2003. Electronic Notes in Theoretical Computer Science, v...

2003
[23]

DΦ(q1, {φ ∈ Max(Φ) | s1 ⊩ φ}, q2)
[24]

D¬Φ(q′ 1, {φ ∈ Max(Φ) | s′ 1 ⊩ φ}, q′ 2)
[25]

If obsk(α2, s2) = obsk(α′ 2, s′ 2), then b2 = b1
[26]

For the first path, we keep track of the corresponding state of AΦ; for the second, we keep track of A¬Φ

If obsk(α2, s2) ̸= obsk(α′ 2, s′ 2), then b2 = 0 Intuitively, walks through the graph consist of two paths in M. For the first path, we keep track of the corresponding state of AΦ; for the second, we keep track of A¬Φ. At the same time, we keep track of a bit b ∈ 2 that expres...
[27]

=⇒ b1=b2 ∧ ⊤obsk(α2,s2)̸=obsk(α′ 2,s′
[28]

So we need to be able to express reachability

=⇒ b2=0 Next, we need to express that there exist some vertex v ∈ F⊙kΦ that is reachable from the root, and that has a non-empty path back to itself. So we need to be able to express reachability. To do this efficiently, we use the method well-known from second-order logic: a ...
[29]

There is α′ ∈ ActAg such that T (s′ 1, α′)(s′
[30]

> 0, and obsi(α, s2) = obsi(α′, s′ 2)
[31]

The set F NBA obsi¬Φ of accepting states is defined as F NBA obsi¬Φ := S × S × F¬Φ

D¬Φ(q1, {φ ∈ Max(Φ) | s′ 1 ⊩ φ}, q2) So transitions follow the symbol on the first M-state, and guess some observa- tionally equivalent transition from the second M-state, while also transitioning the original NBA for the second state. The set F NBA obsi¬Φ of accepting states ...

2002
[33]

There is at least one ( t, t′, q) ∈ K T v such that v has no child w with (t, t′, q) ∈ K T w
[34]

The DRA ADRA obsi¬Φ = ( QDRA, δDRA, qDRA ∗ , AccDRA) is defined as follows

For all distinct children w ̸= u of v, it holds that K T w ∩ K T u = ∅. The DRA ADRA obsi¬Φ = ( QDRA, δDRA, qDRA ∗ , AccDRA) is defined as follows. Its state space QDRA is the set of Safra trees. The initial state qDRA ∗ is the Safra tree with the single node 1, labelled with ...
[35]

The mark ‘!’ is removed from all nodes in T that contain it
[36]

The macrostate of w is set to be K ∩ F NBA obsi¬Φ

For every node v ∈ N with macrostate K such that K ∩ F NBA obsi¬Φ ̸= ∅, a new node w ∈ V \N is added, and is made the new last child ofv. The macrostate of w is set to be K ∩ F NBA obsi¬Φ
[37]

For every node v, its macrostate K is replaced by the new macrostate {(t2, t′ 2, q2) ∈ S×S×Q¬Φ | DNBA obsi¬Φ((t1, t′ 1, q1), (α, t), (t2, t′ 2, q2)) for some (t1, t′ 1, q1) ∈ K}
[38]

For every node v with macrostate K, and all states ( t, t′, q) ∈ K such that v has an earlier sibling whose macrostate includes ( t, t′, q), we remove (t, t′, q) from the macrostate of v
[39]

We remove all nodes with empty macrostates
[40]

For every node v such that its macrostate is equal to the union of the macrostates of its children, we remove all nodes descended from v, and place the mark ‘!’ on v. The Rabin acceptance condition AccDRA is defined to be AccDRA := {(Ev, Fv) | v ∈ V }, with Ev being the set of...
[41]

Algorithms in Real Algebraic Geometry

to (s2, q2, q′ 2) in the product Markov chain. The formula Prodβ again expresses this, with auxiliary binary variables rTr,AΦ q1,(α,t),q2 and r Tr,Aobsi Φ q′ 1,(α,t),q′ 2 which will numerically hold the truth value of the corresponding transition-formulas. Prodβ := ∃ rTr,AΦ q1...

2006
[2500]

https://doi.org/10.1007/3-540-36387-4_3 Probabilistic Strategy Logic with Degrees of Observability 27 is twice as many symbols as the amount of states in our NBA)

Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36387-4_3 Probabilistic Strategy Logic with Degrees of Observability 27 is twice as many symbols as the amount of states in our NBA). By ordered tree, we mean a tree in which the children of every node carry some line...

doi

Pith tools

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

[1] [1]

˚Agotnes, T.: Action and knowledge in alternating-time temporal logic. Synth. 149(2), 375–407 (2006)

work page 2006

[2] [2]

Information Security and Cryp- tography, Springer (2020)

Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: The Science of Quantitative Information Flow. Information Security and Cryp- tography, Springer (2020)

work page 2020

[3] [3]

In: IJCAI

Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., Rubin, S.: Probabilistic strategy logic. In: IJCAI. pp. 32–38 (2019) 16 C. Mu, N. Motamed, N. Alechina, B. Logan

work page 2019

[4] [4]

In: Dastani, M., Sichman, J.S., Alechina, N., Dignum, V

Ballot, G., Malvone, V., Leneutre, J., Laarouchi, Y.: Strategic reasoning under capacity-constrained agents. In: Dastani, M., Sichman, J.S., Alechina, N., Dignum, V. (eds.) Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024. pp. 123–131. International Foundation for Autonomous Agents and Multiagent Sys...

work page 2024

[5] [5]

CoRR abs/1409.1534 (2014), http://arxiv.org/abs/1409.1534

Basu, S.: Algorithms in real algebraic geometry: A survey. CoRR abs/1409.1534 (2014), http://arxiv.org/abs/1409.1534

arXiv 2014

[6] [6]

In: AAMAS

Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with imperfect information and public actions. In: AAMAS. pp. 1268–

work page

[7] [7]

Artificial Intelligence 285, 103302 (2020)

Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of multi-agent systems with public actions against strategy logic. Artificial Intelligence 285, 103302 (2020)

work page 2020

[8] [8]

ACM Trans

Berthon, R., Maubert, B., Murano, A., Rubin, S., Vardi, M.Y.: Strategy logic with imperfect information. ACM Trans. Comput. Log. 22(1), 5:1–5:51 (2021)

work page 2021