Introduction

Reasoning about knowledge and time is crucial for designing, and verifying properties of, distributed and multiagent systems. A number of temporal-epistemic logics were proposed as logical frameworks for modeling of, and reasoning about, these aspects of distributed systems in the 1980's. This research was summarized in the comprehensive study by Halpern and Vardi [7]. In that study, the authors considered several essential characteristics of temporal-epistemic logics, namely: one vs. several agents, synchrony vs. asynchrony, (no) learning, (no) forgetting, linear vs. branching time, and the (non)existence of a unique initial state. Based on these, they identify and analyze 96 temporal-epistemic logics and obtain lower bounds for the complexity of the satisfiability problem in all of them. It turns out that most of the systems with more than one agents who do not learn or do not forget are undecidable, often Π 1 1 -hard (with common knowledge), or decidable but with non-elementary time lower bound (without common knowledge). For most of the remaining logics, the lower bounds established in [7] for the multiagent case range from PSPACE (synchronous systems without common knowledge), through EXPTIME (with common knowledge), to EXPSPACE (synchronous systems with no learning and unique initial state).

Despite the conceptual importance and wide range of po-tential applications of temporal-epistemic logics, to the best of our knowledge, no efficient decision procedures for logics studied in [7] had been developed until quite recently, even for the systems with a relatively low known lower bounds. The only exception is [11], where a top-down tableau-style decision procedure for the logic ATEL, which subsumes the basic branching-time logic considered in [7] and this paper, was presented. In our view (to be explained further), however, [11] should be seen as a contribution to the complexity-theoretic analysis of the temporal-epistemic logics rather than to the development of efficient decision procedures for them.

In the recent precursor [5] to the present paper, we set out to fill in the above-mentioned gap by developing a practically efficient (within the theoretical complexity bounds) tableau-based decision procedure for the coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT) (for both the synchronous and asynchronous cases), building both on Wolper's incremental tableaux for LTL [13] and on our earlier work on tableaux for the full coalitional multiagent (purely) epistemic logic CMAEL(CD) [6].

In the present paper, we report on the second, and final, part of the project undertaken with the publication of [5]; namely, we present a sound, complete, and terminating incremental tableau for the Coalitional Multi-Agent Temporal Epistemic Logic with operators for Common and Distributed knowledge and Branching Time, CMA-TEL(CD+BT). The tableau procedure presented herein follows the tableau-building philosophy developed for the logics PDL by Pratt in [9], UB by Ben-Ari, Manna and Pnueli in [1], and CTL by Emerson and Halpern in [3]. Our procedure essentially combines incremental tableaux for CTL from the latter (see also [10] for a recent detailed exposition) and tableaux for the full coalitional multiagent epistemic logic CMAEL(CD) developed in [6]. In the present paper, as in [6], we work with a more expressive epistemic language than the one considered in [7], as it contains operators for common and distributed knowledge for all nonempty coalitions (i.e., subsets) of the set of agents. The resulting decision procedure for testing satisfiability in CMA-TEL(CD+BT) runs in exponential time, which is the optimal lower-bound, as established in [11].

We should mention that, even though the procedure presented in [11] can be used to test CMATEL(CD+BT)formulae for satisfiability, this would not give us the optimal procedure, since such a procedure would always require exponential time predicted by the worst-case estimate. The incremental tableau presented in this paper, on the other hand, on average requires much less time than the theoretical upper bound (this claim cannot be made mathematically precise without an a priori probability distribution on formulae; however, it is substantiated by example in [4], where we compare the incremental tableaux presented in that paper with the top-down tableux-style procedure from [12]).

Besides presenting the tableau-based procedure for CMATEL(CD+BT), the other major objective of this paper is to demonstrate how two tableau procedures for logics with non-interacting fixed-point operators (the epistemic and the temporal ones, in our case) can be combined into a tableau procedure for the fusion of these logics, thus offering a contribution to the area of combination of logics (see e.g., [8]).

The present paper is structured as follows. In Section 2, we introduce the logic CMATEL(CD+BT). In Section 3, we introduce Hintikka structures for CMA-TEL(CD+BT) and show that satisfiability of CMA-TEL(CD+BT)-formulae in Hintikka structures is equivalent to satisfiability in models introduced in Section 2. In Section 4, we present the tableau procedure for CMA-TEL(CD+BT) and, in Section 5, sketch out the proofs of soundness and completeness and briefly discuss the complexity of the procedure. The Appendix contains an example of a run of the procedure.

Syntax and semantics of the logic CMA-TEL(CD+BT)

The language L of CMATEL(CD+BT) contains a (possibly infinite) set AP of atomic propositions; the Boolean connectives ¬ ("not") and ∧ ("and"); the unary temporal operators ∃ g and ∀ g (existential and universal "next", respectively); the binary temporal operators ∃(− U−) and ∀(− U−) (existential and universal "until", respectively), as well as the unary epistemic operators D A ϕ ("it is distributed knowledge among agents in A that ϕ"), and C A ϕ ("it is common knowledge among agents of A that ϕ") for every non-empty A ⊆ Σ, where Σ is the finite, non-empty set of names of agents belonging to L. Subsets of Σ are called coalitions. Thus, the formulae of L are defined as follows:

ϕ := p | ¬ϕ | (ϕ 1 ∧ ϕ 2 ) | ∃ g ϕ | ∀ g ϕ | | ∃(ϕ 1 Uϕ 2 ) | ∀(ϕ 1 Uϕ 2 ) | D A ϕ | C A ϕ

where p ranges over AP and A ranges over the set P + (Σ) of non-empty subsets of Σ. We write ϕ ∈ L to mean that ϕ is a formula of L and ∆ ⊆ L to mean that ∆ is a set of such formulae.

Thus, L combines the language of Computational Tree Logic CTL [2] with the language of the full coalitional multi-agent epistemic logic CMAEL(CD) [6]. Although ∀ g ϕ is definable as ¬∃ g ¬ϕ, it is convenient to treat it as a primitive connective. The operator for individual knowledge K a ϕ ("agent a knows that ϕ"), where a ∈ Σ, can then be defined as D {a} ϕ, henceforth written D a ϕ. The other Boolean and temporal connectives can be defined as usual. We omit parentheses when this does not result in ambiguity.

