A context-sensitive system is often employed in a dynamic environment due to its adaptivity. To represent temporal properties over an evolving system, we study an extension of Contextualised Description Logics (ConDLs) with linear temporal logic (LTL) operators, where ConDL axioms are used in place of propositional variables. The resulting language is interpreted over an in nite sequence of nested DLinterpretations. With EL, ALC, and SHOQ in consideration, we show that the formalism is rather well-behaved in the sense that the satis ability problem in most of the instances have the same complexity with underlying ConDLs. This holds even in the presence of rigidity constraints on the object level.
Introduction Contextual knowledge can represent many aspects of a system, either for describing internal structures or adjusting behaviors with accordance to the outside world. For instance, consider role-based paradigm where the contexts are dened by the roles that are currently played by an object. In this setting, an object can adapts its behaviour dynamically instead of getting a xed behaviour. To represent and reason over context-sensitive knowledge, description logics (DLs) of context have been introduced. The notion of context can take many forms in extension of DLs, e.g., as attributes [13,15]. Frequently, they are of the form two-layered DLs, one for the contextual knowledge and another for the domain knowledge [6,11,12].
On the other hand, a role-based system is often employed in a dynamic environment due to its capability to adapt. Objects can adjust their behaviours quickly by taking dierent roles to accommodate a dierent context. Temporal logics are often employed to dynamic properties of an evolving system. These properties can be positive, that should be satised by the system, or negative, that should not happen in any run of the system. Consider an example of a rolebased programming language that span a non-deterministic transition system. This is a standard setting in classical formal verication system where the states are dened over a set of propositional variables that are interpreted true. In our role-based setting, the state will be adjusted with a proper semantics to describe a context-sensitive world. A programmer might want to verify whether a critical role is played by at least one object in any time point.
In this work, we present a family of logic-based language to represent temporal properties over context-sensitive system. We consider the family of contextualized DLs (ConDLs) to describe context-sensitive knowledge [6]. While previous approaches are quite expressive due to possibilities of describing direct relation of object domains between two contexts, this leads to undecidability in the admission of rigid names. ConDLs take a dierent approach by restricting contextual view in top-down manner with a meta-level concept constructor to collect all contexts that satisfy an object-level axiom. The practicability of the language has been shown by utilizing ConDLs to reason over a role-based modeling language [5,14]. For the temporal part, we utilize linear temporal logic (LTL) which is interpreted over innite sequence of states. A similar approach is studied in temporalizing DLs where temporal operators are allowed in front of DL axioms [3,9]. With a similar argument in the complexity perspective, we allow temporal operators only in front of ConDL axioms. The obtained language is a family of three-dimensional description logics where temporal operators are used to express properties over evolving contextual knowledge represented by ConDL axioms.
An example of formula that can be expressed by this logic is (Private v JHasMoney (Bob)K) U (Work v :JworksFor (Bob; CompanyX )K): The axiom says that Bob has money in a private context until he is not working for Company X anymore in a work context. However it is not possible to say that in general if someone has money in private context, until that someone is not working for some companies. We investigate the satisability problem in this family of logic. Furthermore, it is very common in multi-dimensional DLs to desire the ability of expressing rigidity. For example, the role human is rigid since if something is a human, then it holds in any context or time. We say that a concept or role is rigid if their interpretation are the same across dimensions of the interpretation. Such constraints often make the reasoning problem harder. In this work, we consider the setting where rigidity constraints occur only on the object domain level and holds across all contexts and time points. 2 2.1
Basic Notions
For representing context-dependent knowledge, we consider ConDLs, a family of DLs of context studied in [6]. First, we recall the syntax of considered DLs and assume the reader familiar with their standard semantics. For a thorough introduction to DLs (specically ALC, EL and SHOQ), we refer to [1,2,4,10]. Denition 1 (DLs Syntax). Let N = (NC; NR; NI) be a signature of disjoint sets of concept names, role names and individual names, respectively. Let A 2 NC, r 2 NR, a 2 NI, and n 0. A concept C is built according to the following syntax rule
C; D ::= A j :C j C u D j 9r:C j fag j n r:C j >
Let C, D be concepts, r 2 NR and a; b 2 NI. A general concept inclusion (GCI) is of the form C v D. An assertion is of the form C(a) (concept assertion), or r(a; b) (role assertion). A Boolean axiom formula B is a Boolean combination of GCIs and assertions. A role inclusion axiom is of the form r v s and a transitivity axiom is of the form trans(r). Moreover, r is a a subrole of s 2 NR (w.r.t R) if every model of NR is a model of r v s. An RBox axiom is either a role inclusion axiom or a transitivity axiom. An RBox R is a nite set of RBox axioms. A Boolean knowledge base (KB) is a pair B = (B; R), where B is a Boolean axiom formula and R is an RBox.
In the basic DL ALC, these concept constructors are allowed: :C, C u D and 9r:C. An expressive DL which allow all possible concept constructors and axioms introduced above is called the DL SHOQ. In the lightweight DL EL, only C u D, 9r:C and > are allowed. In ALC and EL, RBox is empty. Furthermore, we assume at-most restrictions contains only simple roles, i.e., it has no transitive subroles, in SHQ and all its extensions to maintain the decidability.
The family of logic LM JLOK are two-sorted with a meta level signature M = (MC; MR; MI) and an object level signature O = (OC; OR; OI). We call MC, MR and MI the set of meta concept names , role names, and individual names respectively. Analogously, OC, OR, OI is called the set of object concept names , role names, and individual names respectively. All sets are assumed to be pairwise disjoint. Denition 2 ( LM JLOK Syntax). Let be an LO-axiom over the object level signature O and E 2 MC, s 2 MR and e 2 MI meta level names. An LM JLOKmeta level concept description G over M and O ( m-concept for short) is the smallest set that contains E for all E 2 MC (basic meta concept), J K for all LO-axioms (referring meta concept), and all complex concepts that can be built with the concept constructors allowed in LM .
Let G and H be m-concepts. An LM JLOK-Boolean meta level formula C over M and O ( m-formula for short) is built according to the following syntax rule
C ::= G v H j G(e) j s(e; f ) j C ^ C0 j :C: An m-assertion is either of the form G(e) (m-concept assertion) or s(e; f ) (mrole assertion). Furthermore we call an m-formula of the form G v H an m-GCI. An m-axiom is either an m-GCI, an m-assertion, an RBox axiom over M or an RBox axiom over O. A Boolean knowledge base over M and O (m-KB) is a tuple C = (C; RM ; RO) where C is an m-formula, RM is an RBox over M and RO is an RBox over O.
The semantics of LM JLOK is dened in terms of nested interpretations . The structure consists of a single meta level interpretation over M (called context) where each meta domain element is associated with an object level interpretation over O. Moreover, all object level interpretations have the same domain.
An example of m-axiom that says Bob works for Company X in a work context is Work v JworksFor (Bob; CompanyX )K. A referring meta concept encompasses contexts in which the object-level axiom inside it holds. In the example, JworksFor (Bob; CompanyX )K is interpreted as the set of all contexts that satises worksFor (Bob; CompanyX ).
Denition 3 (Nested Interpretation). A nested interpretation I (over M and O) is a tuple of the form I := (C; I; ; fIcgc2C); where (C; I) is an Minterpretation, and Ic := ( ; Ic ) is an O-interpretation for each c 2 C. Furthermore, we have that aIc = aId for all c; d 2 C (rigid object individual assumption). Denition 4 ( LM JLOK Semantics). Let I = (C; I; ; fIcgc2C) be a nested interpretation. The extension of the mapping I to complex m-concepts is extended to referring meta concepts as follows : J KI := fc 2 C j Ic j= g.
Let C be an m-formula. Satisfaction of C in I, written as I j= C ( I is a model of C), is dened by induction on the structure of C as follows:
I j= s(e; f ) i (eI; f I) 2 sI
I j= G v H i
GI
HI
I j= : i I 6j=
I j= G(e) i eI 2 GI I j= 1 ^ 2 i I j= 1 and I j= 2 Moreover, I is a model of RM (written I j= RM) if (C; I) is a model of RM, and I is a model of RO (written I j= RO) if for all c 2 C, Ic is a model of RO. Finally, I is a model of m-KB C = (C; RM; RO) (written I j= C) if I is a model of C, RM and RO. We say C is consistent if it has a model. 2.2
Temporalizing Contextualized Description Logics We introduce a family of temporalized DLs of context, denoted as LM JLOK-LTL. It is clear that an LM JLOK-LTL formula is an LTL formula where propositional variables are replaced by LM JLOK m-axioms.
Denition 5 ( LM JLOK-LTL Syntax). Let RM be an RBox over M and RO be an RBox over O. The set of LM JLOK-LTL formulae w.r.t. RM and RO is the smallest set satisfying: if is an m-axiom w.r.t. RM and RO then w.r.t. RM and RO; if and are LM JLOK-LTL formulae, then ^ , X are LM JLOK-LTL formulae w.r.t. RM and RO. is an LM JLOK-LTL formula _ , : ,
U , and A temporal context knowledge base (t-KB) is a tuple D = ( ; RM; RO) where RM is an RBox over M, RO is an RBox over O, and is an LM JLOK-LTL formula w.r.t. RM and RO.
The semantics of LM JLOK-LTL is based on LM JLOK-LTL-structures, sequences of nested interpretations. Constant domain assumption is respected on both meta and object level. We also consider rigid object concept and role names which are interpreted as the same across time-points and contexts. Denition 6 ( LiM0JLoOfKn-eLsTtedL-iSnetemrparnettaictiso)n.sAIn(iL)=M J(LCO;KI-(Li)T; L-;sftrIucctgucr2eCis a sequence T = (I(i)) (i) ) obeying the rigid individual assumption such that cI(i) = cI(j) for all meta level individual names c and all i; j 0, and aIc(i) = aId(j) for all object level individual names a, i; j 0, and c; d 2 C.
and a time-point i 0, validity of inductively: , an LM JLOK-LTL-structure T = (I(i))i 0
in T at time i, written T; i j= is dened T; i j= T; i j= T; i j= : T; i j= X T; i j= ^ U i i i i i
I(i) j= T; i j= T; i 6j=
T; i + 1 j= there is k for an m-axiom and T; i j=
i such that
T; k j=
and T; j j=
for all j; i
j < k
Furthermore if (
We say that an LM JLOK-LTL-structure T = (I(i))i 0 respects rigid object concept names (object role names) i for any rigid object concept name A (object role name r), we have that AIc(i) = AId(j) (rIc(i) = rId(j) ) holds for all i; j 2 f0; 1; :::g and all c; d 2 C. We denote the set of all rigid object concept and role names with ORC and ORR, respectively. We say that the OC n ORC are exible (object) concept names and OR n ORR are exible (object) role names.
Let D = ( ; RM; RO) be an t-KB: we say D is satisable w.r.t. rigid names i there is an LM JLOK-LTL-structure T respecting rigid object role names s.t. T is a model of D. Analogously satisable w.r.t. rigid concepts for respecting rigid object concept names, and simply satisable without rigid names in consideration. Notice that rigid concepts can be simulated by rigid roles, therefore there are only three cases. 3
Deciding Satisability in
LM JLOK-LTL We follow a similar idea of checking satisability of DL-LTL formulae and ConDL knowledge base. However, a naive approach to check temporal satisability and the contextual admissibility, i.e., collective satisability of guessed set of possible m-axiom combinations yields a triple exponential time algorithm. We show a double exponential time algorithm for this problem, and hence the same complexity with satisability problem in both SHOQ-LTL and SHOQJSHOQK w.r.t. rigid names. The idea is as follows: we guess the combinations of possible m-axioms that are satisable with appropriate sets of O-axioms for each m-axiom combination. Then, we check the satisability of temporal abstraction with respect of guessed m-axioms. Then, we check the admissibility of the metalevel by checking the existence of M-interpretations with an appropriate referring meta concepts abstraction that are guessed. Finally, we have to check guessed Oaxiom combinations if they are also admissible, i.e., there are O-interpretations that satisfy them. In the following, let D = ( ; RM; RO) be an t-KB to be tested. Let Axm( ) be the set of all m-axioms occuring in . Let p be a bijection mapping every occuring m-axiom in to a propositional variable p . We assume that p does not occur in and we dene P := fp j 2 Axm( )g. Let SX 2P which represents consistent m-axioms combinations.
Denition 7 (Temporal Abstraction). Let RM be an RBox over M, RO be an RBox over O, be an LM JLOK-LTL formula w.r.t. R, and function p : Axm( ) ! P be a bijection where p( ) = p .
The propositional LTL-formula p is obtained from by replacing every occurrence of an m-axiom by p . We call p the propositional abstraction of w.r.t. p.
Given an LM JLOK-LTL-structure T = (I(i))i 0, we obtain the LTL-structure Tp = (w(i))i 0 where w(i) := fp j 2 Axm( ) and I(i) j= g for every i 0. We call Tp the propositional abstraction of T w.r.t. p.
Lemma 1. Let T be an LM JLOK-LTL-structure w.r.t. RM and RO. Then, T is a model of w.r.t. RM and RO i Tp is a model of p.
However, we have to check the existence of each m-axiom combination which induces wi since it is possible that there is no model for such combination. We ensure each world represents one of possible combinations of the guessed set SX . Given a set SX 2P and a propositional LTL formula p, we dene p SX := p ^ G
_ ( ^ X2SX p 2X p ^
^ p 2P nX :p ) Furthermore, we denote the right part of the outer conjunction as SX . Then, we denote the satisability of an temporal abstraction in the notion of t-satisability.
2P . We say that p is t-satisable w.r.t. be an LMpJLOK-LTL formula and SX
SX if SX has a model.
Then, we check the existence of nested interpretations sequence that induces SX . Furthermore, we ensure that they respect rigid names for both meta and object levels.
Denition 9 (c-admissibility). We say that SX = fX1; : : : ; Xng such that
IS(X1) =2P(C;isIc(1-)a;dm;ifsIsic(b1l)egcw2.Cr.)t;.: :R: ;MI(ann)d=RO(Ci;f tIh(ne)r;e e;xfisItc(nn)egsct2edC)instuecrphrethtaattiofnosr
n: (
^ p 2P nXi : ; RM; RO)
We have two dened properties to be tested in order to check the satisability of an LM JLOK LTL formula. This is a similar idea with DL-LTL satisability checking, but we check the existence of appropriate nested interpretations instead of DL interpretations.
Lemma 2. Let D = ( ; RM; RO) be a t-KB, then D is satisable w.r.t. rigid names i there exists a set SX 2P such that p is t-satisable w.r.t. SX , and SX is c-admissible w.r.t. RM and RO.
In fact, this result is enough to give us a procedure to decide satisability in LM JLOK-LTL. One can use a similar approach in DL-LTL [3] for ALC-LTL by guessing an appropriate set SX , then do the checking for two separate satisability problems. However, consider the c-admissibility checking of SX . A naive approach is to build an m-KB
CSX := ^
^ Xi2SX p 2Xi (i) ^
^ with an appropriate renaming technique and then do the consistency checking. Since checking the m-KB C satisability can be done in time doubly exponential in the size of the C and the size of C is exponential in the size of D, this yields a 3-ExpTime decision procedure.
To this end, we split again the c-admissibility into two subproblems. Instead of checking the c-admissibility as a whole, we separate the satisability of meta level abstraction and object level admissibility. We guess a mapping y : SX 7! 2E that denotes possible O-axioms in referring meta concepts that are consistent together. For convenience, we say that we guess S = f(X1; Y1); :::; (Xn; Yn)g that built in such way, where Xi 2 SX and Yi = y(Xi) for each 1 i n.
We recall the approach in [6], by introducing abstraction on the context level. This is done by introducing a fresh concept name E to collect all contexts that are in J K. We dene AxO( ) be the set of all object axioms such that J K occurring in . Let f be a bijection mapping every occurring referring meta concept J K in to a meta concept name E . We assume that E does not occur in and we dene
E := fE j J K 2 AxO( )g.
Denition 10 (Context Level Abstraction). Let C = (C; RM; RO) be an LM JLOK-KB and function f : AxO( ) ! E be a bijection where f ( ) = E .
The outer abstraction of C is the KB Cf = (Cf ; RM) over M, where Cf is obtained from C by replacing every occurrence of a referring meta concept by E .
JGiKven an LM JLOK-structure I = (C; I; ; fIcgc2C), the contextual abstraction of I, denoted by If is the M-interpretation If = (C; If ) where for every x 2 (MC n E ) [ MR [ MI, we have xIf = xI, and for every E 2 E , we have EIf = I.
J K
Similar with the temporal abstraction, we state the connection between a nested interpretation and its abstraction in the following lemma. The complete proof can be found in [7].
LReOm.Tmhaen3,. ILiest aI m=o(dCel; oIf; C ;ifIIcgf c2isCa model of Cf .
) be a nested interpretation such that I j=
As in the temporal case, some combinations of referring meta concepts are not compatible due to the O-axioms that they represent. We recall the notion of weakly respect to restrict the nested-interpretations with allowed combinations of O-axioms.
Denition 11 (Weakly Respect). Let U NC and let V 2U . The Ninterpretation I = ( I ; I ) weakly respects (U ; V) if V Z where Z := fY U j there exists d 2 I with d 2 (CU;V )g and CU;V := dA2Y A u dA2UnY :A. It respects (U ; V) if V = Z.
In [6], the notion of outer consistency was introduced to express the
existence of the abstracted LM -interpretation over M. However, we have to extend
this notion since we have many abstracted LM -KB over M to be checked for
satisability. Furthermore, we recall a lemma from [6] to be used in the proof.
Denition 12 (Outer Consistency). We say that Cf is outer consistent w.r.t.
Y 2E if there exists a model of Cf that weakly respects (E ; Y). Furthermore,
we say that S is conjointly outer consistent i there exist J (
Lemma 4. For every M-interpretation H = ( ; H) the following two statements
are equivalent: (
The existence of rigid object names does not matter for checking outer
consistency since the next procedure will make verify it. Thus, it is possible to check if
the consistency of each CfXi (w.r.t. (E ; Y)) separately. The next step is to check
whether it is possible all of LO-axiom combinations over O in guessed referring
meta concept are satisable w.r.t. object-level rigid names. We check them, as a
KB over O that represent such combinations. We recall the notion of object-level
admissibility from [6,7], and extend it to our setting.
the LO-KB BY(i;j) = (BY(i;j) ; RO) over O where
Denition 13 (Object Level Admissibility). Let Yi 2E . We say that
Yi = fY(i;1); : : : ; Y(i;k)g o-admissible if there exists O-interpretations I(i;1) =
( ; I(i;1) ); : : : ; I(i;k) = ( ; I(i;k) ) such that: (
^ AJ K2Y(i;j) ^
^ AJ K2E nY(i;j) :
We say that SY = fY1; :::; Yng is conjointly o-admissible if every Yi, 1 i n is admissible and xI(i;j) = xI(i0;j0) for all x 2 ORC [ ORR [ OI for any (i; j); (i0; j0) 2 IndS where IndS = f(i; j) j Xi 2 SX and Yj 2 Yig.
Then, we have two properties that determine c-admissibility of SX , shown by the following lemma.
Lemma 5. SX is c-admissible i there exists a mapping y : SX 7! 2E and
SY = fy(Xi) j Xi 2 SX )g such that (
Satisability in expressive
In this subsection, we consider cases where both LM and LO are between ALC and SHOQ. We show that these cases are well-behaved in the sense that have same complexity as consistency problem in underlying ConDLs.
Theorem 1. The consistency problem in LM JLOK-LTL w.r.t. rigid names is 2-ExpTime-complete for if both LM and LO are between ALC and SHOQ. Proof. We begin with showing the hardness for ALCJALCK case. It is easy to see that an ALCJALCK-LTL t-KB is an ALCJALCK m-KB. Since ALCJALCK consistency problem w.r.t. rigid names is already 2- ExpTime-hard [6], we have that ALCJALCK-LTL (and more expressive LM JLOK-LTL) consistency checking w.r.t. rigid names is 2- ExpTime-hard.
We prove the upper bound for SHOQJSHOQK case. Let D = ( ; RM; RO) be an SHOQJSHOQK-LTL t-KB. We enumerate all possible sets SX 2P which can be done in double exponential time in the size of , hence D. For each Xi 2 SX , we enumerate Yi 2P to build S, which can be done, again, in double exponential time. In overall, we need double exponential time to guess a proper set S. Then, we check t-satisability of p w.r.t. SX . As argued in [3], this can be done in time exponential in the size of (and hence D) by constructing an appropriate Bchi automaton.
The next procedure is checking c-admissibility of S. First part is checking whether S is conjointly outer consistent. It is easy to see that there are exponentially many pair (Xi; Yi) to be checked. Furthermore, the size of CfXi is polynomial in the size of D, while Yi are at most exponential in the size of D. Exploiting Lemma 15 in [6], checking each of them can be done in exponential time. In overall, checking meta-level outer consistency can be done in time exponential in the size of .
The last property to be checked is o-admissibility. We have exponentially many Y(i;j) and each of them induces an SHOQ-formula of size polynomial. Hence, the overall size of BO is exponential in the size of D. Since checking the
S satisability of an ALC-KB can be done in exponential time of the size of the input, this yields a 2-ExpTime procedure. In overall we have two procedures that can be done in time doubly exponential to check c-admissibility of S.
We adjust the approach to be in NExpTime in the presence of only rigid concepts. The idea is to guess rigid concept membership for named individuals. On the other hand, the case without rigid names does not suer from exponential blow up from CSX since we can check each possible Xi separately. Theorem 2. The consistency problem in LM JLOK-LTL w.r.t rigid concepts is NExpTime-complete for if both LM and LO are between ALC and SHOQ. Theorem 3. The consistency problem in LM JLOK-LTL without rigid names is ExpTime-complete for if both LM and LO are between ALC and SHOQ. 4
In this section, we consider the case where at least one of LM and LO are EL.
We consider the case where at least one of underlying DLs is EL. First, we consider the case where rigid concepts and role names are present. Theorem 4. Satisability in LM JELK-LTL w.r.t. rigid names is NExpTimecomplete if LM is between ALC and SHOQ.
Proof. (Sketch) The hardness follows immediately from NExpTime-completeness of the consistency problem in ALCJELK [6]. To show the upper bound, we consider the SHOQJELK case. Most of the approach is similar to the case of SHOQJSHOQK-LTL, except in checking o-admisibility. The fact that BSO is a conjunction of EL-literals that can be decided in polynomial time yields an exponential time algorithm for checking o-admissibility instead of 2- ExpTime as in SHOQJSHOQK-LTL case.
We have several other cases that are easy consequences of existing result in this work and previous studies in ConDLs.
Theorem 5. Satisability in ELJLOK-LTL w.r.t. rigid names is 2-ExpTimecomplete if LM is between ALC and SHOQ.
Theorem 6. Satisability in LM JELK-LTL and ELJLOK-LTL w.r.t. rigid concepts is NExpTime-complete if LM and LO are between ALC and SHOQ. Theorem 7. Satisability in LM JELK-LTL and ELJLOK-LTL without rigid names is ExpTime-complete if LM and LO are between ALC and SHOQ.
The consistency of an ELJELK-KB is trivial if only conjunctions of m-axioms are allowed. Obviously, such assumption is not relevant anymore since LTL provides Boolean propositional operators. We consider beforehand the case of conjunctions of ELJELK-literals, i.e., ELJELK m-axioms and negated ELJELK m-axioms. In this setting, it is enough to consider satisability of ELJELK-LTL formula since both RM and RO are always empty.
Proof. We show a reduction from EL-LTL to show the hardness. Note that although an EL-LTL formula is an ELJELK-LTL formula without referring meta concepts, it is not possible to directly consider rigid names since we do not have rigid meta names. However, we can still reduce the problem by moving them to the object level. Given an EL-LTL formula , we dene an ELJELK-LTL formula 0 by replacing any EL-axiom in with fcg v J K where c is a fresh M-individual. Then, we can dene the rigid (object) concepts and role names in ELJELK-LTL problem as rigid concept and role names in EL-LTL problem, respectively. Then, it is easy to see that is satisabile w.r.t. rigid names i 0 is satisable w.r.t. rigid names.
We show the problem is in NExpTime for the upper bound. To check for the satisability, we guess a set SX 2P and we check whether p is t-satisable w.r.t. SX and SX is c-admissible. For t-satisability, we again may use the same argumentation as in Theorem 3 can be done in time exponential. For checking c-admissibility, we can build m-KB CSX and then check for the satisability. We have that CSX is of exponential size in the size of and CSX is a conjunction of ELJELK-literals. Using Claim 4.2, this yields an exponential time procedure for checking c-admissibility. Thus, we have NExpTime upper bound in overall.
The case with rigid concept names is an easy consequence of existing result. On the other hand, we exploit the same idea of checking satisability EL-LTL for the case without rigid names since checking satisability of ELJELK-literals conjunction can be done also in polynomial time.
Theorem 9. Satisability in ELJELK-LTL w.r.t. rigid concept is NExpTimecomplete and without rigid names is PSpace-complete. 5
Conclusion We have introduced and investigated a family of languages to describe temporal properties over contextual knowledge. The formula of the language can be constructed using LTL operators over ConDL axioms. The underlying DLs that are used in particular are EL, ALC and SHOQ. We have shown that most of considered members of the family are well-behaved in the sense that the satisability problem in LM JLOK-LTL has the same complexity as consistency problem in underlying ConDL LM JLOK, except for ELJELK-LTL cases.
For future work, we would like to investigate the use of resulting language in the setting of system verication. One of possible extensions is combining this work with ConDL-based actions as formalized in [17]. We would like to introduce a context-sensitive formal program based on ConDL-based actions. Then, a ConDL-LTLformula can be used to verify whether a property is satised in a (possibly non-deterministic) transition system induced by the program. Acknowledgements. The author wish to thank Stefan Borgwardt for helpful discussions on the idea for the upper bound of expressive LM JLOK-LTL. This work is supported by DFG in the Research Training Group RoSI (GRK 1907). 3. Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. ACM Trans.
Comput. Log. 13(3) (2012) 4. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description
Logic. Cambridge University Press (2017) 5. B hme, S., K hn, T.: Reasoning on context-dependent domain models. In: Wang, Z., Turhan, A., Wang, K., Zhang, X. (eds.) Semantic Technology - 7th Joint International Conference, JIST 2017, Gold Coast, QLD, Australia, November 1012, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10675, pp. 69 85.
Springer (2017), https://doi.org/10.1007/978-3-319-70682-5_5 6. B hme, S., Lippmann, M.: Decidable description logics of context with rigid roles.
In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9322, pp. 17 32. Springer (2015), https: //doi.org/10.1007/978-3-319-24246-0_2 7. B hme, S., Lippmann, M.: Description logics of context with rigid roles revisited.
LTCS-Report 15-04, Chair of Automata Theory, TU Dresden (2015), see http: //lat.inf.tu-dresden.de/research/reports.html . 8. Borgwardt, S., Thost, V.: LTL over EL axioms. LTCS-Report 15-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit t Dresden, Dresden, Germany (2015), see http://lat.inf.tudresden.de/research/reports.html. 9. Borgwardt, S., Thost, V.: Temporal query answering in the description logic EL. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the 24th International Joint Conference on Arti cial Intelligence (IJCAI’15). pp. 2819 2825. AAAI Press, Buenos Aires, Argentina (2015) 10. Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: Nebel, B. (ed.) Proceedings of the Seventeenth International Joint Conference on Arti cial Intelligence, IJCAI 2001, Seattle, Washington, USA, August 4-10, 2001. pp. 199 204. Morgan Kaufmann (2001) 11. Klarman, S., GutiØrrez-Basulto, V.: ALCALC: A context description logic.
In: Logics in Arti cial Intelligence - 12th European Conference, JELIA 2010, Helsinki, Finland, September 13-15, 2010. Proceedings. pp. 208 220 (2010). https://doi.org/10.1007/978-3-642-15675-5_19, https://doi.org/10. 1007/978-3-642-15675-5_19 12. Klarman, S., GutiØrrez-Basulto, V.: Description logics of context. J. Log. Comput.
26(3), 817 854 (2016), https://doi.org/10.1093/logcom/ext011 13. Kr tzsch, M., Marx, M., Ozaki, A., Thost, V.: Attributed description logics: Reasoning on knowledge graphs. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Arti cial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden. pp. 5309 5313. ijcai.org (2018). https://doi.org/10.24963/ijcai.2018/743, https://doi.org/10. 24963/ijcai.2018/743 14. K hn, T., Leuth user, M., G tz, S., Seidl, C., A mann, U.: A metamodel family for role-based modeling and programming languages. In: Software Language Engineering - 7th International Conference, SLE 2014, V ster s, Sweden, September 15-16, 2014. Proceedings. pp. 141 160 (2014). https://doi.org/10.1007/978-3-31911245-9_8, https://doi.org/10.1007/978-3-319-11245-9_8 15. Sera ni, L., Homola, M.: Contextualized knowledge repositories for the semantic web. J. Web Semant. 12, 64 87 (2012). https://doi.org/10.1016/j.websem.2011.12.003, https://doi.org/10.1016/j. websem.2011.12.003 16. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics.
Journal of the ACM (JACM) 32(3), 733 749 (1985) 17. Tirtarasa, S., Zarrie , B.: Projection in a description logic of context with actions.
In: Calvanese, D., Iocchi, L. (eds.) GCAI 2019. Proceedings of the 5th Global Conference on Arti cial Intelligence. EPiC Series in Computing, vol. 65, pp. 81 93. EasyChair (2019). https://doi.org/https://dx.doi.org/10.29007/s7cm
Proof of Lemma 1 Proof. Let T = (I(i))i 0 be an LM JLOK-LTL-structure such that T j= R and Tp = (w(i))i 0 its propositional abstraction w.r.t. p. We show that T; i j= i Tp; i j= p for every i 0 by induction on the structure of . The base case is wwh(ie)rje= pisianTapx;iiojm=. Tph.en for every i 0, T; i j= i I(i) j= i p 2 wi i Then if is of the form: Proof. =) Assume that there exists a model T = (I(i))i 0 of D w.r.t. rigid names, and Tp = (w(i))i 0 its temporal abstraction. We dene the induced set SX := fw(i) j i 0g which is nite since SX 2P . First we show t-satisability, i.e., there exists M = (wi)i 0 such that M; 0 j= p . We show that in fact Tp; 0 j= p . Due to Lemma 1, we have that Tp; 0 j=SX p. Furthermore, due to
SX the construction we have that every w(i) satises one of disjunctions in SX . Next, we show that SX is c-admissible w.r.t. RM and RO. Since T obeys rigid individual assumptions and respects rigid names, condition 9 - 9 are satised. Due to the construction of SX , we know that for every Xi, there exists w(i), i 0 such that w(i) = fp j p 2 P and I(i) j= g. It is easy to see that I(i) j= CXi .
Assume there exists a set SX 2P , such that p is t-satisable (= swt.rru.tc.tuSrXe aMnd=SX(wi(sj)c)-jad0msiusscihbltehwat.r.Mt. Rj=M apnd. RWOe. dTehneen, there exists an LTLW = fw(i) j i 0g.
Since M is a model of p , then W SX ,ShXence W is c-admissible w.r.t. RM
SX
and RO. Then, there exists nested interpretations I(
Proof of Lemma 5
Proof. =) Assume that SX is c-admissible. Let I(
First, we show that SX is conjointly outer consistent since (I(
Then, we show that SY is conjointly o-admissible. We show that any Yi, 1 i n is o-admissible. Due to the construction, for any Y(i;j), 1 j k there exists c 2 C such that Ic j= for any 2 Y(i;j) and Ic 6j= 0 for any 0 2 E n Y(i;j). Then, it is easy to see that I(i;j) j= CY(i;j) . Finally, it is easy to see that rigidity properties are transferred over from c-admissibility to oadmissibility.
(= Assume that there exists S = f(X1; Y1); : : : ; (Xn; Yn)g such that S is
conjointly outer consistent and SY is conjointly o-admissible. Due to
LwenheimSkolem theorem, we can safely assume that all I(
Proof of Theorem 2 Proof. We begin with showing the hardness for ALCJALCK case. Checking consistency of an ALCJALCK m-KB with rigid concepts is already NExpTime-hard. Thus, we have that checking the consistency of an ALCJALCK-LTL (and more expressive LM JLOK-LTL) t-KB w.r.t. rigid concepts is NExpTime-hard.
For the upper bound, we again have to adjust the previous result to work with our setting. Let D = ( ; RM; RO) be a SHOQJSHOQK-LTL t-KB. We can do the checking t-satisability and c-admissibility as in the case w.r.t. rigid names. This problem has been solved in reasoning over ALC-LTL formula, where we build an appropriate Bchi automaton. The automaton can be checked in exponential time in the size of p, hence in the size of . The full construction can be found in [3]. Thus, we need two exponential time procedures, and an exponential time algorithm for deciding consistency.
We non-deterministically guess the set S which the size is at most exponential in the size of D. We dene ORC := fA1; : : : ; Arg as the set of rigid concept names occurring in and OI be the set of all individuals occurring in . We guess a set Q 2ORC , and a mapping r : OI 7! Q, which both can be done within NExpTime. Then. we dene
BbY(i;j) := (BY(i;j) ^ ^ a2OI
l A2r(a)
A u
l A2ORCnr(a) :A (a); RO) As argued in previous approaches [6,3], we have that SY is conjointly o-admissible i for all (i; j) 2 IndSY , BbY(i;j) has a model that respects (ORC; Q). Since we have that BbY(i;j) is of size polynomial in the size of , and checking the consistency of a SHOQ KB is in ExpTime, then this procedure can be done in exponential time. In overall, we have NExpTime procedure for the case w.r.t. rigid concept only.
E
Proof of Theorem 3 Proof. Notice that checking consistency of ALCJALCK-KB without rigid names is ExpTime-complete. It is easy to see that since any ALCJALCK m-KB is also an ALCJALCK-LTL t-KB, ExpTime-hardness of the satisability problem is carried over.
Next, we prove the upper bound by considering SHOQJSHOQK case. Let D = ( ; RM; RO) be a SHOQJSHOQK-LTL t-KB. Instead of rening each procedure in the case of rigid names, we use a dierent approach for checking csatisability. Instead of breaking down c-admissibility into two procedures, we make use of the fact that SHOQJSHOQK satisability without rigid names is in ExpTime. It is enough for us to have an appropriate SX = fX1; :::; Xng. Instead of guessing SX , we compute a maximal set SbX := fCX j X 2 2P g. We can enumerate all possible subsets of P and for each of them we have an exponential time procedure for checking consistency of CX . This yields an exponential time procedure to get SbX . First, we recall that in other cases we have shown that checking t-satisability is exponential of the size of D. Next, we have to show that SbX is indeed c-admissible. Since each CXi is consistent, there exists a model for each them with countably innite domain. We can assume that they have the same meta-level domain C and object-level domain . Moreover, we assume that M-individual names and O-individual names (for the same c 2 C) are interpreted the same. The conditions (9) and (9) are vacuously satised since there are no rigid names. Thus, we have that SX is c-admissible. In overall, we get an ExpTime procedure for checking consistency of a SHOQJSHOQK-LTL t-KB without rigid names.
F
Proof of Theorem 4 Proof. First, we show the hardness for the case ALCJELK-LTL. Obviously, an ALCJELK m-KB is an ALCJELK-LTL t-KB without temporal operators. Then, NExpTime-hardness for consistency checking of ALCJELK-LTL immediately follows from NExpTime-completeness of the consistency problem in ALCJELK [6].
To show the upper bound, we consider the SHOQJELK case. Let D be an SHOQJELK-LTL t-KB. We guess a set S = f(X1; Y1); : : : ; (Xn; Yn)g that can be done in exponential time. Then, we check t-satisability of p that can be done SX in ExpTime as shown in [3]. Checking whether S is conjointly outer consistent is again in ExpTime since there are exponentially many CfXi to be checked and each of them takes exponential time. In overall, conjointly outer consistency can be tested in time exponentially of the size of D. Finally, notice that BO is a S conjunction of EL-literals. We recall that the satisability of conjunctions of ELliterals can be decided in polynomial time. Since the size of BO is of exponential S size in the size of , checking o-admissibility can be done in exponential time in the size of , and hence B. This yields the NExpTime upperbound for checking satisability in ALCJELK-LTL w.r.t. rigid names.
G
Proof of Theorem 5 Proof. Obviously, the 2-ExpTime-hardness directly follows from 2- ExpTimecompleteness of the consistency problem in ELJALCK. Due to Theorem 1 and the fact that ELJSHOQK-LTL is a fragment of SHOQJSHOQK-LTL, we can use the same procedure to yield the upper bound.
H
Proof of Theorem 6 Proof. Obviously, the NExpTime-hardness for ALCJELK-LTL and ELJALCK-LTL are immediate consequences of NExpTime-hardness of the consistency problem with only rigid concepts in ALCJELK and ELJALCK, respectively. The upper bound are consequences of Theorem 3 since both SHOQJELK-LTL and ELJSHOQK-LTL are fragments of SHOQJSHOQK-LTL.
I
Proof of Theorem 7 Proof. The ExpTime-hardness for ALCJELK-LTL and ELJALCK-LTL follows immediately from the fact that the consistency problem without rigid names in ALCJELK and ELJALCK are ExpTime-hard already. The ExpTime upper bound are consequences of Theorem 2 since both SHOQJELK-LTL and ELJSHOQK-LTL are fragments of SHOQJSHOQK-LTL.
J
Proof of Claim in Section 4.2 Proof. Due to Lemma 2, checking the satisability of an ELJELK m-formula C can be done by checking the existence of a set S := fX1; : : : ; Xkg 2EC such that Cf is consistent w.r.t. S and BXi is consistent for any 1 i k. It is not necessary to construct S explicitly. We recall that Xi represents a combination of referring meta concepts which a domain element can be member of.
We consider again checking the consistency of Cf . Note that the abstraction Cf is a conjunction of EL-literals. As shown in [7,8], checking the satisability of EL-literals can be done in polynomial time by reducing it to the consistency problem of ELO?. We can modify this approach to solve our problem. We recall that the algorithm in [1] compute a mapping S from C to C [ f?g where C is the set that contains top concept, all concepts names used in and all subconcepts of the form fag (nominal) appearing in and a similar mapping R to represent 9r:C. Intuitively, the mapping S represents the subsumption relation in the following sense: D 2 S(C) implies C v D. We can compute this mapping using the algorithm that can be done in polynomial time. Afterwards, we check whether for every C such that there exists fag 2 S(C) for some individual a, BC is consistent where
BC := ^ ^ ^
: E 2S(C) we the combination of referring meta concepts in S(C) are consistent. There is no need to check the one without nominal since such concept can be empty. Note that any BC is a conjunction of EL-literals. Since there are at most polynomial number of C to be checked and each combination can be checked in polynomial time, this yields a polynomial time procedure to check the consistency of conjunction of ELJELK-literals.
K Proof. Case w.r.t. rigid concepts : Since EL-LTL with rigid concept names is NExpTime-hard, we can use the same reduction as in Theorem 8. Furthermore, there are only rigid concept names to be copied to corresponding ELJELK-LTL problem. The upper bound is immediately follows from the case of rigid (concept and role) names.
Case without rigid names : By Lemma 2, checking the satisability of an ELJELK-LTL formula can be done by checking the existence of a set S := fX1; : : : ; Xkg 2EC such that f is consistent w.r.t. SX and SX is c-admissible. We employ the same idea of deciding EL-LTL without rigid names [7,8]. Instead of guessing or building the set SX , we can check the induced Xi of the world wi on the y. As argued in [8], we can exploit the periodic model property of p [16]. With a similar construction, we can build a modied M p for our objective. Instead of checking induced conjunction of EL-literals for each world, we check conjunction of ELJELK-literals. However, by Claim 4.2, this can be done in polynomial time, i.e., the same complexity of checking EL-literals. Thus, we have shown a PSpace algorithm that check satisability of an ELJELK-LTL formula.