=Paper=
{{Paper
|id=Vol-1492/Paper_29
|storemode=property
|title=ExpTime Tableaux with Global Caching for Graded Propositional Dynamic Logic
|pdfUrl=https://ceur-ws.org/Vol-1492/Paper_29.pdf
|volume=Vol-1492
|dblpUrl=https://dblp.org/rec/conf/csp/Nguyen15
}}
==ExpTime Tableaux with Global Caching for Graded Propositional Dynamic Logic==
https://ceur-ws.org/Vol-1492/Paper_29.pdf
ExpTime Tableaux with Global Caching for Graded
Propositional Dynamic Logic
Linh Anh Nguyen
Institute of Informatics, University of Warsaw
Banacha 2, 02-097 Warsaw, Poland
nguyen@mimuw.edu.pl
Abstract. We present the first direct tableau decision procedure for graded PDL,
which uses global caching and has ExpTime (optimal) complexity when numbers
are encoded in unary. It shows how to combine integer linear feasibility checking
with checking fulfillment of existential star modalities for tableaux with global
caching.
1 Introduction
Propositional dynamic logic (PDL) is a well-known modal logic [5, 8]. Originally, it
was developed as a logic for reasoning about programs. However, its extensions are
also used for other purposes. For example, converse-PDL with regular inclusion ax-
ioms (CPDLreg ) can be used as a framework for multiagent logics [4]. As a variant of
PDL, ALC reg is a description logic for representing and reasoning about terminological
knowledge. Several extensions of ALC reg have been studied by the description logic
community [6].
The satisfiability problem in PDL is E XP T IME-complete [5]. In [15], Pratt gave a
tableau decision procedure with global caching for deciding PDL. In [14], Nguyen and
Szałas reformulated that procedure and extended it for dealing with checking consis-
tency of an ABox w.r.t. a TBox in PDL (where PDL is treated as a description logic).
The work [1] by Abate et al. gives another tableau decision procedure with global
caching for PDL, which propagates unfulfillment of existential star modalities on-
the-fly. There are also tableau decision procedures with global caching or state global
caching for CPDL (PDL with converse) [13, 7] and CPDLreg [4, 10].
Graded modal logics allow graded modalities for reasoning about the number of
successor states with a certain property. They have attracted attention from many re-
searchers.1 In description logic, the counterpart of graded modalities is qualified num-
ber restrictions. Some well-known E XP T IME description logics with qualified number
restrictions are SHIQ and SHOQ. The description logic corresponding to graded
CPDL is CIQ [3]. De Giacomo and Lenzerini [3] proved that the satisfiability problem
in CIQ is E XP T IME-complete when numbers are encoded in unary. Tobies [16] proved
that the satisfiability problem in SHIQ is E XP T IME-complete even when numbers are
encoded in binary.
1
See http://www.cs.man.ac.uk/~ezolin/ml/ for a list of related publications.
45
In this paper, we present the first direct tableau decision procedure for GPDL
(graded PDL). Our procedure uses global caching and has E XP T IME (optimal) com-
plexity when numbers are encoded in unary. It shows how to combine integer linear
feasibility checking [9, 12] with checking fulfillment of existential star modalities for
tableaux with global caching.
As related work on automated reasoning in GPDL and its extensions, De Giacomo
and Lenzerini gave methods for translating the satisfiability problem in CIQ into CIF
(a variant of CPDL with functionalities) [3], and in CIF into CPDL [2]. This estab-
lished the complexity E XP T IME-complete for CIQ (and GPDL) when numbers are
encoded in unary. However, this indirect method cannot give an efficient decision pro-
cedure for GPDL because it is not scalable w.r.t. numbers in graded modalities (i.e.,
qualified number restrictions). In particular, the translation from CIQ to CIF [3] may
result in a formula with a quadratic length, and similarly for the translation from CIF
to CPDL [3].
The rest of this paper is structured as follows. In Section 2, we present the notation
and semantics of GPDL and recall automaton-modal operators [8, 4], which are used
for our tableaux. We omit the feature of “global assumptions” as they can be expressed
in PDL (by “local assumptions”). In Section 3, we present a tableau calculus for GPDL,
starting with the data structure, the tableau rules and ending with the corresponding
tableau decision procedure and its properties. In Section 4, we give an example for
illustrating our procedure. Concluding remarks are given in Section 5.
2 Preliminaries
2.1 Graded Propositional Dynamic Logic
We use Σ to denote the set of atomic programs, and PROP to denote the set of propo-
sitions (i.e., atomic formulas). We denote elements of Σ by letters like σ and ̺, and
elements of PROP by letters like p and q.
A Kripke model is a pair M = h∆M , ·M i, where ∆M is a set of states and ·M is
an interpretation function that maps each proposition p ∈ PROP to a subset pM of
∆M and each atomic program σ ∈ Σ to a binary relation σ M on ∆M . Intuitively, pM
is the set of states in which p is true and σ M is the binary relation consisting of pairs
(input_state, output_state) of the program σ.
Formulas and programs of the base language of GPDL are defined respectively by
the following grammar, where p ∈ PROP, σ ∈ Σ and n is a natural number:
ϕ ::= ⊤ | ⊥ | p | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | hαiϕ | [α]ϕ | ≥ n σ.ϕ | ≤ n σ.ϕ
α ::= σ | α; α | α ∪ α | α∗ | ϕ?
Notice that we use the notation ≥ n σ.ϕ and ≤ n σ.ϕ as in description logic instead
of hσi≥n ϕ and hσi≤n ϕ (as the latter do not look “dual” to each other).
We use letters like α, β to denote programs, and ϕ, ψ, ξ to denote formulas.
The intended meaning of program operators is as follows:
– α; β stands for the sequential composition of α and β
46
(α; β)M = αM ◦ β M (α ∪ β)M = αM ∪ β M
(α∗ )M = (αM )∗ (ϕ?)M = {(x, x) | ϕM (x)}
⊤M = ∆M ⊥M = ∅
(¬ϕ)M = ∆M \ ϕM (ϕ → ψ)M = (¬ϕ ∨ ψ)M
(ϕ ∧ ψ)M = ϕM ∩ ψ M (ϕ ∨ ψ)M = ϕM ∪ ψ M
(hαiϕ)M = {x ∈ ∆M | ∃y(αM (x, y) ∧ ϕM (y))}
([α]ϕ)M = {x ∈ ∆M | ∀y(αM (x, y) → ϕM (y))}
(≥ n σ.ϕ)M = {x ∈ ∆M | #{y ∈ ∆M | σ M (x, y) ∧ ϕM (y)} ≥ n}
(≤ n σ.ϕ)M = {x ∈ ∆M | #{y ∈ ∆M | σ M (x, y) ∧ ϕM (y)} ≤ n}
Fig. 1. Interpretation of complex programs and complex formulas.
– α ∪ β stands for the set-theoretical union of α and β
– α∗ stands for the reflexive and transitive closure of α
– ϕ? stands for the test operator.
Informally, a formula hαiϕ represents the set of states x such that the program α
has a transition from x to a state y satisfying ϕ. Dually, a formula [α]ϕ represents the
set of states x from which every transition of α leads to a state satisfying ϕ. A formula
≥ n σ.ϕ (resp. ≤ n σ.ϕ) represents the set of states x such that the program σ has
transitions from x to at least (resp. at most) n pairwise different states satisfying ϕ.
Formally, the interpretation function of a Kripke model M is extended to interpret
complex formulas and complex programs as shown in Figure 1.
We write M, w |= ϕ to denote w ∈ ϕM . For a set Γ of formulas, we write M, w |=
Γ to denote that M, w |= ϕ for all ϕ ∈ Γ . If M, w |= ϕ (resp. M, w |= Γ ), then we
say that M satisfies ϕ (resp. Γ ) at w, and that ϕ (resp. Γ ) is satisfied at w in M.
A formula is in negation normal form (NNF) if it does not use → and it uses ¬ only
immediately before propositions, and furthermore, it does not contain subformulas of
the form ≥ 0 σ.ϕ or ≤ 0 σ.ϕ. Every formula can be transformed to an equivalent formula
in NNF. By ϕ we denote the NNF of ¬ϕ.
2.2 Automaton-Modal Operators
The alphabet Σ(α) of a program α and the regular language L(α) generated by α are
specified as follows:2
2
Note that Σ(α) contains not only atomic programs but also expressions of the form (ϕ?), and
a program α is a regular expression over its alphabet Σ(α).
47
Σ(σ) = {σ} L(σ) = {σ}
Σ(ϕ?) = {ϕ?} L(ϕ?) = {ϕ?}
Σ(β; γ) = Σ(β) ∪ Σ(γ) L(β; γ) = L(β).L(γ)
Σ(β ∪ γ) = Σ(β) ∪ Σ(γ) L(β ∪ γ) = L(β) ∪ L(γ)
Σ(β ∗ ) = Σ(β) L(β ∗ ) = (L(β))∗
where for sets of words M and N , M.N = {αβ | α ∈ M, β ∈ N }, S M 0 = {ε} (where
n+1
ε denotes the empty word), M = M.M for n ≥ 0, and M = n≥0 M n .
n ∗
We will use letters like ω to denote either an atomic program from Σ or a test (of
the form ϕ?). A word ω1 . . . ωk ∈ L(α) can be treated as the program (ω1 ; . . . ; ωk ),
especially when it is interpreted in a Kripke model.
Recall that a finite automaton A over alphabet Σ(α) is a tuple hΣ(α), Q, I, δ, F i,
where Q is a finite set of states, I ⊆ Q is the set of initial states, δ ⊆ Q × Σ(α) × Q is
the transition relation, and F ⊆ Q is the set of accepting states. A run of A on a word
ω1 . . . ωk is a finite sequence of states q0 , q1 , . . . , qk such that q0 ∈ I and δ(qi−1 , ωi , qi )
holds for every 1 ≤ i ≤ k. It is an accepting run if qk ∈ F . We say that A accepts a
word w if there exists an accepting run of A on w. The set of words accepted by A is
denoted by L(A).
We will use the following convention:
– given a finite automaton A, we always assume that A = (ΣA , QA , IA , δA , FA )
– for q ∈ QA , we define δA (q) = {(ω, q ′ ) | (q, ω, q ′ ) ∈ δA }.
As a finite automaton A over alphabet Σ(α) corresponds to a program (the regu-
lar expression recognizing the same language), it is interpreted in a Kripke model as
follows: [
AM = {γ M | γ ∈ L(A)}. (1)
For each program α, let Aα be a finite automaton recognizing the regular language
L(α). The automaton Aα can be constructed from α in polynomial time. We extend
the base language with the auxiliary modal operators [A, q] and hA, qi, where A is Aα
for some program α and q is a state of A. Here, [A, q] and hA, qi stand respectively
for [(A, q)] and h(A, q)i, where (A, q) is the automaton that differs from A only in
that q is its only initial state. We call [A, q] (resp. hA, qi) a universal (resp. existential)
automaton-modal operator.
In the extended language, if ϕ is a formula, then [A, q]ϕ and hA, qiϕ are also formu-
las. The semantics of these formulas are defined as usual, treating (A, q) as a program
with semantics specified by (1).
Given a Kripke model M and a state x ∈ ∆M , we have that x ∈ ([A, q]ϕ)M (resp.
x ∈ (hA, qiϕ)M ) iff
xk ∈ ϕM for all (resp. some) xk ∈ ∆M such that there exist a word ω1 . . . ωk
(with k ≥ 0) accepted by (A, q) with (x, xk ) ∈ (ω1 ; . . . ; ωk )M .
The condition (x, xk ) ∈ (ω1 ; . . . ; ωk )M means there exist states x0 = x, x1 , . . . , xk−1
of M such that, for each 1 ≤ i ≤ k, if ωi ∈ Σ then (xi−1 , xi ) ∈ ωiM , else ωi = (ψi ?)
for some ψi and xi−1 = xi and xi ∈ ψiM . Clearly, hA, qi is dual to [A, q] in the sense
that hA, qiϕ ≡ ¬[A, q]¬ϕ for any formula ϕ.
48
3 A Tableau Calculus for GPDL
In this section we present a tableau calculus for checking whether a given finite set
of formulas in NNF is satisfiable. We specify the data structure, the tableau rules, the
corresponding tableau decision procedure and state its properties.
3.1 The Data Structure
Let EdgeLabels = {testingUnsat, checkingFeasibility} × Σ. For e ∈ EdgeLabels, let
e = (πT (e), πΣ (e)). Thus, πT (e) is called the type of the edge label e, and πΣ (e) is an
atomic program.
A tableau is a rooted graph G = (V, E, ν), where V is a set of nodes, E ⊆ V × V
is a set of edges, ν ∈ V is the root, each node v ∈ V has a number of attributes, and
each edge (v, w) may be labeled by a set ELabels(v, w) ⊆ EdgeLabels. The attributes
of a tableau node v are:
– Type(v) ∈ {state, non-state},
– Status(v) ∈ {unexpanded, p-expanded, f-expanded, unsat},
– Label (v), which is a finite set of formulas, called the label of v,
– RFmls(v), which is a finite set of so called reduced formulas of v,
– ILConstraints(v), which is a finite set of integer linear constraints.
We call v a state if Type(v) = state, and a non-state otherwise. If (v, w) ∈ E
then we call v a predecessor of w and w a successor of v. An edge outgoing from
a node v is labeled iff Type(v) = state. The statuses p-expanded, f-expanded and
unsat mean “partially expanded”, “fully expanded”, and “unsatisfiable”, respectively.
Status(v) may be p-expanded only when Type(v) = state, and RFmls(v) 6= ∅ only
when Type(v) = non-state.
ILConstraints(v) is available only when Type(v) = state and
Status(v) ∈
/ {unexpanded, p-expanded}.
The constraints use variables xw,e indexed by a pair (w, e) such that (v, w) ∈ E, e ∈
ELabels(v, w) and πT (e) = checkingFeasibility. Such a variable specifies how many
copies of the successor w using the edge label e will be created for v.
We apply global caching in the sense that if v1 and v2 are different nodes then either
Type(v1 ) 6= Type(v2 ) or Label (v1 ) 6= Label (v2 ) or RFmls(v1 ) 6= RFmls(v2 ).
By FullLabel (v) we denote the set Label (v) ∪ RFmls(v).
3.2 Tableau Rules
Our tableau calculus CGPDL for the GPDL is specified by a number of static rules, the
(forming-state) rule, two transitional rules and the (unsat) rule for updating unsatisfi-
ability of nodes. The rules except (unsat) are used to expand nodes of tableaux. Static
rules are written downwards, with a set of formulas above the line as the premise, which
represents the label of the node to which the rule is applied, and a number of sets of
formulas below the line as the (possible) conclusions, which represent the labels of the
49
Table 1. The static rules of CGPDL
X, ϕ ∧ ψ X, ϕ ∨ ψ
(∧) (∨)
X, ϕ, ψ X, ϕ | X, ψ
/ Σ, α is not a test, and IAα = {q1 , . . . , qk } :
if α ∈
X, [α]ϕ
(aut✷ )
X, [Aα , q1 ]ϕ, . . . , [Aα , qk ]ϕ
X, hαiϕ
(aut✸ )
X, hAα , q1 iϕ | . . . | X, hAα , qk iϕ
if δA (q) = {(ω1 , q1 ), . . . , (ωk , qk )} and q ∈
/ FA :
X, [A, q]ϕ
([A])
X, [ω1 ][A, q1 ]ϕ, . . . , [ωk ][A, qk ]ϕ
X, hA, qiϕ
(hAi)
X, hω1 ihA, q1 iϕ | . . . | X, hωk ihA, qk iϕ
if δA (q) = {(ω1 , q1 ), . . . , (ωk , qk )} and q ∈ FA :
X, [A, q]ϕ
([A]f )
X, [ω1 ][A, q1 ]ϕ, . . . , [ωk ][A, qk ]ϕ, ϕ
X, hA, qiϕ
(hAif )
X, hω1 ihA, q1 iϕ | . . . | X, hωk ihA, qk iϕ | X, ϕ
X, [ψ?]ϕ X, hψ?iϕ
(✷? ) (✸? )
X, ψ | X, ϕ X, ψ, ϕ
X, ≥ n σ.ϕ
(≥✸ ) (n ≥ 1)
X, ≥ n σ.ϕ, hσiϕ
X, hσiϕ
(✸≥ ) if X does not contain any ≥ n σ.ϕ with n ≥ 1
X, hσiϕ, ≥ 1 σ.ϕ
successor nodes resulting from the application of the rule. Possible conclusions of a
static rule are separated by |. If a rule is unary (i.e. with only one possible conclusion)
then its only conclusion is “firm” and we ignore the word “possible”. The meaning of a
static rule is that if the premise is satisfiable then some of the possible conclusions are
also satisfiable.
We use Γ , X, Y to denote sets of formulas and write Γ, ϕ to denote Γ ∪ {ϕ}. The
static rules of CGPDL are specified in Table 1. For any among them, the distinguished
50
Function NewSucc(v, type, label, rF mls, eLabel)
Global data: a rooted graph (V, E, ν).
Purpose: create a new successor for v.
create a new node w, V := V ∪ {w}, E := E ∪ {(v, w)};
Type(w) := type, Status(w) := unexpanded;
Label (w) := label, RFmls(w) := rF mls;
if Type(v) = state then ELabels(v, w) := {eLabel};
return w;
Function ConToSucc(v, type, label, rF mls, eLabel)
Global data: a rooted graph (V, E, ν).
Purpose: connect a node v to a successor, which is created if necessary.
if there exists a node w such that Type(w) = type, Label (w) = label and
RFmls(w) = rF mls then
E := E ∪ {(v, w)};
if Type(v) = state then ELabels(v, w) := ELabels(v, w) ∪ {eLabel};
else
w := NewSucc(v, type, label, rF mls, eLabel);
return w;
formula of the premise is called the principal formula of the rule. A static rule ρ is
applicable to a node v if the following conditions hold:
– Status(v) = unexpanded and Type(v) = non-state,
– the premise of the rule is equal to Label (v),
– the conditions accompanied with ρ are satisfied,
– the principal formula of ρ does not belong to RFmls(v).
The last condition means that if the principal formula belongs to RFmls(v) then ρ has
been applied to an ancestor node of v that corresponds to the same state in the intended
Kripke model as v, and therefore should not be applied again.
If ρ is a static rule applicable to v, then the application is as follows:
– Let ϕ be the principal formula and X1 , . . . , Xk the possible conclusions of ρ.
– For each 1 ≤ i ≤ k, do ConToSucc(v, non-state, Xi , RFmls(v) ∪ {ϕ}, null),
which is specified on page 50.
– Status(v) := f-expanded.
The (forming-state) rule is applicable to a node v if Type(v) = non-state and no
static rule is applicable to v. Application of this rule to such a node v is done by calling
ConToSucc(v, state, Label (v), ∅, null).
The transitional partial-expansion rule (TP) is applicable to a node v if Type(v) =
state and Status(v) = unexpanded. Application of this rule to such a node v is done
as follows:
1. for each hσiϕ ∈ Label (v) (where σ ∈ Σ), do
51
(a) label := {ϕ} ∪ {ψ | [σ]ψ ∈ Label (v)}
(b) eLabel := (testingUnsat, σ)
(c) ConToSucc(v, non-state, label, ∅, eLabel)
2. Status(v) := p-expanded.
The transitional full-expansion rule (TF) is applicable to a node v if Type(v) =
state and Status(v) = p-expanded. Application of this rule to such a node v is done as
follows:
1. E := ∅, E ′ := ∅
2. for each (≥ n σ.ϕ) ∈ Label (v) do
E := E ∪ {(σ, X)}, where X = {ϕ} ∪ {ψ | [σ]ψ ∈ Label (v)}
3. for each (≤ n σ.ϕ) ∈ Label (v) do
(a) for each (σ, X) ∈ E do
i. if {ϕ, ϕ} ∩ X = ∅ then E ′ := E ′ ∪ {(σ, X ∪ {ϕ}), (σ, X ∪ {ϕ})}
(i.e., (σ, X) is replaced by (σ, X ∪ {ϕ}) and (σ, X ∪ {ϕ}))
ii. else E ′ := E ′ ∪ {(σ, X)}
(b) E := E ′ , E ′ := ∅
4. repeat
for each (≤ n σ.ϕ) ∈ Label (v), (σ, X) ∈ E and (σ, X ′ ) ∈ E such that ϕ ∈
X ∩ X ′ , (σ, X ∪ X ′ ) ∈/ E and X ∪ X ′ does not contain any pair of the form ψ,
ψ, add (σ, X ∪ X ) to E (i.e., the merger of (σ, X) and (σ, X ′ ) is added to E)
′
until no tuples were added to E during the last iteration
5. for each (σ, X) ∈ E do
ConToSucc(v, non-state, X, ∅, (checkingFeasibility, σ))
6. ILConstraints(v) := {xw,e ≥ 0 | (v, w) ∈ E, e ∈ ELabels(v, w) and
πT (e) = checkingFeasibility}
7. for each ϕ ∈ Label (v) do
Pϕ is of the form ≥ n σ.ψ then add to ILConstraints(v) the constraint
(a) if
{xw,e | (v, w) ∈ E, e ∈ ELabels(v, w), e = (checkingFeasibility, σ),
ψ ∈ Label (w)} ≥ n
Pϕ is of the form ≤ n σ.ψ then add to ILConstraints(v) the constraint
(b) if
{xw,e | (v, w) ∈ E, e ∈ ELabels(v, w), e = (checkingFeasibility, σ),
ψ ∈ Label (w)} ≤ n
8. Status(v) := f-expanded.
We give here an explanation for the rule (TF). To satisfy a requirement (≥ n σ.ϕ) ∈
Label (v), one can first create a successor w of v specified by the pair (σ, X) computed
at the step 2, where X presents Label (w), and then clone w to create n successors
for v (or only record the intention somehow). The label of w contains only formulas
necessary for realizing the requirement ≥ n σ.ϕ and the related ones of the form [σ]ψ at
v. To satisfy requirements of the form ≤ n′ σ.ϕ′ at v, we tend to use only copies of such
nodes like w extended with either ϕ′ or ϕ′ (for easy counting) as well as the mergers of
such extended nodes. So, we first start with the set E constructed at the step 2, which
consists of pairs with information about successors to be created for v. We then modify
E by taking into account necessary extensions for the nodes (see the step 3). After that
we continue modifying E by taking into account also appropriate mergers of nodes (see
52
the step 4). Successors for v are created at the step 5. The number of copies of a node
w that are intended to be used as successors of v with an edge label e is represented by
the variable xw,e (we will not actually create such copies). The set ILConstraints(v)
consisting of appropriate constraints about such variables are set at the steps 6-7.
Definition 1. Suppose Status(v) 6= unsat and hA, qiϕ ∈ Label (v). A trace of hA, qiϕ
starting from v is a sequence (v0 , ϕ0 ), . . . , (vk , ϕk ) such that:
– v0 = v and ϕ0 = hA, qiϕ,
– for every 1 ≤ i ≤ k, vi is a successor of vi−1 , Status(vi ) 6= unsat, and ϕi is a
formula of FullLabel (vi ) such that
• if the tableau rule expanding vi−1 is a static rule and ϕi−1 is not its principal
formula then ϕi = ϕi−1 ,
• else if the rule is (hAi) or (hAif ) then ϕi−1 is the principal formula of the form
hA, q ′ iϕ and ϕi is the formula obtained from ϕi−1 ,
• else if the rule is (✸? ) then ϕi−1 is the principal formula of the form
hψ?ihA, q ′ iϕ and ϕi = hA, q ′ iϕ,
• else Type(vi−1 ) = state, ϕi−1 is of the form hσihA, q ′ iϕ, vi is a succes-
sor of vi−1 resulting from the application of the tableau rule (TP) to vi−1 ,
(testingUnsat, σ) ∈ ELabels(vi−1 , vi ), and ϕi = hA, q ′ iϕ.
The trace is called a ✸-realization for hA, qiϕ at v0 if ϕk = ϕ.
The (unsat) rule is specified as follows: set Status(v) := unsat if Status(v) 6=
unsat and one of the following holds:
1. ⊥ ∈ Label (v) or there exists {ϕ, ¬ϕ} ⊆ Label (v);
2. Type(v) = non-state and, for every (v, w) ∈ E, Status(w) = unsat;
3. Type(v) = state and there exist (v, w) ∈ E and e ∈ ELabels(v, w) such that
πT (e) = testingUnsat and Status(w) = unsat;
4. Type(v) = state, Status(v) = f-expanded and ILConstraints(v) ∪ {xw,e = 0 |
(v, w) ∈ E, e ∈ ELabels(v, w), πT (e) = checkingFeasibility and Status(w) =
unsat} is infeasible;
5. there does not exist any ✸-realization for some hA, qiϕ ∈ Label (v) at v when all
paths starting from v do not contain any node that can be modified by some tableau
rule.
3.3 Checking Unsatisfiability
Let Γ be a finite set of formulas in NNF. A CGPDL -tableau for Γ is a tableau G =
(V, E, ν) constructed as follows. At the beginning, V = {ν}, E = ∅ and the attributes
of the root ν are specified as follows: Type(ν) = non-state, Status(ν) = unexpanded,
Label (ν) = Γ and RFmls(ν) = ∅. Then, while Status(ν) 6= unsat and there is a
tableau rule applicable to some node v, apply that rule to v.3 Observe that the set of all
formulas that may appear in the labels of the nodes of G is finite. Due to global caching,
G is finite and can be effectively constructed.
3
As an optimization, it makes sense to expand v only when there may exist a path from the root
to v that does not contain any node with status unsat.
53
Theorem 1. Let Γ be a finite set of formulas in NNF and G = (V, E, ν) an arbitrary
CGPDL -tableau for Γ . Then, Γ is unsatisfiable iff Status(ν) = unsat.
To check satisfiability of a finite set Γ of formulas in NNF, one can construct a
CGPDL -tableau G = (V, E, ν) for Γ and return “no” when Status(ν) = unsat, or “yes”
otherwise. We call this the CGPDL -tableau decision procedure. Various optimization
techniques [11] can be applied to this procedure.
Corollary 1. The CGPDL -tableau decision procedure has E XP T IME complexity when
numbers are encoded in unary.
Theorem 1 and Corollary 1 can be proved in a similar way as done for the tableau
decision procedures for CPDLreg [10], SHIQ [9] and SHOQ [12]. Proofs for them
will be provided later for the full version of the current paper.
4 An Illustrative Example
Consider
Γ = {hσ ∗ ip, ¬p, [σ; σ; σ ∗ ]¬p, [σ](¬p ∨ ¬q), ≥ 1000 σ.q, ≤ 1000 σ.(p ∨ q)},
and let
A1 = A σ ∗ = ({σ}, {0}, {0}, {(0, σ, 0)}, {0})
A2 = Aσ;σ;σ∗ = ({σ}, {0, 1, 2}, {0}, {(0, σ, 1), (1, σ, 2), (2, σ, 2)}, {2}).
A CGPDL -tableau G = (V, E, ν) for Γ is constructed as follows:
– At the beginning, G contains only the non-state ν with Label (ν) = Γ .
– Applying (aut✸ ) to ν, this node is connected to a new non-state v1 with
Label (v1 ) = Γ − {hσ ∗ ip} ∪ {hA1 , 0ip}.
– Applying (aut✷ ) to v1 , this node is connected to a new non-state v2 with
Label (v2 ) = Label (v1 ) − {[σ; σ; σ ∗ ]¬p} ∪ {[A2 , 0]¬p}.
– Applying ([A]) to v2 , this node is connected to a new non-state v3 with
Label (v3 ) = Label (v2 ) − {[A2 , 0]¬p} ∪ {[σ][A2 , 1]¬p}.
– Applying (≥✸ ) to v3 , this node is connected to a new non-state v4 with
Label (v4 ) = Label (v3 ) ∪ {hσiq}.
– Applying (hAif ) to v4 using the principal formula hA1 , 0ip, this node is connected
to two new non-states v5 and v6 with
Label (v5 ) = Label (v4 ) − {hA1 , 0ip} ∪ {p}
Label (v6 ) = Label (v4 ) − {hA1 , 0ip} ∪ {hσihA1 , 0ip}.
54
– Since {p, ¬p} ⊆ Label (v5 ), applying the (unsat) rule to v5 , this node gets status
unsat.
– Applying (✸≥ ) to v6 , this node is connected to a new non-state v7 with
Label (v7 ) = Label (v6 ) ∪ {≥ 1 σ.hA1 , 0ip}
= {hσihA1 , 0ip, ≥ 1 σ.hA1 , 0ip, ¬p, [σ][A2 , 1]¬p, [σ](¬p ∨ ¬q),
≥ 1000 σ.q, hσiq, ≤ 1000 σ.(p ∨ q)}.
– Applying the (forming-state) rule to v7 , this node is connected to a new state v8
with Label (v8 ) = Label (v7 ).
– Applying (TP) to v8 , this state is connected to two new non-states v9 and v10 , with
ELabels(v8 , v9 ) = ELabels(v8 , v10 ) = {(testingUnsat, σ)} and
Label (v9 ) = {hA1 , 0ip, [A2 , 1]¬p, ¬p ∨ ¬q}
Label (v10 ) = {q, [A2 , 1]¬p, ¬p ∨ ¬q}.
– Applying (TF) to v8 , this state is connected to additional new non-states v11 – v16 ,
with ELabels(v8 , vi ) = {e}, where e = (checkingFeasibility, σ) and 11 ≤ i ≤ 16,
and
Label (v11 ) = Label (v9 ) ∪ {p ∨ q}
Label (v12 ) = Label (v9 ) ∪ {¬p ∧ ¬q}
Label (v13 ) = Label (v10 ) ∪ {p ∨ q}
Label (v14 ) = Label (v10 ) ∪ {¬p ∧ ¬q}
Label (v15 ) = Label (v11 ) ∪ Label (v13 )
Label (v16 ) = Label (v12 ) ∪ Label (v14 ).
ILConstraints(v8 ) consists of xvi ,e ≥ 0, for 11 ≤ i ≤ 16, and the following:
xv11 ,e + xv12 ,e + xv15 ,e + xv16 ,e ≥ 1
xv13 ,e + xv14 ,e + xv15 ,e + xv16 ,e ≥ 1000
xv11 ,e + xv13 ,e + xv15 ,e ≤ 1000.
– Consider the node v12 . To shorten the presentation, we ignore details about expan-
sions for v12 and its descendants. We have {hA1 , 0ip, [A2 , 1]¬p, ¬p ∧ ¬q} ⊂
Label (v12 ). It can be seen that there will not be any ✸-realization for hA1 , 0ip at
v12 (there will be a cycle going through nodes with status different from unsat). As
a consequence, Status(v12 ) will be changed at some step to unsat by the (unsat)
rule.
– Consider the node v15 . We have {hA1 , 0ip, [A2 , 1]¬p, q, ¬p ∨ ¬q} ⊂ Label (v15 ).
Similarly as for v12 , it can be seen that there will not be any ✸-realization for
hA1 , 0ip at v15 . As a consequence, Status(v15 ) will be changed at some step to
unsat by the (unsat) rule.
– Observe that {q, ¬p ∧ ¬q} ⊂ Label (v14 ) ⊂ Label (v16 ). Clearly, Status(v14 ) and
Status(v16 ) will be changed at some steps to unsat.
– Consider the moment when the statuses of the nodes v12 , v14 , v15 and v16 have
been changed to unsat and consider the set that extends ILConstraints(v8 ) with
55
xvi ,e = 0 for i ∈ {12, 14, 15, 16}. This set is reduced to the following one w.r.t.
feasibility:
xv11 ,e ≥ 1
xv13 ,e ≥ 1000
xv11 ,e + xv13 ,e ≤ 1000.
Clearly, it is infeasible. As a consequence, Status(v8 ) is changed to unsat by the
(unsat) rule. By applying this rule in the propagation manner, the statuses of the
nodes v7 , v6 , v4 – v1 , ν are changed to unsat one after the other. According to
Theorem 1, we claim that the set Γ is unsatisfiable.
5 Conclusions
We have given the first direct tableau decision procedure for GPDL, which has E XP -
T IME (optimal) complexity when numbers are encoded in unary. It uses global caching
and exploits our technique of integer linear feasibility checking [9].
We have implemented our procedure in the scope of the reasoner TGC2.4 This rea-
soner also allows converse modalities [13, 9] and ABoxes [14, 9]. As far as we know, it
is the first reasoner that can decide GPDL.
Preliminary experiments with TGC2 showed that our method deals with num-
ber restrictions (graded modalities) much better than the well-known reasoners Racer,
FaCT++, HermiT and Pellet for description logics.
Acknowledgments
This work was done in cooperation with the project 2011/02/A/HS1/00395, which is
granted by the Polish National Science Centre (NCN).
References
1. Abate, P., Goré, R., Widmann, F.: An on-the-fly tableau-based decision procedure for PDL-
satisfiability. Electr. Notes Theor. Comput. Sci. 231, 191–209 (2009)
2. De Giacomo, G., Lenzerini, M.: Boosting the correspondence between description logics
and propositional dynamic logics. In: Proceedings of AAAI 1994. pp. 205–212. AAAI Press
/ The MIT Press (1994)
3. De Giacomo, G., Lenzerini, M.: What’s in an aggregate: Foundations for description logics
with tuples and sets. In: Proceedings of IJCAI 95. pp. 801–807. Morgan Kaufmann (1995)
4. Dunin-Kȩplicz, B., Nguyen, L., Szałas, A.: Converse-PDL with regular inclusion axioms: a
framework for MAS logics. Journal of Applied Non-Classical Logics 21(1), 61–91 (2011)
5. Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst.
Sci. 18(2), 194–211 (1979)
6. Giacomo, G.D., Lenzerini, M.: TBox and ABox reasoning in expressive description logics.
In: Proceedings of KR’1996. pp. 316–327 (1996)
4
See http://www.mimuw.edu.pl/~nguyen/TGC2.
56
7. Goré, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with
converse. In: Proceedings of IJCAR 2010. LNCS, vol. 6173, pp. 225–239. Springer (2010)
8. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
9. Nguyen, L.: ExpTime tableaux for the description logic SHIQ based on global state caching
and integer linear feasibility checking. arXiv:1205.5838 (2012)
10. Nguyen, L.: Cut-free ExpTime tableaux for Converse-PDL extended with regular inclusion
axioms. In: Proc. of KES-AMSTA’2013. Frontiers in Artificial Intelligence and Applications,
vol. 252, pp. 235–244. IOS Press (2013)
11. Nguyen, L.: Designing a tableau reasoner for description logics. In: Proc. of ICC-
SAMA’2015. Advances in Intelligent Systems and Computing, vol. 358, pp. 321–333.
Springer (2015)
12. Nguyen, L., Golińska-Pilarek, J.: An ExpTime tableau method for dealing with nominals
and qualified number restrictions in deciding the description logic SHOQ. Fundam. Inform.
135(4), 433–449 (2014)
13. Nguyen, L., Szałas, A.: An optimal tableau decision procedure for Converse-PDL. In:
Nguyen, N.T., Bui, T.D., Szczerbicki, E., Nguyen, N.B. (eds.) Proceedings of KSE’2009.
pp. 207–214. IEEE Computer Society (2009)
14. Nguyen, L., Szałas, A.: Checking consistency of an ABox w.r.t. global assumptions in PDL.
Fundamenta Informaticae 102(1), 97–113 (2010)
15. Pratt, V.: A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20(2),
231–254 (1980)
16. Tobies, S.: Complexity results and practical algorithms for logics in knowledge representa-
tion. Ph.D. thesis, RWTH-Aachen (2001)