Strategies, Credences, and Shannon Entropy: Reasoning about Strategic Uncertainty in Stochastic Environments

1 Introduction

Motivation. In the field of formal reasoning about multiagent systems (MAS), strategic uncertainty plays a critical role in decision-making processes (see [Bulling et al., 2015; ˚Agotnes et al., 2015]). Agents within such systems often need to reason about the outcomes of actions in environments that are not fully observable or deterministic. Therefore, strategic reasoning of individual agents and their groups must account for both incomplete information about their environment and the stochastic nature of this environment when formulating strategic decisions and plans. This requires the development of formal models that allow agents to make strategic decisions despite various layers of uncertainty, and take into account the stochastic behavior of MAS.

Knowledge and information play a vital role in interactions, especially with the rise of the Internet and social networks. Information is both a key resource for strategy formation and often the primary goal of interaction. Agents may act to learn new information or to protect secrets. For example, people seek economic trends, fashion updates, or even the quality of workplace coffee. Such scenarios inherently involve both knowledge and uncertainty. Analyzing probabilistic information is essential in these contexts. By computing the likelihood of outcomes and integrating uncertainty into decision-making, agents can make informed choices in environments where complete knowledge is unattainable.

Logics for strategic uncertainty. Alternating-time temporal logic ATL [Alur et al., 2002]is a widely recognized framework for reasoning about strategic capabilities in MAS. ATL allows for the expression of strategic abilities of groups of agents, where certain outcomes can be guaranteed through cooperative strategies. A probabilistic extension of the logic, PATL [Chen and Lu, 2007; Huang et al., 2012; Belardinelli et al., 2024], enhanced ATL by probabilistic reasoning about the likelihood of achieving certain outcomes, rather than deterministic guarantees.

An important step towards reasoning about strategic uncertainty was made with ATLH [Tabatabaei and Jamroga, 2023]. ATLH extended ATL with modalities based on the Hartley measure [Hartley, 1928a], that can be seen as a nonprobabilistic restriction of Shannon entropy [Shannon, 1948]. However, in scenarios where agents do have beliefs about the likelihoods of events, the information gain from revealing certain facts is intimately related to those likelihoods.

Contribution. To fill this major gap, we consider "PATL with Credences" (PATLC), which is in fact a more general version of PATEL [Huang and Luo, 2013]. PATLC extends Probabilistic ATL by graded epistemic operators K≥q a φ for probabilistic beliefs (or credences), with the intended meaning: "agent a believes that φ holds with probability at least q." In contrast to PATL with binary knowledge, this allows us to incorporate the stochastic behavior of the environment and its influence on the epistemic aspects of strategic reasoning.

Even more importantly, we introduce "PATL with Shannon uncertainty" (PATLH). PATLH is an informationtheoretic extension of PATL that adds quantitative uncertainty modalities based on Shannon entropy - a foundational concept in information theory. By incorporating entropybased reasoning, PATLH allows agents to reason about both their strategic options and their epistemic uncertainty. This is particularly useful in scenarios where agents must either reduce the uncertainty to gain knowledge about specific facts or, conversely, maintain a high level of uncertainty to keep sensitive information hidden from adversaries. The added layer of expressiveness makes PATLH suited, e.g., for reasoning about security and privacy in MAS, where the control of information flow is as important as the control of outcomes. To our best knowledge, this is the first logical formalism that incorporates stochastic aspects of the system directly into strategic reasoning about uncertainty of information flow.

In terms of technical results, we prove that (1) PATLC and PATLH have the same model checking complexity; (2) PATLC is strictly more expressive than PATLH; and conjecture that (3) PATLH is exponentially more succinct than PATLH. Thus, PATLC allows for expressing more properties, but PATLH may offer exponentially shorter encodings for those that it can express. In consequence, the practical verification of PATLH would be often exponentially easier, which makes both logics interesting for applications that require both strategic and information-theoretic reasoning.

Related Work Strategic-epistemic reasoning gained significant attention in the early 2000s, particularly within frameworks like ATEL [van der Hoek and Wooldridge, 2003; ˚Agotnes, 2006; Jamroga and ˚Agotnes, 2007] and DEL [van Ditmarsch et al., 2007; ˚Agotnes and van Ditmarsch, 2008], To the best of our knowledge, the only works that combine logical approaches to strategic reasoning with information-theoretic concepts are [Jamroga and Tabatabaei, 2013; Tabatabaei and Jamroga, 2023], and both concern non-probabilistic interaction. MAS with stochastic interactions has been extensively studied, see e.g. [Hansson and Jonsson, 1994; Chen and Lu, 2007; Huang et al., 2012; Huang and Luo, 2013; Belardinelli et al., 2024]. However, these works did not focus on epistemic or informationtheoretic aspects. A notable exception is [Huang and Luo, 2013] which proposed PATEL, i.e., Probabilistic ATL extended with probabilistic belief operators, and investigated its model checking complexity. Metrics of uncertainty and information gain were introduced by Hartley [Hartley, 1928a] and extended by Shannon [Shannon, 1948]. The latter is commonly used in information security to measure the amount of information leaking to the intruder [Alvim et al., 2020]. An extension of ATL with modalities based on Hartley measure was recently introduced in [Tabatabaei and Jamroga, 2023]. In this paper, we extend this framework to probabilistic concepts and models.