Formulae of the form ¬C A ϕ are epistemic eventualities, while those of the form ∃(ϕ Uψ) and ∀(ϕ Uψ) are temporal eventualities.

The semantics of temporal-epistemic logics considered in [7] is based on system of runs with m processors (agents). A run is a function from (the set of natural numbers) N to the product L m regarded as the set of global states, where L is the set of local states; each agent can be in one of local states at any moment in time. Thus, a global state is a tuple l 1 , . . . , l m ; the i-th component l i of this global state representing the local view of the agent i. The pair (r, n), where r is a run and n ∈ N, is called in [7] a point. With every agent i, the authors of [7] associate the binary epistemic indistinguishability relation ∼ i on L m , defined as follows:

l 1 , . . . , l m ∼ i l ′ 1 , . . . , l ′ m if l i = l ′ i ; i.e.

, if the agent i has the same local views in these states.

According to [7], a system is synchronous when it has a 'global clock' observable by all agents and thus synchronizing their local times; formally, a system is synchronous if (r, n) ∼ i (r ′ , n ′ ) implies n = n ′ , for every i = 1, . . . , m, runs r, r ′ , and time moments n, n ′ . It turns out that the presence or absence of synchrony, under no other assumptions, does not affect the outcome of our tableau procedure, and therefore, the satisfiability of formulae.

The systems with (global) states represented as tuples of local states are generalized in [7] to systems where global states are abstract primitive entities and the epistemic relations are abstract equivalence relations on the set of such states. In the present paper, we work with this abstract semantics from [7]. We note that, as we show later, this semantics is more general than the above mentioned 'concrete' semantics from [7], despite the apparent assumption made in [7] that the two semantics are equivalent. We now turn to the presentation of the abstract semantics from [7].

Definition 2.1 A temporal-epistemic system (TES) is a tu- ple G = (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ) )

, where:

1. Σ is a finite, non-empty set of agents;

2. S = ∅ is a set of states;

3. R = ∅ is a set of runs: each r ∈ R′ ⊆A R D A ′ . A TES G is synchronous (STES) if ((r, n), (r ′ , n ′ )) ∈ R D A implies n = n ′ for every A ∈ P + (Σ).

Hereafter we write '(S)TES' to refer to general or synchronous temporal-epistemic system. Definition 2.2 Let (r, n) ∈ P (G) for some (S)TES G with a set of runs R and let r ′ ∈ R. We say that r ′ extends (r, n) if r(m) = r ′ (m) holds for all m ≤ n.

Definition 2.3 A (synchronous) temporal- epistemic frame ((S)TEF) is a (S)TES G = (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ) ), where each R D

A is an equivalence relation satisfying the following condition:

( †) R D A = a∈A R D {a}

If condition ( †) is replaced by the following, weaker one:

( † †) R D A ⊆ R D B whenever B ⊆ A,

then F is a (synchronous) temporal-epistemic pseudo-frame (pseudo-(S)TEF).

Notice that in (pseudo-)(S)TEFs R C A is the transitive closure of a∈A R D {a} , for every A ∈ P + (Σ); furthermore, in such structures, each R C

A is an equivalence relation.

Definition 2.4 A (synchronous) temporal-epistemic model ((S)TEM, for short) is a tuple M = (F, L), where (i) F is a (S)TEF with a set of runs R;

(ii) L : R × N → P(AP) is a labeling function, such that L(r, n) is the set of atomic propositions 'true' at a point (r, n).

If condition (i) is changed so that F is a pseudo-(S)TEF, then

M is a (synchronous) temporal-epistemic pseudo-model (pseudo-(S)TEM).

Definition 2.5 The satisfaction relation between (pseudo-)(S)TEMs, points, and formulae of L is recursively defined as follows:

M, (r, n) p iff p ∈ L(r, n); M, (r, n) ¬ϕ iff M, (r, n) ϕ; M, (r, n) ϕ∧ψ iff M, (r, n) ϕ and M, (r, n) ψ; M, (r, n) ∃ g ϕ iff M, (r ′ , n + 1) ϕ holds for some r ′ extending (r, n); M, (r, n) ∀ g ϕ iff M, (r ′ , n + 1) ϕ holds for every r ′ extending (r, n); M, (r, n) ∃(ϕ Uψ) iff, for some r ′ extending (r, n), there exists i ≥ n such that M, (r ′ , i) ψ and M, (r ′ , j) ϕ holds for every n ≤ j < i; M, (r, n) ∀(ϕ Uψ) iff, for every r ′ extending (r, n), there exists i ≥ n such that M, (r ′ , i) ψ and M, (r ′ , j) ϕ holds for every n ≤ j < i;

M, (r, n)

D A ϕ iff M, (r ′ , n ′ ) ϕ for every ((r, n), (r ′ , n ′ )) ∈ R D A ; M, (r, n) C A ϕ iff M, (r ′ , n ′ ) ϕ for every ((r, n), (r ′ , n ′ )) ∈ R C

A . Satisfiability and validity of formulae are defined as usual.

Note that in the semantics above the labeling function L acts on points, not states, i.e., the semantics is point-based.

To make the semantics state-based, one needs to impose the additional condition 1

: r(n) = r ′ (n ′ ) implies L(r, n) = L(r ′ , n ′ ).

The two semantics differ: e.g., the formula p → ∀(⊤ Up) is valid in the state-based semantics, but not in the point-based one.

The satisfaction condition for the operator C A can be paraphrased in terms of reachability. Let F be a (pseudo)-(S)TEF over the set of runs R and let

(r, n) ∈ R × N. We say that point (r ′ , n ′ ) is A-reachable from (r, n) if ei- ther (r, n) = (r ′ , n ′ ) or there exists a sequence (r, n) = (r 0 , n 0 ), (r 1 , n 1 ), . . . , (r m−1 , n m−1 ), (r m , n m ) = (r ′ , n ′ ) of points in R × N such that, for every 0 ≤ i < m, there exists a i ∈ A such that (r i , n i ), (r i+1 , n i+1 )) ∈ R D ai .

It is then easy to see that the following satisfaction condition for C A is equivalent to the one given above:

M, (r, n) C A ϕ iff M, (r ′ , n ′ ) ϕ for every (r ′ , n ′ ), A-reachable from (r, n).

