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)