Our main technical results concern the comparison of expressiveness between epistemic and information-theoretic modalities, and the succinctness of information-theoretic modalities based on Shannon entropy. The study of the succinctness of logical representations dates back to the early 1970s [Stockmeyer, 1972]. The relative succinctness of branching-time logics was explored in [Wilke, 1999; Adler and Immerman, 2001; Markey, 2003], while the succinctness of ATL* with past-time operators was studied in [Bozzelli et al., 2020]. The method of proving succinctness using formula size games was first introduced in [Adler and Immerman, 2001], and later generalized in [French et al., 2013b]. In this work, we build on the latter approach, and follow [Tabatabaei and Jamroga, 2023] in establishing our result.

2 Preliminaries

Distributions and Markov Chains. Let X be a finite nonempty set. A probability distribution over X is a function p : X → [0, 1] such that ∑x∈X p(x) = 1, and Dist(X) is the set of probability distributions over X. A Markov Chain M is a tuple (St, p) where St is a nonempty set of states and p ∈ Dist(St × St) is a distribution. The values p(s, t) are transition probabilities of M denoting the likelihood of a transition from s to t. A path is an infinite sequence of states.

Stochastic iCGS. Stochastic Imperfect Information Concurrent Game Structures (Stochastic iCGS, or SiCGS) extend the well-known Concurrent Game Structures [Alur et al., 2002] to allow for both imperfect information and stochastic transitions. Formally, a Stochastic iCGS is a tuple G = (Agt, St,Act, d, δ, {∼a}a∈Agt), where Agt is a finite set of agents, St is a finite set of states, Act is a finite set of actions, d : Agt×St → 2Act \{∅} is a function defining the available actions for each agent in each state, δ : St ×Act n →D(St) is a stochastic transition function (where D(St) denotes the set of probability distributions over St) that gives the (conditional) probability δ(s, c) of a transition from state s for all s′ ∈ St if each player a ∈ Agt plays the action ca (we also write this probability as δ(s, c)(s′ ) to emphasize that δ(s, c) is a probability distribution on St), and ∼a⊆ St × St for each a ∈ Agt is an equivalence relation capturing the indistinguishability of states for agent a.

Strategies and Probabilistic Outcomes. For the interplay between a coalition C ⊆ Agt and its opponents C = Agt\C, we follow [Belardinelli et al., 2023a] and assume that C play uniform deterministic memoryless strategies (ir-strategies in short), whereas C can respond with any pattern of behavior (possibly probabilistic and history-based). Formally, an irstrategy for agent a is a function σa : St → Actin which: (i) for each s, we have σa(s) ∈ d(s, a); and (ii) if s ∼a s′ then σa(s) = σa(s′ ). Moreover, a general strategy for agent a ∈ Agt is represented by σa : St+ → D(Act) that maps each finite history to a probability distribution over the agent's actions, such that σa(h) ∈ d(last(h), a). A collective strategy σC for C is a tuple of strategies σa, one per agent a ∈ C.

The outcome of strategy σC from state s is the set outC(σC, s) of probability distributions over infinite paths in the model, consistent with C's choices prescribed by σC. Each distribution µσC,s ∈ outC(σC, s) is obtained from the Markov chain that combines the Stochastic iCGS M with σC and a possible general strategy of C. We refer to [Belardinelli et al., 2023a] for the detailed construction.

Probabilistic Alternating-Time Logic PATL. We now introduce Probabilistic Alternating-Time The language of PATL∗ is defined as follows:

where ⟨⟨C⟩⟩∝pφ means that there exists a strategy for the coalition C to collaboratively enforce φ with a probability in relation ∝ with constant p, where ∝∈ {=, ̸=, >, <, ≥, ≤}.

The language of PATL is a restriction of the language of PATL∗ and is defined by the following grammar:

C to collaboratively enforce φ with a probability in relation ∝ with constant p.

An iSCGS together with a set of atomic propositions AP and a valuation function V : AP → 2St is called a stochastic concurrent game model (SCGM). The formulas of PATL are interpreted over pairs (M, π), consisting of an SCGM and an infinite path in it.