Note that if Σ = {a}, then D a ϕ ↔ C a ϕ is valid in every (S)TEM, for all ϕ ∈ L. Thus, the single-agent case is essentially trivialized, so we assume throughout the rest of the paper that Σ contains at least 2 (names of) agents.

Also note that in models where states are tuples of local states, if s ∼ i s ′ holds for every i = 1, . . . , m, then s = s ′ and, therefore, the formula p → D Σ p is valid in every such model, but it is not valid in every (S)TEM. Thus, the abstract semantics presented above differs from the 'concrete' semantics presented in [7], despite the apparent assumption to the contrary made in [7].

Hereafter, we consider general temporal-epistemic systems; all definitions and results also apply to the synchronous variety, unless stated otherwise.

Hintikka structures for CMA-TEL(CD+BT)

Even though we are ultimately interested in testing formulae of L for satisfiability in a TEM, the tableau procedure we present tests for satisfiability in a more general kind of semantic structure-a Hintikka structure. We will show that θ ∈ L is satisfiable in a TEM iff it is satisfiable in a Hintikka structure, hence the latter test is equivalent to the former. The advantage of working with Hintikka structures lies in the fact that they contain just as much semantic information about θ as is necessary for computing its truth value at a distinguished state. More precisely, while models provide the truth value of every formula of L at every state, Hintikka structures only determine the truth values of formulae directly involved in the evaluation of a fixed formula θ, in the satisfiability of which we are interested. Another important difference between models and Hintikka structures is that, in Hintikka structures, the epistemic relations R D A and R C A only have to satisfy the properties laid down in Definition 2.1. All the other information about the desirable properties of epistemic relations is contained in the labeling of states in Hintikka structures. This labeling ensures that every Hintikka structure generates a pseudo-model (by the construction of Lemma 3.5), which can then be turned into a model.

Definition 3.1 A set ∆ ⊆ L is patently inconsistent if it contains a complementary pair of formulae (i.e., formulae ψ and ¬ψ for some formula ψ).

A set ∆ ⊆ L is fully expanded if it is not patently inconsistent 2 and satisfies the following conditions, where Sub(ψ) stands for the set of subformulae of a formula ψ:

1. if ¬¬ϕ ∈ ∆, then ϕ ∈ ∆; 2. if ϕ ∧ ψ ∈ ∆, then ϕ ∈ ∆ and ψ ∈ ∆; 3. if ¬(ϕ ∧ ψ) ∈ ∆, then ¬ϕ ∈ ∆ or ¬ϕ ∈ ∆; 4. if ¬∃ g ϕ ∈ ∆, then ∀ g ¬ϕ ∈ ∆; 5. if ¬∀ g ϕ ∈ ∆, then ∃ g ¬ϕ ∈ ∆; 6. if ∃(ϕ Uψ) ∈ ∆, then ψ ∈ ∆ or ϕ, ∃ g ∃(ϕ Uψ) ∈ ∆; 7. if ¬∃(ϕ Uψ) ∈ ∆, then ¬ψ, ¬ϕ ∈ ∆ or ¬ψ, ¬∃ g ∃(ϕ Uψ) ∈ ∆; 8. if ∀(ϕ Uψ) ∈ ∆, then ψ ∈ ∆ or ϕ, ∀ g ∀(ϕ Uψ) ∈ ∆; 9. if ¬∀(ϕ Uψ) ∈ ∆, then ¬ψ, ¬ϕ ∈ ∆ or ¬ψ, ¬∀ g ∀(ϕ Uψ) ∈ ∆; 10. if D A ϕ ∈ ∆, then D A ′ ϕ ∈ ∆ for every A ′ such that A ⊆ A ′ ⊆ Σ; 11. if D A ϕ ∈ ∆, then ϕ ∈ ∆; 12. if C A ϕ ∈ ∆, then D a (ϕ∧C A ϕ) ∈ ∆ for every a ∈ A; 13. if ¬C A ϕ ∈ ∆, then ¬D a (ϕ ∧ C A ϕ) ∈ ∆ for some a ∈ A; 14. if ψ ∈ ∆ and D A ϕ ∈ Sub(ψ), then either D A ϕ ∈ ∆ or ¬D A ϕ ∈ ∆. Definition 3.2 A temporal-epistemic Hin- tikka structure (TEHS) is a tuple (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ) , H) such that (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ)

) is a TES, and H is a labeling of points (r, n) ∈ R × N with sets of formulae of L satisfying the following constraints, for all (r, n):

H1 H(r, n) is fully expanded; H2 if ¬ϕ ∈ H(r, n), then ϕ / ∈ H(r, n); H3 if ∃ g ϕ ∈ H(r, n), then ϕ ∈ H(r ′ , n + 1) holds for some r ′ extending (r, n); H4 if ∀ g ϕ ∈ H(r, n), then ϕ ∈ H(r ′ , n + 1) holds for every r ′ extending (r, n); H5 if ∃(ϕ Uψ) ∈ H(r, n), then, for some r ′ extending (r, n), there exists i ≥ n such that ψ ∈ H(r ′ , i) and ϕ ∈ H(r ′ , j) holds for every n ≤ j < i; H6 if ∀(ϕ Uψ) ∈ H(r, n), then, for every r ′ extending (r, n), there exists i ≥ n such that ψ ∈ H(r ′ , i) and ϕ ∈ H(r ′ , j) holds for every n ≤ j < i; H7 if ¬D A ϕ ∈ H(r, n), then there ex- ists r ′ ∈ R and n ′ ∈ N such that ((r, n), (r ′ , n ′ )) ∈ R D A and ¬ϕ ∈ H(r ′ , n ′ ); H8 if ((r, n), (r ′ , n ′ )) ∈ R D A , then D A ′ ϕ ∈ H(r, n) iff D A ′ ϕ ∈ H(r ′ , n ′ ) holds for every A ′ ⊆ A; H9 if ¬C A ϕ ∈ H(r, n), then there ex- ists r ′ ∈ R and n ′ ∈ N such that ((r, n), (r ′ , n ′ )) ∈ R C

A and ¬ϕ ∈ H(r ′ , n ′ ). Synchronous temporal-epistemic Hintikka structures are defined accordingly.

