The Complexity of Model Checking Knowledge and Time

1 Introduction

A central aspect of multi-agent systems is that agents only have partial knowledge about the system [Parikh and Ramanujam, 1985]. Epistemic logics are a standard framework to reason about what agents know about the world and each others' knowledge. In order to talk about behaviours of ongoing multi-agent systems, epistemic logics have been combined with temporal logics such as LTL [Pnueli, 1977], CTL and CTL∗ [Emerson and Halpern, 1986]. The resulting epistemic temporal logics can express properties of the evolution of agents' knowledge over time. These logics have been applied to the modelling and analysis of, e.g., distributed protocols [Ladner and Reif, 1986; Fagin et al., 2004], information flow and cryptographic protocols [van der Meyden and Su, 2004; Halpern and O'Neill, 2005] and knowledge-based programs [van der Meyden and Vardi, 1998].

The satisfiability problem for this family of logics has been thoroughly studied in [Halpern and Vardi, 1986; Halpern and Vardi, 1989], which categorise epistemic temporal logics according to a number of criteria: (1) is the system synchronous or asynchronous; (2) does it have a unique initial state known to all agents; (3) do agents have bounded memory or perfect recall; (4) can agents learn; (5) is the temporal part of the language linear or branching; (6) can the epistemic part of the language talk about the knowledge of several agents; and (7) can it talk about common knowledge. By considering all the possible combinations, the authors identify 96 logics and study their satisfiability/validity problem. Sound and complete axiomatization for those of these logics that admit one are also provided in [Halpern et al., 2004].

While the picture is clear for satisfiability and axiomatization of these logics, it is not entirely the case for the modelchecking problem, which is arguably at least as important for the verification of multi-agent systems as satisfiability or axiomatization (see for instance [Dechesne and Wang, 2010]).

For agents with bounded memory the situation is well understood. In particular, for the asynchronous setting, adding knowledge operators and even common-knowledge operators to LTL, CTL or CTL∗ does not increase the complexity of model checking: it is PSPACE-complete for extensions of LTL and CTL∗ [Kong and Lomuscio, 2017] and PTIMEcomplete for extensions of CTL [Raimondi, 2006]. For the synchronous setting, the situation is similar, but for extensions of CTL, the problem becomes PSPACE-complete [Engelhardt et al., 2007; Huang and van der Meyden, 2010].

For agents with perfect recall, the problem is undecidable when common knowledge is part of the language [van der Meyden and Shilov, 1999]. For the extensions of LTL, CTL and CTL∗ with knowledge but no common knowledge operators, denoted respectively LTLK, CTLK and CTLK∗ , model checking is instead decidable but non-elementary [van der Meyden and Shilov, 1999; Alur et al., 2007; Dima, 2009; Aucher, 2014; Bozzelli et al., 2015]. It was noted that the non-elementary blow-up depends on the alternation depth of formulas, the maximal number of alternations between knowledge operators for different agents: each additional alternation forces to maintain in the model-checking procedure an additional layer of information about what agents know. For a fixed alternation depth k ≥ 1, in the synchronous setting model checking is known to be in k-EXPSPACE for LTLK [van der Meyden and Shilov, 1999]. For both the synchronous and asynchronous semantics, it is known to be in (k - 1)-EXPSPACE for CTLK [Alur et al., 2007], and in kEXPTIME for CTLK∗ [Aucher, 2014; Bozzelli et al., 2015]. However it is not known whether these bounds are tight.

We show that they are tight only for CTLK: we prove that model-checking for LTLK, CTLK and CTLK∗ is actually (k - 1)-EXPSPACE-complete for alternation depth at most k, both for synchronous and asynchronous semantics. The upper bounds for synchronous and asynchronous CTLK∗ and LTLK are new, and the lower bounds are new for all six logics. We summarise the main results in Table 1. We point out that our PSPACE-completeness result for the fragment of LTLK with alternation depth one generalises that for synchronous LTLK with one agent proved in [Engelhardt et al., 2007].

Note that the complexity of model checking is often studied for models that are given by an explicit description of their states and transitions, which is what we consider in this work. More recently some works started to study the complexity of model checking multi-agent systems for succinct representations [Lomuscio and Raimondi, 2006; Huang et al., 2015].

2 Preliminaries

Let N be the set of natural numbers. For all n, k ∈ N, define Tower(n, 0) = n and Tower(n, k + 1) = 2Tower(n,k) .

Let w be a finite or infinite word over some finite alphabet Σ. We denote by |w| the length of w (we set |w| = ∞ if w is infinite). For all 0 ≤ i, j < |w|, with i ≤ j, wi is the i-th letter of w, w≤i is the prefix of w that ends at position i, w≥i is the suffix that starts at position i, and w[i,j] = wi . . .wj. For words w and w′ , we write w ≼ w′ if w is a prefix of w′ .

2.1 Epistemic Temporal Logics

We recall the logic CTLK∗ and its fragments LTLK and CTLK, which respectively correspond to extensions of CTL∗ , LTL and CTL with knowledge operators.

Let us fix a countably infinite set of atomic propositions AP and a finite set of agents Ag. The sets of history formulas ϕ and path formulas ψ are defined as follows:

where p ∈ AP and a ∈ Ag, X and U are the standard next and until temporal operators of LTL, E is the existential path quantifier of CTL∗ , and Ka is the knowledge operator for agent a from epistemic logics. Formula Kaϕ reads as "agent a knows that ϕ is true". As usual we define Aψ := ¬E¬ψ. The language of CTLK∗ consists of the history formulas. We let Sub(ϕ) be the set of subformulas in ϕ, and we define the size of a formula ϕ as |ϕ| = |Sub(ϕ)|. We call alternation depth of a formula ϕ, written ad(ϕ), the maximum number of alternations between knowledge operators for different agents in the formula. For instance, ad(p) = 0, ad(Kap) = 1, ad(Ka¬Kap) = 1 and ad(KbKaq ∨ Kap) = 2.

Fragments of CTLK∗ We consider the usual syntactic fragments LTLK and CTLK of CTLK∗ . LTLK consists of formulas of the form Aψ or ¬Aψ where path quantifiers in ψ are immediately preceded by knowledge modalities. CTLK is obtained by requiring that the temporal modalities X and U are immediately preceded by a path quantifier . For every k ∈ N, we define LTLKk, CTLKk and CTLK∗k the restrictions of LTLK, CTLK and CTLK∗ , respectively, to formulas of alternation depth at most k.

Semantics CTLK∗ formulas are interpreted over Kripke structures equipped with one indistinguishability relation ∼a for each agent a.

Definition 1 (Models). A Kripke structure (KS) is a structure M = (AP, S,R, V, {∼a}a∈Ag, sι ), where AP ⊂ AP is a finite subset of atomic propositions, S is a set of states, R ⊆ S × S is a left-total transition relation, V : S → 2AP is a valuation function, ∼a ⊆ S × S is an equivalence relation, for each a ∈ Ag, and sι ⊆ S is an initial state.

The size |M| of M is the number of states in M. A path is an infinite sequence of states π = s0s1 . . . such that for all i ≥ 0, siRsi+1, and a history τ is a non-empty prefix of a path. We denote by Hist(s) (resp., Path(s)) the set of histories (resp., paths) that start in s. Unless specified otherwise, all histories and paths are assumed to start in the initial state sι . For I ⊆ S, we write R(I) = {s′ | ∃s ∈ I s.t. sRs′ } for the set of successors of states in I. Finally, for a ∈ Ag and s ∈ S, we let [s]a be the equivalence class of s for relation ∼a. For a history τ, lst(τ) is the last state of τ.

We consider the classic synchronous and asynchronous perfect recall semantics of knowledge modalities, where agents remember all of the past. While in synchronous systems, agents always observe when a transition takes place, in asynchronous ones agents cannot tell that a transition occurred if their observation of the state remains unchanged.

Definition 2. Two histories τ and τ ′ are indistinguishable for an agent a with synchronous perfect recall (SPR for short), written τ ≈sa τ ′ , if they are point-wise indistinguishable to a, i.e. |τ| = |τ ′ | and τi ≈a τ ′ i for each i < |τ|.

To define asynchronous perfect recall, we first define the sequence of observations that an agent has along a history, in which sequences of successive identical observations collapse to a single observation. Formally, for an agent a, we let Obsa(s) = [s]a, Obsa(τ · s) = Obsa(τ) · [s]a if [s]a ̸= lst(Obsa(τ)), and Obsa(τ) otherwise.

Definition 3. Two histories τ and τ ′ are indistinguishable for an agent a with asynchronous perfect recall (APR for short), written τ ≈as a τ ′ , if Obsa(τ) = Obsa(τ ′ ).

Definition 4 (Semantics). Fix a model M. The SPR (resp., APR) semantics of a history formula ϕ on a history τ and a path formula ψ on a path π and a point in time n ∈ N is defined by induction as follows (Boolean cases are omitted):

A model M with initial state sι satisfies a CTLK∗ formula ϕ under the SPR (resp., APR) semantics, written M |=sy ϕ (resp., M |=as ϕ), if sι |= ϕ under the SPR (resp., APR) semantics. The model-checking problem for the SPR (resp., APR) semantics, of which we study the complexity, is checking for a finite model M and a formula ϕ, whether M |=sy ϕ (resp., M |=as ϕ). In this work we prove the following result.

Theorem 1. For every k ∈ N, the model-checking problem for LTLKk+1, CTLKk+1 and CTLK∗k+1 is k-EXPSPACEcomplete, both for SPR and APR semantics.

In the rest of this work, every time a definition or result holds for both semantics, we write ≈a instead of ≈sa or ≈as a .

3 Powerset Construction

In this section we recall a classic powerset construction for algorithmic questions related to imperfect information. It was first used by Reif in [Reif, 1984] to eliminate imperfect information from two-player games, and in [van der Meyden, 1998; van der Meyden and Shilov, 1999; Alur et al., 2007] to model check variants of LTLK and CTLK. We show that it also can be used to model check CTLK∗ .

3.1 Information Sets and Updates

An information set captures the set of states that an agent considers possible at a given moment. The following definition is common to synchronous and asynchronous perfect recall.

Definition 5. Given a model M with state set S, an information set I ⊆ S is a set of states. Given a history τ and an agent a, the information set of a at τ is defined as

We will write I sy a when referring to the synchronous semantics, and I as a for the asynchronous one.

We now define two different update functions, one for the synchronous and one for the asynchronous case. The role of these functions is to compute the new information set of an agent after a transition, given her former information set and the new state. We start with the synchronous case.

Definition 6. The synchronous update of an information set Ia for agent a with a new state s is

This definition says that the set of states that agent a considers possible after taking a transition that arrives in state s consists of all states that are successors of states she previously considered possible, and that are compatible with what she observes of the new state. For asynchronous perfect recall, the update is slightly more involved, as the agent may consider that arbitrarily many steps occurred that did not change his observation. We call invisible step (for some agent a) a transition between two states s and s′ such that s ∼a s′ , and given a set of states I, we let Reachai (I) ⊇ I be the set of states reachable from I via steps invisible for a. We can now define the update as follows:

Definition 7. The asynchronous update of an information set Ia for agent a with a new state s is

This definition is an adaptation to our setting of the one in [Puchala, 2010], which considers two-player games. The following result follows directly by applying the definitions:

3.2 Powerset Construction

Given a model M we define a powerset model ̂ M of exponential size in which formulas of alternation depth 1 can be evaluated positionally. States of ̂ M contain, in addition to the current state in M, the current information set of each agent. This construction can be instantiated either for the synchronous or asynchronous semantics by choosing the appropriate update function for information sets. In the following we will often omit to specify which semantics is considered, because the construction and reasoning work for both.

Definition 8. Given M = (AP, S, R, V, {∼a}a∈Ag , sι ), we define ̂ M = (AP, ̂ S, ̂R, ̂ V , {̂∼a}a∈Ag , ̂ s ι ), where

• ̂ S = S × (2S )Ag
• (s, 〈Ia〉a∈Ag) ̂R(s′ , 〈I ′a 〉a∈Ag) if sRs′ and for each a ∈ Ag, I ′a = Up(Ia, s′ )
• ̂ V (s, 〈Ia〉a∈Ag ) = V (s)
• for b ∈ Ag, (s, 〈Ia〉a∈Ag)̂∼b(s′ , 〈I ′a 〉a∈Ag) if s′ ∈ Ib and Ib = I ′b
• ̂ s ι = (sι , 〈{sι }〉a∈Ag )

Note that |̂ M| = |M|2|Ag||M| . Because the update of information sets with a new state is deterministic, every history τ in M defines a unique history ̂ τ of length |τ| in ̂ M, that starts in ̂ s ι and follows transitions in τ. The next lemma follows by definition of ̂ M, ̂ τ and application of Lemma 2.

Lemma 3. For every history τ,

We now describe how formulas of alternation depth one can be evaluated positionally in the powerset model ̂ M.

Definition 9. Given a powerset model ̂ M, a state ̂ s ∈ ̂ S and a path ̂ π, the alternative semantics of a CTLK∗1 formula is defined inductively as follows (we omit Boolean cases):

We cannot evaluate nested knowledge operators for different agents because we have only one "level" of knowledge in the states of ̂ M. However we can evaluate nested knowledge operators for a same agent because indistinguishability relations between states ∼a, and thus also relations ≈a between histories, are equivalence relations: if τ ≈a τ ′ , then agent a knows the same things in τ and in τ ′ .

Proposition 4. For every history formula ϕ ∈ CTLK∗1 , each model M and history τ , τ |= ϕ iff lst(̂ τ) |=I ϕ.

4 Upper Bounds

In this section we establish the upper bounds in Theorem 1. All the reasoning in this section is independent of the chosen semantics, synchronous or asynchronous perfect recall. We first show how to solve the case of alternation depth one in PSPACE, and then how to eliminate one level of alternation at the cost of an exponential blowup in the size of the model.

4.1 Alternation Depth One

Our PSPACE model-checking procedure contains three main ingredients. The first one is the on-the-fly construction and resolution of B¨uchi automata for LTL formulas [Vardi and Wolper, 1994]. We combine it with an on-the-fly construction of the powerset model, already used in [Alur et al., 2007] for a variant of CTLK, which allows us to evaluate LTLK formulas of alternation depth one positionally. Finally, we use the meta-algorithm by Emerson and Lei [Emerson and Lei, 1987] to extend this procedure from LTLK to CTLK∗ .

In the main model-checking procedure, formulas of the form Eψ are dealt with by guessing a path in the powerset model and evaluating ψ on it. However for our algorithm to terminate, we need to bound the length of paths that need to be searched, and we need this bound to be at most exponential so that we can count up to it in polynomial space. We now prove that this can be done.

An infinite word w is ultimately periodic if there exist i, j ∈ N such that w = w≤i-1w∗ [i,j] . Letting i and j be the smallest such values, we call i the start index of π, and j - i + 1 is called its period.

Lemma 5. Let ψ be a CTLK∗ path formula of alternation depth at most 1, let M be a model, ̂ M the powerset model, and ̂ s a state in ̂ M. If ̂ s |= Eψ, then there exists a path ̂ π starting in ̂ s such that ̂ π |=I ψ and ̂ π is ultimately periodic with start index and period less than |M|2|Ag||M|+|ψ| .

Proof sketch. We turn ψ into an LTL formula ψ′ by evaluating and marking its maximal history subformulas in the powerset model ̂ M. We then build a nondeterministic B¨uchi word automaton Aψ′ that accepts exactly the models of ψ′ and has at most 2|ψ′ | states [Vardi and Wolper, 1994]. By taking the product of Aψ with ̂ M, we obtain an automaton  M′ ,ψ′ over the states of ̂ M ′ that has size at most |M|2|Ag||M|+|ψ′ | and accepts precisely paths in ̂ M ′ that satisfy ψ′ . By definition of the B¨uchi acceptance condition, if there is such a path ̂ π′ , there is an ultimately periodic one of start index and period less than the size of  M′ ,ψ′ , i.e. |M|2|Ag||M|+|ψ| .

Proposition 6. Model checking CTLK∗1 is in PSPACE.

Proof sketch. We adapt Emerson and Lei's algorithmwhich shows how to turn a polynomial-space model-checking procedure for LTL into one for CTL∗ that also runs in polynomial space [Emerson and Lei, 1987]. The interesting case is for formulas of the form Eψ. The proof of Lemma 5 provides a model-checking procedure for such formulas, but building the full automaton Aψ and powerset model ̂ M takes exponential space. We tackle this by building them both on the fly. The marking procedure of maximal history subformulas in states of ̂ M is replaced with recursive calls to the model-checking procedure for CTLK∗1 , and by Lemma 5 we can implement in polynomial space a counter that indicates when the nondeterministic search of a satisfying path can be stopped.

4.2 Reducing Alternation

We show how to use the powerset construction to eliminate one level of alternation of knowledge operators.

Proposition 7. Given a CTLK∗ formula Φ of alternation depth k + 1 and a model M, one can build a model M ′ of size at most |M|2|Ag||M| and a CTLK∗ formula Φ′ of alternation depth k and size |Φ′ | ≤ |Φ| such that

The construction of M ′ is as follows. First, build the powerset model ̂ M as in Definition 9. In this model, history formulas of alternation depth one can be evaluated positionally, as stated in Proposition 4. Let Sub1(Φ) be the set of such formulas in Sub(Φ). For each formula ϕ in Sub1(Φ) and each state ̂ s of ̂ M, evaluate whether ̂ s |=I ϕ (since |=I is the memoryless semantics of CTLK∗ , this can be done in PSPACE [Kong and Lomuscio, 2017]), and mark state ̂ s with the fresh atomic proposition pϕ if ̂ s |=I ϕ. We abuse notation and still call ̂ M the model obtained after this marking procedure (and similarly, ̂ s, ̂ τ and ̂ π refer to states, histories and paths in the marked model). Also, for every subformula ϕ of Φ, define ̂ ϕ by replacing each ϕ′ in Sub1(ϕ) with atom pϕ′ .

Unlike in Proposition 4, where we use the alternative memoryless semantics to evaluate positionally formulas of alternation depth one, this time we interpret ̂ ϕ on ̂ M with the perfectrecall semantics. One can prove the following lemma:

Lemma 8. For every history subformula ϕ and every history τ inM, it holds that τ |= ϕ iff ̂ τ |= ̂ ϕ.

Using Proposition 7 for the inductive case and Proposition 6 for the base case, we prove by induction on k that:

Theorem 9. For k ∈ N, model checking of CTLK∗k+1 for both the SPR and APR semantics is in k-EXPSPACE.

5 Lower Bounds

In this section, we establish the following result which provides lower bounds for model checking against CTLK∗ , matching the upper bounds of Theorem 9.

Theorem 10. For k ∈ N, model checking of CTLK∗k+1 for both the SPR and APR semantics is k-EXPSPACE-hard even if the formula is assumed to be a fixed LTLKk+1 ⋂ CTLKk+1 formula and the number of agents is 2.

Theorem 10 is proved by a polynomial-time reduction from a suitable domino-tiling problem [Boas, 1997]. An instance I of such a problem is a tuple I = (C,∆, n, din, dacc), where C is a finite set of colours, ∆ ⊆ C 4 is a set of tuples (cdown, cleft, cup, cright) of four colours, called dominotypes, n > 0 is a natural number encoded in unary, and din, dacc ∈ ∆ are domino-types. Given k ∈ N, a k-grid of I is a mapping f : [0, ℓ] × [0, Tower(n, k) - 1] → ∆ for some ℓ ∈ N. Intuitively, a k-grid is a finite grid, where each row consists of Tower(n, k) cells, and each cell contains a domino type. A k-tiling of I is a k-grid f satisfying:

Initialisation and Acceptance: f(0, 0) = din and f(ℓ, j) = dacc for some j ∈ [0, Tower(n, k) - 1];

Row adjacency: two adjacent cells in a row have the same color on the shared edge: for all (i, j) ∈ [0, ℓ] × [0, Tower(n, k) - 2], [f(i, j)]right = [f(i, j + 1)]left

Column adjacency: two adjacent cells in a column have the same color on the shared edge: for all (i, j) ∈ [0, ℓ -

Given k ∈ N, the problem of checking the existence of a k-tiling for I is k-EXPSPACE-complete [Boas, 1997]. Hence, Theorem 10 directly follows from the following proposition.

Proposition 11. Let k ≥ 0. There is a fixed formula ϕk of LTLKk+1 ⋂ CTLKk+1 s.t. one can build, in time polynomial in the size of I, a Kripke structure MI,k with two agents so that I has a k-tiling iff MI,k |=sy ϕk (resp., MI,k |=as ϕk).

Proof of Proposition 11 for the synchronous setting We first provide a proof of Proposition 11 for the synchronous setting. At the end of this section, we explain the easy adaptation for the asynchronous case. Fix k ≥ 0. We assume that k ≥ 1 (the proof for the case k = 0 being simpler).

First, we define a suitable encoding of the k-grids by infinite words over the set of propositions AP := Main ∪ Tags, where Main := ∆∪ {$1, . . . , $k, $, acc, ⊥, 0, 1} and Tags := {#1, #2, col, good} ∪ ⋃h=k h=1 {(h, =), (h, inc), (inc, h)}. The propositions in Main are used to encode the k-grids, while the propositions in Tags, whose meaning will be explained later, are used to mark in a suitable way the codes of k-grids.

In the encoding of a cell of a k-grid, we keep track of the content of the cell together with a suitable encoding of the cell number which is a natural number in [0, Tower(n, k) - 1]. Thus, for all 1 ≤ h ≤ k, we define the notions of h-block and well-formed h-block, where for h < k, well-formed hblocks are finite words over {$1, . . . , $h, 0, 1} encoding integers in [0, Tower(n, h) - 1], while well-formed k-blocks are finite words over ∆ ∪ {$1, . . . , $k, 0, 1} encoding the cells of k-grids. In particular, for h > 1, a well-formed h-block encoding a natural number m ∈ [0, Tower(n, h) - 1] is a sequence of Tower(n, h - 1) (h - 1)-blocks, where the ith (h - 1)-block encodes both the value and (recursively) the position of the ith -bit in the binary representation of m.

The set of (well-formed) h-blocks is defined by induction on h as follows. A 0-block is a bit b ∈ {0, 1}. The content of b is b itself, and b is initial (resp., final) if b = 0 (resp., b = 1).

For 1 ≤ h ≤ k, an h-block is a finite word bl of the form $hτsb0 . . . sbℓ$h such that (i) ℓ > 0, and ℓ = n - 1 if h = 1, (ii) τ ∈ {0, 1} if h < k, and τ ∈ ∆ otherwise (τ is the content of bl), (iii) for all 1 ≤ i ≤ ℓ, sbi is a (h-1)-block (the ith subblock of bl), and (iv) sb1 is initial and sbℓ is the unique final sub-block. The block bl is initial (resp., final) if the content of each sub-block sbi is 0 (resp., 1). The h-block bl is wellformed if either h = 1, or h > 1, ℓ = Tower(n, h - 1) - 1 and for all 0 ≤ i ≤ ℓ, sbi is well-formed and has index i. If bl is well-formed, then its index is the natural number in [0, Tower(n, h)-1] whose binary code is bit0, . . . , bitℓ, where bitj is the content of sbj for all 0 ≤ j ≤ ℓ.

Encoding k-grids A row-code wr = $bl0 . . . blℓ$ is a finite word such that bl0, . . . , blℓ are k-blocks, bl0 is initial, and blℓ is the unique final k-block. The row-code wr is well-formed if additionally, ℓ = Tower(n, k) - 1 and for all 0 ≤ i ≤ ℓ, bli is well-formed and has index i. A k-grid code (resp., wellformed k-grid code) is an infinite word over AP of the form w · τ ω such that (i) w is a finite sequence of row-codes (resp., well-formed row-codes), and (ii) τ = acc if the last row-code of w contains a block whose content is dacc (acceptance), and τ = ⊥ otherwise. A k-grid code is initialised if the first k-block of the first row-code is din. Note that while k-grid codes encode grids of I having rows of arbitrary length, wellformed k-grid codes encode the k-grids of I.

Construction of MI,k in Proposition 11 For the fixed k ≥ 1, we now illustrate the construction of the finite Kripke structure MI,k over two agents, say a1 and a2, in Proposition 11. Essentially, MI,k nondeterministically generates all the initialised k-grid codes with the additional ability of nondeterministically marking some positions with the propositions in Tags. The main idea is to decompose the verification that a k-grid code is well-formed and encodes a ktiling in layers implementable with polynomially many states of MI,k, and invoking other layers thanks to the knowledge modalities for the two agents a1 and a2. In particular, the propositions in Main are observable by both agents, while the tag propositions in Tags \ {#1,#2} are not observable by any agent. For the remaining two tag propositions #1 and #2, #1 (resp., #2) is observable by agent a1 (resp., a2) but not observable by agent a2 (resp., a1).

We now define the marking performed by the Kripke structure MI,k. For a word w over 2AP , the content of w is the word over 2AP\Tags obtained by removing from each letter in w the propositions in Tags. Let 1 ≤ h ≤ k. A tagged h-block is a word bl over 2AP whose content is an h-block and:

• the initial position of bl is marked by the tag #1 if h is odd, and the tag #2 otherwise;
• there is exactly one (h - 1)-sub-block sb of bl whose first position is marked by the tag #2 if h is odd, and the tag #1 otherwise; no other position of bl is marked.

A simple tagged h-block bl is defined in a similar way but we require that only the first position of bl is marked.

The initialised k-grid codes are marked by the model MI,k as follows. A tagged k-grid code is an infinite word ν over 2AP s.t. the content of ν is an initialised k-grid code and there are two (simple) tagged h-blocks bl and bl ′ along ν for some 1 ≤ h ≤ k so that: (i) bl ′ follows bl, (ii) there is a non-empty set O ⊆ Tags \ {#1, #2} so that each position in ν following the last position of bl ′ is marked by the tags in O, (iii) no other position of ν is marked, and (iv) the following holds:

(h,=)-tagging: bl and bl ′ are tagged h-blocks, {(h,=)} ⊆ O ⊆ {(h, =), good}, and good ∈ O iff the marked sub-block sb of bl and the marked sub-block sb ′ of bl ′ have the same content. Moreover, if h = 1, then sb (which is a marked bit) has the same position as sb ′ .

(h, inc)-tagging: bl and bl ′ are adjacent tagged h-blocks (i.e., adjacent within the same (h + 1)-block if h < k, and within the same row-code otherwise), {(h, inc)} ⊆ O ⊆ {(h, inc), good}, and good ∈ O iff for the last (h - 1)-subblock sb0 of bl whose content is 0, the marked sub-blocks of bl and bl ′ have the same content if the marked sub-block of bl precedes sb0, and have distinct content otherwise. Moreover, if h = 1, then the marked sub-block of bl has the same position as the marked sub-block of bl ′ .

simple (inc, h)-tagging: bl and bl ′ are adjacent simple tagged h-blocks, {(inc, h)} ⊆ O ⊆ {(inc, h), good}. Moreover, if h < k, then O = {(inc, h)}. If instead h = k, then good ∈ O iff [d]right = [d ′ ]left, where d ∈ ∆ (resp., d ′ ∈ ∆) is the content of bl (resp., bl ′ ).

column-tagging: h = k, bl and bl ′ are simple tagged kblocks belonging to two adjacent row-codes in ν, {col} ⊆ O ⊆ {col, good}, and good ∈ O iff [d]up = [d ′ ]down, where d ∈ ∆ (resp., d ′ ∈ ∆) is the content of bl (resp., bl ′ ).

A partial tagged k-grid code is the prefix of some tagged k-grid code whose last position is labelled by tags in Tags \ {#1,#2}. Thus, we have four different types of partial tagged k-grid codes ρ, where a type is identifiable by the tag proposition in Tags \ {#1,#2, good} which marks the last position of ρ. The additional proposition good is used to check whether some additional condition is fulfilled depending on the specific type. Intuitively, partial (h,=)-tagged kgrid codes are exploited as nested layers for checking that distinct well-formed h-blocks along the given initialised kgrid code have the same index, while partial (h, inc)-tagged k-grid codes are used as nested layers to check that the indices of adjacent h-blocks bl1 and bl2 are consecutive (i.e, bl1 is not final and the index of bl2 is the index of bl1 plus one). Finally, partial simple (inc, h)-tagged k-grid codes and partial column-tagged k-grid-codes are exploited as first-level layers for verifying well-formedness and the row adjacencyrequirement and column adjacency-requirement.

Let M be a Kripke structure over AP with valuation function V . A trace of M is a word ρ over 2AP of the form ρ = V (s0)V (s1) . . . where s0s1 . . . is a path or history of M (we say that ρ is the trace of s0s1 . . .). By construction, the following result is straightforward.

Lemma 12. Let k ≥ 1. One can construct in time polynomial in the size of I, a finite Kripke structure MI,k = (AP, S, R, V, {∼a}a∈{a1,a2}, sι ) such that:

1. the set of finite traces of MI,k coincides with the set of prefixes of tagged k-grid codes, and every initialised kgrid code is a trace of MI,k;
2. for all i = 1, 2 and states s and s′ , s ∼ai s′ iff V (s) ∩ (Main ∪ {#i}) = V (s′ ) ∩ (Main ∪ {#i}).

Construction of the fixed formula ϕk in Proposition 11 A K-propositional formula (resp., Kh-propositional formula for h ∈ N) is a CTLK∗ (resp., CTLKh) formula which does not have occurrences of temporal modalities and path quantifiers. By Lemma 12, histories of MI,k which have the same trace are indistinguishable by any agent and satisfy the same K-propositional formulas. Thus, for a finite trace ρ of MI,k and a K-propositional formula ψ, we write ρ |= ψ to mean that τ |= ψ under the SPR semantics for any history whose trace is ρ. We establish the following crucial technical lemma.

Lemma 13. Let k ≥ 1 and MI,k be the Kripke structure of Lemma 12. Then there are two fixed Kk+1-propositional formulas ϕrow and ϕcol, and for all 2 ≤ h ≤ k, a fixed Khpropositional formula ϕhbl , satisfying the following for each initialised k-grid code ν:

• if the (h - 1)-blocks in ν are well-formed, then ν≤i |= ϕhbl for all i ≥ 0 iff the h-blocks in ν are well-formed;
• if all k-blocks in ν are well-formed, then ν≤i |= ϕrow for all i ≥ 0 iff the row-codes in ν are well-formed and for all adjacent k-blocks bl and bl ′ in a row-code of ν such that bl ′ follows bl, [d]right = [d ′ ]left, where d ∈ ∆ (resp., d ′ ∈ ∆) is the content of bl (resp., bl ′ ).
• if ν is well-formed, then ν≤i |= ϕcol for all i ≥ 0 iff for all the k-blocks bl and bl ′ such that bl and bl ′ belong to two adjacent row-codes, bl ′ follows bl, and bl and bl ′ have the same index, it holds that [d]up = [d ′ ]down, where d ∈ ∆ (resp., d ′ ∈ ∆) is the content of bl (resp., bl ′ ).

Due to lack of space, the proof of Lemma 13 is omitted. Let ϕrow, ϕcol, ϕhbl be the fixed Kk+1-propositional formulas of Lemma 13, and ϕk be the fixed LTLKk+1 ⋂ CTLKk+1 formula E ((∧t∈Tags ¬t ∧ ϕrow ∧ ϕcol ∧ ∧kh=2 ϕhbl ) U acc). By Lemmata 12-13, MI,k |=sy ϕk iff there is a path of MI,k whose trace is a well-formed k-code encoding a k-tiling of I, which concludes the proof of Proposition 11 for the synchronous case. For the asynchronous case, we slightly modify the construction of model MI,k in Lemma 12 by incorporating a bit represented by a fresh proposition pb that is flipped at every transition and is observed by all agents. In such a way the resulting model M ′I,k generates the same traces as MI,k (modulo pb), and for all histories τ and τ ′ , τ ≈as a τ ′ iff τ ≈sa τ ′ (the asynchronous and synchronous semantics coincide). Lemma 13 holds for the new model as well. Hence, MI,k |=sy ϕk iff M ′I,k |=as ϕk and we are done.

6 Conclusion

In this work we settle the exact complexity of model checking epistemic temporal logics with synchronous and asynchronous perfect recall, a 20-year-old problem, by showing that it is (k - 1)-EXPSPACE-complete for formulas of alternation depth at most k ≥ 1. This almost closes the picture for the 96 logics identified by Halpern and Vardi in their seminal work on epistemic temporal logics [Halpern and Vardi, 1986], with the exception of the "no learning" assumption which has, up to our knowledge, never been studied in conjunction with model checking. With no learning most cases seem to boil down to known cases of bounded memory. The only exception is for synchronous bounded memory for CTLK, which we plan to investigate in order to finally close the full picture.