Satisfaction relation. The semantics of PATL extends the semantics of ATL and is defined by the following clauses:

M, π |= p iff p ∈ V (π0);

M, π |= ¬φ iff M, π ̸|= φ;

M, π |= φ∧ψ iff M, π |= φ andM, π |= ψ;

M, π |= ⟨⟨C⟩⟩∝pφ iff there is an ir-strategy σC s.t. for all µσC,π0 ∈ outC(σC, π0) we have µσC,π0 ({ρ : M, ρ |= φ}) ∝ p;

M, π |= φUψ iff there is a k s.t. M, π≥k |= ψ and for all j < k we have M, π≥j |= φ.

We define M, s |= φ iff M, π |= φ holds for any π starting in s. Sat(M, φ) = {s ∈ St | M, s |= φ} is the subset of states in M satisfying φ. Moreover, pointed models are pairs (M, s) consisting of an SCGM and a state in it. For a subset of pointed models A, we use A |= φ to mean that for all (M, s) ∈ A it holds that M, s |= φ. We also use ˆM to denote the set of all pointed models in M.

3 Adding Knowledge and Uncertainty

In this section we introduce probabilistic extensions of ATLK [van der Hoek and Wooldridge, 2003] and ATLH [Tabatabaei and Jamroga, 2023] that can be simultaneously seen as epistemic and information-theoretic extensions of PATL [Belardinelli et al., 2023b].

Knowledge andCredences Inmulti-agent epistemic logic, knowledge of agents is formalized by epistemic formulas Kaφ, stating "agent a knows that φ holds." They are interpreted by the following clause:

where ∼a⊆ St×St is an epistemic equivalence relation connecting states that are indistinguishable to a.

Analogously, PATL can be extended by operators K∝q a for probabilistic knowledge/beliefs, or credences (where ∝∈ {< ,>,≤,≥,=}). To provide semantics, we augment SiGS by a probabilistic observation function obsa : St → Dist(St), with the idea that obsa(s)(t) gives the subjective probability with which agent a believes that the current state is t, provided that the actual current state is, in fact, s. We will often write obsa(t|s) instead of obsa(s)(t) to make this even clearer. Additionally, we lift the notation to subsets of states by defining obsa(T |s) = ∑t∈T obsa(t|s).

We require that epistemic indistinguishability, captured by ∼a, is consistent with obsa as follows: s ∼a t (when in s, the agent considers t as possible) iff obsa(t|s) > 0 (when in s, the agent considers t with nonzero probability). Since ∼a is an equivalence, this implies the following requirements: obs(s|s) > 0 (due to reflexivity of ∼a); if obs(t|s) > 0 then obs(s|t) > 0 (due to symmetry); if obs(t|s) > 0 and obs(s|w) > 0 then obs(t|w) > 0 (due to transitivity).

An SiCGS extended by observation functions obsa is called a Stochastic Observational CGS (SOCGS). An SOCGS together with a set of atomic propositions AP and a valuation function V : AP → 2St is called a Stochastic Observational CGM (SOCGM). The semantics of PATLC extends PATL by the clause:

We note in passing that, for finite models, we can express classical knowledge by credences with Kaφ ≡ K=1 a φ.

Probabilistic Uncertainty Operators We propose modal operators H∝m a Φ, based on the fundamental notion of information entropy, due to [Shannon, 1948]. Let X = {x1, . . . , xn} be a countable set of possible outcomes (typically, values of a given random variable), and Pr ∈ Dist(X) a probability distribution over X. Then, its Shannon entropy is defined as HS(X) = - ∑ni=1 Pr(xi) log Pr(xi). Clearly, Shannon entropy is minimal (and equal to 0) if p is a Dirac distribution, i.e., we are certain with probability 1 which outcome is the right one. Conversely, HS is maximal when Pr is uniform, i.e., the subjective randomness of the system is highest. In that case, Shannon entropy coincides with Hartley uncertainty, defined as H(X) = log(|X|) [Hartley, 1928b].

Syntax. PATLH extends PATL with a family of operators H∝ m a Φ, where a ∈ Agt, Φ is a finite nonempty subset of PATLH formulas, and ∝∈ {<,≤,>,≥,=}. The reading of H∝ m a {φ1, . . . , φn} is "the uncertainty of a about the actual values of φ1, . . . , φn is at least (at most, equal to, etc.) m."