Definition 3.3 A formula θ is satisfiable in a TEHS H with a labeling function H if θ ∈ H(r, n) for some point (r, n) of H. A set of formulae Θ is satisfiable in H if Θ ⊆ H(r, n) for some point (r, n) of H.

Now, we show that θ ∈ L is satisfiable in a TEM iff it is satisfiable in a TEHS. One direction is almost immediate, as every TEM naturally induces a TEHS. More precisely, given a TEM M, we define the extended labeling L + M on the set of points of M as follows:

L + M (r, n) = { ϕ | M, (r, n) ϕ } for every (r, n). The following claim is then straightforward. Lemma 3.4 Let M = (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ) , L) be a TEM satisfying θ ∈ L

, and let L + M be the extended labeling on M.

Then,

H = (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ) , L + ) is a TEHS satisfying θ.

To establish the converse, we first prove that the existence of a Hintikka structure satisfying θ implies the existence of a pseudo-model satisfying θ; then, we prove that this in turn implies the existence of a model satisfying θ.

Lemma 3.5 If θ ∈ L is satisfiable in a TEHS, then it is satisfiable in a pseudo-TEM. Proof. Let H = (Σ, S, R, {R D A } A∈P + (Σ) , {R C A } A∈P + (Σ)

, H) be a TEHS satisfying θ. We build a pseudo-TEM satisfying θ as follows. First, for every A ∈ P + (Σ), let R ′D A be the reflexive, symmetric, and transitive closure of A⊆B R D B and let

R ′C A be the transitive closure of a∈A R ′D a . Notice that R D A ⊆ R ′D A and R C A ⊆ R ′C A for every A ∈ P + (Σ). Next, let L(r, n) = H(r, n) ∩ AP, for every point (r, n) ∈ R × N. It is then easy to check that M ′ = (Σ, S, R, {R ′D A } A∈P + (Σ) , {R ′C A } A∈P + (Σ) , L) is a pseudo-TEM.

To complete the proof of the lemma, we show, by induction on the formula χ ∈ L that, for every point (r, n) and every χ ∈ L, the following hold:

(i) χ ∈ H(r, n) implies M ′ , (r, n) χ; (ii) ¬χ ∈ H(r, n) implies M ′ , (r, n) ¬χ.

Let χ be some p ∈ AP. Then, p ∈ H(r, n) implies p ∈ L(r, n) and thus, M ′ , (r, n) p; if, on the other hand, ¬p ∈ H(r, n), then due to (H2), p / ∈ H(r, n) and thus p / ∈ L(r, n); hence, M ′ , (r, n) ¬p.

Assume that the claim holds for all subformulae of χ; then, we have to prove that it holds for χ, as well.

Suppose that χ = ¬ϕ. If ¬ϕ ∈ H(r, n), then the inductive hypothesis immediately gives us M ′ , (r, n) ¬ϕ; if ¬¬ϕ ∈ H(r, n), then by virtue of (H1), ϕ ∈ H(r, n) and hence, by inductive hypothesis, M ′ , (r, n) ϕ and thus M ′ , (r, n) ¬¬ϕ.

The cases of χ = ϕ ∧ ψ, χ = ∃ g ϕ, and χ = ∀ g ϕ are straightforward, using (H1) -(H4).

Let χ be ∃(ϕ Uψ). If ∃(ϕ Uψ) ∈ H(r, n), then the desired conclusion immediately follows from (H5) and the inductive hypothesis. If ¬∃(ϕ Uψ) ∈ H(r, n), then due to (H1), either ¬ψ, ¬ϕ ∈ H(r, n) or ¬ψ, ¬∃ g ∃(ϕ Uψ) ∈ H(r, n). In the former case, the conclusion immediately follows from the inductive hypothesis. Otherwise, due to (H1) and (H4), ¬∃(ϕ Uψ) ∈ H(r ′ , n + 1) holds for every run r ′ extending (r, n). By repeating the argument, we obtain that, for every run r ′ extending (r, n), either ¬ϕ ∈ H(r ′ , i) for some i ≥ 0 and ¬ψ ∈ H(r ′ , j) for every 0 ≤ j ≤ i or ¬ψ ∈ H(r ′ , i) for every i ≥ 0. In either case, the inductive hypothesis implies that M, (r, n) ¬∃(ϕ Uψ), as desired.

The case of χ = ∀(ϕ Uψ) is similar to the previous one and is left to the reader.

Suppose that χ = D A ϕ. Assume, first, that D A ϕ ∈ H(r, n). In view of the inductive hypothesis, it suffices to show that ((r, n), (r

′ , n ′ )) ∈ R ′D A implies ϕ ∈ H(r ′ , n ′ ).

So, assume that ((r, n), (r ′ , n ′ )) ∈ R ′D A . There are two cases to consider. If (r, n) = (r ′ , n ′ ), then the conclusion immediately follows from (H1). Otherwise, there exists an undirected path from (r, n) to (r ′ , n ′ ) the relations R D A ′ , where each A ′ is a superset of A. Then, due to (H8), D A ϕ ∈ H(r ′ , n ′ ); hence, by (H1), ϕ ∈ H(r ′ , n ′ ), as desired. Now, let ¬D A ϕ ∈ H(r, n). In view of the inductive hypothesis, it suffices to show that there exist r ′ ∈ R and n ′ ∈ N such that ((r, n), (r ′ , n ′ )) ∈ R ′D A and ¬ϕ ∈ H(r ′ , n ′ ). By (H7), there exists r ′ ∈ R and

n ′ ∈ N such that ((r, n), (r ′ , n ′ )) ∈ R D A and ¬ϕ ∈ H(r ′ , n ′ ). As R D A ⊆ R ′D A , the desired conclusion follows. Suppose that χ = C A ϕ. Assume that C A ϕ ∈ H(r, n).

In view of the inductive hypothesis, it suffices to show that if

