We develop a sound and complete tableau-based decision procedure for the full coalitional multiagent temporalepistemic logic of branching time CMATEL(CD+BT) that extends logic CTL with epistemic operators for common and distributed knowledge for all coalitions of agents referred to in the language. The procedure runs in exponential time, which matches the lower bound established by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal decision procedure and a complete deductive system for our logic.
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 [
Despite the conceptual importance and wide range of
potential applications of temporal-epistemic logics, to the best
of our knowledge, no efficient decision procedures for
logics studied in [
In the recent precursor [
In the present paper, we report on the second, and
final, part of the project undertaken with the publication
of [
We should mention that, even though the procedure
presented in [
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., [
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 CMATEL(CD+BT) and show that satisfiability of CMATEL(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 CMATEL(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. 2
Syntax and semantics of the logic CMATEL(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 DAϕ (“it is distributed knowledge among agents in A that ϕ”), and CAϕ (“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) | DAϕ | CAϕ 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 [
Formulae of the form ¬CAϕ are epistemic eventualities, while those of the form ∃(ϕ U ψ) and ∀(ϕ U ψ) are temporal eventualities.
The semantics of temporal-epistemic logics considered
in [
According to [
The systems with (global) states represented as tuples of
local states are generalized in [
A TES G is synchronous (STES) if ((r, n), (r′, n′)) ∈ RAD 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) temporalepistemic frame ((S)TEF) is a (S)TES G = (Σ, S, R, {RAD}A∈P+(Σ), {RCA}A∈P+(Σ)), where each RAD is an equivalence relation satisfying the following condition: (†)
RAD = T a∈AR{Da} If condition (†) is replaced by the following, weaker one: (††)
RAD ⊆ RBD whenever B ⊆ A, then F is a (synchronous) temporal-epistemic pseudo-frame (pseudo-(S)TEF).
Notice that in (pseudo-)(S)TEFs RCA is the transitive closure of S a∈AR{Da}, for every A ∈ P+(Σ); furthermore, in such structures, each RCA 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 7→ 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) 1 ϕ; 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) DAϕ iff M, (r′, n′) ϕ for every ((r, n), (r′, n′)) ∈ RAD;
M, (r, n) CAϕ iff M, (r′, n′) ϕ for every ((r, n), (r′, n′)) ∈ RCA.
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 condition1: r(n) = r′(n′) implies L(r, n) = L(r′, n′). The two semantics differ: e.g., the formula p → ∀(⊤ U p) is valid in the state-based semantics, but not in the point-based one.
The satisfaction condition for the operator CA 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 either (r, n) = (r′, n′) or there exists a sequence (r, n) = (r0, n0), (r1, n1), . . . , (rm−1, nm−1), (rm, nm) = (r′, n′) of points in R × N such that, for every 0 ≤ i < m, there exists ai ∈ A such that (ri, ni), (ri+1, ni+1)) ∈ RaDi . It is then easy to see that the following satisfaction condition for CA is equivalent to the one given above:
M, (r, n) CAϕ iff M, (r′, n′) ϕ for every (r′, n′), A-reachable from (r, n).
Note that if Σ = {a}, then Daϕ ↔ Caϕ 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 [
Hereafter, we consider general temporal-epistemic systems; all definitions and results also apply to the synchronous variety, unless stated otherwise.
1This condition is not imposed in [
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 RAD and RCA 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 inconsistent2 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 DAϕ ∈ Δ, then DA′ ϕ ∈ Δ for every A′ such that
A ⊆ A′ ⊆ Σ; 11. if DAϕ ∈ Δ, then ϕ ∈ Δ; 12. if CAϕ ∈ Δ, then Da(ϕ∧CAϕ) ∈ Δ for every a ∈ A; 2Even though in general, not being patently inconsistent is a weaker condition than a propositional consistency, in the case of fully expanded sets, they coincide. 13. if ¬CAϕ ∈ Δ, then ¬Da(ϕ ∧ CAϕ) ∈ Δ for some a ∈ A; 14. if ψ ∈ Δ and DAϕ ∈ Sub(ψ), then either DAϕ ∈ Δ or ¬DAϕ ∈ Δ.
Definition 3.2 A temporal-epistemic Hintikka structure (TEHS) is a tuple (Σ, S, R, {RAD}A∈P+(Σ), {RCA}A∈P+(Σ), H) such that (Σ, S, R, {RAD}A∈P+(Σ), {RCA}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 ¬DAϕ ∈ H(r, n), then there exists r′ ∈ R and n′ ∈ N such that ((r, n), (r′, n′)) ∈ RAD and ¬ϕ ∈ H(r′, n′); H8 if ((r, n), (r′, n′)) ∈ RAD, then DA′ ϕ ∈ H(r, n) iff
DA′ ϕ ∈ H(r′, n′) holds for every A′ ⊆ A; H9 if ¬CAϕ ∈ H(r, n), then there exists r′ ∈ R and n′ ∈ N such that ((r, n), (r′, n′)) ∈ RCA 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, {RAD}A∈P+(Σ), {RCA}A∈P+(Σ), L) be a TEM satisfying θ ∈ L, and let L+M be the extended labeling on M. Then, H = (Σ, S, R, {RAD}A∈P+(Σ), {RCA}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, {RAD}A∈P+(Σ), {RCA}A∈P+(Σ), H) be a TEHS satisfying θ. We build a pseudo-TEM satisfying θ as follows. First, for every A ∈ P+(Σ), let R′AD be the reflexive, symmetric, and transitive closure of S A⊆BRBD and let R′AC be the transitive closure of S a∈AR′aD. Notice that RAD ⊆ R′AD and RCA ⊆ R′AC 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′AD}A∈P+(Σ), {R′AC }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 χ = DAϕ. Assume, first, that DAϕ ∈ H(r, n). In view of the inductive hypothesis, it suffices to show that ((r, n), (r′, n′)) ∈ R′AD implies ϕ ∈ H(r′, n′). So, assume that ((r, n), (r′, n′)) ∈ R′AD. 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′) along the relations RAD′ , where each A′ is a superset of A. Then, due to (H8), DAϕ ∈ H(r′, n′); hence, by (H1), ϕ ∈ H(r′, n′), as desired.
Now, let ¬DAϕ ∈ 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′AD and ¬ϕ ∈ H(r′, n′). By (H7), there exists r′ ∈ R and n′ ∈ N such that ((r, n), (r′, n′)) ∈ RAD and ¬ϕ ∈ H(r′, n′). As RAD ⊆ R′AD, the desired conclusion follows.
Suppose that χ = CAϕ. Assume that CAϕ ∈ 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) = (r0, n0), . . . , (rm−1, nm−1), (rm, nm) = (r′, n′) such that, for every 0 ≤ i < m, there exists ai ∈ A such that ((ri, ni), (ri+1, ni+1)) ∈ R′aDi . Then, for every 0 ≤ i < m, there exists a path from (ri, ni) to (ri+1, ni+1) along relations RAD′ such that ai ∈ A′ for every A′. Then, we can show by induction on i, using (H1) and (H8), that CAϕ ∈ H(ri, ni) 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 Dai (ϕ ∧ CAϕ) ∈ H(ri, ni), hence, by (H1)(10) and (H8), ϕ ∈ H(ri+1, ni+1). Now, by taking i = m − 1 we obtain ϕ ∈ H(r′, n′), as required.
Finally, assume that ¬CAϕ ∈ H(r, n). Then, the desired conclusion follows from (H9), the fact that RCA ⊆ R′AC , 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 satisfiable in a TEHS. 4
Tableau procedure for CMATEL(CD+BT) In this section, we present a tableau procedure for CMATEL(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. 4.1
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
[
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 in 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 CA, ∃ 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: CAϕ is decomposed into the formulae Da(ϕ ∧ CAϕ); 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 ¬CAϕ 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 RBD, where RBD ⊆ RAD) 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 T0θ, the initial tableau for θ. Finally, we remove from T0θ 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 T0θ, 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. 4.2
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 ¬DAϕ, as can be seen from Definition 3.2. Intuitively if, say ¬DAϕ ∈ Δ[k], then we need some pre-state Γ[k] containing ¬ϕ to be accessible from Δ[k] by RAD.3 The reason we mark these single arrows by a formula ¬DAϕ (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.
3We require the newly created pre-states to bear the same time stamp as the source state for the sake of synchrony, as this reflects the fact that all epistemic alternatives belong to the same temporal level of any TEHS.
Rule (DR): Given a state Δ[k] such that ¬DAϕ ∈ Δ[k] and (DR) has not been applied to Δ[k] earlier, do the following: 1. Create a new pre-state Γ[k] = {¬ϕ} ∪ S A′⊆A{ DA′ ψ | DA′ ψ ∈ Δ } ∪ S A′⊆A{ ¬DA′ ψ | ¬DA′ ψ ∈ Δ }. 2. If pre-state Γ[k] is patently inconsistent, remove it. 3. Otherwise, connect Δ[k] to Γ[k] with ¬−D→Aϕ. 4. If, however, the tableau already contains a pre-state Γ′[k] = Γ[k], do not add another copy of Γ′[k], but simply connect Δ[k] to Γ′[k] with ¬−D→Aϕ.
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 immediately. ∃ gϕ 3. Otherwise, connect Δ[k] to Γ[k+1] with −→ . 4. If, however, the tableau already contains a pre-state Γ′[m] = Γ[k+1], do not add another copy of Γ′[m], but ∃ gϕ simply connect Δ[k] to Γ′[m] with −→ .
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. 4.3
At this phase we remove from P θ all pre-states and double arrows, which results in a smaller graph T0θ 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 Δ −→ Δ′.
4Note that, due to step 2 in the (SR) rule, every state contains at least one formula of the form ∃ eϕ.
During this phase we remove from T0θ states that are not satisfiable in a TEHS. As we do not create patently inconsistent states, there are two reasons why a state Δ of T0θ 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 T0θ; at stage n + 1, we remove exactly one state from the tableau Tnθ obtained at the previous stage, by applying one of the elimination rules, obtaining the tableau Tnθ+1. In the rules below, Smθ denotes the set of states of tableau Tmθ .
(E1) If Δ contains a formula χ of the form ¬DAϕ or χ ∃ gϕ, and Δ −→ Δ′ does not hold for any Δ′ ∈ Snθ , obtain Tnθ+1 by eliminating Δ from Tnθ.
For the other elimination rule, we need the concept of eventuality realization in a tableau.
Definition 4.1 (Eventuality realization) • The eventuality ¬CAϕ is realized at Δ in Tnθ if there exists a path Δ = Δ0, Δ1, . . . , Δm, where m ≥ 0, such that ¬ϕ ∈ Δm and, for every 0 ≤ i < m, there exist χi = DBψi such that B ⊆ A and Δi −χ→i Δi+1. • The eventuality ∃(ϕ U ψ) is realized at Δ in Tnθ 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 Tnθ” recursively as follows: (i) If ψ ∈ Δ then ∀(ϕ U ψ) is realized at Δ; (ii) If ϕ ∈ Δ and, for every ∃ gχ ∈ Δ, there is a state Δ′ ∈ Tnθ such that Δ ∃−→gχ Δ′ and ∀(ϕ U ψ) is realized at Δ′, then ∀(ϕ U ψ) is realized at Δ.
Now, we can state our second state elimination rule. (E2) If Δ ∈ Snθ contains an eventuality ξ that is not realized at Δ in Tnθ, then obtain Tnθ+1 by removing Δ from Tnθ.
We check for realization of eventualities by running the following iterative procedures that eventually marks all states realizing a given eventuality ξ in Tnθ: • If ξ = ¬CAϕ, then we initially mark all Δ ∈ Snθ such that ¬ϕ ∈ Δ. Then, we repeat the following subprocedure until no more states get marked: for every smtialrlkuendmΔar′kseudchΔth∈atSΔnθ ,D−mB→aψrkΔΔ′, iffotrhseoremies Bat ⊆leaAst.one • If ξ = ∃(ϕ U ψ), then we initially mark all Δ ∈ Snθ such that ψ ∈ Δ. Then, we repeat the following subprocedure until no more states get marked: for every still unmarked Δ ∈ Snθ , mark Δ if ϕ ∈ Δ and there is at least one marked Δ′ such that Δ ∃−→gξ Δ′. • If ξ = ∀(ϕ U ψ), then we initially mark all Δ ∈ Snθ such that ψ ∈ Δ, and then we repeat the following subprocedure until no more states get marked: for every still unmarked Δ ∈ Snθ , mark Δ if ϕ ∈ Δ and, for every formula ∃ gχ ∈ Δ, there is a marked state Δ′ ∈ Snθ 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 T0θ 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 tableau T θ 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. 5
Soundness, completeness, and complexity The soundness of a tableau procedure amounts to claiming that if the input formula θ is satisfiable, then the tableau 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 ¬DAϕ ∈ Δ. Then, there exists a point (r′, n) ∈ M such that ((r, n), (r′, n′)) ∈ RAD and M, (r′, n′) Δ′ where Δ′ = {¬ϕ} ∪ S A′⊆A{ DA′ ψ | DA′ ψ ∈ Δ } ∪ S A′⊆A{ ¬DA′ ψ | ¬DA′ ψ ∈ Δ }.
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 ¬CAϕ ∈ Δ. Then, ¬CAϕ is realized at Δ in T θ.
Proof idea. Since ¬CAϕ 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 ¬CAϕ) 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 [
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 ¬DAψ, for each ¬DAψ ∈ Δ[0]; if, on the other hand, ¬CAϕ ∈ Δ[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 ¬DBχ 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 ([
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 [
We have presented an incremental tableau-based
decision procedure for the full coalitional temporal-epistemic
logic of branching time CMATEL(CD+BT). The
procedure is complexity-optimal, intuitive, and practically
reasonably efficient (as the number of (pre)states it creates is
usually significantly smaller that the powerset of all subsets
of the close of the formula that is tested for satisfiability); it
is, therefore, suitable for both manual and automated
execution. Moreover, it is fairly flexible and easily amenable to
modifications for variations of the semantics, such as those
mentioned in section 2. Since in the semantics considered
in this paper there is essentially no interaction between the
temporal and epistemic fragments, our procedure combines
in a modular way tableaux for the full coalitional
multiagent epistemic logic CMAEL(CD) and for CTL. Such
interaction, however, can be triggered by imposing various
natural semantic conditions, such as “no learning” or “no
forgetting”. As shown in [
A
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. Γ[0]
0 I
χ0 ?@@R χ0
χ1Δ[
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.