Semantics. We define the semantics of PATLH over SOCGMs, as for PATLK and PATLC. We follow the approach of [Tabatabaei and Jamroga, 2023]. The idea is that, in order to measure agent a's uncertainty about formulas Φ = {φ1, . . . , φn}, we take the different valuations of Φ as the "possible outcomes." Then, we take a's subjective probabilities about each possible valuation, and compute Shannon entropy for the resulting distribution.

Formally, we start by defining relation ∼φ∈ St × St that connects states with the same valuation of φ, i.e.: s ∼φ t iff M, s |= φ ⇔M, t |= φ. This can be lifted to indiscernibility of states w.r.t. a set of formulas Φ in a natural way: ∼Φ= ⋂nφ∈Φ ∼φ. Moreover, we combine syntactic and semantic indistinguishability through relation ∼Φa =∼a ∩ ∼Φ. In other words, s ∼Φa t iff s and t are epistemically indistinguishable and no formula in Φ can distinguish between them. Clearly, ∼Φa is an equivalence relation.

Next, we define the relevant outcomes as the abstraction classes of ∼Φa that are contained in the current epistemic class due to ∼a, i.e.: Ra,s(Φ) = {[t]∼Φa | t ∼a s}. Then, we construct Pra,s,Φ ∈ Dist(Ra,s(Φ)) with Pra,s,Φ([t]) being the (normalized) aggregate probability that a associates with the states in [t] when the real state of the system is s, i.e.:

Finally, we can define the semantics of Shannon uncertainty modalities via the following clause:

Simple Example Consider the following scenario: a voter v decides to vote for or against A, by choosing (at the initial state s0) whether to proceed to state s1 (with proposition VA) or to s2 (with ¬VA). After v has voted, the coercer c learns the value of the vote with 70% confidence, represented by: obsc(s1|s1) = obsc(s2|s2) = 0.7, obsc(s2|s1) = obsc(s1|s2) = 0.3. The following PATLC formula holds in s0:

⟨⟨v⟩⟩♢(VA ∧ ¬K≥0.9 c VA) ∧ ⟨⟨v⟩⟩♢(¬VA ∧¬K≥0.9 c ¬VA), expressing that the voter can vote for or against A in such a way that the coercer does not learn about that with confidence 90% or more. Note that the analogous formula for confidence level of 0.7 would not be true anymore. Moreover, the following PATLH formula is also true in s0: ⟨⟨v⟩⟩□H≥0.88 c {VA, ¬VA}, saying that the voter can keep the coercer's uncertainty about v's vote at a reasonable level of at least 0.88 bits.

The above formulas allow us to pinpoint two distinct flavors of information leakage: one based on the coercer's increased confidence in the actual value of the vote, and the other on the reduction of his subjective information entropy.

4 Model Checking

In this section we show that adding probabilistic knowledge and uncertainty does not increase the complexity of verification. More precisely, model checking of all the considered logics (PATLH, PATLK, and PATLC) is ∆P2 -complete for uniform deterministic strategies of the coalition, and thus no worse than for ATLir and PATLir. Since the input to model checking should be finite, we only consider finite state and action spaces, and rational probability values.

Theorem 1. Model checking of PATLK with deterministic irstrategies is ∆P2 -complete.

Proof. We recall that model checking of epistemic logic is in P [Halpern and Vardi, 1991], and model checking PATL with deterministic ir-strategies is ∆P2 -complete w.r.t. the size of the model and the length of the formula [Belardinelli et al., 2023b]. Moreover, model checking PATL formulas of type ⟨⟨C⟩⟩γ with no nested strategic operators is NP-complete.

The lower bound for PATLK is immediate from the fact that PATLK subsumes PATL. The upper bound can be obtained via the standard recursive algorithm that starts from the simplest subformulas (i.e., ones with no nested strategic nor epistemic modalities), computes their extensions (i.e., subsets of states that satisfy the formula), and replaces each of them with a fresh atomic proposition with exactly the same extension. Clearly, the complexity of the algorithm is PP∪NP = ∆P2 .

The next results are proved analogously.

Theorem 2. Model checking of PATLCir with deterministic ir-strategies is ∆P2 -complete Proof. The lower bound for PATLC is immediate as PATLC subsumes PATL. For the upper bound, it suffices to prove that the extension of K∝q a φ in model M, for φ containing no nested modal operators, can be computed in polynomial time. To do this, for each state s ∈ St, we compute Bel(s, a, φ) = ∑t∈Sat(M,φ) obsa(t|s), and check if Bel(a, s, φ) ∝ q. Clearly, the procedure runs in polynomial time w.r.t. the number of states, transitions, and representation of probabilities in the model and the formula.

To model-check an arbitrary formula of PATLC, we apply the same recursive algorithm as in Theorem 1.

Theorem 3. Model checking of PATLH with deterministic ir-strategies is ∆P2 -complete.