(r ′ , n ′ ) is A-reachable from (r, n) in M ′ , then ϕ ∈ H(r ′ , n ′ ). If (r, n) = (r ′ , n ′

) the claim follows from (H1). So, suppose that, for some m ≥ 1, there exists a sequence of points (r, n) = (r 0 , n 0 ), . . . , (r m−1 , n m−1 ), (r m , n m ) = (r ′ , n ′ ) such that, for every 0 ≤ i < m, there exists a i ∈ A such that ((r i , n i ), (r i+1 , n i+1 )) ∈ R ′D ai . Then, for every 0 ≤ i < m, there exists a path from (r i , n i ) to (r i+1 , n i+1 ) along relations R D A ′ such that a i ∈ A ′ for every A ′ . Then, we can show by induction on i, using (H1) and (H8), that C A ϕ ∈ H(r i , n i ) holds for every 0 ≤ i < m. Indeed, this holds for i = 0; assuming that it holds for some i, by (H1) (12) we have that D ai (ϕ ∧ C A ϕ) ∈ H(r i , n i ), hence, by (H1) (10) and (H8), ϕ ∈ H(r i+1 , n i+1 ). Now, by taking i = m − 1 we obtain ϕ ∈ H(r ′ , n ′ ), as required.

Finally, assume that ¬C A ϕ ∈ H(r, n). Then, the desired conclusion follows from (H9), the fact that R C A ⊆ R ′C A , and the inductive hypothesis. 2 Lemma 3.6 If θ ∈ L is satisfiable in a pseudo-TEM, then it is satisfiable in a TEM.

Proof. The proof is exactly the same as in [5, Section 3], as the pseudo-models are only 'defective' with respect to epistemic, but not temporal, relations; therefore, the construction for branching time is the same as for linear time. 2

Lemmas 3.4, 3.5, and 3.6 immediately give us the following theorem.

Theorem 3.7 A θ ∈ L is satisfiable in a TEM iff it is satis- fiable in a TEHS.

Tableau procedure for CMATEL(CD+BT)

In this section, we present a tableau procedure for CMA-TEL(CD+BT). We describe a procedure for testing for satisfiability in synchronous models, as it requires extra care. We then briefly mention how the general case is different and argue that the outcome of the procedure is the same in both cases, implying that, satisfiability-wise, general and synchronous semantics are equivalent.

Overview of the procedure

The tableau procedure for testing a formula θ ∈ L for satisfiability attempts to construct a non-empty graph T θ (called tableau), whose nodes are finite sets of L-formulae, encoding 'sufficiently many' TEHSs for θ, in the sense that if θ is satisfiable, then it is satisfiable in a TEHS represented by T θ . The main ideas underlying our tableau algorithm come from the tableau procedures for the logics PDL in [9], UB in [1] and CTL in [3] (see also a detailed exposition of tableaux for CTL in [10]), as well as recently developed tableaux for multiagent epistemic logics in [6]. To make the present paper self-contained, we outline the basic ideas behind our tableau algorithm in line with those references, and then describe the particulars specific to CMA-TEL(CD+BT).

Usually, tableaux work by decomposing the input formula into simpler formulae, in accordance with the semantics of the logical connectives. In the classical propositional case, "simpler" implies shorter, thus ensuring the termination of the procedure. The decomposition into simpler formulae the tableau for classical propositional logic produces a tree representing an exhaustive search for a Hintikka set, the classical propositional analogue of Hintikka structures, for the input formula θ. If at least one leaf of that tree is a Hintikka set for θ, the search has succeeded and θ is proved satisfiable; otherwise, it is declared unsatisfiable.

When applied to logics containing fixpoint-definable operators, such as C A , ∃ U, and ∀ U, these two defining features of the classical tableau method no longer apply. First, the decomposition of the fixpoint formulae, which is done by unfolding their fixpoint definitions, usually produces larger formulae: C A ϕ is decomposed into the formulae D a (ϕ ∧ C A ϕ); analogously for formulae of the form ∃(ϕ Uψ) and ∀(ϕ Uψ). Hence, we need a terminationensuring mechanism. In our tableaux, such a mechanism is provided by the use (and reuse) of so called "pre-states", whose role is to ensure the finiteness of the construction and, hence, termination of the procedure. Second, the only reason why a tableau may fail to produce a Hintikka set for the input formula in the classical case is that every attempt to build such a set results in a collection of formulae containing a patent inconsistency, i.e., a complementary pair of formulae ϕ, ¬ϕ. In the case of CMATEL(CD+BT), there are other such reasons, specific to TEHS, which are more involved structures than classical Hintikka sets. One such reason has to do with eventualities: the truth of an eventuality at a state s in a TEM M requires existence of a path going from s to a state of M at which the 'promise' of that eventuality is fulfilled. Since truth in TEMs is simulated by membership in state labels of Hintikka structures, eventualities impose respective conditions on the labels. Thus, the presence of an eventuality ¬C A ϕ in the label of a state s of a TEHS H requires the existence in H of an A-path (i.e. a path along relations of the form R D B , where R D B ⊆ R D A ) from s to a state t whose label contains ¬ϕ, due to condition (H9) of Definition 3.2. Similar requirements apply to eventualities of the form ∃(ϕ Uψ) and ∀(ϕ Uψ) due to conditions (H5) and (H6) of Definition 3.2. The tableau analogs of these conditions are called realization of eventualities. If a tableau contains a node with an unrealized eventuality in its label, then it cannot produce a TEHS, and thus is 'bad' and needs repairing by removing such nodes. The third possible reason for a tableau to be 'bad' has to do with successor nodes: it may so happen that some of the required successors of a node s are missing from the tableau; then, s is 'bad', and hence needs to be removed. Notice that in TEHSs, and thus in tableaux, states have two kinds of successors: temporal and epistemic. The absence of either kind of successor can ruin the chances of a tableau node to correspond to a state of a TEHS.

The tableau procedure consists of three major phases: pretableau construction, pre-state elimination, and state elimination. During the first, we produce the pretableau for θ-a directed graph P θ , from which the tableau T θ will be extracted. The nodes of P θ are sets of formulae coming in two varieties: states and pre-states. States are fully expanded sets, meant to represent (labels of) states of a Hintikka structure, while pre-states only play a temporary role in the construction of T θ . During the second phase, all prestates from P θ are removed and their incoming edges are redirected, creating a smaller graph T θ 0 , the initial tableau for θ. Finally, we remove from T θ 0 all states, if any, that cannot be satisfied in a TEHS, for any of the reasons mentioned above. The elimination procedure results in a (possibly empty) subgraph T θ of T θ 0 , called the final tableau for θ. If some state ∆ of T θ contains θ, we declare θ satisfiable; otherwise, we declare it unsatisfiable. An example illustrating the tableau construction is provided in Appendix A.

