=Paper=
{{Paper
|id=Vol-2211/paper-06
|storemode=property
|title=Temporal Description Logics over Finite Traces
|pdfUrl=https://ceur-ws.org/Vol-2211/paper-06.pdf
|volume=Vol-2211
|authors=Alessandro Artale,Andrea Mazzullo,Ana Ozaki
|dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleMO18
}}
==Temporal Description Logics over Finite Traces==
https://ceur-ws.org/Vol-2211/paper-06.pdf
Temporal Description Logics over Finite Traces
Alessandro Artale, Andrea Mazzullo, Ana Ozaki
KRDB Research Centre, Free University of Bozen-Bolzano, Italy
surname@inf.unibz.it
Abstract. Linear temporal logic interpreted over finite traces (LTLf )
has been used as a formalism for temporal specification in automated
planning, process modelling and (runtime) verification. In this paper, we
lift some results from the propositional case to a decidable fragment of
first-order temporal logic obtained by combining the description logic ALC
with LTLf , denoted as TfU ALC. We show that the satisfiability problem
in TfU ALC is ExpSpace-complete, as already known for the infinite trace
case, while it decreases to NExpTime when we consider finite traces
with a fixed number of instants, and even to ExpTime when additionally
restricting to globally interpreted TBoxes. Moreover, we investigate two
model-theoretical notions for TfU ALC: we show that, differently from the
infinite trace case, it enjoys the bounded model property; we also discuss
the notion of insensitivity to infiniteness, providing characterisations and
sufficient conditions to preserve it.
1 Introduction
Since the introduction of linear temporal logic (LTL) by Pnueli [33], several
(propositional and first-order) LTL-based formalisms have been developed for
applications such as automated planning [11, 12, 15–17], process modelling [1,
31] and (runtime) verification of programs [14, 24, 32–35]. Related research in
knowledge representation has focussed on decidable fragments of first-order
LTL [28], many of them obtained by combining LTL with description logics
(DLs), and for this reason called temporal description logics (TDLs) [3, 4, 30, 36].
In this latter setting, the complexity of satisfiability problems can range from
ExpSpace-complete, for the full-fledged combination of the description logic
ALC with LTL [23, 27], down to ExpTime- or PSpace-complete, by restricting
the application of temporal operators [10, 23], or even in NP or NLogSpace, by
weakening both the temporal and the description logic components, for some
TDLs used in temporal conceptual data modelling [5, 6].
Besides the usual LTL semantics defined over the natural numbers, rececently
attention has been devoted to study LTL semantics based on finite traces, which
are temporal structures having only a finite number of time points, with the result-
ing logic sometimes known as linear temporal logic over finite traces (LTLf ) [13,
18–22]. Indeed, for several of the already mentioned applications, the finiteness
of the time dimension is a fairly natural restriction, since the processes involved
are usually required to terminate within a finite amount of time. Motivated by
similar applications, some recent work has considered TDLs in the context of
runtime verification [8] and business process modelling [2]. Nonetheless, these
attempts are still based on the infinite trace semantics for temporal operators
(sometimes allowed only over axioms [8]).
On the way to overcome such limitations, in this work we combine DLs
with LTLf . In particular, we consider the logic TfU ALC defined as the DL ALC
extended with temporal operators on both concepts and formulas (but without
temporalised or rigid roles), and interpreted over models with a finite time
dimension. We show that the complexity of the satisfiability problem in TfU ALC
is ExpSpace-complete, as for the infinite case, and lowers down to NExpTime
if we restrict to traces with a bound k on the number of instants, and even to
ExpTime for a fragment with only globally interpreted TBoxes. We then consider
two model-theoretical notions. Firstly, we show that TfU ALC has the bounded
model property, with the bound being double exponential in the size of the formula.
We then study the notion of a formula being insensitive to infiniteness, considered
in [19, 8, 13, 14] for dealing with the possibility to preserve the satisfiability of
formulas from the finite to the infinite case and thus to reuse TDL algorithms
developed for the infinite case.
This paper is organised as follows. In Section 2, we introduce TU ALC and
we provide the semantics both over infinite and over finite traces. In Section 3
we study the complexity of the satisfiability problem for TfU ALC formulas, while
Section 4 refines these results for traces with fixed k instants. Section 5 investigates
model-theoretical notions of TfU ALC formulas. Finally, in Section 6, we conclude
with some open problems and possible directions for future work.
2 Temporal Description Logics
In the following, we first define the temporal language TU ALC as a temporal
extension of the description logic ALC. The language TU ALC is obtained by
extending ALC with the binary temporal operator until (U). We then define
the semantics based on traces, which are temporal structures having either a
finite or an infinite number of time points. We denote by TfU ALC the language
TU ALC interpreted over finite traces. We further add the upperscript k and write
TkU ALC to indicate that the formulas are interpreted over finite traces with at
most k ∈ N, k > 0, time points.
Syntax. Let NC , NR and NI be countably infinite and pairwise disjoint sets of
concept names, role names, and individual names, respectively. A TU ALC concept
is an expression of the form:
C, D ::= A | ¬C | C u D | ∃R.C | C U D,
where A ∈ NC and R ∈ NR . For instance, the expression A U (B u ∃R.¬A) is a
TU ALC concept. A TU ALC axiom is either a concept inclusion (CI) of the form
C v D, or an assertion of the form A(a) or R(a, b), where C, D are TU ALC
concepts, A ∈ NC , R ∈ NR , and a, b ∈ NI . TU ALC formulas are of the form:
ϕ, ψ ::= α | ¬ϕ | ϕ ∧ ψ | ϕ U ψ,
where α is a TU ALC axiom.
Semantics. A (TDL) interpretation is a structure I = (∆I , (In )n∈I ), where I is
an interval of the form [0, ∞) or [0, l], with l ∈ N, and each In is a classical DL
interpretation with domain ∆I : we have AIn ⊆ ∆I , RIn ⊆ ∆I ×∆I , and aIi =
aIj ∈ ∆I for all a ∈ NI and i, j ∈ N, i.e., the interpretation of individual names
is fixed (in the following denoted as aI ). We refer to a temporal interpretation
I = (∆I , (In )n∈I ) as a finite trace if I = [0, l], and as an infinite trace if
I = [0, ∞). The stipulation that all time points share the same domain ∆I is
called the constant domain assumption (meaning that objects are not created or
destroyed over time), and it is the most general choice in the sense that increasing,
decreasing, and varying domains can all be reduced to it [23]. We now define
the semantics of TU ALC considering I = [0, ∞). The semantics of TfU ALC is
defined in the same way except that I is of the form [0, l], for some l ∈ N. For
a fixed k ∈ N, k > 0, we define the semantics of TkU ALC considering I = [0, l]
with l ≤ k − 1. The interpretation of concepts at instant n of interpretation
I = (∆I , (In )n∈I ) is defined as follows:
(¬C)In = ∆I \ C In , (C u D)In = C In ∩ DIn ,
(∃R.C)In = {d ∈ ∆I | ∃d0 ∈ C In : (d, d0 ) ∈ RIn },
(C U D)In = {d ∈ ∆I | ∃m ∈ I, m > n : d ∈ DIm ∧ ∀i ∈ (n, m) : d ∈ C Ii }.
We say that a concept C is satisfied in I if C I0 6= ∅. Satisfaction of a formula ϕ
in I at time point n ∈ I (written I, n |= ϕ) is inductively defined as follows:
I, n |= C v D iff C In ⊆ DIn , I, n |= ¬φ iff not I, n |= φ,
I, n |= A(a) iff aI ∈ AIn , I, n |= φ ∧ ψ iff I, n |= φ and I, n |= ψ,
I, n |= R(a, b) iff (aI , bI ) ∈ RIn , I, n |= φ U ψ iff ∃m ∈ I, m > n : I, m |= ψ,
and ∀i ∈ (n, m) : I, i |= φ
We say that ϕ is satisfied in I, writing I |= ϕ, if I, 0 |= ϕ. A formula ϕ logically
implies a formula ψ if every I that satisfies ϕ satisfies also ψ, and we write ϕ |= ψ.
Moreover, ϕ is said to be TfU ALC satisfiable (or satisfiable over finite traces) if it
is satisfied in some finite trace. Given a concept C and a formula ϕ, we say that
C is satisfiable over finite traces with respect to ϕ if there is a finite trace I such
that ϕ is satisfied in I and C is satisfied in I, in symbols ϕ 6|= C v ⊥. Concept
satisfiability w.r.t. ϕ can be reduced to formula satisfiability by checking whether
the following formula is satisfiable: ϕ ∧ C(a), for a fresh a ∈ NI .
We will use the following standard equivalences for concepts: ⊥ ≡ A u ¬A,
> ≡ ¬⊥; ∀R.C ≡ ¬∃R.¬C; (C t D) ≡ ¬(¬C u ¬D); #C ≡ #1 C ≡ ⊥ U C;
#n C ≡ # #n−1 C, with n > 1; 3C ≡ > U C; 2C ≡ ¬3¬C. Similar abbreviations
also hold for formulas. We often write F = (∆F , (Fn )n∈[0,l] ) to indicate that a
trace is finite and I = (∆I , (In )n∈I ) when it is infinite.
3 Satisfiability over Finite Traces
In the following we show how to reduce the formula satisfiability problem over
finite traces to the same problem over infinite traces. Similar to the encoding
proposed in [20] for propositional LTL, we introduce a fresh concept name E to
capture the finiteness of the temporal dimension. The fundamental properties
regarding the end of time can be described as follows. (i) There is a least one
instant before the end of time (E is initially false). (ii) The end of time comes
for all objects (E is unavoidable). (iii) The end of time comes at the same time
for every object (E is synchronous). (iv) The end of time never goes away (E is
persistent). We axiomatise the above end of time properties:
ψf1 = > v ¬E, ψf2 = (> v ¬E) U (> v E), ψf3 = 2(E v #E).
Intuitively, ψf1 captures Point (i), ψf2 captures Points (ii), (iii), and ψf3 captures
Point (iv). In the following, we use ψf = ψf1 ∧ ψf2 ∧ ψf3 .
We now show that satisfiability in TfU ALC is ExpSpace-complete. We start
by characterising, in Lemma 1, models satisfying the end of time formula, ψf .
Our characterisation uses the following notion of an extension of a finite trace.
Let F = (∆F , (Fn )n∈[0,l] ) and I = (∆I , (In )n∈[0,∞) ) be, respectively, a finite and
an infinite trace s.t. ∆F = ∆I (with a small abuse, we will write just ∆) and
aF = aI , for all a ∈ NI . We denote by F · I = (∆F·I , (F · In )n∈[0,∞) ) the extension
of F with I defined as the infinite trace with ∆F·I = ∆, aF ·I = aF , for all a ∈ NI ,
and for n ∈ N:
( (
F ·In X Fn , if n ∈ [0, l] F ·In ∅, if n ∈ [0, l]
X = , E = ,
X In−(l+1) , if n ∈ [l + 1, ∞) ∆, if n ∈ [l + 1, ∞)
where X ∈ (NC \ {E}) ∪ NR and E is the concept name encoding the end of time.
Clearly, the interpretation of E characterises the satisfiability of ψf .
Lemma 1. For every infinite trace I, I |= ψf iff I = F · I0 , for some finite trace
F and some infinite trace I0 .
We now introduce a translation ·† of TfU ALC concepts and formulas into
TU ALC concepts and formulas, respectively, such that, together with the end
of time formula, ψf , captures those concepts and formulas satisfiable over finite
traces. More formally, a concept C (formula ϕ) of TfU ALC is satisfiable if and
only if its translation C † (ϕ† ) is satisfiable in a TU ALC model that also satisfies
the formula ψf . Our translation ·† is defined as:
(α)† 7→ α (¬β)† 7→ ¬β †
(C u D)† 7→ C † u D† (φ ∧ ψ)† 7→ φ† ∧ ψ †
(∃R.C)† 7→ ∃R.C † (C v D)† 7→ C † v D†
(C U D)† 7→ C † U (D† u ¬E) (φ U ψ)† 7→ φ† U (ψ † ∧ ¬(> v E))
where α can be an assertion or a concept name A ∈ NC , β can be a concept C or
a formula ϕ, and R ∈ NR . Lemma 2 states the correctness of ·† .
Lemma 2. Let F be a finite trace, and let F · I be an extension of F. Then, for
every TfU ALC formula ϕ, we have: F |= ϕ iff F · I |= ϕ† .
From the previous lemmas, we obtain a reduction of the TfU ALC satisfiability
problem to the corresponding problem for TU ALC.
Theorem 3. Let ϕ be a TfU ALC formula. Then ϕ is satisfiable iff ϕ† ∧ ψf is a
satisfiable TU ALC formula.
Since it is known that the TU ALC formula satisfiability problem is ExpSpace-
complete [23, Theorem 14.15], the above theorem gives us an ExpSpace upper
bound for checking satisfiability in TfU ALC. The lower bound can be proved
using similar ideas as those used to prove hardness of TU ALC. We are now ready
to state the main theorem of this section.
Theorem 4. Satisfiability in TfU ALC is ExpSpace-complete.
4 Traces with at Most k Time Points
In this section we study the satisfiability in TkU ALC, where we restrict the problem
to traces with at most k time points, with k given in binary, as part of the input.
We provide for this case a lower NExpTime complexity result which further
reduces to ExpTime when just global CIs are allowed. To prove our upper bound
for the satisfiability problem in this setting we use quasimodels, which have been
used to prove the satisfiability of various TDLs [5, 9, 23, 25, 26, 36]. In particular,
we show that there is a model with at most k time points iff there is a quasimodel
with a sequence of quasistates of length at most k. Then, our upper bound is
obtained by guessing an exponential size sequence of sets of types which serves
as a certificate for the existence of a quasimodel (and therefore a model) for the
input formula.
Let ϕ be a TkU ALC formula. Assume w.l.o.g. that ϕ does not contain abbre-
viations (i.e., it only contains the logical connectives ¬, u, ∧, the existential
quantifier ∃, and the temporal operator U). Denote by clc (ϕ) and clf (ϕ) the
closures under single negation of the sets of all concepts and formulas occurring
in ϕ, respectively. Also, let ind(ϕ) be the set of individuals occurring in ϕ. A
concept type for ϕ is any subset t of clc (ϕ) ∪ ind(ϕ) such that:
T1 ¬C ∈ t iff C 6∈ t, for all ¬C ∈ clc (ϕ);
T2 C u D ∈ t iff C, D ∈ t, for all C u D ∈ clc (ϕ); and
T3 t contains at most one individual name in ind(ϕ).
Similarly, we define formula types t ⊆ clf (ϕ) for ϕ with the conditions:
T10 ¬φ ∈ t iff φ 6∈ t, for all ¬φ ∈ clf (ϕ); and
T20 φ ∧ ψ ∈ t iff φ, ψ ∈ t, for all φ ∧ ψ ∈ clf (ϕ).
We may omit ‘for ϕ’ if there is no risk of confusion. A concept type describes one
domain element at a single time point, while a formula type expresses constraints
on all domain elements. If a ∈ t ∩ ind(ϕ), then t describes an named element. We
may write ta to indicate this and call it a named type.
The next notion captures how sets of types need to be constrained so that
the DL dimension is respected. We say that a pair of concept types (t, t0 ) is
R-compatible if {¬F | ¬∃R.F ∈ t} ⊆ t0 . A quasistate for ϕ is a set S of concept
or formula types for ϕ such that:
Q1 S contains exactly one formula type tS ;
Q2 S contains exactly one named type ta for each a ∈ ind(ϕ);
Q3 for all C v D ∈ clf (ϕ), we have C v D ∈ tS iff C ∈ t implies D ∈ t for all
concept types t ∈ S;
Q4 for all A(a) ∈ clf (ϕ), we have A(a) ∈ tS iff A ∈ ta
Q5 t ∈ S and ∃R.D ∈ t implies there is t0 ∈ S such that D ∈ t0 and (t, t0 ) is
R-compatible;
Q6 for all R(a, b) ∈ clf (ϕ), we have R(a, b) ∈ tS iff (ta , tb ) is R-compatible.
A (concept/formula) run segment for ϕ is a finite sequence σ = σ(0) . . . σ(n)
composed exclusively of concept or formula types, respectively, such that:
R1 for all a ∈ ind(ϕ) and all i ∈ (0, n], we have a ∈ σ(0) iff a ∈ σ(i);
R2 for all α U β ∈ cl∗ (ϕ) and all i ∈ [0, n], we have α U β ∈ σ(i) iff there is
j ∈ (i, n] such that β ∈ σ(j) and α ∈ σ(m) for all m ∈ (i, j),
where cl∗ is either clc or clf (as appropriate), and R1 does not apply to formula
run segments. Intuitively, a concept run segment describes the temporal dimension
of a single domain element, whereas a formula run segment describes constraints
on the whole DL interpretation.
Finally, a quasimodel for ϕ is a pair (S, R), with S a finite sequence of
quasistates S(0)S(1) . . . S(n) and R a non-empty set of run segments such that:
M1 ϕ ∈ tS where tS is the formula type in S(0);
M2 for every σ ∈ R and every i ∈ [0, n], σ(i) ∈ S(i); and, conversely, for every
t ∈ S(i), there is σ ∈ R with σ(i) = t.
By M2 and the definition of a quasistate for ϕ, R always contains exactly one
formula run segment and one named run segment for each a ∈ ind(ϕ).
Every quasimodel for ϕ describes an interpretation satisfying ϕ and, conversely,
every such interpretation can be abstracted into a quasimodel for ϕ. We formalise
this notion for finite traces with the following lemma.
Lemma 5. There is a finite trace satisfying ϕ with at most k time points iff
there is a quasimodel for ϕ with a sequence of quasistates of length at most k.
We devise a non-deterministic algorithm to check satisfiability of a TkU ALC
formula ϕ in NExpTime. First we compute in exponential time w.r.t. |ϕ| the
sets of all concept and formula types for ϕ, i.e., satisfying conditions T1-T3
and conditions T10 -T20 , respectively. We then guess a sequence S(0), . . . , S(n)
of sets of (concept/formula) types for ϕ of length n ≤ k; and for each type
at position i in this sequence we also guess a sequence of types of length n.
Denote by R the set of such sequences of types. We now check (1) whether
each S(i) satisfies conditions Q1-Q6; (2) whether each sequence in R satisfies
conditions R1-R2 (where R1 only applies for concept run segments); and (3)
whether ϕ is in the formula type in S(0) (condition M1) and each sequence in
R satisfies condition M2. All these conditions can be checked in exponential
time w.r.t. |ϕ| and |k|. The algorithm returns ‘satisfiable’ iff all conditions are
satisfied. Since the conditions exactly match the definition of a quasimodel for
ϕ, their satisfaction implies that (S, R) is a quasimodel for ϕ. Hardness can be
proved by adapting Lemma 6.2 by Baader et al. [10], for ALC-LTL with rigid
concepts. We are now ready to state our main result in this section.
Theorem 6. Satisfiability in TkU ALC is NExpTime-complete.
We end this section considering the satisfiability problem in TkU ALC restricted
to global CIs, defined as the fragment of TkU ALC in which formulas can only be of
the form T ∧ 2(T ) ∧ φ, where T is a conjunction of CIs and φ does not contain
CIs. We write TkU (g)ALC to denote this fragment interpreted over finite traces
with at most k time points. We establish that satisfiability in TkU (g)ALC is in
ExpTime, which is tight since satisfiability in ALC is already ExpTime-hard [7].
Our upper bound is based on type elimination [23, 26, 30].
Theorem 7. Satisfiability in TkU (g)ALC is ExpTime-complete.
We leave satisfiability in TfU ALC restricted to global CIs, analogously defined
as the fragment TfU (g)ALC of TfU ALC with only formulas of the form T ∧2(T )∧φ,
as an open problem. It is known that the complexity of the satisfiability problem
in this fragment over infinite traces is ExpTime-complete [9, 30]1 . Though, the
end of time formula ψf is not in TfU (g)ALC. We cannot use the same strategy
of defining a translation for the semantics based on infinite traces, as we did
in Section 3. The upper bound in [30] is based on type elimination. The main
difficulty of devising a type elimination procedure for TfU (g)ALC is that the
number of time points is not fixed and the argument in [30] showing that there
is a quasimodel iff there is a quasimodel (S, R) such that S(i + i) ⊆ S(i), for
all i ≥ 0, is not applicable to finite traces. A type with a concept equivalent to
¬ # > can only be in the last quasistate of the quasimodel. So it is not clear
whether one can show that if there is a quasimodel then there is a quasimodel
with an exponential sequence of quasistates, as in TkU (g)ALC (Theorem 7).
5 Model-Theoretical Properties
In this section we discuss some model-theoretical properties of TfU ALC. In
particular, we show that formulas of TfU ALC enjoy the bounded model property:
if there is a finite trace (which can be arbitrarily large) satisfying a formula ϕ
1
In [30, Theorem 3] the authors show that satisfiability in LTLALC w.r.t. TBoxes with
constant domains is ExpTime-complete. An argument in [9, Theorem 1] extends this
result to TU ALC formulas, which include assertions.
then there is a finite trace with at most double exponentially many time points
w.r.t. the size of ϕ. Moreover, the bound on the number of time points implies a
bound on the size of the domain, in the DL dimension of the model. Finally, we
discuss insensitivity to infiniteness, a model-theoretical property introduced by
De Giacomo et al. [19]. We lift to TfU ALC a characterisation for propositional
LTL [19]. We then discuss a limitation of this notion and propose a new related
notion of insensitivity to infiniteness.
5.1 Bounded Model Property
We first show that if there is a finite trace which satisfies a TfU ALC formula ϕ
then there is a finite trace with at most k time points, with k double exponentially
large w.r.t. the size of ϕ. This bound is obtained by (1) showing that if there is a
quasimodel for ϕ then there is a quasimodel for ϕ where there is no repetition
of quasistates, except for the last quasistate; and (2) applying Lemma 5 from
Section 4, which correlates the length of a sequence of quasistates with the
number of time points in a finite trace. Since the number of formula types is
f
bounded by tpf (ϕ) = 2|cl (ϕ)| and the number of concept types is bounded by
c c
tpc (ϕ) = |ind(ϕ)| · 2|cl ϕ| , there are at most tpf (ϕ) · 2tp (ϕ) quasistates for ϕ: each
quasistate contains one formula type and a subset of the set of concept types.
The next lemma formalises Point (1) above and can be proved with an argument
similar as that of Lemma 11.27 by Gabbay et al. [23].
Lemma 8. There is a quasimodel for ϕ iff there is a quasimodel for ϕ of the
c
form (S, R) where S is a sequence of length at most tpf (ϕ) · 2tp (ϕ) + 1.
Lemmas 5 and 8 directly imply that TfU ALC enjoys the bounded model
property. We formalise this result with the following theorem.
Theorem 9. Satisfiability of a formula ϕ in TfU ALC implies satisfiability of ϕ
c
in TkU ALC with k bounded by tpf (ϕ) · 2tp (ϕ) .
We now show that if a formula is satisfiable in TkU ALC then there is a model
where the size of the domain is exponential in k. Since satisfiability in TfU ALC
implies satisfiability in TkU ALC for some k > 0, the formula:
#A(a) ∧ 2(A v 2(¬A u ∃R.A))
which only admits models with an infinite domain [30] (recall that in this paper
we use the irreflexive until) is unsatisfiable over finite traces. We formalise the
bounded domain property with the following theorem.
Theorem 10. Satisfiability of a formula ϕ in TkU ALC implies the existence of
a model with domain size bounded by |tpc (ϕ)|k .
5.2 Insensitivity to Infiniteness
In this subsection, we investigate the notion of insensitivity to infiniteness,
introduced by De Giacomo et al. [19] for propositional LTL formulas. This
property is meant to capture those LTLf formulas that can be equivalently
interpreted over infinite traces, provided that, from a certain instant, these traces
satisfy an end event forever, falsifying all other atomic propositions. Firstly, we
lift this notion of insensitivity to our TDL setting, providing a characterisation
analogous to the propositional one [19]. Secondly, we propose a different definition
for insensitivity, closer to other notions from the the literature on runtime
verification [8, 13, 14] and motivated by the following idea: a TfU ALC formula
should be considered as insensitive whenever being satisfiable on a finite trace
implies that it is satisfiable on every infinite trace extending the finite one,
provided that it satisfies the end of time formulas.
We introduce the following definitions. Let Σ be a finite subset of NC ∪ NR .
Assume w.l.o.g. that TfU ALC concepts and formulas we mention in this subsection
have concept and role names in Σ and that Σ contains the end concept E.
Given an infinite trace I, the Σ-reduct of I is the infinite trace I|Σ coinciding
I
with I on Σ and such that X |Σn = ∅, for X 6∈ Σ and n ∈ [0, ∞) [29]. Let
F = (∆ , (Fn )n∈[0,l] ) be a finite trace, and let E = (∆E , (En )n∈[0,∞) ) be the
F
infinite trace such that ∆E = ∆F (for simplicity, we may write just ∆), aE = aF
for all a ∈ NI , and for all A ∈ NC \ {E}, R ∈ NR , AEn = ∅ and REn = ∅ while
E En = ∆, where n ∈ [0, ∞). The extension of F with E (see its definition in
Section “Satisfiability over Finite Traces”), F · E, will be denoted as the end
extension of F. Recalling the definition of ψf , we define, χf = ψf ∧ χf1 ∧ χf2 ,
where l l
χf1 = 2(E v ¬A), χf2 = 2(E v ¬∃R.>).
A∈Σ\{E} R∈Σ
The following two lemmas correspond to Theorems 2 and 3 in [19], respectively.
In particular, Lemma 11 characterises infinite traces of the form F · E, for a finite
trace F.
Lemma 11. For every infinite trace I, I |= χf iff I|Σ = F · E, for some finite
trace F.
Lemma 12, which specialises Lemma 2, shows the equivalence between TfU ALC
satisfiability of a formula ϕ, and satisfiability of its TU ALC translation ϕ† (see
Section ‘Satisfiability over Finite Traces’) on end extensions of finite traces.
Lemma 12. Let F be a finite trace and let ϕ be a TfU ALC formula. We have
that: F |= ϕ iff F · E |= ϕ† .
We are now ready to state the first definition of insensitivity to infiniteness.
Given a TfU ALC formula ϕ, we say that ϕ is insensitive to infiniteness if:
I1 for every finite trace F, F |= ϕ iff F · E |= ϕ.
The next characterisation result, obtained from Lemmas 11 and 12, corresponds
to Theorem 4 in [19].
Theorem 13. A TfU ALC formula ϕ is insensitive to infiniteness I1 iff the
following TU ALC logical implication holds: χf |= ϕ ↔ ϕ† .
Thus, insensitive I1 formulas allow us to blur the distinction between finite and
infinite traces, provided that the infinite ones are as described in Lemma 11.
We now analyse some features of this property. Firstly, notice that TfU ALC for-
mulas without any occurrence of temporal operators, are insensitive I1. Moreover,
given a TfU ALC formula ϕ, this property is preserved under boolean operators
[19, Theorem 5]: if ϕ is insensitive I1, ¬ϕ is insensitive as well, and similarly for
conjunction. It is also possible to capture several standard temporal patterns
derived from the declarative process modelling language declare [1, 19]. For
instance, given a TfU ALC assertion α, we have that 3α is insensitive I1. On
the other hand, a formula of the form 2α (which is not included among the
standard declare patterns) is not I1. However, we have also that 3¬α is not
insensitive I1, while 2¬α is, due to the condition on the interpretation of concept
and role names after the end of time. Therefore, in general, if a TfU ALC formula
ϕ is I1, neither 3ϕ nor 2ϕ are. The same holds for formulas of the form ϕ U ψ.
In order to overcome this temporal asymmetry, and so to obtain a notion
of insensitivity to infiniteness that is preserved by the application of the until
operator, we propose the following definition. Given a TfU ALC formula ϕ, we say
that ϕ is insensitive to infiniteness if:
I2 for every finite trace F and every extension F · I, if F |= ϕ, then F · I |= ϕ.
We will use similar notational conventions as for I1. Notice that this definition
matches the first condition of the impartiality maxim introduced by Bauer et
al. [14]. It is possible to provide an analogous characterisation of insensitive I2
formulas, as we did above for the I1 case.
Theorem 14. A TfU ALC formula ϕ is insensitive to infiniteness I2 iff the
following TU ALC logical implication holds: ψf |= ϕ† → ϕ.
As a consequence of Theorems 13 and 14, checking I1 or I2 can be done
in ExpSpace using the same algorithms developed for TDLs on infinite traces [30].
As before, TfU ALC formulas without any occurrence of temporal operators
are clearly insensitive I2. However, being insensitive I2 is not preserved under
negation. For instance, we have that 3α (with α a TfU ALC assertion) is insensi-
tive I2, but its negation, ¬3α ≡ 2¬α, is not insensitive I2. The theorem below
states that the property of being insensitive I2 is preserved under conjunction
and the until operator. Thus, differently from Theorem 5 in [19], we are now
able to provide a recursive sufficient condition of insensitivity also in the case of
temporal operators.
Theorem 15. Let ϕ and ψ be insensitive I2 TfU ALC formulas. Then ϕ ∧ ψ and
ϕ U ψ are insensitive I2.
In particular, as a consequence of the above statement, both 3ϕ and #ϕ are
insensitive I2, if ϕ is, thus overcoming the temporal asymmetry discussed for
insensitivity I1. On the other hand, formulas of the form 2ϕ should not be
considered, in general, as insensitive I2, since the infinite interpretation of such
formulas, when lifted from a finite trace, depends on how the finite trace is
Formula I1 I2
ϕ (ϕ no temporal operators) Y Y
¬ϕ (ϕ insensitive) Y N
ϕ ∧ ψ (ϕ, ψ insensitive) Y Y
ϕ U ψ (ϕ, ψ insensitive) N Y
2ϕ (ϕ insensitive) N N
Table 1. Comparison between I1 and I2
extended. Notice, however, that concepts and formulas equivalent to (respec-
tively) 2> and 2(> v >), where > and > v > are clearly insensitive I2, are
insensitive I2 as well. Table 1 summarizes differences and similarities between I1
and I2. Finally, notice that both I1 and I2 definitions can be easily adapted
to finite traces with fixed length k > 0. This allows us to compare the cases
of nested next operators. For example, we have that #n ¬A(a) is I1 iff n < k.
On the other hand, #n ¬A(a) turns out to be insensitive I2 for both n < k and
n ≥ k, since in the latter case the I2 condition is vacuously satisfied.
6 Conclusion
We presented TfU ALC, a TDL obtained by combining ALC with LTLf . Firstly,
we have focussed on the complexity of the TfU ALC formula satisfiability problem.
Despite a result of ExpSpace-completeness for the general case, coinciding with
the complexity of the same problem over infinite traces, we have shown how to
improve it to NExpTime, when considering finite traces with a fixed number
k of instants, and even to ExpTime, if additionally we consider the language
restricted with only global CIs, namely TkU (g)ALC. We leave the complexity of
satisfiability in TfU (g)ALC as an open problem. In order to further refine these
results, we plan to consider temporal DL-Lite logics interpreted over finite traces.
Concerning the section on model-theoretical properties, we have shown that
the logic TfU ALC has the bounded model property. Moreover, we have studied
the notion of insensitivity to infiniteness, both as found in the literature (I1),
and as re-defined here (I2). We have shown their characterisations, and sufficient
conditions to preserve I2. As future work, we plan to refine our results, so to cover
the case of CIs with temporal operators applied on concepts, that are nonetheless
insensitive I2 (such as > v 3A). A characterisation of insensitive CIs could in
turn be based on a suitably defined notion of insensitivity for concepts. We leave
this task for future work, together with an in depth discussion of the interaction
between temporal operators (including additional ones, as weak next , release
R, or weak until W) and insensitivity.
References
1. van der Aalst, W.M.P., Pesic, M.: Decserflow: Towards a truly declarative service
flow language. In: Web Services and Formal Methods, Third International Workshop,
WS-FM 2006 Vienna, Austria, September 8-9, 2006, Proceedings. pp. 1–23 (2006)
2. van der Aalst, W., Artale, A., Montali, M., Tritini, S.: Object-centric behavioral
constraints: Integrating data and declarative process modelling. In: CEUR Workshop
Proceedings. vol. 1879 (2017)
3. Artale, A., Franconi, E.: A survey of temporal extensions of description logics.
Annals of Mathematics and Artificial Intelligence 30(1-4), 171–210 (2000)
4. Artale, A., Franconi, E.: Temporal description logics. In: Handbook of Temporal
Reasoning in Artificial Intelligence, pp. 375–388. Elsevier (2005)
5. Artale, A., Kontchakov, R., Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal-
ising tractable description logics. In: 14th International Symposium on Temporal
Representation and Reasoning (TIME 2007), Alicante, Spain, 28-30 June 2007. pp.
11–22 (2007)
6. Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: A cookbook for
temporal conceptual data modelling with description logics. ACM Transactions on
Computational Logic (TOCL) 15(3), 25 (2014)
7. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applications.
Cambridge University Press (2003)
8. Baader, F., Bauer, A., Lippmann, M.: Runtime verification using a temporal
description logic. In: Frontiers of Combining Systems, 7th International Symposium,
FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings. pp. 149–164 (2009)
9. Baader, F., Borgwardt, S., Koopmann, P., Ozaki, A., Thost, V.: Metric temporal
description logics with interval-rigid names. In: Frontiers of Combining Systems
- 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29,
2017, Proceedings. pp. 60–76 (2017)
10. Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. ACM Trans.
Comput. Log. 13(3), 21:1–21:32 (2012)
11. Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge
for planning. Artif. Intell. 116(1-2), 123–191 (2000)
12. Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals
using heuristic search. In: Proceedings, The Twenty-First National Conference
on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial
Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA. pp. 788–795
(2006)
13. Bauer, A., Haslum, P.: LTL goal specifications revisited. In: Proc. of the 19th
European Conference on Artificial Intelligence, ECAI’10. pp. 881–886 (2010)
14. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime
verification. J. Log. Comput. 20(3), 651–674 (2010)
15. Calvanese, D., De Giacomo, G., Vardi, M.Y.: Reasoning about actions and planning
in LTL action theories. In: Proc. of the 8th International Conference on Principles
and Knowledge Representation and Reasoning (KR-02). pp. 593–602 (2002)
16. Camacho, A., Triantafillou, E., Muise, C.J., Baier, J.A., McIlraith, S.A.: Non-
deterministic planning with temporally extended goals: LTL over finite and infinite
traces. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence,
February 4-9, 2017, San Francisco, California, USA. pp. 3716–3724 (2017)
17. Cerrito, S., Mayer, M.C.: Bounded model search in linear temporal logic and its
application to planning. In: Automated Reasoning with Analytic Tableaux and
Related Methods, International Conference, TABLEAUX ’98, Oisterwijk, The
Netherlands, Proceedings, May 5-8, 1998. pp. 124–140 (1998)
18. Cerrito, S., Mayer, M.C., Praud, S.: First order linear temporal logic over finite time
structures. In: Logic Programming and Automated Reasoning, 6th International
Conference, LPAR’99, Tbilisi, Georgia, Proceedings, September 6-10, 1999. pp.
62–76 (1999)
19. De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces:
Insensitivity to infiniteness. In: Proceedings of the Twenty-Eighth AAAI Conference
on Artificial Intelligence, Québec City, Québec, Canada, July 27 -31, 2014. pp.
1027–1033 (2014)
20. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on
finite traces. In: IJCAI, Proceedings of the 23rd International Joint Conference on
Artificial Intelligence. pp. 854–860 (2013)
21. De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In:
Proceedings of the Twenty-Fourth International Joint Conference on Artificial
Intelligence, IJCAI. pp. 1558–1564 (2015)
22. Fionda, V., Greco, G.: The complexity of LTL on finite traces:
Hard and easy fragments. In: Proc. of the Thirtieth AAAI Con-
ference on Artificial Intelligence. pp. 971–977. AAAI Press (2016),
http://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12250
23. Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional
Modal Logics: Theory and Applications, Studies in Logic and The Foundations of
Mathematics, vol. 148. North Holland Publishing Company (2003)
24. Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal prop-
erties on running programs. In: 16th IEEE International Conference on Automated
Software Engineering (ASE 2001), 26-29 November 2001, Coronado Island, San
Diego, CA, USA. pp. 412–416 (2001)
25. Gutiérrez-Basulto, V., Jung, J.C., Lutz, C.: Complexity of branching temporal
description logics. In: Proc. ECAI (2012)
26. Gutiérrez-Basulto, V., Jung, J.C., Ozaki, A.: On metric temporal description logics.
In: ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2
September 2016, The Hague, The Netherlands - Including Prestigious Applications
of Artificial Intelligence (PAIS 2016). pp. 837–845 (2016)
27. Hodkinson, I.M., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: On
the computational complexity of decidable fragments of first-order linear temporal
logics. In: 10th International Symposium on Temporal Representation and Reasoning
/ 4th International Conference on Temporal Logic (TIME-ICTL 2003), Cairns,
Queensland, Australia, 8-10 July 2003. pp. 91–98 (2003)
28. Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: Decidable fragment of first-order
temporal logics. Ann. Pure Appl. Logic 106(1-3), 85–134 (2000)
29. Konev, B., Lutz, C., Wolter, F., Zakharyaschev, M.: Conservative rewritability of
description logic tboxes. In: Proceedings of the Twenty-Fifth International Joint
Conference on Artificial Intelligence, IJCAI. pp. 1153–1159 (2016)
30. Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey. In:
15th International Symposium on Temporal Representation and Reasoning, TIME
2008, Université du Québec à Montréal, Canada, 16-18 June 2008. pp. 3–14 (2008)
31. Maggi, F.M., Montali, M., Westergaard, M., van der Aalst, W.M.P.: Monitoring
business constraints with linear temporal logic: An approach based on colored
automata. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) Proc. of Business
Process Management (BPM’11). pp. 132–147. Springer (2011)
32. Manna, Z., Pnueli, A.: Temporal verification of reactive systems - safety. Springer
(1995)
33. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foun-
dations of Computer Science, Providence, Rhode Island, USA, 31 October - 1
November 1977. pp. 46–57 (1977)
34. Reger, G., Rydeheard, D.E.: From first-order temporal logic to parametric trace
slicing. In: Runtime Verification - 6th International Conference, RV 2015 Vienna,
Austria, September 22-25, 2015. Proceedings. pp. 216–232 (2015)
35. Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Proc.
of Logics for Concurrency - Structure versus Automata, 8th Banff Higher Order
Workshop. pp. 238–266 (1995)
36. Wolter, F., Zakharyaschev, M.: Temporalizing description logics. In: Proceedings of
FroCoS’98. pp. 104–109 (1998)