Proof. The lower bound is immediate as PATLH subsumes PATL. For the upper bound, we prove that the extension of H∝ m a Φ, for Φ = {φ1, . . . , φn} containing no nested modal operators, can be computed in polynomial time.

To do this, for each state s ∈ St, we construct the set of equivalence classes Ra,s(Φ) by checking the values of φ1, . . . , φn in all states t ∈ [s]∼a . Then, we compute Pra,s,Φ(x) for every x ∈ Ra,s(Φ). Finally, we calculate the Shannon entropy HS(Ra,s(Φ)) and compare it with m according to operator ∝. The procedure runs in polynomial time w.r.t. the number of states, transitions, representation of probabilities, and the precision with which logarithms are computed. For arbitrary formulas, we proceed recursively.

5 Expressiveness

We start by recalling the semantic concepts of comparative expressiveness [Wang and Dechesne, 2009]. Then, we prove that PATLC is strictly more expressive than PATLH.

Definition 1 (Distinguishing and expressive power). Let L1 = (L1, |=1) and L2 = (L2, |=2) be two logical systems with sets of formulas L1,L2 and semantic relations |=1, |=2 interpreted over the same class of models M. By Sat (ϕ) = {(M, q) | M, q |= ϕ}, we denote the class of pointed models that satisfy ϕ in the semantics given by |=. Likewise, Sat (M, ϕ) = {q | M, q |= ϕ} is the set of states (or, equivalently, pointed models) that satisfy ϕ in a given structure M.

L2 is at least as expressive as L1 (L1 ⪯e L2) iff for every ϕ1 ∈ L1 there is ϕ2 ∈ L2 such that SatL1 (ϕ1) = SatL2 (ϕ2).

L2 is at least as distinguishing as L1 (L1 ⪯d L2) iff for every model M and formula ϕ1 ∈ L1 there exists ϕ2 ∈ L2 such that SatL1 (ϕ1,M) = SatL2 (ϕ2,M). Equivalently: every pair of pointed models that can be distinguished by some

ϕ1 ∈ L1 can be also distinguished by some ϕ2 ∈ L2.

Note that L1 ⪯e L2 implies L1 ⪯d L2. By transposition, it also holds that L1 ̸⪯d L2 implies L1 ̸⪯e L2.

Theorem 4. PATLH covers neither the expressive nor the distinguishing power of PATLC.

Proof. We show that PATLC ̸⪯d PATLH, and thus also PATLC ̸⪯e PATLH.

Take two models M1,M2, each with a single agent a, two states s1, s2, only self-loops as transitions, and a sole proposition p holding only in s2. The observations in (M1, s1) are:

obs(s1|s1) = 14 , obs(s2|s1) = 34 ; in (M2, s1): obs(s1|s1) = 34 , obs(s2|s1) = 1 4 . Notice that: (1) (M1, s1) and (M2, s1) satisfy the same formulas of PATL (obvious), and the only nontrivial uncertainty formulas are H∝q a {p} (or, equivalently, H∝q a {¬p}. But the Shannon entropy for Φ = {p} is the same in (M1, s1) and (M2, s1). So, they satisfy exactly the same formulas of PATLH. (2) The models can be discerned by the PATLC formula K≥3/4 a p, which holds in (M1, s1) but not in (M2, s1). Hence, we have that PATLC ̸⪯d PATLH.

Theorem 5. PATLC covers both the expressive and the distinguishing power of PATLH.

Proof. We show a translation of formulas H∝q a {Φ} into PATLC that preserves the set of satisfying pointed models.

Let Φ = {φ1, . . . , φn}, and let VΦ be the set of all possible valuations for Φ (there are 2n such valuations). We write φi ∈ v iff v(φi) = true. Clearly, each v ∈ VΦ can be characterized by a conjunction ψv ≡ (∧φi∈v φi ) ∧ (∧φi /∈v ¬φi ). Moreover, given a pointed model (M, s), each v ∈ VΦ corresponds to a different outcome [tv] ∈ Ra,s(Φ), assigned probability pv = Pra,s,Φ([tv]). 1

Now, the condition for M, s |= H∝q a {Φ} can be written as - ∑v∈VΦ pv log pv ∝ q (*). The set of probability distributions (pv)v∈VΦ satisfying (*) is a finite union of hypercubes H1, . . . ,Hm ∈ [0, 1]|VΦ| , obtained as the solution of inequality (*), together with constraints (**) pv ≥ 0, v ∈ VΦ, and (***) ∑v∈VΦ pv = 1. Moreover, each hypercube Hi can be characterized by a conjunction of conditions pv ∝iv qiv , v ∈ VΦ, 2 and hence equivalently by ∧v∈VΦ Pra,s,Φ([tv]) ∝iv qiv

which is in turn equivalent to M, s |= ∧v∈VΦ K∝iv qiv a φv. Putting it all together, we obtain

Thus, ∨mi ∧v∈VΦ K∝iv qiv a φv is an extension-preserving translation of H∝q a {Φ}, which concludes the proof.

Corollary 1. PATLC has strictly more expressive and distinguishing power than PATLC.

So, formulas based on probabilistic knowledge allow for expressing a strictly larger class of properties than uncertainty-based ones. This is a big surprise, and makes probabilistic logics distinctly different from non probabilistic ones (where both kinds of modalities were equally expressive). On the other hand, note that the PATLC translation of H∝q a {Φ}, used in Theorem 5, is quite complicated and at least exponentially longer than its PATLH counterpart. As we show in the next section, this is no coincidence.

6 Succinctness

The concept of succinctness focuses on whether there is a substantial difference in the length of encodings provided by logics L1, L2 for some scalable property [Stockmeyer, 1972;

1 Possibly with probability pv = 0.

2 Note that the comparison operators ∝iv do not have to be the same, and in particular can be different from the operator ∝ in the translated uncertainty formula.

Wilke, 1999; Adler and Immerman, 2001]). In this section, we show that PATLH is exponentially more succinct than PATLC. To prove this, we follow [Tabatabaei and Jamroga, 2023] and use formula size games (FSG) introduced in [French et al., 2013b]. Specifically, we demonstrate that there is a sequence of PATLH formulas (φn)n∈N with length O(n), such that any PATLC formula ψn with the extension as φn has a parse tree with at least 2n distinct vertices, and thus that the length of ψn must be at least O(2n ). 3