Pretableau construction phase

All states and pre-states of the pretableau P θ constructed during this phase are 'time-stamped'. Whenever necessary to make it explicit, we will use the notation Γ [k] indicating that pre-state Γ was created as the kth component of a run; likewise for states.

The pretableau contains three types of edge, described below. As already mentioned, a procedure attempts to produce a compact representation of a sufficiently many TEHSs for the input formula θ by organizing an exhaustive search for such structures. One type of edge, depicted by unmarked double arrows =⇒, represents the search transitions in the tableau. The exhaustive search considers all possible alternatives that arise when expanding pre-states into states through branching when dealing with disjunctive formulae. Thus, when we draw a double arrow from a pre-state Γ to states ∆ and ∆ ′ (depicted as Γ =⇒ ∆ and Γ =⇒ ∆ ′ , respectively), this intuitively means that, in any TEHS, a state whose label extends the set Γ has to contain at least one of ∆ and ∆ ′ . Our first construction rule, (SR), prescribes how to create tableau states from pre-states.

Given a set Γ ⊆ L, we say that ∆ is a minimal, fully expanded extension of Γ if ∆ is fully expanded, Γ ⊆ ∆, and there is no ∆ ′ such that Γ ⊆ ∆ ′ ⊂ ∆ and ∆ ′ is fully expanded.

Rule (SR) Given a pre-state Γ [k] such that (SR) has not been applied to Γ [k] earlier, do the following:

1. Add to the pretableau all minimal fully expanded extensions ∆ [k] of Γ [k] as states; 2. if ∆ [k] contains no formulae of the form ∃ g ϕ, add

∃ g ⊤ to it; 3. for each so obtained state ∆ [k] , put Γ [k] =⇒ ∆ [k] ; 4. if, however, the pretableau already contains a state

∆ ′[m] that coincides with ∆ [k] , do not create another copy of ∆ ′[m] , but only put Γ [k] =⇒ ∆ ′[m] .

We denote by states(Γ) the (finite) set of states

{ ∆ | Γ =⇒ ∆ }.

Notice that in all construction rules, as in (SR), we allow reuse of (pre)states, which were originally stamped with a possibly different time-stamp. This does not correspond to one (pre)state being part of two different runs at different moments of time; rather, the 'futures' of these runs, starting from the reused (pre)state, can be assumed to be identical, modulo the time difference.

The second type of edge in a pretableau represents epistemic relations in the TEHS that the procedure attempts to build. This type of edge is represented by single arrows marked with epistemic formulae whose presence in the source state requires the presence in the tableau of a target state, reachable by a particular epistemic relation. All such formulae have the form ¬D A ϕ, as can be seen from Definition 3.2. Intuitively if, say ¬D A ϕ ∈ ∆ [k] , then we need some pre-state Γ [k] containing ¬ϕ to be accessible from ∆ [k] by R D A . 3 The reason we mark these single arrows by a formula ¬D A ϕ (rather than by just coalition A), is that we have to remember why we had to create this particular Γ, and not just what relation connects ∆ to Γ. This information will be needed during the elimination phases. We now formulate the rule producing this second type of edge.

Rule (DR):

Given a state ∆ [k] such that ¬D A ϕ ∈ ∆ [k] and (DR) has not been applied to ∆ [k] earlier, do the following:

Create a new pre-state

Γ [k] = {¬ϕ} ∪ A ′ ⊆A { D A ′ ψ | D A ′ ψ ∈ ∆ } ∪ A ′ ⊆A { ¬D A ′ ψ | ¬D A ′ ψ ∈ ∆ }. 2. If pre-state Γ [k] is patently inconsistent, remove it.

3. Otherwise, connect ∆ [k] to Γ [k] with ¬DAϕ −→ . 4. If, however, the tableau already contains a pre-state

Γ ′[k] = Γ [k] , do not add another copy of Γ ′[k] , but sim- ply connect ∆ [k] to Γ ′[k] with ¬DAϕ −→ .

The third type of edge, depicted by single arrows marked with formulae of the form ∃ g ϕ, represent temporal transitions in TEHSs that the tableau is trying to build. The rationale for this rule is similar to that for (DR), the only difference being that we are now considering temporal, rather than epistemic, formulae forcing creation of new pre-states.

Rule (Next):

Given a state ∆ [k] such that (Next) has not been applied to ∆ [k] earlier, do the following:

1. For each ∃ g ϕ ∈ ∆ [k] create a new pre-state Γ [k+1] = {ϕ} ∪ { ψ | ∀ g ψ ∈ ∆ [k] }. 4 2. If pre-state Γ [k] is patently inconsistent, remove it im- mediately. 3. Otherwise, connect ∆ [k] to Γ [k+1] with ∃ g ϕ −→ . 4. If, however, the tableau already contains a pre-state Γ ′[m] = Γ [k+1] , do not add another copy of Γ ′[m] , but simply connect ∆ [k] to Γ ′[m] with ∃ g ϕ −→ .

We now describe the order of application of the above rules. We start off by creating a single pre-state {θ}, containing the input formula. Then, we alternatingly apply (DR) and (Next) to the states created at the previous stage and then applying (SR) to the newly created pre-states. The construction stage is over when the applications of (DR) and (Next) do not produce any new pre-states.

Pre-State elimination phase

At this phase we remove from P θ all pre-states and double arrows, which results in a smaller graph T θ 0 called the initial tableau. Formally, we apply the following rule:

Rule (PR) For every pre-state Γ in P θ , do the following:

1. Remove Γ from P θ . 2. If there is a state ∆ in P θ with ∆ χ −→ Γ, then for every state ∆ ′ ∈ states(Γ), put ∆ χ −→ ∆ ′ .

State elimination phase

During this phase we remove from T θ 0 states that are not satisfiable in a TEHS. As we do not create patently inconsistent states, there are two reasons why a state ∆ of T θ 0 can turn out to be unsatisfiable: either satisfiability of ∆ requires satisfiability of some other (epistemic or temporal) successor states which turn out unsatisfiable, or ∆ contains an eventuality that is not realized in the tableau. Accordingly, we have two elimination rules: (E1) and (E2).

