Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

1 Introduction

Epistemic logic has a long tradition in knowledge representation and reasoning, multi-agent systems (MAS), and more broadly in artificial intelligence [Meyer and Hoek, 1995]. A significant line of research over the past twenty years has concerned its combination with various temporal logics such as LTL, CTL, and the like [Clarke et al., 2002]. The resulting syntax can express a wide range of properties of multiagent systems, including the knowledge agents have about the world, about each other's knowledge, how this evolves over time and whether sophisticated epistemic states such as common knowledge are acquired in a system's run [Halpern and Vardi, 1989].

Temporal-epistemic properties of multi-agent systems have been studied under a variety of assumptions, including synchronicity, asynchronicity, perfect recall, bounded recall, no learning, and observational semantics [Fagin et al., 1995]. These aspects are now known to impact the resulting axiomatisations [Halpern et al., 2003; Belardinelli and Lomuscio, 2009] as well as the complexity of the verification problem [Meyden and Shilov, 1999]. For these reasons, a key aspect in this line of work has been the identification of expressive fragments with relatively low complexity.

Recently there has been considerable interest in the extension of the formalisms above to languages sufficiently expressive to capture strategic abilities of agents. Towards this aim, alternating-time temporal logic (ATL) [Alur et al., 2002] and strategy logic (SL) [Mogavero et al., 2014] have been put forward and combined with epistemic modalities and uniform strategies [Hoek and Wooldridge, 2003; Belardinelli, 2014;

AnielloMurano and Sasha Rubin DIETI Universit`a degli Studi di Napoli

murano@na.infn.it rubin@unina.it

Huang and Meyden, 2014; ˇCerm´ak et al., 2014; Berthon et al., 2017a].

Reasoning about strategic abilities of MAS under imperfect information is known to be difficult. For example, model checking MAS against ATL specifications under incomplete information goes from PTIME-complete to ∆p2 -complete under memoryless strategies (i.e., imperfect recall) [Jamroga and Dix, 2006] and is undecidable under memoryfull strategies (i.e., perfect recall) [Dima and Tiplea, 2011]. For this reason it is of interest to identify expressive classes of MAS for which the model checking problem is decidable. The aim of this paper is to make a contribution in this direction.

Specifically, we introduce ESL, an epistemic extension of SL based on synchronous perfect-recall strategies (Section 2). The language introduced can express rational synthesis [Fisman et al., 2010; Wooldridge et al., 2016; Kupferman et al., 2016], but its model-checking problem is undecidable. However, we identify a significant class BA-iCGS of systems: those having broadcast (i.e., fully observable) actions (Section 2.2) and prove that model checking BA-iCGS against ESL is non-elementary decidable (Section 4). This is a tight result as a matching lower-bound already holds in the perfectinformation case. We illustrate our formalism on a rational secret-sharing scenario with broadcast actions (Section 3).

Related Work. As mentioned above, several approaches have been put forward to reason about strategies and knowledge in the context of MAS.

SL and knowledge have been combined before in the context of MAS. In [Cerm´ak, 2014; ˇCerm´ak et al., 2014], an epistemic variant of SL [Mogavero et al., 2014] was introduced. However, this was limited to epistemic sentences, whereas we consider the full combined language, and the approach assumed observational semantics, whereas we here consider synchronous perfect recall. Although not studied in these papers these formalisms have an undecidable model checking problem if evaluated under synchronous perfect recall. Also, [Berthon et al., 2017b] defines a variant of SL with uniform strategies. They achieve decidability by a variation of the tradition of assuming a hierarchy on the observations. In this paper we do not make any hierarchical assumptions.

A key aspect of the work here presented is that it relies on broadcasting to achieve decidability in the context of a very expressive specification language. The notion of broadcast has already been studied in the context of knowledge [Fagin et al., 1995; Lomuscio et al., 2000]. A further important result in this area is that for broadcast systems the synthesis problem of specifications in LTL and knowledge is decidable [Meyden and Wilke, 2005]. However, ESL is strictly more expressive and synthesis, which in our case can be expressed via model checking, can also be shown to be decidable. An approach to reasoning about strategies and knowledge under broadcast was also recently presented in [Belardinelli et al., 2017]. However, their logic is considerably less expressive than ours, as it is based on ATL and not SL. In particular, it cannot express Nash equilibria and rational synthesis, which are essential features of this contribution.

Rational synthesis has been studied before in the context of perfect information. In [Kupferman et al., 2016] the strongrational synthesis problem with LTL objectives (and aggregation of finitely many objectives), is shown to be 2EXPTIMEcomplete.In [Gutierrez et al., 2017], Equilibrium Logic is introduced to reason about Nash equilibria in games with LTL and CTL objectives. However, both cases assume perfect information of the agents. Synthesis under imperfect information has been first tackled in [Gutierrez et al., 2016] albeit for a restricted class of CGS, viz. reactive modules. In this paper we explore synthesis in CGS under imperfect information.

2 Strategy Logic with Imperfect Information

In this section we present strategy logic (SL) (see [Mogavero et al., 2014] for a definition of SL) in an imperfect information setting. In particular, we introduce the class of imperfect information concurrent game structures (iCGS) with broadcast actions only (BA-iCGS). We start with some preliminaries. For an infinite or non-empty finite sequence u ∈ Xω ∪X+ of elements in X, we write ui for the (i+1)-th element of u, i.e., u = u0u1 . . .. For i ≥ 0, u≤i is the prefix of u of length i + 1, i.e., u≤i = u0u1 . . . ui. The empty sequence is denoted as ϵ. The length of a finite sequence u ∈ X∗ is denoted as |u|. For a vector v ∈ ∏i Xi we denote the i-th co-ordinate of v by v(i). In particular, for F ∈ ∏i (Xi)Y we may write F (i) ∈ XY i and F(i)(y) ∈ Xi.

2.1 iCGS

Hereafter we consider concurrent game structures enriched with indistinguishability relations. These are the standard setting for agent-based logics under imperfect information [Jamroga and van der Hoek, 2004; Bulling and Jamroga, 2014].

Definition 1 (iCGS). An imperfect information concurrent game structure (iCGS) is a tuple S = 〈Ag,AP, {Acta}a∈Ag, S, S0, tr, {∼a}a∈Ag, λ〉, where:

1. Ag is the finite non-empty set of agent names.
2. AP is the finite non-empty set of atomic propositions.
3. Acta is the finite non-empty set of actions for a ∈ Ag; for A ⊆ Ag, let ActA = ∪a∈AActa, and let Act = ActAg.
4. S is the finite non-empty set of states and S0 ⊆ S is the non-empty set of initial states.
5. tr : S × ACT → S is the transition function, where ACT = ∏a∈Ag Acta is the set of all joint actions.
6. ∼a⊆ S2 is the indistinguishability relation for agent a, which is an equivalence relation.
7. λ : AP → 2S is the labelling function that assigns to each atom p the set of states λ(p) in which p holds.

A concurrent game structure (CGS) is an iCGS for which ∼a= {(s, s) : s ∈ S} for all a ∈ Ag. This corresponds to the perfect-information setting [Alur et al., 2002].

We now define what it means for an agent to have synchronous perfect-recall in an iCGS S. A history in S is a non-empty finite sequence h0h1 . . . in S+ such that for all i ≥ 0, there exists a joint action Ji ∈ ACT such that hi+1 ∈ tr(hi, Ji). The set of all histories in S is denoted as hist(S), and the set of histories h′ that extend history h is denoted as hist(S, h), that is, h′≤|h| = h.

Hereafter we use the following notation: if ∼ is a binary relation on S, we define the extension of ∼ to histories as the binary relation ≡ on hist(S) such that h ≡ h′ iff |h| = |h′ | (i.e., synchronicity) and hj ∼ h′j for all 0 ≤ j ≤ |h| (i.e., perfect recall). We consider three instantiations for individual, common and distributed knowledge respectively. If ∼a is the indistinguishability relation for agent a, then two histories h, h′ are indistinguishable to agent a, if h ≡a h′ . For A ⊆ Ag, let ∼CA= (∪a∈A ∼a)∗ , where ∗ denotes the reflexive and transitive closure (w.r.t. relation composition), and its extension to histories is denoted ≡CA. For A ⊆ Ag, let ∼DA= ∩a∈A ∼a, and its extension to histories is denoted ≡DA. A deterministic memoryfull strategy, or simply strategy, is a function σ : hist(S) → Act (recall that Act = ∪a∈AgActa). The set of all strategies is denoted Σ(S). Further, a strategy σa is coherent for a if for every h ∈ hist(S), σa(h) ∈ Acta; while σa is uniform for a if for all h, h′ ∈ hist(S), h ≡a h′ implies σa(h) = σa(h′ ). Then, a joint full strategy is a function σAg : Ag → Σ(S) that associates to each agent a ∈ Ag a strategy that is both coherent and uniform for a. We write σAg(a) = σa. For every s0 ∈ S0, a joint full strategy σAg defines a unique infinite sequence π(σAg) = s0s1 . . . of states, i.e., for all i ≥ 0, si+1 = tr(si, σAg(s0s1 . . . si)). A history h is consistent with σAg if h is a prefix of π(σAg). Given h ∈ hist(S), define the set out(h, σAg) of outcomes of σAg from h as the set of histories h′ ∈ hist(S, h) that extend h and are consistent with σAg. Notice that for every i ≥ 0, there is unique h′ ∈ out(h, σAg) of length |h|+i. Thus, write π(h, σAg) ∈ Sω for the infinite sequence all of whose prefixes are in out(h, σAg).

2.2 BA-iCGS- iCGS with Broadcast Actions only

In this paper we focus on a particular class of iCGS, those having broadcast actions only. This section is reported from [Belardinelli et al., 2017] (where these were called iCGS with public actions only).

Definition 2 (BA-iCGS). An iCGS S only has broadcast actions if for every agent a ∈ Ag, states s, s′ ∈ S, and joint actions J, J ′ ∈ ACT, if J ̸= J ′ and s ∼a s′ then tr(s, J) ̸∼a tr(s′ , J ′ ). In this case we call S a broadcast iCGS. We write BA-iCGS for the set of broadcast iCGS.

Broadcast iCGS arise naturally in several MAS scenarios, including epistemic puzzles (e.g., the muddy children puzzle) and games (e.g., battleship). In Section 3 we discuss an application to rational synthesis.

We define the following natural encoding of histories.

Definition 3. Let S be an iCGS. Define the encoding function µ : S0×ACT∗ → hist(S) that maps (s0, u) to the history h of length |u|+1 and such that h0 = s0 and hj = tr(hj-1, uj-1) for 1 ≤ j ≤ |u|.

In case S is a BA-iCGS, then µ is a bijection, i.e., for every h ∈ hist(S) there exists a unique (sh, uh) ∈ S0 ×ACT∗ such that µ(sh, uh) = h. Moreover, the moment different joint actions are taken, two histories become distinguishable:

Proof. Indeed, if µ(s, u) ≡a µ(s′ , u′ ) then |u| = |u′ | and, for all 0 ≤ j ≤ |u|, µ(s, u)j ∼a µ(s′ , u′ )j. By the definition of having only broadcast actions, uj = u′j for all j < |u|.

The next characterisation of uniformity in BA-iCGS follows from Lemma 1 and is central to our decidability result:

Proposition 1. Let S be a BA-iCGS, and let σ be a coherent strategy for agent a. Then σ is uniform for agent a if and only if for all v ∈ ACT∗ , s, s′ ∈ S0 we have that µ(s, v) ≡a µ(s′ , v) implies σ(µ(s, v)) = σ(µ(s′ , v)).

2.3 The Logic ESL

We now introduce ESL, an epistemic extension of SL. We interpret it on iCGS with history-based semantics.

Syntax. Fix a finite set of atomic propositions (atoms) AP, a finite set of agents Ag, and an infinite set Var of strategy variables x0, x1, . . .. The formulas over AP , Ag, and Var are built according to the following grammar: ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | Xϕ | ϕUϕ | 〈〈x〉〉ϕ | (x, a)ϕ | Kaϕ | CAϕ | DAϕ, where p ∈ AP, x ∈ Var, a ∈ Ag, and A ⊆ Ag. The set of ESL formulas is the one generated by the grammar. The temporal operators are X (read "next") and U (read "until"). The strategy quantifier is 〈〈x〉〉 ("for some strategy x, . . . ") and the binding operator (x, a) ("by using strategy x, agent a can enforce . . . "); whilst the epistemic operators are Ka ("agent a knows that"), CA ("it is common-knowledge amongst A that"), and DA ("the agents in A distributively know that"). We use the usual shorthands, e.g., true for p ∨ ¬p, [[x]]ϕ for ¬〈〈x〉〉¬ϕ, and EAϕ for ∧a∈AKaϕ. The sets free(ϕ) and bnd(ϕ) of free and bound variables appearing in a formula ϕ are defined as standard [Mogavero et al., 2014]. Intuitively, x ∈ free(ϕ) if x does not occur in ϕ within the scope of any strategy quantifier of the form 〈〈x〉〉; while a ∈ free(ϕ) if some temporal operator is not in the scope of a binding (x, a) for agent a. Hereafter we assume that sets free(ϕ) and bnd(ϕ) are disjoint. Moreover, as in [Cerm´ak, 2014] we assume that every variable is quantified at most once in a given formula. All these properties can be ensured w.l.o.g. by renaming bound variables. A sentence is a formula ϕ with free(ϕ) = ∅. Finally, we define shr(x, ϕ) = {a ∈ Ag | (x, a)ψ is a subformula of ϕ} as the set of agents using strategy x in evaluating ϕ.

Semantics. Fix an iCGS S. An assignment is a function χ : Var ∪ Ag → Σ(S) such that for every agent a ∈ Ag, the strategy χ(a) is coherent and uniform for a. For x ∈ Var∪Ag and σ ∈ Σ(S), the variant χxσ is the assignment that maps x to σ and coincides with χ on all other variables and agents. Moreover, if x = a ∈ Ag then we require σ to be coherent and uniform for a. An assignment χ is ϕ-compatible if, for every x ∈ Var, the strategy χ(x) is coherent and uniform for every agent in shr(x, ϕ).

We define (S, h, χ) |= ϕ where h ∈ hist(S), ϕ is a formula, χ is a ϕ-compatible assignment, and π := π(h, χ|Ag) is the unique infinite sequence that extends h by following the restriction of χ to Ag:

The following says that the satisfaction is well-defined:

Lemma 2. In the expressions (S, h, χ′ ) |= ϕ′ on the righthand sides, χ′ is always a ϕ′ -compatible assignment.

For a history formula ϕ, we write S |= ϕ to mean that (S, s, χ) |= ϕ for every s ∈ S0 and assignment χ (observe that states are histories of length 1). One can prove (as usual) that the satisfaction of ESL-formulas depends only on their free variables and agents, that is, if assignments χ and χ′ coincide on free(ϕ), then (S, h, χ) |= ϕ iff (S, h, χ′ ) |= ϕ. Thus, e.g., if ϕ is a sentence, then S, s |= ϕ iff (S, s, χ) |= ϕ for some assignment χ.

Clearly ESL extends SL. Indeed, one restricts the syntax of ESL to the epistemic-free fragment, and the models to CGS (i.e., ∼a:= {(s, s) : s ∈ S} for every a ∈ Ag):

Proposition 2. For every SL sentence ϕ there is an ESL sentence ˆ ϕ s.t. for all CGS S, we have that S |= ϕ iff S |= ˆ ϕ.

The proof simply requires to show that the state-based semantics of SL in [Mogavero et al., 2014] can be captured by our history-based semantics.

The next proposition says that ATL∗K embeds in ESL (see [Jamroga and van der Hoek, 2004] for the definitions of ATL∗K). Although the embedding is as expected, the proof that it is correct is subtle.

Proposition 3. For every ATL∗K formula ϕ there is an ESL sentence ˆ ϕ s.t. for all iCGS S, we have that S |= ϕ iff S |= ˆ ϕ.

Proof. The main difficulty is to translate the ATL∗ operator 〈〈A〉〉 in ESL, which we illustrate. Consider Ag = {a1, a2, a3, a4}, A = {1, 2}, and the ATL∗K formula ϕ = 〈〈A〉〉ψ. The formula says that for every set of uniform strategies, one for each agent in A, every path consistent with these strategies satisfies ψ. Consider the ESL formula ˆ ϕ = 〈〈x1〉〉〈〈x2〉〉 [[x3]][[x4]](x1, a1)(x2, a2)(x3, a3)(x4, a4) ˆ ψ. Clearly, ϕ logically implies ˆ ϕ since the paths consistent with x1, x2 include those generated by uniform strategies x1, x2, x3, x4. On the other hand, let π be any path consistent with strategies σ1, σ2 (for agents a1, a2). It is sufficient to show that there exist uniform strategies, σ3 for agent a3 and σ4 for agent a4, such that π(s, σAg) = π. Indeed, for every n ≥ 0, let J ∈ ACT be a joint action such that i) σi(π≤n) = J(i) for i = 1, 2, and ii) tr(πn, J) = πn+1. Define σi(π≤n) = J(i) for i = 3, 4. Since the uniformity condition only restricts pairs of histories of the same length, we can extend σ3 and σ4 to uniform strategies. Note that π(s, σAg) = π, as required.

We now introduce the main decision problem of this work.

Definition 4 (Model Checking). Let C be a class of iCGS and F a sublanguage of ESL. Model checking C against F specifications is the following decision problem: given S ∈ C and ϕ ∈ F as input, decide whether S |= ϕ.

Model checking iCGS against ATL is undecidable [Dima and Tiplea, 2011]. Thus, applying Proposition 3, we get:

Proposition 4. Model checking iCGS against ESL is undecidable.

Indeed, it is undecidable even if C consists of all iCGS with |Ag| = 3 and F contains just the ATL formula 〈〈{1, 2}〉〉 Gp, see [Dima and Tiplea, 2011]. The source of the undecidability is the interplay between two assumptions: a) ∼1 and ∼2 are incomparable under the refinement-order on equivalence relations, and b) agent 3 can privately communicate with agents 1 and 2. In the sequel we prove that model checking is decidable assuming all agents only have broadcast actions. Thus, we keep property a) while dropping property b).

3 Rational Synthesis under Imperfect Information

In this section we show how to express central game-theoretic properties in ESL, e.g., the existence of Nash equilibria in multi-player games of imperfect information with epistemic objectives. Moreover, we illustrate that ESL can be used to reason about rational secret-sharing, i.e., rational agents that communicate by broadcast actions in order to learn a secret whose "shares" have been distributed amongst them.

3.1 Expressing Rational Synthesis in ESL

Several questions in computer science can be cast as the problem of deciding if there exists a joint winning strategy for a coalition of agents against a coalition of adversarial agents (and computing one if it exists). In the verification literature this problem is called synthesis.

However, as argued in [Wooldridge et al., 2016; Kupferman et al., 2016; Abraham et al., 2011], the partition of agents into "good" and "bad" is often insufficient, and it is more appropriate to view agents as rational. That is, agents have preferences over outcomes and act in a way that increases their own utility. Then, instead of reasoning about winning strategies, one should reason about rational strategy profiles, i.e., that satisfy some notion of equilibrium. Application domains include rational distributed computing and rational cryptography [Abraham et al., 2011], and negotiating systems with self-interested agents [Jennings and others,

2001]. Technically, suppose we are given an iCGS S representing the multi-agent system, and LTLK-formulas γa representing the objective of agent a ∈ Ag. Here, LTLK is the logic consisting of the set of path-formulas of ATL∗K. We can then talk about Nash equilibria σ in games of the form G = 〈S, {γa}a∈Ag〉1 . Rational synthesis considers the following decision problem (sometimes called E-NASH) :

Definition 5 (Rational Synthesis for LTLK objectives, cf. [Kupferman et al., 2016]). Given an iCGS S, LTLK-formulas γa for every a ∈ Ag, and an LTLK-formula ϕ, decide whether there exists a Nash equilibrium σ in the game G = 〈S, {γa}a∈Ag〉 such that the path induced by σ satisfies ϕ.

Intuitively, ϕ represents some global property that the designer wants to ensure given that agents are self-interested. In case ϕ = true, this simply asks if there exists a Nashequilibrium. Moreover, if there is such a Nash equilibrium, the synthesis problem concerns deriving one such strategy profile σ. The dual problem, called Strong Rational Synthesis (sometimes called A-NASH), concerns deciding whether all Nash equilibria induce a path that satisfies ϕ [Kupferman et al., 2016].

We now show that rational synthesis for LTLK objectives reduces to model checking against ESL. Suppose Ag = {a1, a2, . . . , an}, and let x be an n-tuple of variables. Let β be the expression (x1, a1)(x2, a2) . . . (xn, an) that binds agent ai to strategy xi. The following formula RatSynϕ(x) in ESL expresses that x is a Nash equilibrium whose induced execution satisfies ϕ: (x1, a1) . . . (xn, an) [ϕ ∧ ∧a∈Ag (〈〈y〉〉(y, a)γa → γa)] .

In words, if agent ai uses xi then the resulting execution satisfies ϕ, and no agent has an incentive to unilaterally deviate from the strategy profile x. Then:

Lemma 3. Rational synthesis for LTLK objectives is reducible to model checking against the ESL-formula 〈〈x1〉〉 . . . 〈〈xn〉〉RatSynϕ(x).

A universally quantified formula is used for Strong Rational Synthesis. It is important to observe that ESL can express other equilibrium concepts such as subgame-perfect equilibria, concepts that capture deviations by groups of players such as k-resilience and t-immunity, and the combination (k, t)-robustness that captures fault-tolerance [Abraham et al., 2011]. Also, ESL is able to express the existence of Nash equilibria w.r.t. epistemic objectives, which, to the best of our knowledge, has not yet been considered in the literature. We illustrate this last point in the next section.

3.2 Rational Secret-Sharing with Broadcast

We illustrate the model-checking problem for BA-iCGS against ESL with a simple scenario inspired by [Abraham et al., 2006] that uses broadcast. In the classic m-out-ofn secret-sharing problem, for Ag = {1, 2, . . . , n}, initially each agent i ∈ Ag privately holds a "share" fi of a secret f0, and any m "good" agents can collaborate to learn the secret in spite of the remaining n-m "bad" agents 2 . In the rational version of this scenario, the objective of each agent is to learn the secret, i.e., she prefers to learn the secret rather than not to learn it. Richer, non-binary, preferences can also be handled, including the fact that an agent may prefer that the least number of other agents learn the secret. For simplicity we do not consider such extensions here.

1 The framework can also support every agent having finitelymany Boolean objectives aggregated by means of a reward function such as max, cf. [Kupferman et al., 2016].

We can model this scenario as an iCGS as follows. The secret is the value of a variable s initially hidden from all agents (formally, a variable v with finite domain D is modelled as |D|-many atomic propositions); agent i's share is modelled as a private variable fi; each agent has a private variable si that represents what she thinks the secret is; at every step, every agent broadcasts a message (from some fixed finite set of M messages). Finally, the objective γi of each agent i can be formalised as the LTLK-formula FGKi(si = s): from some point on, agent i knows the secret. Thus, the ESLformula 〈〈x1〉〉 . . . 〈〈xn〉〉RatSynϕ(x) expresses that there is a Nash equilibrium satisfying ϕ in the rational secret-sharing scenario. For instance, one can use ϕ to express that agents make "true" statements, e.g., that if agent i broadcasts "my share is x", then indeed fi = x. Observe that by using ESL specifications we can naturally express secrecy and strategic concepts.

4 Model Checking BA-iCGS against ESL

In this section we prove the main technical result of this paper.

Theorem 6. Model checking BA-iCGS against ESL specifications is decidable and non-elementary complete.

For the non-elementary lower-bound we use the observation that model-checking SL on CGS (i.e., with perfectinformation) is non-elementary [Mogavero et al., 2014], together with the fact that by encoding the last joint action into the states, one can translate a CGS S into a BA-iCGS S′ such that for all sentences ϕ in ESL, we have that S |= ϕ iff S′ |= ϕ (the same procedure is used in [Belardinelli et al., 2017]).

For the non-elementary upper-bound, we reduce the model-checking problem of BA-iCGS against ESL specifications to model checking regular-trees against Monadic Second-Order Logic (MSO). The na¨ıve approach is to code every tuple (S, h, χ) by a tuple of functions (̂S, ̂h, ̂ χ) each of whose domain is the set ACT∗ of finite sequences of joint actions, and whose ranges are finite (to be specified later). This encoding allows us to build, for every ESL-sentence ϕ, an MSO-formula Φ, such that (S, h, χ) |= ϕ iff T |= Φ(̂S, ̂h, ̂ χ), where T is the infinite ACT-ary tree generated by ̂S, ̂h, and ̂ χ. The latter problem is decidable if ̂S, ̂h, and ̂ χ are regular functions (a function f : D∗ → L is regular if, for each l ∈ L, the set f -1 (l) ⊆ D∗ is accepted by a finite automaton). Since ϕ is a sentence we can choose χ arbitrarily, in particular so that it is regular (on the other hand, both ̂S and ̂h are always regular).

2 In Shamir's scheme this is implemented by an initially unknown polynomial f of degree m - 1 in some finite field F with |F | > n and f(0) ̸= 0; the secret is f(0), each share is f(i), and thus any m shares uniquely determine the secret (by interpolation).

Monadic Second-Order Logic. Below we summarise MSO, which extends first-order logic with variables for sets, and recall the fundamental theorem, i.e., that MSO is decidable on regular-trees [Rabin, 1969]. The syntax of MSO includes Boolean operators ¬ and ∧; individual variables u, v,w, . . .; set variables U, V,W, . . .; quantifiers over these variables ∃u, ∃U, . . .; binary relation symbols ∈, =, and ⪯; and unary function symbols sucd for every d in a finite set ∆ of directions. We denote formulas of MSO by Φ,Ψ, . . .. The semantics of MSO is defined over the structure T∆ = 〈∆∗ , {sucd}d∈∆〉, called the unlabelled ∆-ary tree. The interpretation of individual variables are elements in ∆∗ , of set variables are subsets of ∆∗ ; Boolean operators and quantifiers are interpreted as usual; atoms u ∈ U and u = v as usual; while u ⪯ v is the prefix relation, and sucd(u) = ud for d ∈ ∆, u ∈ ∆∗ . We will often think of u ∈ ∆∗ as the singleton set U = {u} ⊆ ∆∗ . Formulas Φ(U) with free variables U are interpreted in expanded structures (T∆,A), called labelled ∆-ary trees, where each Ai ⊆ ∆∗ . Instead of writing (T∆, A) |= Φ(U), we may write T∆ |= Φ(A), or simply A |= Φ. A labelled-tree (T∆,A) is regular if each Ai ⊆ ∆∗ is accepted by a finite automaton.

Theorem 7. [Rabin, 1969] There is a non-elementary time algorithm that, given an MSO-formula Φ(U) and a regular labelled-tree (T∆, A), decides whether T∆ |= Φ(A). Also, if T∆ |= ∃U Φ(U) then there is a regular labelled-tree (T∆, A) such that T∆ |= Φ(A), and the finite automata for all Ai ⊆ ∆∗ are computable.

We use standard shorthands, e.g., ϵ for the root; X = Y for ∀v(v ∈ X ↔ v ∈ Y ), etc. Say that A′ is definable from A if for each i there is an MSO-formula ϕi(x) such that A |= ∀x(ϕi(x) ↔ x ∈ A′i ). For an MSO-formula Φ(U), we define Φ[A′ ← A] for the MSO-formula formed from Φ in which every variable Ui is replaced by the definition ϕi of A′i . Then A′ |= Φ iff A |= Φ[A′ ← A]. We now introduce some abbreviations, i.e., variables for functions with finite ranges:

Definition 8 (Unary Function Variables). Let Θ be a finite set of sorts. Associate with each type θ ∈ Θ a finite set of labels Lθ. For every sort θ, we introduce unary function variables α, β, . . . of that sort, and quantification, i.e, ∃α, ∃β, . . .. Define the interpretation of variable α of sort θ by a function of the form α : ∆∗ → Lθ. We write α |= Φ to denote (T∆, α) |= Φ. If α′ is definable from α, we write Φ[α′ ← α] for the substitution as above.

We remark that this extension does not add expressive power. Indeed, we can replace the function variable α of sort θ by a |Lθ|-tuple of set variables X, and replace every term α(v) = d by the expression v ∈ Xd.

Directions and sorts. Fix a BA-iCGS S, the direction set ∆ = ACT, and the set Θ to consists of four sorts:

• D with labels LD = S0 → S (for representing iCGS);
• H with LH = S0 ∪ {⊥} (for histories);
• R with LR = S0 → Act (for strategies);
• K with LK = S0 → ((Var ∪ Ag) → Act) (for assignments).

Encoding (S, h, χ) by functions. Recall the bijection µ : hist(S) → S0 × ACT∗ in Def. 3 and that we write h =

µ(sh, uh) (Section 2.2). The structure S is encoded by a function ˆS of sort D; a history h by a function ˆh of sort H; an assignment χ by a function ˆχ of sort K; and a strategy σ by a function ˆσ of sort R, as follows 3 :

• ̂S(v)(t) = tr(t, v) for all v ∈ ACT∗ , t ∈ S0.
• ̂h(uh) = sh, and ̂h(v) = ⊥ for all v ∈ ACT∗ with v ̸= uh.
• ̂ σ(v)(t) = σ(µ(t, v)) for all v ∈ ACT∗ , t ∈ S0.
• ̂ χ(v)(t)(x) = χ(x)(µ(t, v)) for all v ∈ ACT∗ , t ∈ S0, x ∈ Var ∪ Ag.

Expressing ESL in MSO. We now show how to express in MSO that a function variable α of a given sort is a valid encoding. First, we can express that a function variable α of sort H is of the form ̂h for some history h, i.e., ∃x(α(x) ∈ S0 ∧ ∀y(y ̸= x → (α(y) = ⊥))). Second, we can express that a function variable α of sort D is of the form ̂S, i.e., ∧t∈S (α(ϵ)(t) = t ∧ α(sucd(v))(t) = tr(α(v)(t), d)). Third, for every ESL formula ϕ, we can express that a function variable of sort K is of the form ̂ χ for some ϕ-compatible assignment χ. To do this, it is sufficient to express, for a ∈ Ag, that a function variable α of sort R is of the form ̂ σ for some strategy σ that is coherent and uniform for agent a. Coherency is easy: Ca(α) := ∀v ∧s∈S0 α(v)(s) ∈ Acta. For uniformity, we use the characterisation in Proposition 1: Ua(α) := ∧s,s′∈S0 ∀v (Ea s,s′ (v) → (α(v)(s) = α(v)(s′ ))) where Ea s,s′ (v) is ∀w(w ⪯ v → (̂S(w)(s) ∼a ̂S(w)(s′ ))).

The remainder of the proof is by structural induction. Inductive hypothesis. For every ESL-sentence ϕ and BAiCGS S one can construct an MSO-formula Φ such that (S, h, χ) |= ϕ if and only if (̂S, ̂h, ̂ χ) |= Φ (for all h, χ).

Atomic predicate ϕ = p. Define Φ by ∨s0∈S0,s∈λ-1 (p) ∃v(̂h(v) = s0 ∧ ̂ S(v)(s0) = s).

Boolean operators. For ϕ = ¬ϕ1 define Φ = ¬Φ1; and for ϕ = ϕ1 ∧ ϕ2 define Φ = Φ1 ∧ Φ2.

Strategic operator ϕ = 〈〈x〉〉ϕ1. Define Φ by ∃α ∧a∈shr(x,ϕ) (Ca(α) ∧ Ua(α) ∧ Φ′1 ), where Φ′1 is Φ1 in which ̂ χ(v)(s)(x) is replaced by α(v)(s).

Binding operator ϕ = (x, a)ϕ1. Define Φ by Φ1[ ̂ χ′ ← ̂ χ] where, writing χ′ for χaχ(x) , the encoding ̂ χ′ is definable from ̂ χ as follows: ̂ χ′ (v)(t)(y) equals ̂ χ(v)(t)(y) if y ̸= a, and equals ̂ χ(v)(t)(x) if y = a.

Epistemic operator ϕ = Kaϕ1. The formula Φ is ∧s,t∈S0 ∀u ((̂h(u) = s ∧ Ea s,t (u)) → Φ1[ ̂ h′ ←̂h]), where h′ = µ(t, u) (note that ̂ h′ is definable from u and t). The other epistemic operators are treated similarly.

Next operator ϕ = Xϕ1. It is sufficient to note that, writing h′ = π(h, χ|Ag)≤|h|+1, the encoding ̂ h′ is definable from ̂ χ and ̂h as follows: ̂ h′ (v) = t if ̂h(u) = t and v = sucJ(u) and J(a) = ̂ χ(u)(t)(a), else ̂h(v) = ⊥.

Until operator ϕ = ϕ1 Uϕ2. Note that a) for every s ∈ S0 there is an MSO-formula Ps(U, u) that says that U is an infinite branch, u ∈ U, and that after u the branch U continues by following the joint full strategy induced by ̂ χ from initial state s; and b) µ(s, u) ∈ out(S, h) can be expressed in terms of ̂h by ∃x(u ⪯ x ∧ ̂h(x) = s). Thus, the translation of Fϕ2 ≡ trueUϕ2 (the full operator U is similar) is ∨s∈S0 ∃U∃u(Ps(U, u) ∧ ̂h(u) = s ∧ ∃̂ h′∃v ∈ U(u ⪯ v ∧ ̂ h′ (v) = s ∧ Φ2[ ̂ h′ ← ̂h])). This completes the induction.

3 Hereafter tr : S0 × ACT∗ → S is defined by tr(s, ϵ) = s and tr(s, vx) = tr(tr(s, v), x) for v ∈ ACT∗ , x ∈ ACT.

The size of Φ is polynomial in the size of the input (i.e., ϕ, S). Applying Theorem 7 we get the stated non-elementary upper-bound. This completes the proof of Theorem 6.

Application to Rational Synthesis. By the discussion in Section 3.1, we immediately get the first part of the following:

Corollary 1. Rational synthesis for LTLK objectives on BAiCGS is decidable. Moreover, if a given instance returns "yes", then a finite-state Nash equilibrium can be computed.

For the second part, apply the translation presented above to the ESL-formula RatSyntrue(x) and a BA-iCGS S (say with |Ag| = n) to get an MSO-formula Φ(U) such that for all strategy profiles σ, we have that S |= RatSyntrue(x) iff (̂ σ1, . . . , ̂ σn) |= Φ. Now, by Theorem 7 applied to Φ, one can compute regular languages Ai ⊆ ACT∗ such that A |= Φ. Since these languages code strategies, we have computed finite-state strategies σi such that S |= RatSyntrue(σ).

5 Conclusions

One of the key problems in reasoning about strategic abilities in MAS under incomplete information and perfect recall is that the model checking and synthesis problems are undecidable even for relatively weak logics such as ATL. Yet, MAS applications require specifications that are more expressive than ATL, e.g., capable of expressing solution concepts such as Nash equilibria. Identifying classes of systems for which these two desiderata can be combined remains a challenge. In this paper we have made a contribution towards this aim.

Specifically, we defined ESL, a combination of Strategy Logic and Epistemic Logic. We observed that model checking and synthesis are undecidable under synchronous perfectrecall semantics. However, we showed that a noteworthy subclass of systems, those that admit only broadcast actions, admit decidable model checking and synthesis, and identified tight bounds for the model-checking problem.

We have illustrated the expressivity of the formalism by phrasing rational synthesis under incomplete information, a previously unexplored set-up, as an instance of model checking for ESL. This has the noteworthy consequence that rational synthesis is decidable in the framework. It follows that we can decide expressive strategic properties of rational secretsharing scenarios like the one presented in Section 3.2 under the assumption of non-randomised strategies. We leave the exploration of other scenarios for future work.

Acknowledgements

This research was partly supported by EPSRC (grant EP/I00529X), INdAM (grant "Logica e Automi per il Model Checking"), the ANR JCJC (project SVeDaS) and an INdAM Marie Curie fellowship to S. Rubin. The authors thank Benjamin Aminof for fruitful discussions.