Definition 2 (Succinctness, [Adler and Immerman, 2001]). Let L1 = (L1, |=1) and L2 = (L2, |=2) be two logical systems as in Definition 1. Further, suppose f, g : N → N are two functions such that f(n) = O(g(n)) is a strictly increasing function.

L1 is exponentially more succinct than L2 (L1 ̸⪯subexp M L2) iff for each n ∈ N there are formulas φn ∈ L1 and ψn ∈ L2 with: (1) |φn| = f(n), (2) |ψn| = 2g(n) , (3) ψn is the shortest formula in L2, equivalent to φn.

We now adapt the one-person formula size games of [French et al., 2013a], where the player, called the spoiler tries to synthesize a formula to discern between sets of models A and B, i.e., some φ ∈ PATLC such that A |= φ and B |= ¬φ.

Definition 3 (FSG for Credences). The game is defined for two given sets of pointed models A, B ⊆ ˆM, and played according to the following rules. The player, called the spoiler, constructs a game tree in such a way that each vertex is labeled with a pair (C,D) of subsets of pointed models. The possible moves for the spoiler on each vertex of the tree are {{p}p∈AP ¬, ∨, {K∝q a }a∈Agt;q∈Q∩[0,1]}. A vertex can be open or closed, and once it becomes closed, no further move can be played from it. The rules for each of possible moves are defined as follows:

1. (Atomic move (p ∈ AP)): the spoiler chooses p ∈ AP s.t. C |= p and D |= ¬p. The vertex becomes closed.
2. (¬ move): A new vertex (D,C) is added to the tree.
3. (∨ move): two vertices (C1,D) and (C2,D) are added to the tree, where C1∪C2 = C are chosen by the spoiler.
4. (K∝q a move): For each (M, s) ∈ C the spoiler chooses a subset of pointed models Cs ⊆ ˆM such that obsa(Cs|s) ∝ q. Moreover, for each (M, s) ∈ D, the spoiler chooses a subset of pointed models Ds ⊆ ˆM such that obsa(Cs|s)̂∝1 - q, where ̂= denotes ̸=, ̂≥ is >, ̂≤ is <, and vice versa. Then a new vertex (⋃s∈C Cs, ⋃s∈D Ds) is added to the tree.

We say that the spoiler wins the FSG starting at (A,B) in n moves iff there exists a game tree T with the root (A,B) and precisely n vertices such that every leaf of T is closed.

We can now state the following result, which is an adaptation of a classical theorem in [French et al., 2013b] to probabilistic modal operators.

3 The length of formula φ is defined as the total number of symbols in φ, including atomic propositions, boolean, modal and arithmetic operators, and numbers (treated each as a single symbol).

Theorem 6. Spoiler can win FSG starting at (A,B) in n moves iff there exists a PATLC formula φ (without strategic operators) where A |= φ, B |= ¬φ, and |φ| = n.