Formally, the state elimination phase is divided into stages; we start at stage 0 with T θ 0 ; at stage n + 1, we remove exactly one state from the tableau T θ n obtained at the previous stage, by applying one of the elimination rules, obtaining the tableau T θ n+1 . In the rules below, S θ m denotes the set of states of tableau T θ m . (E1) If ∆ contains a formula χ of the form ¬D A ϕ or ∃ g ϕ, and ∆ χ −→ ∆ ′ does not hold for any ∆ ′ ∈ S θ n , obtain T θ n+1 by eliminating ∆ from T θ n . For the other elimination rule, we need the concept of eventuality realization in a tableau.

Definition 4.1 (Eventuality realization)

• The eventuality ¬C A ϕ is at ∆ in T θ n if there exists a path ∆ = ∆ 0 , ∆ 1 , . . . , ∆ m , where m ≥ 0, such that ¬ϕ ∈ ∆ m and, for every 0 ≤ i < m, there exist

χ i = D B ψ i such that B ⊆ A and ∆ i χi −→ ∆ i+1 .

• The eventuality ∃(ϕ Uψ) is realized at ∆ in T θ n if there exists a path ∆ = ∆ 0 , ∆ 1 , . . . , ∆ m , where m ≥ 0, such that ψ ∈ ∆ m , and for every 0 ≤ i < m, there exist a formula χ i such that ∆ i ∃ g χi −→ ∆ i+1 and ϕ ∈ ∆ i .

• For eventualities of the form ∀(ϕ Uψ), we define the notion "is realized at ∆ in T θ n " recursively as follows:

(i) If ψ ∈ ∆ then ∀(ϕ Uψ) is realized at ∆; (ii) If ϕ ∈ ∆ and, for every ∃ g χ ∈ ∆, there is a state ∆ ′ ∈ T θ n such that ∆ ∃ g χ −→ ∆ ′ and ∀(ϕ Uψ) is realized at ∆ ′ , then ∀(ϕ Uψ) is realized at ∆.

Now, we can state our second state elimination rule. (E2) If ∆ ∈ S θ n contains an eventuality ξ that is not realized at ∆ in T θ n , then obtain T θ n+1 by removing ∆ from T θ n .

We check for realization of eventualities by running the following iterative procedures that eventually marks all states realizing a given eventuality ξ in T θ n :

• If ξ = ¬C A ϕ, then we initially mark all ∆ ∈ S θ n such that ¬ϕ ∈ ∆. Then, we repeat the following subprocedure until no more states get marked: for every still unmarked ∆ ∈ S θ n , mark ∆ if there is at least one marked ∆ ′ such that ∆ DB ψ −→ ∆ ′ , for some B ⊆ A.

• If ξ = ∃(ϕ Uψ), then we initially mark all ∆ ∈ S θ n such that ψ ∈ ∆. Then, we repeat the following subprocedure until no more states get marked: for every still unmarked ∆ ∈ S θ n , mark ∆ if ϕ ∈ ∆ and there is at least one marked ∆ ′ such that ∆ ∃ g ξ −→ ∆ ′ .

• If ξ = ∀(ϕ Uψ), then we initially mark all ∆ ∈ S θ n such that ψ ∈ ∆, and then we repeat the following subprocedure until no more states get marked: for every still unmarked ∆ ∈ S θ n , mark ∆ if ϕ ∈ ∆ and, for every formula ∃ g χ ∈ ∆, there is a marked state

∆ ′ ∈ S θ n such that ∆ ∃ g χ −→ ∆ ′ .

We now describe the order of application of the above rules. We have to be careful, since having applied (E2) to a tableau, we could have removed all the states accessible from some ∆ along the arrows marked with some χ; hence, we need to reapply (E1) to the resultant tableau to remove such ∆'s. Conversely, having applied (E1), we could have thrown away states needed for realizing certain eventualities; hence, we need to reapply (E2). Thus, we need to apply (E1) and (E2) in an alternating sequence that cycles through all eventualities. More precisely, we arrange all eventualities occurring in the states of T θ 0 in a list ξ 1 , . . . , ξ m . Then, we proceed in cycles. Each cycle consists of alternatingly applying (E2) to the pending eventuality, starting with ξ 1 , and then applying (E1) to the resulting tableau, until all the eventualities have been dealt with, i.e., we have reached ξ m . These cycles are repeated until no state is removed in a whole cycle. Then, the state elimination phase is over.

The graph produced at the end of the state elimination phase is called the final tableau for θ, denoted by T θ , whose set of states is denoted by S θ .

Definition 4.2 The final tableauT θ is open if θ ∈ ∆ for some ∆ ∈ S θ ; otherwise, T θ is closed.

If the final tableau is closed, the tableau procedure returns "no"; otherwise, it returns "yes".

We briefly mention that, to test for satisfiability in general models, we relax the rule (DR), allowing states to have epistemic successors from different temporal levels. As such a modification does not result in the outcome of the procedure, we conclude that, satisfiability-wise, the semantics based on general models is equivalent to the one based on synchronous models.

for θ is open. To establish soundness of the overall procedure, we use a series of lemmas showing that every rule by itself is sound; the soundness of the overall procedure is then an easy consequence. We give the proofs for the synchronous case, the modification for the general case being straightforward. The proofs of the following three lemmas are straightforward. Lemma 5.1 Let Γ be a pre-state of P θ such that M, (r, n)

Γ for some TEM M and point (r, n). Then, M, (r, n) ∆ holds for at least one ∆ ∈ states(Γ). Lemma 5.2 Let ∆ ∈ S θ be such that M, (r, n) ∆ for some TEM M and point (r, n), and let ¬D A ϕ ∈ ∆. Then, there exists a point (r

′ , n) ∈ M such that ((r, n), (r ′ , n ′ )) ∈ R D A and M, (r ′ , n ′ ) ∆ ′ where ∆ ′ = {¬ϕ} ∪ A ′ ⊆A { D A ′ ψ | D A ′ ψ ∈ ∆ } ∪ A ′ ⊆A { ¬D A ′ ψ | ¬D A ′ ψ ∈ ∆ }. Lemma 5.3 Let ∆ ∈ S θ be such that M, (r, n)

