=Paper=
{{Paper
|id=Vol-494/paper-25
|storemode=property
|title=Tableau-based Decision Procedure for the Full Coalitional Multiagent Logic of Branching Time
|pdfUrl=https://ceur-ws.org/Vol-494/famaspaper7.pdf
|volume=Vol-494
|dblpUrl=https://dblp.org/rec/conf/mallow/GorankoS09
}}
==Tableau-based Decision Procedure for the Full Coalitional Multiagent Logic of Branching Time==
https://ceur-ws.org/Vol-494/famaspaper7.pdf
Tableau-based decision procedure for the full coalitional multiagent
temporal-epistemic logic of branching time
Valentin Goranko Dmitry Shkatov
Abstract tential applications of temporal-epistemic logics, to the best
of our knowledge, no efficient decision procedures for log-
We develop a sound and complete tableau-based deci- ics studied in [7] had been developed until quite recently,
sion procedure for the full coalitional multiagent temporal- even for the systems with a relatively low known lower
epistemic logic of branching time CMATEL(CD+BT) that bounds. The only exception is [11], where a top-down
extends logic CTL with epistemic operators for common tableau-style decision procedure for the logic ATEL, which
and distributed knowledge for all coalitions of agents re- subsumes the basic branching-time logic considered in [7]
ferred to in the language. The procedure runs in exponen- and this paper, was presented. In our view (to be explained
tial time, which matches the lower bound established by further), however, [11] should be seen as a contribution to
Halpern and Vardi for a fragment of our logic, thus pro- the complexity-theoretic analysis of the temporal-epistemic
viding a complexity-optimal decision procedure and a com- logics rather than to the development of efficient decision
plete deductive system for our logic. procedures for them.
In the recent precursor [5] to the present paper, we
set out to fill in the above-mentioned gap by develop-
1 Introduction ing a practically efficient (within the theoretical complex-
ity bounds) tableau-based decision procedure for the coali-
Reasoning about knowledge and time is crucial for de- tional multiagent temporal-epistemic logic of linear time
signing, and verifying properties of, distributed and mul- CMATEL(CD+LT) (for both the synchronous and asyn-
tiagent systems. A number of temporal-epistemic logics chronous cases), building both on Wolper’s incremental
were proposed as logical frameworks for modeling of, and tableaux for LTL [13] and on our earlier work on tableaux
reasoning about, these aspects of distributed systems in for the full coalitional multiagent (purely) epistemic logic
the 1980’s. This research was summarized in the com- CMAEL(CD) [6].
prehensive study by Halpern and Vardi [7]. In that study, In the present paper, we report on the second, and fi-
the authors considered several essential characteristics of nal, part of the project undertaken with the publication
temporal-epistemic logics, namely: one vs. several agents, of [5]; namely, we present a sound, complete, and termi-
synchrony vs. asynchrony, (no) learning, (no) forgetting, nating incremental tableau for the Coalitional Multi-Agent
linear vs. branching time, and the (non)existence of a Temporal Epistemic Logic with operators for Common
unique initial state. Based on these, they identify and ana- and Distributed knowledge and Branching Time, CMA-
lyze 96 temporal-epistemic logics and obtain lower bounds TEL(CD+BT). The tableau procedure presented herein fol-
for the complexity of the satisfiability problem in all of lows the tableau-building philosophy developed for the log-
them. It turns out that most of the systems with more than ics PDL by Pratt in [9], UB by Ben-Ari, Manna and Pnueli
one agents who do not learn or do not forget are unde- in [1], and CTL by Emerson and Halpern in [3]. Our pro-
cidable, often Π11 -hard (with common knowledge), or de- cedure essentially combines incremental tableaux for CTL
cidable but with non-elementary time lower bound (with- from the latter (see also [10] for a recent detailed exposi-
out common knowledge). For most of the remaining log- tion) and tableaux for the full coalitional multiagent epis-
ics, the lower bounds established in [7] for the multiagent temic logic CMAEL(CD) developed in [6]. In the present
case range from PSPACE (synchronous systems without paper, as in [6], we work with a more expressive epistemic
common knowledge), through EXPTIME (with common language than the one considered in [7], as it contains op-
knowledge), to EXPSPACE (synchronous systems with no erators for common and distributed knowledge for all non-
learning and unique initial state). empty coalitions (i.e., subsets) of the set of agents. The re-
Despite the conceptual importance and wide range of po- sulting decision procedure for testing satisfiability in CMA-
1
TEL(CD+BT) runs in exponential time, which is the opti- where p ranges over AP and A ranges over the set P + (Σ)
mal lower-bound, as established in [11]. of non-empty subsets of Σ. We write ϕ ∈ L to mean that ϕ
We should mention that, even though the procedure pre- is a formula of L and ∆ ⊆ L to mean that ∆ is a set of such
sented in [11] can be used to test CMATEL(CD+BT)- formulae.
formulae for satisfiability, this would not give us the optimal Thus, L combines the language of Computational Tree
procedure, since such a procedure would always require ex- Logic CTL [2] with the language of the full coalitional
ponential time predicted by the worst-case estimate. The in- multi-agent epistemic logic CMAEL(CD) [6]. Although
cremental tableau presented in this paper, on the other hand, ∀ gϕ is definable as ¬∃ g¬ϕ, it is convenient to treat it as
on average requires much less time than the theoretical up- a primitive connective. The operator for individual knowl-
per bound (this claim cannot be made mathematically pre- edge Ka ϕ (“agent a knows that ϕ”), where a ∈ Σ, can then
cise without an a priori probability distribution on formu- be defined as D{a} ϕ, henceforth written Da ϕ. The other
lae; however, it is substantiated by example in [4], where Boolean and temporal connectives can be defined as usual.
we compare the incremental tableaux presented in that pa- We omit parentheses when this does not result in ambiguity.
per with the top-down tableux-style procedure from [12]). Formulae of the form ¬CA ϕ are epistemic eventualities,
Besides presenting the tableau-based procedure for while those of the form ∃(ϕ Uψ) and ∀(ϕ Uψ) are temporal
CMATEL(CD+BT), the other major objective of this pa- eventualities.
per is to demonstrate how two tableau procedures for log- The semantics of temporal-epistemic logics considered
ics with non-interacting fixed-point operators (the epistemic in [7] is based on system of runs with m processors (agents).
and the temporal ones, in our case) can be combined into a A run is a function from (the set of natural numbers) N to
tableau procedure for the fusion of these logics, thus offer- the product Lm regarded as the set of global states, where
ing a contribution to the area of combination of logics (see L is the set of local states; each agent can be in one of
e.g., [8]). local states at any moment in time. Thus, a global state
The present paper is structured as follows. In Sec- is a tuple hl1 , . . . , lm i; the i-th component li of this global
tion 2, we introduce the logic CMATEL(CD+BT). In state representing the local view of the agent i. The pair
Section 3, we introduce Hintikka structures for CMA- (r, n), where r is a run and n ∈ N, is called in [7] a point.
TEL(CD+BT) and show that satisfiability of CMA- With every agent i, the authors of [7] associate the binary
TEL(CD+BT)-formulae in Hintikka structures is equiva- epistemic indistinguishability relation ∼i on Lm , defined as
lent to satisfiability in models introduced in Section 2. In ′
follows: hl1 , . . . , lm i ∼i hl1′ , . . . , lm i if li = li′ ; i.e., if the
Section 4, we present the tableau procedure for CMA- agent i has the same local views in these states.
TEL(CD+BT) and, in Section 5, sketch out the proofs of According to [7], a system is synchronous when it has
soundness and completeness and briefly discuss the com- a ‘global clock’ observable by all agents and thus synchro-
plexity of the procedure. The Appendix contains an exam- nizing their local times; formally, a system is synchronous
ple of a run of the procedure. 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 pres-
2 Syntax and semantics of the logic CMA- ence or absence of synchrony, under no other assumptions,
TEL(CD+BT) does not affect the outcome of our tableau procedure, and
therefore, the satisfiability of formulae.
The language L of CMATEL(CD+BT) contains a (pos- The systems with (global) states represented as tuples of
sibly infinite) set AP of atomic propositions; the Boolean local states are generalized in [7] to systems where global
connectives ¬ (“not”) and ∧ (“and”); the unary temporal states are abstract primitive entities and the epistemic rela-
operators ∃ g and ∀ g (existential and universal “next”, tions are abstract equivalence relations on the set of such
respectively); the binary temporal operators ∃(− U−) and states. In the present paper, we work with this abstract
∀(− U−) (existential and universal “until”, respectively), semantics from [7]. We note that, as we show later, this
as well as the unary epistemic operators DA ϕ (“it is dis- semantics is more general than the above mentioned ‘con-
tributed knowledge among agents in A that ϕ”), and CA ϕ crete’ semantics from [7], despite the apparent assumption
(“it is common knowledge among agents of A that ϕ”) for made in [7] that the two semantics are equivalent. We now
every non-empty A ⊆ Σ, where Σ is the finite, non-empty turn to the presentation of the abstract semantics from [7].
set of names of agents belonging to L. Subsets of Σ are
called coalitions. Thus, the formulae of L are defined as Definition 2.1 A temporal-epistemic system (TES) is a tu-
follows: ple G = (Σ, S, R, {RD C
A }A∈P + (Σ) , {RA }A∈P + (Σ) ), where:
ϕ := p | ¬ϕ | (ϕ1 ∧ ϕ2 ) | ∃ gϕ | ∀ gϕ | 1. Σ is a finite, non-empty set of agents;
| ∃(ϕ1 Uϕ2 ) | ∀(ϕ1 Uϕ2 ) | DA ϕ | CA ϕ 2. S 6= ∅ is a set of states;
3. R 6= ∅ is a set of runs: each r ∈ R is a function M, (r, n) ¬ϕ iff M, (r, n) 1 ϕ;
r : N 7→ S. A state visited by a computation can, then, M, (r, n) ϕ∧ψ iff M, (r, n) ϕ and M, (r, n) ψ;
be represented as r(n), where r ∈ R and n ∈ N. Also, M, (r, n) ∃ gϕ iff M, (r′ , n + 1) ϕ holds for some
′
with a state r(n) we associate a pair (r, n), referred r extending (r, n);
to as a point; the set of all points in G is denoted by M, (r, n) ∀ gϕ iff M, (r′ , n + 1) ϕ holds for every
′
P (G). Notice that different points may be associated r extending (r, n);
with the same state. M, (r, n) ∃(ϕ Uψ) iff, for some r′ extending (r, n),
4. for every A ∈ P + (Σ), RD C
A and RA are binary rela-
there exists i ≥ n such that M, (r′ , i) ψ and
tions on P(G), such that R C
is the reflexive and tran- M, (r′ , j) ϕ holds for every n ≤ j < i;
S A
sitive closure of A′ ⊆A RA D
′ . M, (r, n) ∀(ϕ Uψ) iff, for every r′ extending (r, n),
there exists i ≥ n such that M, (r′ , i) ψ and
A TES G is synchronous (STES) if ((r, n), (r′ , n′ )) ∈ M, (r′ , j) ϕ holds for every n ≤ j < i;
′ +
RD
A implies n = n for every A ∈ P (Σ). M, (r, n) DA ϕ iff M, (r′ , n′ ) ϕ for every
′ ′
((r, n), (r , n )) ∈ RD A ;
Hereafter we write ‘(S)TES’ to refer to general or syn- M, (r, n) CA ϕ iff M, (r′ , n′ ) ϕ for every
chronous temporal-epistemic system. ((r, n), (r′ , n′ )) ∈ RC .
A
Definition 2.2 Let (r, n) ∈ P (G) for some (S)TES G with Satisfiability and validity of formulae are defined as
a set of runs R and let r′ ∈ R. We say that r′ extends (r, n) usual.
if r(m) = r′ (m) holds for all m ≤ n. Note that in the semantics above the labeling function L
acts on points, not states, i.e., the semantics is point-based.
Definition 2.3 A (synchronous) temporal- To make the semantics state-based, one needs to impose
epistemic frame ((S)TEF) is a (S)TES G = the additional condition1 : r(n) = r′ (n′ ) implies L(r, n) =
(Σ, S, R, {RD C
A }A∈P + (Σ) , {RA }A∈P + (Σ) ), where each L(r′ , n′ ). The two semantics differ: e.g., the formula p →
RDA is an equivalence relation satisfying the following ∀(⊤ Up) is valid in the state-based semantics, but not in the
condition: point-based one.
T The satisfaction condition for the operator CA can be
(†) RD A =
D
a∈A R{a}
paraphrased in terms of reachability. Let F be a (pseudo)-
If condition (†) is replaced by the following, weaker one: (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-
(††) RD D
A ⊆ RB whenever B ⊆ A, ther (r, n) = (r′ , n′ ) or there exists a sequence (r, n) =
(r0 , n0 ), (r1 , n1 ), . . . , (rm−1 , nm−1 ), (rm , nm ) = (r′ , n′ )
then F is a (synchronous) temporal-epistemic pseudo-frame
of points in R × N such that, for every 0 ≤ i < m, there
(pseudo-(S)TEF).
exists ai ∈ A such that (ri , ni ), (ri+1 , ni+1 )) ∈ RaDi . It is
C then easy to see that the following satisfaction condition for
S that inD(pseudo-)(S)TEFs R+
Notice A is the transitive clo-
CA is equivalent to the one given above:
sure of a∈A R{a} , for every A ∈ P (Σ); furthermore, in
M, (r, n) CA ϕ iff M, (r′ , n′ ) ϕ for every (r′ , n′ ),
such structures, each RCA is an equivalence relation. A-reachable from (r, n).
Definition 2.4 A (synchronous) temporal-epistemic model Note that if Σ = {a}, then Da ϕ ↔ Ca ϕ is valid in
((S)TEM, for short) is a tuple M = (F, L), where every (S)TEM, for all ϕ ∈ L. Thus, the single-agent case is
essentially trivialized, so we assume throughout the rest of
(i) F is a (S)TEF with a set of runs R; the paper that Σ contains at least 2 (names of) agents.
Also note that in models where states are tuples of local
(ii) L : R × N 7→ P(AP) is a labeling function, such states, if s ∼i s′ holds for every i = 1, . . . , m, then s = s′
that L(r, n) is the set of atomic propositions ‘true’ at and, therefore, the formula p → DΣ p is valid in every such
a point (r, n). model, but it is not valid in every (S)TEM. Thus, the ab-
If condition (i) is changed so that F is a pseudo-(S)TEF, then stract semantics presented above differs from the ‘concrete’
M is a (synchronous) temporal-epistemic pseudo-model semantics presented in [7], despite the apparent assumption
(pseudo-(S)TEM). to the contrary made in [7].
Hereafter, we consider general temporal-epistemic sys-
Definition 2.5 The satisfaction relation between tems; all definitions and results also apply to the syn-
(pseudo-)(S)TEMs, points, and formulae of L is recursively chronous variety, unless stated otherwise.
defined as follows: 1 This condition is not imposed in [7], but this is an apparent omission
M, (r, n) p iff p ∈ L(r, n); because it is essentially assumed there.
3 Hintikka structures for CMA- 13. if ¬CA ϕ ∈ ∆, then ¬Da (ϕ ∧ CA ϕ) ∈ ∆ for some
TEL(CD+BT) a ∈ A;
14. if ψ ∈ ∆ and DA ϕ ∈ Sub(ψ), then either DA ϕ ∈ ∆
Even though we are ultimately interested in testing for- or ¬DA ϕ ∈ ∆.
mulae of L for satisfiability in a TEM, the tableau proce- Definition 3.2 A temporal-epistemic Hin-
dure we present tests for satisfiability in a more general kind tikka structure (TEHS) is a tuple
of semantic structure—a Hintikka structure. We will show (Σ, S, R, {RD C
A }A∈P + (Σ) , {RA }A∈P + (Σ) , H) such that
that θ ∈ L is satisfiable in a TEM iff it is satisfiable in a
(Σ, S, R, {RD C
A }A∈P + (Σ) , {RA }A∈P + (Σ) ) is a TES, and H
Hintikka structure, hence the latter test is equivalent to the
is a labeling of points (r, n) ∈ R × N with sets of formulae
former. The advantage of working with Hintikka structures
of L satisfying the following constraints, for all (r, n):
lies in the fact that they contain just as much semantic in-
formation about θ as is necessary for computing its truth H1 H(r, n) is fully expanded;
value at a distinguished state. More precisely, while models H2 if ¬ϕ ∈ H(r, n), then ϕ ∈ / H(r, n);
provide the truth value of every formula of L at every state, H3 if ∃ gϕ ∈ H(r, n), then ϕ ∈ H(r′ , n + 1) holds for
Hintikka structures only determine the truth values of for- some r′ extending (r, n);
mulae directly involved in the evaluation of a fixed formula H4 if ∀ gϕ ∈ H(r, n), then ϕ ∈ H(r′ , n + 1) holds for
θ, in the satisfiability of which we are interested. Another every r′ extending (r, n);
important difference between models and Hintikka struc- H5 if ∃(ϕ Uψ) ∈ H(r, n), then, for some r′ extending
tures is that, in Hintikka structures, the epistemic relations (r, n), there exists i ≥ n such that ψ ∈ H(r′ , i) and
RD C
A and RA only have to satisfy the properties laid down in ϕ ∈ H(r′ , j) holds for every n ≤ j < i;
Definition 2.1. All the other information about the desirable H6 if ∀(ϕ Uψ) ∈ H(r, n), then, for every r′ extending
properties of epistemic relations is contained in the labeling (r, n), there exists i ≥ n such that ψ ∈ H(r′ , i) and
of states in Hintikka structures. This labeling ensures that ϕ ∈ H(r′ , j) holds for every n ≤ j < i;
every Hintikka structure generates a pseudo-model (by the H7 if ¬DA ϕ ∈ H(r, n), then there ex-
construction of Lemma 3.5), which can then be turned into ists r′ ∈ R and n′ ∈ N such that
a model. ((r, n), (r′ , n′ )) ∈ RD and ¬ϕ ∈ H(r ′
, n′ );
A
′ ′ D
H8 if ((r, n), (r , n )) ∈ RA , then DA′ ϕ ∈ H(r, n) iff
Definition 3.1 A set ∆ ⊆ L is patently inconsistent if it
DA′ ϕ ∈ H(r′ , n′ ) holds for every A′ ⊆ A;
contains a complementary pair of formulae (i.e., formulae
H9 if ¬CA ϕ ∈ H(r, n), then there ex-
ψ and ¬ψ for some formula ψ).
ists r′ ∈ R and n′ ∈ N such that
A set ∆ ⊆ L is fully expanded if it is not patently
((r, n), (r′ , n′ )) ∈ RC and ¬ϕ ∈ H(r ′
, n′ ).
inconsistent2 and satisfies the following conditions, where A
Sub(ψ) stands for the set of subformulae of a formula ψ: Synchronous temporal-epistemic Hintikka structures are
defined accordingly.
1. if ¬¬ϕ ∈ ∆, then ϕ ∈ ∆;
2. if ϕ ∧ ψ ∈ ∆, then ϕ ∈ ∆ and ψ ∈ ∆; Definition 3.3 A formula θ is satisfiable in a TEHS H with
3. if ¬(ϕ ∧ ψ) ∈ ∆, then ¬ϕ ∈ ∆ or ¬ϕ ∈ ∆; a labeling function H if θ ∈ H(r, n) for some point (r, n)
4. if ¬∃ gϕ ∈ ∆, then ∀ g¬ϕ ∈ ∆; of H. A set of formulae Θ is satisfiable in H if Θ ⊆ H(r, n)
for some point (r, n) of H.
5. if ¬∀ gϕ ∈ ∆, then ∃ g¬ϕ ∈ ∆;
6. if ∃(ϕ Uψ) ∈ ∆, then ψ ∈ ∆ or ϕ, ∃ g∃(ϕ Uψ) ∈ ∆; Now, we show that θ ∈ L is satisfiable in a TEM iff
7. if ¬∃(ϕ Uψ) ∈ ∆, then ¬ψ, ¬ϕ ∈ ∆ or it is satisfiable in a TEHS. One direction is almost imme-
¬ψ, ¬∃ g∃(ϕ Uψ) ∈ ∆; diate, as every TEM naturally induces a TEHS. More pre-
8. if ∀(ϕ Uψ) ∈ ∆, then ψ ∈ ∆ or ϕ, ∀ g∀(ϕ Uψ) ∈ ∆; cisely, given a TEM M, we define the extended labeling
9. if ¬∀(ϕ Uψ) ∈ ∆, then ¬ψ, ¬ϕ ∈ ∆ or L+ +
M on the set of points of M as follows: LM (r, n) =
¬ψ, ¬∀ g∀(ϕ Uψ) ∈ ∆; { ϕ | M, (r, n) ϕ } for every (r, n). The following claim
10. if DA ϕ ∈ ∆, then DA′ ϕ ∈ ∆ for every A′ such that is then straightforward.
A ⊆ A′ ⊆ Σ; Lemma 3.4 Let M =
11. if DA ϕ ∈ ∆, then ϕ ∈ ∆; (Σ, S, R, {RD }A∈P
C
+ (Σ) , {R }A∈P + (Σ) , L) be
A A
12. if CA ϕ ∈ ∆, then Da (ϕ∧CA ϕ) ∈ ∆ for every a ∈ A; a TEM satisfying θ ∈ L, and let L+ M be
2 Even though in general, not being patently inconsistent is a weaker the extended labeling on M. Then, H =
+
condition than a propositional consistency, in the case of fully expanded (Σ, S, R, {RD } +
A A∈P (Σ) , {RC
} +
A A∈P (Σ) , L ) is a TEHS
sets, they coincide. satisfying θ.
To establish the converse, we first prove that the exis- So, assume that ((r, n), (r′ , n′ )) ∈ R′D A . There are two
tence of a Hintikka structure satisfying θ implies the exis- cases to consider. If (r, n) = (r′ , n′ ), then the conclusion
tence of a pseudo-model satisfying θ; then, we prove that immediately follows from (H1). Otherwise, there exists an
this in turn implies the existence of a model satisfying θ. undirected path from (r, n) to (r′ , n′ ) along the relations
′
RD A′ , where each A is a superset of A. Then, due to (H8),
Lemma 3.5 If θ ∈ L is satisfiable in a TEHS, then it is DA ϕ ∈ H(r , n ); hence, by (H1), ϕ ∈ H(r′ , n′ ), as de-
′ ′
satisfiable in a pseudo-TEM. sired.
Now, let ¬DA ϕ ∈ H(r, n). In view of the inductive
Proof. Let H = (Σ, S, R, {RD C
A }A∈P + (Σ) , {RA }A∈P + (Σ) , H) hypothesis, it suffices to show that there exist r′ ∈ R
be a TEHS satisfying θ. We build a pseudo-TEM satis- and n′ ∈ N such that ((r, n), (r′ , n′ )) ∈ R′D A and ¬ϕ ∈
fying θ as follows. First, for every A ∈ P + (Σ), let H(r′ , n′ ). By (H7), there exists r′ ∈ R and n′ ∈ N
R′DAS be the reflexive, symmetric, and transitive closure such that ((r, n), (r′ , n′ )) ∈ RD ′ ′
D ′C A and ¬ϕ ∈ H(r , n ). As
of
S A⊆B RB and let RA be the transitive closure of D ′D
RA ⊆ RA , the desired conclusion follows.
′D D ′D C ′C
a∈A Ra . Notice that RA ⊆ RA and RA ⊆ RA for Suppose that χ = CA ϕ. Assume that CA ϕ ∈ H(r, n).
+
every A ∈ P (Σ). Next, let L(r, n) = H(r, n) ∩ AP, for In view of the inductive hypothesis, it suffices to show that
every point (r, n) ∈ R × N. It is then easy to check that if (r′ , n′ ) is A-reachable from (r, n) in M′ , then ϕ ∈
M′ = (Σ, S, R, {R′D ′C
A }A∈P + (Σ) , {RA }A∈P + (Σ) , L) is a H(r′ , n′ ). If (r, n) = (r′ , n′ ) the claim follows from (H1).
pseudo-TEM. So, suppose that, for some m ≥ 1, there exists a sequence of
To complete the proof of the lemma, we show, by induc- points (r, n) = (r0 , n0 ), . . . , (rm−1 , nm−1 ), (rm , nm ) =
tion on the formula χ ∈ L that, for every point (r, n) and (r′ , n′ ) such that, for every 0 ≤ i < m, there exists ai ∈ A
every χ ∈ L, the following hold: such that ((ri , ni ), (ri+1 , ni+1 )) ∈ R′D ai . Then, for every
(i) χ ∈ H(r, n) implies M′ , (r, n) χ; 0 ≤ i < m, there exists a path from (ri , ni ) to (ri+1 , ni+1 )
(ii) ¬χ ∈ H(r, n) implies M′ , (r, n) ¬χ. along relations RD ′ ′
A′ such that ai ∈ A for every A . Then,
Let χ be some p ∈ AP. Then, p ∈ H(r, n) implies we can show by induction on i, using (H1) and (H8), that
p ∈ L(r, n) and thus, M′ , (r, n) p; if, on the other hand, CA ϕ ∈ H(ri , ni ) holds for every 0 ≤ i < m. Indeed,
¬p ∈ H(r, n), then due to (H2), p ∈ / H(r, n) and thus this holds for i = 0; assuming that it holds for some i, by
p∈ / L(r, n); hence, M′ , (r, n) ¬p. (H1)(12) we have that Dai (ϕ ∧ CA ϕ) ∈ H(ri , ni ), hence,
Assume that the claim holds for all subformulae of χ; by (H1)(10) and (H8), ϕ ∈ H(ri+1 , ni+1 ). Now, by taking
then, we have to prove that it holds for χ, as well. i = m − 1 we obtain ϕ ∈ H(r′ , n′ ), as required.
Suppose that χ = ¬ϕ. If ¬ϕ ∈ H(r, n), then the induc- Finally, assume that ¬CA ϕ ∈ H(r, n). Then, the
tive hypothesis immediately gives us M′ , (r, n) ¬ϕ; if desired conclusion follows from (H9), the fact that
¬¬ϕ ∈ H(r, n), then by virtue of (H1), ϕ ∈ H(r, n) and RC ′C
A ⊆ RA , and the inductive hypothesis. 2
hence, by inductive hypothesis, M′ , (r, n) ϕ and thus
M′ , (r, n) ¬¬ϕ.
The cases of χ = ϕ ∧ ψ, χ = ∃ gϕ, and χ = ∀ gϕ are Lemma 3.6 If θ ∈ L is satisfiable in a pseudo-TEM, then
straightforward, using (H1) – (H4). it is satisfiable in a TEM.
Let χ be ∃(ϕ Uψ). If ∃(ϕ Uψ) ∈ H(r, n), then the de-
sired conclusion immediately follows from (H5) and the in- Proof. The proof is exactly the same as in [5, Section 3],
ductive hypothesis. If ¬∃(ϕ Uψ) ∈ H(r, n), then due to as the pseudo-models are only ‘defective’ with respect to
(H1), either ¬ψ, ¬ϕ ∈ H(r, n) or ¬ψ, ¬∃ g∃(ϕ Uψ) ∈ epistemic, but not temporal, relations; therefore, the con-
H(r, n). In the former case, the conclusion immediately struction for branching time is the same as for linear time. 2
follows from the inductive hypothesis. Otherwise, due to
(H1) and (H4), ¬∃(ϕ Uψ) ∈ H(r′ , n + 1) holds for ev- Lemmas 3.4, 3.5, and 3.6 immediately give us the fol-
ery run r′ extending (r, n). By repeating the argument, lowing theorem.
we obtain that, for every run r′ extending (r, n), either
Theorem 3.7 A θ ∈ L is satisfiable in a TEM iff it is satis-
¬ϕ ∈ H(r′ , i) for some i ≥ 0 and ¬ψ ∈ H(r′ , j) for
fiable in a TEHS.
every 0 ≤ j ≤ i or ¬ψ ∈ H(r′ , i) for every i ≥ 0. In ei-
ther case, the inductive hypothesis implies that M, (r, n)
¬∃(ϕ Uψ), as desired. 4 Tableau procedure for CMATEL(CD+BT)
The case of χ = ∀(ϕ Uψ) is similar to the previous one
and is left to the reader. In this section, we present a tableau procedure for CMA-
Suppose that χ = DA ϕ. Assume, first, that DA ϕ ∈ TEL(CD+BT). We describe a procedure for testing for sat-
H(r, n). In view of the inductive hypothesis, it suffices to isfiability in synchronous models, as it requires extra care.
show that ((r, n), (r′ , n′ )) ∈ R′D ′
A implies ϕ ∈ H(r , n ).
′
We then briefly mention how the general case is different
and argue that the outcome of the procedure is the same eventuality is fulfilled. Since truth in TEMs is simulated by
in both cases, implying that, satisfiability-wise, general and membership in state labels of Hintikka structures, eventual-
synchronous semantics are equivalent. ities impose respective conditions on the labels. Thus, the
presence of an eventuality ¬CA ϕ in the label of a state s
4.1 Overview of the procedure of a TEHS H requires the existence in H of an A-path (i.e.
a path along relations of the form RD D
B , where RB ⊆ RA )
D
from s to a state t whose label contains ¬ϕ, due to con-
The tableau procedure for testing a formula θ ∈ L for
dition (H9) of Definition 3.2. Similar requirements apply
satisfiability attempts to construct a non-empty graph T θ
to eventualities of the form ∃(ϕ Uψ) and ∀(ϕ Uψ) due to
(called tableau), whose nodes are finite sets of L-formulae,
conditions (H5) and (H6) of Definition 3.2. The tableau
encoding ‘sufficiently many’ TEHSs for θ, in the sense that
analogs of these conditions are called realization of even-
if θ is satisfiable, then it is satisfiable in a TEHS represented
tualities. If a tableau contains a node with an unrealized
by T θ . The main ideas underlying our tableau algorithm
eventuality in its label, then it cannot produce a TEHS, and
come from the tableau procedures for the logics PDL in
thus is ‘bad’ and needs repairing by removing such nodes.
[9], UB in [1] and CTL in [3] (see also a detailed exposi-
The third possible reason for a tableau to be ‘bad’ has to do
tion of tableaux for CTL in [10]), as well as recently de-
with successor nodes: it may so happen that some of the re-
veloped tableaux for multiagent epistemic logics in [6]. To
quired successors of a node s are missing from the tableau;
make the present paper self-contained, we outline the basic
then, s is ‘bad’, and hence needs to be removed. Notice that
ideas behind our tableau algorithm in line with those refer-
in TEHSs, and thus in tableaux, states have two kinds of
ences, and then describe the particulars specific to CMA-
successors: temporal and epistemic. The absence of either
TEL(CD+BT).
kind of successor can ruin the chances of a tableau node to
Usually, tableaux work by decomposing the input for-
correspond to a state of a TEHS.
mula into simpler formulae, in accordance with the seman-
The tableau procedure consists of three major phases:
tics of the logical connectives. In the classical propositional
pretableau construction, pre-state elimination, and state
case, “simpler” implies shorter, thus ensuring the termina-
elimination. During the first, we produce the pretableau
tion of the procedure. The decomposition into simpler for-
for θ—a directed graph P θ , from which the tableau T θ will
mulae in the tableau for classical propositional logic pro-
be extracted. The nodes of P θ are sets of formulae com-
duces a tree representing an exhaustive search for a Hintikka
ing in two varieties: states and pre-states. States are fully
set, the classical propositional analogue of Hintikka struc-
expanded sets, meant to represent (labels of) states of a Hin-
tures, for the input formula θ. If at least one leaf of that tree
tikka structure, while pre-states only play a temporary role
is a Hintikka set for θ, the search has succeeded and θ is
in the construction of T θ . During the second phase, all pre-
proved satisfiable; otherwise, it is declared unsatisfiable.
states from P θ are removed and their incoming edges are
When applied to logics containing fixpoint-definable op-
redirected, creating a smaller graph T0θ , the initial tableau
erators, such as CA , ∃ U, and ∀ U, these two defining
for θ. Finally, we remove from T0θ all states, if any, that
features of the classical tableau method no longer apply.
cannot be satisfied in a TEHS, for any of the reasons men-
First, the decomposition of the fixpoint formulae, which
tioned above. The elimination procedure results in a (possi-
is done by unfolding their fixpoint definitions, usually pro-
bly empty) subgraph T θ of T0θ , called the final tableau for
duces larger formulae: CA ϕ is decomposed into the formu-
θ. If some state ∆ of T θ contains θ, we declare θ satisfiable;
lae Da (ϕ ∧ CA ϕ); analogously for formulae of the form
otherwise, we declare it unsatisfiable. An example illustrat-
∃(ϕ Uψ) and ∀(ϕ Uψ). Hence, we need a termination-
ing the tableau construction is provided in Appendix A.
ensuring 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 4.2 Pretableau construction phase
and, hence, termination of the procedure. Second, the only
reason why a tableau may fail to produce a Hintikka set for All states and pre-states of the pretableau P θ constructed
the input formula in the classical case is that every attempt during this phase are ‘time-stamped’. Whenever necessary
to build such a set results in a collection of formulae con- to make it explicit, we will use the notation Γ[k] indicating
taining a patent inconsistency, i.e., a complementary pair of that pre-state Γ was created as the kth component of a run;
formulae ϕ, ¬ϕ. In the case of CMATEL(CD+BT), there likewise for states.
are other such reasons, specific to TEHS, which are more The pretableau contains three types of edge, described
involved structures than classical Hintikka sets. One such below. As already mentioned, a procedure attempts to
reason has to do with eventualities: the truth of an eventu- produce a compact representation of a sufficiently many
ality at a state s in a TEM M requires existence of a path TEHSs for the input formula θ by organizing an exhaustive
going from s to a state of M at which the ‘promise’ of that search for such structures. One type of edge, depicted by
unmarked double arrows =⇒, represents the search tran- Rule (DR): Given a state ∆[k] such that ¬DA ϕ ∈ ∆[k]
sitions in the tableau. The exhaustive search considers all and (DR) has not been applied to ∆[k] earlier, do the fol-
possible alternatives that arise when expanding pre-states lowing:
into states through branching when dealing with disjunc-
tive formulae. Thus, when we draw a double arrow from a Create a new pre-state Γ[k] S =
1. S {¬ϕ} ∪
pre-state Γ to states ∆ and ∆′ (depicted as Γ =⇒ ∆ and A ⊆A
′ { D A ′ ψ | D A ′ ψ ∈ ∆ } ∪ A ⊆A ¬DA′ ψ |
′ {
Γ =⇒ ∆′ , respectively), this intuitively means that, in any ¬DA′ ψ ∈ ∆ }.
TEHS, a state whose label extends the set Γ has to contain 2. If pre-state Γ[k] is patently inconsistent, remove it.
at least one of ∆ and ∆′ . Our first construction rule, (SR), 3. Otherwise, connect ∆[k] to Γ[k] with −→ .
¬DA ϕ
prescribes how to create tableau states from pre-states. 4. If, however, the tableau already contains a pre-state
Given a set Γ ⊆ L, we say that ∆ is a minimal, fully Γ′[k] = Γ[k] , do not add another copy of Γ′[k] , but sim-
expanded extension of Γ if ∆ is fully expanded, Γ ⊆ ∆, ¬DA ϕ
and there is no ∆′ such that Γ ⊆ ∆′ ⊂ ∆ and ∆′ is fully ply connect ∆[k] to Γ′[k] with −→ .
expanded. The third type of edge, depicted by single arrows marked
Rule (SR) Given a pre-state Γ[k] such that (SR) has not with formulae of the form ∃ gϕ, represent temporal transi-
been applied to Γ[k] earlier, do the following: tions in TEHSs that the tableau is trying to build. The ra-
1. Add to the pretableau all minimal fully expanded ex- tionale for this rule is similar to that for (DR), the only dif-
tensions ∆[k] of Γ[k] as states; ference being that we are now considering temporal, rather
than epistemic, formulae forcing creation of new pre-states.
2. if ∆[k] contains no formulae of the form ∃ gϕ, add
∃ g⊤ to it; Rule (Next): Given a state ∆[k] such that (Next) has not
3. for each so obtained state ∆[k] , put Γ[k] =⇒ ∆[k] ; been applied to ∆[k] earlier, do the following:
4. if, however, the pretableau already contains a state
1. For each ∃ gϕ ∈ ∆[k] , create a new pre-state Γ[k+1] =
∆′[m] that coincides with ∆[k] , do not create another
{ϕ} ∪ { ψ | ∀ gψ ∈ ∆[k] }.4
copy of ∆′[m] , but only put Γ[k] =⇒ ∆′[m] .
2. If pre-state Γ[k] is patently inconsistent, remove it im-
We denote by states(Γ) the (finite) set of states { ∆ | mediately.
Γ =⇒ ∆ }. ∃ gϕ
3. Otherwise, connect ∆[k] to Γ[k+1] with −→ .
Notice that in all construction rules, as in (SR), we allow
4. If, however, the tableau already contains a pre-state
reuse of (pre)states, which were originally stamped with a
Γ′[m] = Γ[k+1] , do not add another copy of Γ′[m] , but
possibly different time-stamp. This does not correspond to
∃ gϕ
one (pre)state being part of two different runs at different simply connect ∆[k] to Γ′[m] with −→ .
moments of time; rather, the ‘futures’ of these runs, starting
from the reused (pre)state, can be assumed to be identical, We now describe the order of application of the above
modulo the time difference. rules. We start off by creating a single pre-state {θ}, con-
The second type of edge in a pretableau represents epis- taining the input formula. Then, we alternatingly apply
temic relations in the TEHS that the procedure attempts (DR) and (Next) to the states created at the previous stage
to build. This type of edge is represented by single ar- and then applying (SR) to the newly created pre-states. The
rows marked with epistemic formulae whose presence in construction stage is over when the applications of (DR)
the source state requires the presence in the tableau of a tar- and (Next) do not produce any new pre-states.
get state, reachable by a particular epistemic relation. All
such formulae have the form ¬DA ϕ, as can be seen from 4.3 Pre-State elimination phase
Definition 3.2. Intuitively if, say ¬DA ϕ ∈ ∆[k] , then we
need some pre-state Γ[k] containing ¬ϕ to be accessible At this phase we remove from P θ all pre-states and dou-
from ∆[k] by RD 3
A . The reason we mark these single ar- ble arrows, which results in a smaller graph T0θ called the
rows by a formula ¬DA ϕ (rather than by just coalition A), initial tableau. Formally, we apply the following rule:
is that we have to remember why we had to create this par- Rule (PR) For every pre-state Γ in P θ , do the following:
ticular Γ, and not just what relation connects ∆ to Γ. This
information will be needed during the elimination phases. 1. Remove Γ from P θ .
We now formulate the rule producing this second type of χ
2. If there is a state ∆ in P θ with ∆ −→ Γ, then for every
edge. χ
state ∆′ ∈ states(Γ), put ∆ −→ ∆′ .
3 We 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 4 Note that, due to step 2 in the (SR) rule, every state contains at least
epistemic alternatives belong to the same temporal level of any TEHS. one formula of the form ∃ eϕ.
4.4 State elimination phase still unmarked ∆ ∈ Snθ , mark ∆ if there is at least one
DB ψ
marked ∆′ such that ∆ −→ ∆′ , for some B ⊆ A.
During this phase we remove from T0θ states that are not
satisfiable in a TEHS. As we do not create patently incon- • If ξ = ∃(ϕ Uψ), then we initially mark all ∆ ∈ Snθ
sistent states, there are two reasons why a state ∆ of T0θ such that ψ ∈ ∆. Then, we repeat the following sub-
can turn out to be unsatisfiable: either satisfiability of ∆ re- procedure until no more states get marked: for every
quires satisfiability of some other (epistemic or temporal) still unmarked ∆ ∈ Snθ , mark ∆ if ϕ ∈ ∆ and there is
successor states which turn out unsatisfiable, or ∆ contains ∃ gξ
at least one marked ∆′ such that ∆ −→ ∆′ .
an eventuality that is not realized in the tableau. Accord-
ingly, we have two elimination rules: (E1) and (E2). • If ξ = ∀(ϕ Uψ), then we initially mark all ∆ ∈ Snθ
Formally, the state elimination phase is divided into such that ψ ∈ ∆, and then we repeat the following sub-
stages; we start at stage 0 with T0θ ; at stage n + 1, we re- procedure until no more states get marked: for every
move exactly one state from the tableau Tnθ obtained at the still unmarked ∆ ∈ Snθ , mark ∆ if ϕ ∈ ∆ and, for
previous stage, by applying one of the elimination rules, ob- every formula ∃ gχ ∈ ∆, there is a marked state ∆′ ∈
θ
taining the tableau Tn+1 θ
. In the rules below, Sm denotes the ∃ gχ
θ
Snθ such that ∆ −→ ∆′ .
set of states of tableau Tm .
(E1) If ∆ contains a formula χ of the form ¬DA ϕ or We now describe the order of application of the above
χ rules. We have to be careful, since having applied (E2) to
∃ gϕ, and ∆ −→ ∆′ does not hold for any ∆′ ∈ Snθ , obtain
θ
Tn+1 by eliminating ∆ from Tnθ . a tableau, we could have removed all the states accessible
from some ∆ along the arrows marked with some χ; hence,
For the other elimination rule, we need the concept of
we need to reapply (E1) to the resultant tableau to remove
eventuality realization in a tableau.
such ∆’s. Conversely, having applied (E1), we could have
Definition 4.1 (Eventuality realization) thrown away states needed for realizing certain eventuali-
ties; hence, we need to reapply (E2). Thus, we need to apply
• The eventuality ¬CA ϕ is realized at ∆ in Tnθ if there (E1) and (E2) in an alternating sequence that cycles through
exists a path ∆ = ∆0 , ∆1 , . . . , ∆m , where m ≥ 0, all eventualities. More precisely, we arrange all eventuali-
such that ¬ϕ ∈ ∆m and, for every 0 ≤ i < m, there ties occurring in the states of T0θ in a list ξ1 , . . . , ξm . Then,
χi
exist χi = DB ψi such that B ⊆ A and ∆i −→ ∆i+1 . we proceed in cycles. Each cycle consists of alternatingly
applying (E2) to the pending eventuality, starting with ξ1 ,
• The eventuality ∃(ϕ Uψ) is realized at ∆ in Tnθ if there
and then applying (E1) to the resulting tableau, until all
exists a path ∆ = ∆0 , ∆1 , . . . , ∆m , where m ≥ 0,
the eventualities have been dealt with, i.e., we have reached
such that ψ ∈ ∆m , and for every 0 ≤ i < m, there
ξm . These cycles are repeated until no state is removed in a
∃ gχi
exist a formula χi such that ∆i −→ ∆i+1 and ϕ ∈ whole cycle. Then, the state elimination phase is over.
∆i . The graph produced at the end of the state elimination
phase is called the final tableau for θ, denoted by T θ , whose
• For eventualities of the form ∀(ϕ Uψ), we define the set of states is denoted by S θ .
notion “is realized at ∆ in Tnθ ” recursively as follows:
(i) If ψ ∈ ∆ then ∀(ϕ Uψ) is realized at ∆; Definition 4.2 The final tableau T θ is open if θ ∈ ∆ for
some ∆ ∈ S θ ; otherwise, T θ is closed.
(ii) If ϕ ∈ ∆ and, for every ∃ gχ ∈ ∆, there is a
∃ gχ If the final tableau is closed, the tableau procedure re-
state ∆′ ∈ Tnθ such that ∆ −→ ∆′ and ∀(ϕ Uψ) is
turns “no”; otherwise, it returns “yes”.
realized at ∆′ , then ∀(ϕ Uψ) is realized at ∆.
We briefly mention that, to test for satisfiability in gen-
Now, we can state our second state elimination rule. eral models, we relax the rule (DR), allowing states to have
(E2) If ∆ ∈ Snθ contains an eventuality ξ that is not re- epistemic successors from different temporal levels. As
alized at ∆ in Tnθ , then obtain Tn+1
θ
by removing ∆ from such a modification does not result in the outcome of the
θ
Tn . procedure, we conclude that, satisfiability-wise, the seman-
tics based on general models is equivalent to the one based
We check for realization of eventualities by running on synchronous models.
the following iterative procedures that eventually marks all
states realizing a given eventuality ξ in Tnθ :
5 Soundness, completeness, and complexity
• If ξ = ¬CA ϕ, then we initially mark all ∆ ∈ Snθ
such that ¬ϕ ∈ ∆. Then, we repeat the following sub- The soundness of a tableau procedure amounts to claim-
procedure until no more states get marked: for every ing that if the input formula θ is satisfiable, then the tableau
for θ is open. To establish soundness of the overall pro- Lemma 5.8 If T θ is open, then θ is satisfiable in a (syn-
cedure, we use a series of lemmas showing that every rule chronous) TEHS.
by itself is sound; the soundness of the overall procedure is
then an easy consequence. We give the proofs for the syn- Proof sketch. We build the TEHS H for θ by induction on
chronous case, the modification for the general case being the temporal levels. The main concern is to ensure that all
straightforward. The proofs of the following three lemmas eventualities in the resultant structure are realized, i.e. the
are straightforward. properties (H5), (H6) and (H9) from the definition of Hin-
tikka structures hold; all the other properties of Hintikka
Lemma 5.1 Let Γ be a pre-state of P θ such that structures transfer, more or less immediately, from an open
M, (r, n) Γ for some TEM M and point (r, n). Then, tableau. We alternate between realizing epistemic eventu-
M, (r, n) ∆ holds for at least one ∆ ∈ states(Γ). alities (formulae of the form ¬CA ϕ) and temporal eventu-
alities (formulae of the form ∃(ϕ Uψ) and ∀(ϕ Uψ)). Es-
Lemma 5.2 Let ∆ ∈ S θ be such that M, (r, n) ∆
sentially, the construction combines the construction used
for some TEM M and point (r, n), and let ¬DA ϕ ∈
in proving completeness of multi-agent epistemic Hintikka
∆. Then, there exists a point (r′ , n) ∈ M such that
structures from [6] and the one used in proving complete-
((r, n), (r′ , n′ )) ∈S RD ′ ′
A and M, (r , n ) ∆′ where
′ ness of CTL (see [10], which essentially uses the construc-
S = {¬ϕ} ∪
∆ A′ ⊆A { DA′ ψ | DA′ ψ ∈ ∆ } ∪
tion that is a simplification of the construction for ATL
A′ ⊆A { ¬DA′ ψ | ¬DA′ ψ ∈ ∆ }.
from [4]).
Lemma 5.3 Let ∆ ∈ S θ be such that M, (r, n) ∆ for We start by building the 0th level of our prospective Hin-
some TEM M and point (r, n), and ∃ gϕ ∈ ∆. Then, tikka structure from the level 0 of an open tableau. For each
M, (r′ , n + 1) {ϕ} ∪ { ψ | ∀ gψ ∈ ∆ } holds for some state ∆[0] on this level, if ∆[0] does not contain any epis-
r′ extending (r, n). temic eventualities, we define ∆[0] -epistemic component to
be ∆[0] with exactly one successor reachable by ¬DA ψ, for
Lemma 5.4 Let ∆ ∈ S θ be such that M, (r, n) ∆ for
each ¬DA ψ ∈ ∆[0] ; if, on the other hand, ¬CA ϕ ∈ ∆[0] ,
some TEM M and a point (r, n), and let ¬CA ϕ ∈ ∆. Then,
then the ∆[0] -epistemic component is a tree obtained from
¬CA ϕ is realized at ∆ in T θ .
a path in the tableau leading from ∆[0] along the arrows
Proof idea. Since ¬CA ϕ is true at s, there is a path in marked with formulae of the form ¬DB χ to a state ∆′[0]
M from s leading to a state satisfying ¬ϕ. As the tableau containing ϕ; the tree is obtained from the path by giv-
organizes an exhaustive search, a chain of tableau states ing each component of the path enough successors, as de-
corresponding to those states in the model will be produced. scribed above. As all the unrealized epistemic eventualities
2 are propagated down the components (hence, appear in the
leaves of the tree), we can stitch them up together to obtain
The next two lemmas are proved likewise. a graph where each epistemic eventuality is realized.
Now, having built the 0th level of our prospective Hin-
Lemma 5.5 Let ∆ ∈ S θ be such that M, (r, n) ∆ for
tikka structure, we take care of realizing all the temporal
some TEM M and a point (r, n), and let ∃(ϕ Uψ) ∈ ∆.
eventualities contained in the states of level 0. This is done
Then, ∃(ϕ Uψ) is realized at ∆ in T θ .
exactly as in the completeness proof of the tableau proce-
Lemma 5.6 Let ∆ ∈ S θ be such that M, (r, n) ∆ for dure for CTL ([10]): we define the ∆[0] -temporal compo-
some TEM M and a point (r, n), and let ∀(ϕ Uψ) ∈ ∆. nent for each ∆[0] as follows: if it does not contain any
Then, ∀(ϕ Uψ) is realized at ∆ in T θ . temporal eventualities, then we take ∆[0] with one temporal
successor for each ∃ gϕ ∈ ∆. If ∃(ϕ Uψ) ∈ ∆, then we
Theorem 5.7 If θ ∈ L is satisfiable in a TEM, then T θ is
take a temporal path realizing ∃(ϕ Uψ) ∈ ∆ and give to
open.
every node enough temporal successors, as describe above.
Proof sketch. Using the preceding lemmas, we show by Lastly, if ∀(ϕ Uψ) ∈ ∆, then we take a temporal tree wit-
induction on the number of stages in the state elimina- nessing the the realizion of ∀ϕ ∈ ∆ in the tableau (for de-
tion phase that no satisfiable state can be eliminated due tails, see [10]). As eventualities are again passed down, we
to (E1) or (E2). The claim then follows from Lemma 5.1. 2 can stitch up an infinite tree realizing all the eventualities
contained in the states making up the tree.
The completeness of a tableau procedure means that if Next, we repeat the procedure inductively. For the mth
the tableau for a formula θ is open, then θ is satisfiable in epistemic level, we independently apply to each state on this
a TEM. In view of Theorem 3.7, it suffices to show that level the procedure described above for level 0, so that the
an open tableau for θ can produce a TEHS satisfying θ. epistemic structures unfolding from any two points on level
Moreover, we show that this TEHS can be constructed syn- m are disjoint, and also give to each newly created point a
chronous. ‘history’ consisting of a path of m−1 states of the form {⊤}
(so that we do not create any new epistemic eventualities). [2] E. Allen Emerson. Temporal and modal logics. In
Having fixed all the epistemic eventualities at the mth level, J. van Leeuwen, editor, Handbook of Theoretical
we repeat the procedure described in the previous paragraph Computer Science, volume B, pages 995–1072. MIT
to fix all the temporal eventualities contained in states of Press, 1990.
level m.
[3] E. Allen Emerson and Joseph Halpern. Decision pro-
Thus, we produce a chain of structures ordered by
cedures and expressiveness in the temporal logic of
inclusion. Eventually, we take the (infinite) union of all the
branching time. Journal of Computer and System Sci-
structures defined at the finite states of that construction,
ences, 30(1):1–24, 1985.
and then put H(∆[k] ) = ∆[k] for every ∆[k] , to obtain a
TEHS satisfying θ. 2 [4] Valentin Goranko and Dmitry Shkatov. Tableau-
based decision procedures for logics of strategic abil-
The completeness is now immediate from Lemma 5.8 ity in multi-agent systems. To appear in ACM
and Theorem 3.7. Transactions on Computational Logic. Available at
http://tocl.acm.org/accepted.html.
Theorem 5.9 (Completeness) If T θ is open, then θ is sat-
isfiable, in a (synchronous) TEM. [5] Valentin Goranko and Dmitry Shkatov. Tableau-
based decision procedure for full coalitional multi-
As for the complexity, for lack of space, we only mention agent temporal-epistemic logic of linear time. In
that the above procedure runs in exponential time (the cal- Decker, Sichman, Sierra, and Castelfranchi, editors,
culations are fairly routine), thus matching the lower bound Proc. of the 8th Int. Conf. on Autonomous Agents and
known from [7]. Multiagent Systems (AAMAS 2009), May 2009, Bu-
dapest, Hungary, 2009.
6 Concluding remarks [6] Valentin Goranko and Dmitry Shkatov. Tableau-based
procedure for deciding satisfiability in the full coali-
We have presented an incremental tableau-based deci- tional multiagent epistemic logic. In Sergei Artemov
sion procedure for the full coalitional temporal-epistemic and Anil Nerode, editors, Proc. of the Symposium
logic of branching time CMATEL(CD+BT). The proce- on Logical Foundations of Computer Science (LFCS
dure is complexity-optimal, intuitive, and practically rea- 2009), volume 5407 of Lecture Notes in Computer
sonably efficient (as the number of (pre)states it creates is Science, pages 197–213. Springer-Verlag, 2009.
usually significantly smaller that the powerset of all subsets
of the close of the formula that is tested for satisfiability); it [7] Joseph Y. Halpern and Moshe Y. Vardi. The complex-
is, therefore, suitable for both manual and automated exe- ity of reasoning about knowledge and time I: Lower
cution. Moreover, it is fairly flexible and easily amenable to bounds. Journal of Computer and System Sciences,
modifications for variations of the semantics, such as those 38(1):195–237, 1989.
mentioned in section 2. Since in the semantics considered [8] Agi Kurucz, Frank Wolter, Michael Zakharyaschev,
in this paper there is essentially no interaction between the and Dov Gabbay. Multi-dimentional Modal Logics:
temporal and epistemic fragments, our procedure combines Theory and Applications. Elsevier, 2003.
in a modular way tableaux for the full coalitional multia-
gent epistemic logic CMAEL(CD) and for CTL. Such in- [9] Vaughan R. Pratt. A practical decision method for
teraction, however, can be triggered by imposing various propositional dynamic logic. In Proceedings of the
natural semantic conditions, such as “no learning” or “no 10th Annual ACM Symposium on the Theory of Com-
forgetting”. As shown in [7], such conditions may increase puting, pages 326–227, San Diego, California, May
dramatically the complexity of the logic, up to highly un- 1979.
decidable. However, even for the relatively ‘easy’ cases of [10] Dmitry Shkatov. Incremental CTL-tableaux revisited.
EXPSPACE-hard logics, the construction of a tableau pro- Submitted.
cedures is still an open challenge, which we intend to ad-
dress in the future. [11] Dirk Walther. ATEL with common and distributed
knowledge is ExpTime-complete. In Proceedings of
References Methods for Modalities 4, Berlin, 2005.
[12] Dirk Walther, Carsten Lutz, Frank Wolter, and
[1] Mordechai Ben-Ari, Amir Pnueli, and Zohar Manna. Michael Wooldridge. ATL satisfiability is indeed
The temporal logic of branching time. Acta Informat- ExpTime-complete. Journal of Logic and Computa-
ica, 20:207–226, 1983. tion, 16(6):765–787, 2006.
[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 exam-
ple of how our procedure works on the formula
∀(¬C{a,b} p U ¬D{a,c} p). To simplify the exam-
ple, 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
[0] [0] [0]
∆1 ∆2 ∆3
χ 1 χ 2
? ?
Γ1 χ1 χ2- Γ2
[0] [0]
I
?I@ @R I@
? @
R
χ1 χ1 χ2 χ2
[0] [0] [0] [0] [0]
∆4 ∆5 ∆6 ∆7 ∆8
@
χ0
R ?
@
χ0 χ0 χ0 χ0
- [1]
- Γ3
χ0
I
?[0]
∆9
χ0 = ∃ e⊤;
χ1 = ¬Da (p ∧ C{a,b} p);
χ2 = ¬Db (p ∧ C{a,b} p);
Γ0 = {∀(¬C{a,b} p U D{a,c} p) = θ, ⊤};
∆1 = {θ, ¬C{a,b} p, ∀ eθ, χ1 , ∃ e⊤};
∆2 = {D{a,c} p, p, ∃ e⊤};
∆3 = {θ, ¬C{a,b} p, ∀ eθ, χ2 , ∃ e⊤};
Γ1 = {χ1 , ¬(p ∧ C{a,c} p)};
Γ2 = {χ2 , ¬(p ∧ C{a,c} p)};
∆4 = {χ1 , ¬p, ∃ e⊤};
∆5 = {χ1 , ¬C{a,b} p, ∃ e⊤};
∆6 = {χ1 , ¬C{a,b} p, χ2 , ∃ e⊤};
∆7 = {χ2 , ¬C{a,c} p, ∃ e⊤};
∆8 = {χ2 , ¬p, ∃ e⊤};
Γ3 = {⊤};
∆9 = {⊤, ∃ e⊤}.
The initial tableau is obtained by removing all pre-states
(the Γs) and redirecting the arrows (i.e, ∆1 will be con-
nected 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 satis-
fiable.