Proof. The proof is analogous to [French et al., 2013b, Theorem 3.2], using credence moves instead of epistemic ones. Each credence move corresponds to a K∝q a operator inφ.

The purpose of Theorem 6 is to use Formula Size Games for proving that PATLH is exponentially more succinct than PATLC. Analogous results were presented in [French et al., 2013b] for mutual knowledge vs. standard epistemic logic, and in [Tabatabaei and Jamroga, 2023] for Hartley uncertainty vs. standard knowledge. Unfortunately, those proofs cannot be easily adapted to the case of Shannon uncertainty vs. probabilistic beliefs. We are still convinced that the analogous relationship holds, but for now we only formulate it as a conjecture, and leave its ultimate proof for future work.

Conjecture 1. PATLH ̸⪯subexp PATLC.

Proof idea. For every natural number n ∈ N, we define a formula φn in the language of PATLH and consider the shortest formula ψn in the language of PATLC that is expressively equivalent to φn. The existence of such ψn is guaranteed by Theorem 5. Further, we construct two sets of pointed models An and Bn, such that An |=H φn and Bn |=H ¬φn,

The idea is to use An = {M} with two agents {a, b} and the state space divided into n "layers," where obsa is defined within each layer according to the geometric probability distribution (a.k.a. Furry distribution), and obsb leads to states in the subsequent layer. Moreover, Bn is the set of possible variants of M obtained by removal of an arbitrary state within each layer. Then, we take: ϕ1 ≡ H≥q a {p1, . . . pk}, ϕ2 ≡ H≥q a {H=0 b H≥q a {p1, . . . pk}, . . . pk}, and so on, for an appropriately chosen q.

We will thus have that An |= ψn and Bn |= ¬ψn. Hence, in the FSG with the starting point at the vertex labelled by (An, Bn), the spoiler has a winning strategy given by playing the moves in accordance with the syntactic structure of ψn. Still, the last step remains to demonstrate that any such winning strategy requires that the length of the play of the game (starting at (An,Bn)) is no shorter than 2n .

7 Case Studies

Scenario 1: Probabilistic Analysis of Voting ThreeBallot [Rivest, 2006], is an end-to-end verifiable voting protocol designed to ensure both vote privacy and coercion resistance. In this protocol, each voter fills out three ballots per issue. To cast a 'yes' vote for an issue, the voter fills two of the three corresponding fields, leaving one blank. Conversely, for a 'no' vote, the voter fills one field and leaves the other two blank. The voter then separates the three columns to create three individual ballots, retains one as a receipt, and submits the rest to the ballot box. After tallying, all ballots are published on a public bulletin board for verification.

A key property of ThreeBallot is coercion resistance. A coercer, even with access to a voter's receipt, cannot deduce the voter's complete voting choice due to the indistinguishability sets formed by the combinations of filled and blank spaces.

An example ThreeBallot configuration for a two-issue referendum is shown in Table 1. The voter votes 'yes' on Issue A and 'no' on Issue B, resulting in the following ballots:

• Ballot 1: Filled for Issue A, blank for Issue B.
• Ballot 2: Filled for both Issues A and B.
• Ballot 3: Blank for Issue A, filled for Issue B.

In contrast to [Tabatabaei and Jamroga, 2023], we consider a probabilistic model of ThreeBallot, with the probabilities coming from opinion polls about voters' preferences. Based on that, we will demonstrate how PATLH and PATLC capture coercion resistance in stochastic models of voting.

Probabilistic model of voting. Consider a two-issue referendum with propositions A and B. The voters' preferences are influenced by opinion polls, which provide the following probabilities for the outcomes: p(VA) = 0.6, p(¬VA) = 0.4, p(VB) = 0.7, p(¬VB) = 0.3. Here, VA and VB represent votes in favor of A and B, while ¬VA and ¬VB represent votes against them. The ballots are filled following the ThreeBallot rules: voters fill two fields for a "yes" vote and one for a "no" vote for each issue. After filling the ballots, voters retain one as a receipt and submit the others to the ballot box.

How to specify coercion resistance. The coercer attempts to deduce the voter's choices using the receipt and published data. To ensure coercion resistance, we evaluate the uncertainty of the coercer about the voter's choices using PATLH and PATLC. In what follows we use (V1 = Vi) in as an atomic proposition that is evaluated as true if V1 is equal to Vi. Condition (V1 ̸= V2) is interpreted in an analogous manner.

The coercion resistance property can be expressed in PATLH as

where V otes = {VAVB, VA¬VB, ¬VAVB, ¬VA¬VB} represents all possible combinations of votes. Here, Hc quantifies the coercer's entropy regarding the voter's choices. By maintaining an entropy of at least 1.8 bits, the coercer's maximal uncertainty about the votes is guaranteed. This formula ensures that no strategy allows the coercer to achieve a lower level of uncertainty.