∆ for some TEM M and point (r, n), and ∃ g ϕ ∈ ∆. Then, M, (r ′ , n + 1) {ϕ} ∪ { ψ | ∀ g ψ ∈ ∆ } holds for some r ′ extending (r, n). Lemma 5.4 Let ∆ ∈ S θ be such that M, (r, n)

∆ for some TEM M and a point (r, n), and let

¬C A ϕ ∈ ∆. Then, ¬C A ϕ is realized at ∆ in T θ .

Proof idea. Since ¬C A ϕ is true at s, there is a path in M from s leading to a state satisfying ¬ϕ. As the tableau organizes an exhaustive search, a chain of tableau states corresponding to those states in the model will be produced. 2

The next two lemmas are proved likewise. Lemma 5.5 Let ∆ ∈ S θ be such that M, (r, n)

∆ for some TEM M and a point (r, n), and let ∃(ϕ Uψ) ∈ ∆. Then, ∃(ϕ Uψ) is realized at ∆ in T θ . Lemma 5.6 Let ∆ ∈ S θ be such that M, (r, n)

∆ for some TEM M and a point (r, n), and let ∀(ϕ Uψ) ∈ ∆.

Then, ∀(ϕ Uψ) is realized at ∆ in T θ . Theorem 5.7 If θ ∈ L is satisfiable in a TEM, then T θ is open.

Proof sketch. Using the preceding lemmas, we show by induction on the number of stages in the state elimination phase that no satisfiable state can be eliminated due to (E1) or (E2). The claim then follows from Lemma 5.1. 2

The completeness of a tableau procedure means that if the tableau for a formula θ is open, then θ is satisfiable in a TEM. In view of Theorem 3.7, it suffices to show that an open tableau for θ can produce a TEHS satisfying θ. Moreover, we show that this TEHS can be constructed synchronous.

Lemma 5.8 If T θ is open, then θ is satisfiable in a (synchronous) TEHS.

Proof sketch. We build the TEHS H for θ by induction on the temporal levels. The main concern is to ensure that all eventualities in the resultant structure are realized, i.e. the properties (H5), (H6) and (H9) from the definition of Hintikka structures hold; all the other properties of Hintikka structures transfer, more or less immediately, from an open tableau. We alternate between realizing epistemic eventualities (formulae of the form ¬C A ϕ) and temporal eventualities (formulae of the form ∃(ϕ Uψ) and ∀(ϕ Uψ)). Essentially, the construction combines the construction used in proving completeness of multi-agent epistemic Hintikka structures from [6] and the one used in proving completeness of CTL (see [10], which essentially uses the construction that is a simplification of the construction for ATL from [4]).

We start by building the 0th level of our prospective Hintikka structure from the level 0 of an open tableau. For each state ∆ [0] on this level, if ∆ [0] does not contain any epistemic eventualities, we define ∆ [0] -epistemic component to be ∆ [0] with exactly one successor reachable by ¬D A ψ, for each ¬D A ψ ∈ ∆ [0] ; if, on the other hand, ¬C A ϕ ∈ ∆ [0] , then the ∆ [0] -epistemic component is a tree obtained from a path in the tableau leading from ∆ [0] along the arrows marked with formulae of the form ¬D B χ to a state ∆ ′[0] containing ϕ; the tree is obtained from the path by giving each component of the path enough successors, as described above. As all the unrealized epistemic eventualities are propagated down the components (hence, appear in the leaves of the tree), we can stitch them up together to obtain a graph where each epistemic eventuality is realized. Now, having built the 0th level of our prospective Hintikka structure, we take care of realizing all the temporal eventualities contained in the states of level 0. This is done exactly as in the completeness proof of the tableau procedure for CTL ( [10]): we define the ∆ [0] -temporal component for each ∆ [0] as follows: if it does not contain any temporal eventualities, then we take ∆ [0] with one temporal successor for each ∃ g ϕ ∈ ∆. If ∃(ϕ Uψ) ∈ ∆, then we take a temporal path realizing ∃(ϕ Uψ) ∈ ∆ and give to every node enough temporal successors, as describe above. Lastly, if ∀(ϕ Uψ) ∈ ∆, then we take a temporal tree witnessing the the realizion of ∀ϕ ∈ ∆ in the tableau (for details, see [10]). As eventualities are again passed down, we can stitch up an infinite tree realizing all the eventualities contained in the states making up the tree.

Next, we repeat the procedure inductively. For the mth epistemic level, we independently apply to each state on this level the procedure described above for level 0, so that the epistemic structures unfolding from any two points on level m are disjoint, and also give to each newly created point a 'history' consisting of a path of m−1 states of the form {⊤} (so that we do not create any new epistemic eventualities). Having fixed all the epistemic eventualities at the mth level, we repeat the procedure described in the previous paragraph to fix all the temporal eventualities contained in states of level m.

Thus, we produce a chain of structures ordered by inclusion. Eventually, we take the (infinite) union of all the structures defined at the finite states of that construction, and then put H(∆ [k] ) = ∆ [k] for every ∆ [k] , to obtain a TEHS satisfying θ.

2

The completeness is now immediate from Lemma 5.8 and Theorem 3.7.

Theorem 5.9 (Completeness) If T θ is open, then θ is satisfiable, in a (synchronous) TEM.

As for the complexity, for lack of space, we only mention that the above procedure runs in exponential time (the calculations are fairly routine), thus matching the lower bound known from [7].

[13] Pierre Wolper. The tableau method for temporal logic: an overview. Logique et Analyse, 28(110-111):119-136, 1985.

A Example

In the present appendix, we provide an example of how our procedure works on the formula ∀(¬C {a,b} p U ¬D {a,c} p).

To simplify the example, we test for satisfiability of the equivalent set {∀(¬C {a,b} p U ¬D {a,c} p, ⊤}.

Displayed below is the complete pretableau for this set. The initial tableau is obtained by removing all pre-states (the Γs) and redirecting the arrows (i.e, ∆ 1 will be connected by unmarked single arrows to itself, ∆ 2 , and ∆ 3 ). It is easy to check that no states get removed during the state elimination stage; hence, the tableau is open and θ is satisfiable.