Following the translation from Theorem 5, we can express the same property in PATLC as:

where Φ = {VA, VB}, VΦ is the set of valuations for Φ, and 1.8jv are the numbers corresponding to the hypercubes in [0, 1]|VΦ| , as in the proof of Theorem 5. This formula ensures that no strategy allows the coercer to achieve a degree of belief exceeding max{1.8jv : v ∈ VΦ, j = 1, . . . ,m} for any specific vote combination. Clearly, using PATLH, we express the same property more succinctly.

Analysis and comparison. The PATLH representation leverages entropy to directly capture the coercer's uncertainty, avoiding the need to enumerate all vote combinations explicitly. This succinctness highlights PATLH's advantage in scenarios with probabilistic uncertainty.

In contrast, PATLC relies on probabilistic beliefs, which, while expressive, require detailed enumeration of strategies and outcomes. Both approaches demonstrate coercion resistance, but PATLH provides a more compact formalization.

Scenario 2: Signal Integrity To illustrate the differences between the expressive power of PATLC and PATLH, consider a story of a cybersecurity analyst, Alice, investigating potential vulnerabilities in a communication system. Alice is analyzing two models of data transmission security, M1 and M2, to assess their ability to handle interference. Both models describe a device operating in two states: s1 represents a state where data is partially corrupted but recoverable, and s2 represents a state of complete recovery. The device transmits a key signal σ, which holds specific integrity information: in s2, the signal σ is fully verified as correct (pσ), while in s1, it is not (¬pσ).

The device observations of its signal integrity are modeled as follows. In M1, the probabilities are obs(s1|s1) = 1 4 and obs(s2|s1) = 34 ; inM2, the probabilities are obs(s1|s1) = 34 and obs(s2|s1) = 1 4 , see also Figure 2. We emphasize that agent a in the model represents the entity making observations about the signal integrity and reasoning about its states, i.e., the device. Alice is an external entity using PATLH and PATLC to evaluate the properties of the system.

Alice first uses PATLH to evaluate the system's uncertainty. By calculating the Shannon entropy for Φ = {pσ}, she finds that the entropy is identical in both models, and thus they satisfy the same formulas of PATLH.

However, Alice may turn to PATLC to gain a more granular understanding. In particular, she can check formula K≥3/4 a pσ, which is satisfied in (M1, s1) but not in (M2, s1). This allows Alice to identify M1 as a system where the device has higher probabilistic confidence in its recovery signal, a critical feature in detecting and managing interference.

8 Summary

This work introduces PATLH, a groundbreaking extension of probabilistic alternating-time temporal logic. PATLH incorporates Shannon entropy to provide a formal framework for reasoning about uncertainty and information gain. By combining strategic reasoning with a measure of probabilistic uncertainty, PATLH fills a significant gap in the study of stochastic MAS where agents operate under imperfect information. The logic enables a nuanced approach to both reducing and maintaining uncertainty, addressing real-world needs in scenarios like privacy protection and information security, where agents aim to control the flow of sensitive information.

The introduction of entropy-based reasoning is particularly innovative, as it allows for the modeling of agents' strategic capabilities in controlling uncertainty, something that previous epistemic logics have struggled to express succinctly. PATLH 's application to security and privacy concerns in multi-agent systems sets a new standard for addressing these challenges, providing a richer, more flexible framework for researchers and practitioners alike. Moreover, the work also extends the capabilities of existing probabilistic logics by introducing PATLC, which facilitates reasoning about probabilistic beliefs (credences) instead of full knowledge, and turns out to be strictly more expressive than PATLH.

Future work. First and foremost, we plan to complete the proof of the succinctness claim. As for longer-term plans, the study opens the door to further extensions in strategic logics. One particularly promising avenue for future research is extending PATLH to more expressive frameworks, such as Strategy Logic (SL, see e.g., [Berthon et al., 2017]). These extensions would enable reasoning about complex solution concepts like Nash equilibria, subgame-perfect equilibria, and other cooperative or adversarial strategies in multi-agent systems. SL, which allows explicit quantification over strategies, would benefit from the integration of entropy-based reasoning, enabling the representation of complex objectives related to information control and uncertainty.

Acknowledgments

M.T. Godziszewski and A. Murano's research was supported by the PRIN project RIPER (No. 20203FFYLK), and the PNRR MUR projects PE0000013-FAIR and INFANT (No. E23C24000390006). W. Jamroga's research was supported by NCBR Poland under the project POLLUXXI/14/SpaceVote/2023.