# Optimal Alignment of Temporal Knowledge Bases

Oliver Fernández Gil Corresponding Author. Email: oliver.fernandez@tu-
dresden.de Fabio Patrizi Email<EMAIL_ADDRESS>Giuseppe Perelli
Email<EMAIL_ADDRESS>Anni-Yasmin Turhan Email: anni-yasmin.turhan@tu-
dresden.de Theoretical Computer Science, TU Dresden, Germany  Sapienza
University of Rome  Center for Scalable Data Analytics and Artificial
Intelligence (ScaDS.AI) Dresden/Leipzig, Germany

###### Abstract

Answering temporal CQs over temporalized Description Logic knowledge bases
(TKB) is a main technique to realize ontology-based situation recognition. In
case the collected data in such a knowledge base is inaccurate, important
query answers can be missed. In this paper we introduce the TKB Alignment
problem, which computes a variant of the TKB that minimally changes the TKB,
but entails the given temporal CQ and is in that sense (cost-)optimal. We
investigate this problem for $\mathcal{ALC}$ TKBs and conjunctive queries with
LTL operators and devise a solution technique to compute (cost-optimal)
alignments of TKBs that extends techniques for the alignment problem for
propositional LTL over finite traces.

1742

##  1 Introduction

Observing complex systems over time and drawing conclusions about their
behavior is a core task for many AI systems. In particular, adaptive systems
have to recognize situations in which an adaptation is useful. A well-
investigated approach to do this is ontology-based situation recognition [3,
1, 23]. This approach is usually realized by modeling the observed system by a
temporal knowledge base (TKB), where the data from the observed system is
collected over time and stored in a sequence of ABoxes and a TBox that models
important notions from the application domain. The situation to be recognized
by the system is then modeled by a temporal query that will be answered over
the sequence of ABoxes and the TBox. The situation recognition is then to
detect predefined situations that are formalized as temporal (conjunctive)
queries over the observed and enriched ABox sequence. As in classical
ontology-mediated query answering [8], the TBox enriches the data in the ABox
sequence as it restricts its interpretation and allows for more conclusions.
The semantics of TKBs is given by an infinite sequence of first-order
interpretations. TKBs can be queried by temporal conjunctive queries (TCQs),
which combine ltl with conjunctive queries. Methods for answering temporal
queries over TKBs and testing entailment of Boolean TCQs have been intensively
investigated ([4, 9, 1]).

Now, in many applications, the data is collected from several sources and need
not always be accurate. Consider the medical domain, where deviations of
classical symptoms are frequent for certain patient groups or where
examination methods such as blood test results can be inaccurate or
discretized unsuitably. Thus the query need not return the expected answer,
although the patient or, in the general case, the observed system is in a
critical state that requires adaptation. The problem is to find a version of
the TKB that admits to detect “near misses”.

There are mainly two approaches developed to address the problem of errors or
inaccuracies in DL knowledge bases. In case of inconsistent TKBs, ontology
repairs restore consistent versions by deleting statements from the ABoxes
[10, 7]. In case that information is missing in the ABoxes for the query to
return answers, ABox abduction, i.e., adding new statements to the ABoxes has
been investigated—mostly in the atemporal setting [14, 17].

In this paper, we investigate the new task of TKB Alignment, i.e., to modify
the sequence of ABoxes by deletions or additions of statements so as to yield
answers for the TCQ. Surprisingly, this problem has not been addressed in the
literature yet. The goal of this paper is to develop an approach to solve
instances of this new problem.

The well-known problem of Trace Alignment realizes a very similar task to TKB
alignment: for a finite trace of observations and a property specification
expressed in Linear Temporal Logic (ltl), a minimal modification of the trace
is produced that satisfies the specification. This task has been extensively
studied by the Business Process (BP) and AI communities, leading to effective
solutions and implemented tools; see, e.g., [11, 13, 12]. In all these
settings, the observations recorded in a trace are propositional, i.e., each
time point of the trace represents one of finitely many possible observables,
modeled as propositions.

In this paper, we address the problem of TKB Alignment as a Trace Alignment
problem in a much richer setting, where observables are described by DL
concepts and roles, and properties are specified by a temporalized query using
DL atoms. Furthermore, the open world semantics of DLs is adopted, since
entailment is considered instead of satisfaction as in classical propositional
trace alignment.

We investigate the following setting for TKB alignment: a TCQ using (future)
ltl operators and a TKB written in the DL $\mathcal{ALC}$, together with a
cost measure for edit operations on the ABox sequence. Solving TKB alignment
is then to compute an ABox sequence which, together with the TBox, entails the
Boolean TCQ, while guaranteeing cost-optimality of the modification.
Intuitively, the cost-optimal version of the TKB states which minimal changes
of the TKB would result in answers to the TCQ.

The technique we develop builds on an approach for deciding temporal query
entailment over TKBs by [4] and one for solving ltl Trace Alignment for finite
traces by [11], and extends them non-trivially. Our technique extends the
former approach from verification to synthesis and the latter from the
propositional to the DL setting, from propositional traces to TKBs, and from
finite to infinite traces. This ultimately results in an effective solution
approach which can assess the deviation of irregular observations wrt standard
ones and define corrective actions to recover a standard observation.

The detailed proofs for all results are supplied in the Appendix.

##  2 Preliminaries

In this section we recap basic notions on description logics, LTL, and trace
alignment.

###  2.1 Description Logic Knowledge Bases

Description Logics (DLs) are a family of formal languages for representing
knowledge and reasoning about it. In this work, we focus on the DL
$\mathcal{ALC}$ ([22]).

We fix three countably infinite sets of names: $\mathsf{N_{C}}$ for concepts,
$\mathsf{N_{R}}$ for roles and $\mathsf{N_{I}}$ for individuals. _Concepts_ in
$\mathcal{ALC}$ are defined inductively as follows:

$C:=A\mid\neg C\mid C\sqcup C\mid\exists r.C\mid\top,$

where $A\in\mathsf{N_{C}}$, $r\in\mathsf{N_{R}}$, $\top$ is the _top-concept_
and $\bot$ the _bottom-concept_. We use the following standard abbreviations:
$C\sqcap D$ for $\neg(\neg C\sqcup\neg D)$, $\forall r.C$ for $\neg(\exists
r.\neg C)$, and $\bot$ for $\neg\top$.

DL concepts are interpreted over (first-order, FO) interpretations. An
_interpretation_ $\mathcal{I}=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$
consists of a domain $\Delta^{\mathcal{I}}$ and a function
$\cdot^{\mathcal{I}}$ mapping each concept name $A$ to a set
$A^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}$, each role name $r$ to a binary
relation
$r^{\mathcal{I}}\subseteq\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$, and
each individual name $a$ to an element
$a^{\mathcal{I}}\in\Delta^{\mathcal{I}}$. Based on this, the semantics of
(complex) concepts is defined as follows: $(\neg
C)^{\mathcal{I}}=\Delta^{\mathcal{I}}\setminus C^{\mathcal{I}}$, $(\exists
r.C)^{\mathcal{I}}=\\{d\in\Delta^{\mathcal{I}}\mid\exists e.((d,e)\in
r^{\mathcal{I}}\wedge e\in C^{\mathcal{I}})\\}$, $(C\sqcup
D)^{\mathcal{I}}=C^{\mathcal{I}}\cup D^{\mathcal{I}}$, and
$\top^{\mathcal{I}}=\Delta^{\mathcal{I}}$.

_General concept inclusions_ (GCIs) are statements of the form $C\sqsubseteq
D$, expressing inclusion relationships between concepts. A _TBox_ (denoted
$\mathcal{T}$) is a finite set of GCIs. A _model_ of a TBox $\mathcal{T}$ is
an interpretation $\mathcal{I}$ that satisfies all GCIs in $\mathcal{T}$,
i.e., for all $C\sqsubseteq D\in\mathcal{T}$, it holds that
$C^{\mathcal{I}}\subseteq D^{\mathcal{I}}$. A TBox is _satisfiable_ if it has
a model.

Statements $A(a)$ and $r(a,b)$ are called, respectively, _concept assertion_
and _role assertion_ , where $a,b\in\mathsf{N_{I}}$, $A\in\mathsf{N_{C}}$ and
$r\in\mathsf{N_{R}}$. An interpretation $\mathcal{I}$ satisfies $A(a)$ if
$a^{\mathcal{I}}\in A^{\mathcal{I}}$, and satisfies $r(a,b)$ if
$(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}$. An _ABox_
$\mathcal{A}$ is a finite set of (concept or role) assertions. An
interpretation $\mathcal{I}$ is a _model_ of an ABox $\mathcal{A}$, if
$\mathcal{I}$ satisfies all assertions in $\mathcal{A}$.

A _DL knowledge base_ (KB) is a pair $\mathcal{K}=(\mathcal{T},\mathcal{A})$,
with $\mathcal{T}$ a TBox and $\mathcal{A}$ an ABox. An interpretation
$\mathcal{I}$ is a _model_ of $\mathcal{K}=(\mathcal{T},\mathcal{A})$, written
$\mathcal{I}\models\mathcal{K}$, if $\mathcal{I}$ is a model of $\mathcal{T}$
and $\mathcal{A}$. A KB is _consistent_ if it has a model.

###  2.2 Conjunctive Queries

Prominent reasoning problems investigated in the last decade concern
_conjunctive queries_. We briefly recap related definitions and results.

######  Definition 1 (Conjunctive query)

Let $\mathsf{N_{V}}$ be a set of variables. A _conjunctive query (CQ)_ is an
expression of the form $\phi=\exists\bar{y}.\psi$, where $\bar{y}$ is a tuple
of variables from $\mathsf{N_{V}}$ and $\psi$ is a finite conjunction of
_atoms_ of the form: $A(z)$, for $A\in\mathsf{N_{C}}$ and
$z\in\mathsf{N_{V}}\cup\mathsf{N_{I}}$, or $r(z,z^{\prime})$, for
$r\in\mathsf{N_{R}}$ and $z,z^{\prime}\in\mathsf{N_{V}}\cup\mathsf{N_{I}}$.

By cq we denote the set of all CQs (over $\mathsf{N_{C}}$, $\mathsf{N_{R}}$,
$\mathsf{N_{I}}$, $\mathsf{N_{V}}$). We write $A(z)\in\phi$ to state that atom
$A(z)$ occurs in $\phi$, and likewise for $r(z,z^{\prime})$.

In this work, we combine CQs using Boolean connectives.

######  Definition 2 (Boolean combination of CQs)

A formula $\phi$ is a _Boolean combination of CQs_ iff:

$\phi:=\phi^{\prime}\mid\neg\phi\mid\phi\lor\phi,\text{ where
}\phi^{\prime}\in\textsc{cq}.$

As standard, $\phi_{1}\land\phi_{2}$ abbreviates
$\lnot(\neg\phi_{1}\lor\neg\phi_{2})$. Given a Boolean combination of CQs
$\phi$, we denote by $\mathsf{Var}(\phi)$, $\mathsf{FVar}(\phi)$ and
$\mathsf{Ind}(\phi)$ the set of variables, free variables and individual names
occurring in $\phi$, respectively. A query with no free variables is called
_Boolean_ , whereas a query with $\mathsf{Ind}(\phi)=\emptyset$ is called
_pure_. bcq denotes the set of _Boolean CQs_ (BCQs),
$\mathcal{B}(\textsc{cq})$ the set of Boolean combinations of CQs, and
$\mathcal{B}(\textsc{bcq})$ the set of Boolean combinations of BCQs.

The semantics of BCQs is defined in terms of a satisfaction relation between
interpretations and BCQs.

######  Definition 3 (Semantics of BCQs)

An interpretation $\mathcal{I}$ is _a model_ of (or _satisfies_) a BCQ $\phi$,
written $\mathcal{I}\models\phi$, iff there exists a mapping
$h:\mathsf{Var}(\phi)\cup\mathsf{Ind}(\phi)\rightarrow\Delta^{\mathcal{I}}$,
called a _match_ , s.t.:

  * •

$h(a)=a^{\mathcal{I}}$ for all $a\in\mathsf{Ind}(\phi)$;

  * •

$h(z)\in A^{\mathcal{I}}$ for all $A(z)\in\phi$; and

  * •

$(h(z),h(z^{\prime}))\in r^{\mathcal{I}}$ for all $r(z,z^{\prime})\in\phi$.

These notions straightforwardly extend to $\mathcal{B}(\textsc{bcq})$.

######  Definition 4 (Semantics of Boolean combinations of BCQs)

An interpretation $\mathcal{I}$ is _a model_ of (or _satisfies_) a query
$\phi\in\mathcal{B}(\textsc{bcq})$, written $\mathcal{I}\models\phi$, iff:

  * •

$\phi\in\textsc{bcq}$ and $\mathcal{I}\models\phi$; or

  * •

$\phi=\lnot\phi_{1}$ and $\mathcal{I}\not\models\phi_{1}$; or

  * •

$\phi=\phi_{1}\lor\phi_{2}$ and $\mathcal{I}\models\phi_{1}$ or
$\mathcal{I}\models\phi_{2}$.

A query $\phi\in\mathcal{B}(\textsc{bcq})$ is _satisfiable_ wrt a KB
$\mathcal{K}$, if $\mathcal{I}\models\phi$ for some model $\mathcal{I}$ of
$\mathcal{K}$. A knowledge base $\mathcal{K}$ _entails_ a query $\phi$
(written $\mathcal{K}\models\phi$), if $\mathcal{I}\models\phi$ for all models
$\mathcal{I}$ of $\mathcal{K}$.

In case of non-Boolean queries, one is interested in computing the certain
answers. More precisely, given a KB $\mathcal{K}=(\mathcal{T},\mathcal{A})$
and $\phi\in\mathcal{B}(\textsc{cq})$ with free variables
$\bar{x}=(x_{1},\ldots,x_{k})$, a tuple $\bar{a}=(a_{1},\ldots,a_{k})$ of
individuals in $\mathsf{N_{I}}$ is a _certain answer of $\phi$ wrt
$\mathcal{K}$_ if $\mathcal{K}\models\phi[\bar{a}]$, where $\phi[\bar{a}]$ is
the Boolean query obtained from $\phi$ by replacing each occurrence of $x_{i}$
by $a_{i}$ ($1\leq i\leq k$). We denote by $cert_{\mathcal{K}}(\phi)$ the set
of certain answers of $\phi$ wrt $\mathcal{K}$. If $\phi$ is a Boolean query
and $\mathcal{K}\models\phi$, then $cert_{\mathcal{K}}(\phi)=\\{()\\}$.

The entailment problem for BCQs wrt $\mathcal{ALC}$ knowledge bases is
ExpTime-complete ([19, 20]). It was shown in [4] for
$\mathcal{B}(\textsc{bcq})$ that satisfiability of a conjunction of CQ-
literals (i.e. either a Boolean CQ or a negated Boolean CQ) wrt
$\mathcal{ALC}$ knowledge bases is an ExpTime-complete problem. An easy
consequence of this (and of $\mathcal{B}(\textsc{bcq})$ being _closed under
negation_) is that satisfiability and entailment of arbitrary Boolean
combinations of BCQs w.r.t. $\mathcal{ALC}$ knowledge bases are also ExpTime-
complete problems.

###  2.3 Propositional Linear Temporal Logic

The kind of properties we focus on in this paper concerns the evolution of a
knowledge base over time. To express relevant properties, we need a temporal
logic. We review the basics on propositional Linear Temporal Logic (ltl),
which will be later lifted to CQs and used on to address TKB Alignment.

The language of Linear Temporal Logic (ltl) formulas $\varphi$ is defined over
a finite set of propositions prop, as follows:

$\varphi:=p\mid\neg\varphi\mid\varphi\vee\varphi\mid\operatorname{\mathbf{X}}\varphi\mid\varphi\operatorname{\mathbf{U}}\varphi\text{,~{}
with $p\in\textsc{prop}$.}$

The set
${{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\varphi)$
denotes the finite set of propositions occurring in $\varphi$. ltl formulas
are interpreted over infinite words, also called  _(propositional) traces_ ,
$w=w_{0}w_{1}\cdots\in{(2^{\textsc{prop}})}^{\omega}$.

######  Definition 5 (ltl semantics)

Given a formula $\varphi\in\textsc{ltl}$, a trace $w=w_{0}w_{1}\cdots$, and an
index $i$, we inductively define when $w,i$ _satisfy_ $\varphi$, denoted
$w,i\models\varphi$, as follows:

  * •

$w,i\models p$, if $p\in w_{i}$;

  * •

$w,i\models\neg\varphi$, if $w,i\not\models\varphi$;

  * •

$w,i\models\varphi_{1}\vee\varphi_{2}$, if $w,i\models\varphi_{1}$ or
$w,i\models\varphi_{2}$;

  * •

$w,i\models\operatorname{\mathbf{X}}\varphi$, if $w,i+1\models\varphi$;

  * •

$w,i\models\varphi_{1}\operatorname{\mathbf{U}}\varphi_{2}$ if there exists
$j\geq i$ s.t. $w,j\models\varphi_{2}$ and $w,k\models\varphi_{1}$, for
$k=i,\ldots,j-1$.

We say that $w$ _satisfies_ $\varphi\in\textsc{ltl}$, written
$w\models\varphi$, iff $w,0\models\varphi$.

We denote the set of traces satisfying $\varphi$ as
$\mathcal{L}(\varphi)=\\{w\in{(2^{\textsc{prop}})}^{\omega}\mid
w\models\varphi\\}$. It is well-known that for every $\varphi\in\textsc{ltl}$
there exists a _deterministic parity automaton_ (DPA) $P_{\varphi}$ accepting
exactly $\mathcal{L}(\varphi)$.

A _deterministic parity automaton_ is a tuple
$P=(Al,Q,\delta,q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$,
where: $Al$ is the finite input alphabet, $Q$ is the finite set of states,
$\delta:Q\times Al\rightarrow Q$ is the transition function, $q_{0}\in Q$ is
the initial state, and
${{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}:Q\rightarrow
Col$ is a _coloring function_ , mapping the states of $P$ into a finite set of
_colors_ $Col\subset\mathbb{N}_{0}$. DPAs are similar to deterministic finite-
state automata (DFA), but accept _infinite_ traces and thus have a different
accepting condition.

For a DPA $P$, a _finite run from state $q\in Q$_ is a sequence
$\rho=q\stackrel{{\scriptstyle
w_{0}}}{{\rightarrow}}q_{1}\stackrel{{\scriptstyle
w_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle
w_{n-1}}}{{\rightarrow}}q_{n}$ s.t. $\delta(q,w_{0})=q_{1}$ and
$\delta(q_{i},w_{i})=q_{i+1}$, for $0<i<n$. We define _infinite_ runs
analogously, for $n=\infty$. Unless stated otherwise, runs are always infinite
and start in the initial state $q_{0}$ of $P$.

Given a run $\rho$ of $P$, let
${{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}_{Q}(\rho,P)$
be the set of states occurring infinitely many times in $\rho$. Obviously,
${{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}_{Q}(\rho,P)\neq\emptyset$
iff $\rho$ is infinite. Let
${{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}(\rho,P)=\\{{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}(q)\in
Col\mid
q\in{{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}_{Q}(\rho,P)\\}$
be the set of colors “visited” infinitely many times by $\rho$. A run $\rho$
from a state $q\in Q$ is _accepting_ iff
$\min\\{{{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}(\rho,P)\\}$
is even. When this is the case, $q\in Q$ is an _accepting_ state. By
${{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P)$,
we denote the set of all accepting states of $P$ and call
${{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P)$
the _accepting_ set of $P$.

######  Lemma 1 ([16])

The accepting set
${{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P)$
of a DPA
$P=(Al,Q,\delta,q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$
can be computed in time $(|Q|+|\delta|)\log|Col|$, where
$|\delta|=|\\{(q,q^{\prime})\in Q\times Q\text{
s.t.~{}}q^{\prime}=\delta(a,q)\text{, for some }a\\}|$.

For a DPA
$P=(Al,Q,\delta,q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$
and a trace $w=w_{0}w_{1}\cdots$, the (unique) run _induced_ by $w$ is the run
$\rho=q_{0}\stackrel{{\scriptstyle
w_{0}}}{{\rightarrow}}q_{1}\stackrel{{\scriptstyle
w_{1}}}{{\rightarrow}}\cdots$. A trace $w$ is _accepted_ by $P$ iff the run
$\rho$ induced by $w$ is accepting. By $\mathcal{L}(P)$ we denote the
_language_ of $P$, i.e., the set of all traces accepted by $P$.

######  Theorem 2.1 ([24, 21]).

For every $\varphi\in\textsc{ltl}$ there exists a DPA
$P_{\varphi}=(2,Q,\delta,q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$
s.t. $\mathcal{L}(P_{\varphi})=\mathcal{L}(\varphi)$. $P_{\varphi}$ can be
computed in doubly exponential time and has doubly exponential size wrt
$\varphi$.

###  2.4 Entailment of Temporal Conjunctive Queries

TKB Alignment is closely related to checking _temporal query entailment_
(TQE), studied in [4]. We briefly recall the main definitions and results from
that work, possibly adapted to our setting.

######  Definition 2.2 (Temporal Knowledge Base (TKB)).

A _temporal knowledge base_ (TKB) is a pair $\Gamma=(\mathcal{T},\Lambda)$,
where $\mathcal{T}$ is a TBox and
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$ is a finite sequence of
ABoxes.

A _FO trace_ is an infinite sequence
$\mathfrak{I}=\mathcal{I}_{0}\mathcal{I}_{1}\cdots$ of interpretations
$\mathcal{I}_{i}=(\Delta,.^{\mathcal{I}_{i}})$ over a fixed domain $\Delta$.

######  Definition 2.3 (Model of a TKB).

Given a TKB $\Gamma=(\mathcal{T},\mathcal{A}_{0}\cdots\mathcal{A}_{\ell})$, a
FO trace $\mathfrak{I}=\mathcal{I}_{0}\mathcal{I}_{1}\cdots$ is a _model_ of
$\Gamma$, iff: $\mathcal{I}_{i}\models\mathcal{A}_{i}$, for $0\leq i\leq\ell$;
and $\mathcal{I}_{i}\models\mathcal{T}$ for all $i\geq 0$. If these conditions
hold, $\mathfrak{I}$ _satisfies_ $\Gamma$, written
$\mathfrak{I}\models\Gamma$.

Next, we introduce the language tcq of _(simple) temporal conjunctive queries_
(TCQ), which essentially lifts propositions in ltl to BCQs. tcq formulas are
obtained as in ltl, by replacing with a finite set
$\textsc{pbcq}\subset\textsc{bcq}$:

$\varphi:=\phi\mid\neg\varphi\mid\varphi\vee\varphi\mid\operatorname{\mathbf{X}}\varphi\mid\varphi\operatorname{\mathbf{U}}\varphi\text{,
~{}with $\phi\in\textsc{pbcq}$.}$

tcq formulas are evaluated over FO traces.

######  Definition 2.4 (tcq Semantics).

Given a formula $\varphi\in\textsc{tcq}$, an infinite trace
$\mathfrak{I}=\mathcal{I}_{0}\mathcal{I}_{1}\cdots$, and an index $i$, we
inductively define when $\mathfrak{I}$ _satisfies_ $\varphi$ from $i$, denoted
$\mathfrak{I},i\models\varphi$, as follows:

  * •

$\mathfrak{I},i\models\phi$, if $\mathcal{I}_{i}\models\phi$, for
$\phi\in\textsc{pbcq}$;

  * •

$\mathfrak{I},i\models\neg\varphi$ if $\mathfrak{I},i\not\models\varphi$;

  * •

$\mathfrak{I},i\models\varphi_{1}\vee\varphi_{2}$, if
$\mathfrak{I},i\models\varphi_{1}$ or $\mathfrak{I},i\models\varphi_{2}$;

  * •

$\mathfrak{I},i\models\operatorname{\mathbf{X}}\varphi$, if
$\mathfrak{I},i+1\models\varphi$;

  * •

$\mathfrak{I},i\models\varphi_{1}\operatorname{\mathbf{U}}\varphi_{2}$ if
there exists $j\geq i$ s.t. $\mathfrak{I},j\models\varphi_{2}$ and
$\mathfrak{I},k\models\varphi_{1}$, for $k=i,\ldots,j-1$.

We say that $\mathfrak{I}$ _satisfies_ $\varphi$, written
$\mathfrak{I}\models\varphi$, if $\mathfrak{I},0\models\varphi$.

The semantics of temporal operators for TCQs is analogous to that of ltl (see
Def. 5); however, for TCQs the base case accounts for the satisfaction of BCQs
by the FO interpretations occurring in the trace.

We observe that the variant of TCQs we use here differs from that introduced
in [4], in that we disallow _past_ operators ([15]). However, such restriction
comes without loss of generality. This is because the two semantic variations
have essentially the same expressive power, as future operators have the
ability to mimic the past ones ([25, 18]).

The notion of _temporal conjunctive query entailment_ used here is the same as
that in [4], once past operators are disallowed in TCQs.

######  Definition 2.5 (TCQ Entailment).

Given a TKB $\Gamma$ and a TCQ $\varphi\in\textsc{tcq}$. The TKB $\Gamma$
_entails_ $\varphi$, written $\Gamma\models\varphi$, iff
$\mathfrak{I}\models\varphi$, for every model $\mathfrak{I}$ of $\Gamma$.

Checking TCQ entailment (TQE) is the problem of deciding whether
$\Gamma\models\varphi$.

##  3 The TKB Alignment Problem

We generalize the verification problem of TQE to a _synthesis_ version,
consisting in _minimally_ modifying the sequence $\Lambda$ of a TKB
$\Gamma=(\mathcal{T},\Lambda)$, to obtain a TKB
$\Gamma^{\prime}=(\mathcal{T},\Lambda^{\prime})$, s.t.
$\Gamma^{\prime}\models\varphi$. Observe that if $\Gamma\models\varphi$, the
problem amounts to checking TQE. To define the problem, we formalize next the
notions of ABox- and TKB-modification, and minimality.

To modify the ABoxes occurring in a TKB, we consider two kinds of ABox
operations, namely _insertion_ and _removal_ of a (concept or role) assertion
$\alpha$, respectively denoted as $\operatorname{ins}(\alpha)$ and . The
result of applying such operations to an ABox $\mathcal{A}$ is given by the
function
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}$:
(i)
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\operatorname{ins}(\alpha),\mathcal{A})=\mathcal{A}\cup\\{\alpha\\}$;
(ii)
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}($.
An _ABox-modification_ is a (possibly empty) sequence $\mu=m_{0}\cdots m_{n}$
of ABox operations $m_{i}$. By $\varepsilon$ we denote the empty ABox-
modification. The semantics of applying an ABox-modification $\mu$ to an ABox
$\mathcal{A}$ is obtained by inductively extending
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}$
to sequences of operations:  (i)
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\varepsilon,\mathcal{A})=\mathcal{A};$
(ii)
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(m\operatorname{\cdot}\mu,\mathcal{A})={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(m,\mathcal{A}))$,
where $\operatorname{\cdot}$ is the concatenation operator.

We assume every operation $m$ has a strictly positive cost
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(m)\in\mathbb{R^{+}}$.
The _cost_ of an ABox-modification $\mu=m_{1}\cdots m_{n}$ is defined as
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu):=\sum_{i=1}^{n}{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(m_{i})$,
with
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\varepsilon)=0$.

In addition to modifying its ABoxes, a TKB can be modified by adding or
removing ABoxes. Let
${{\IfStrEqCase{Fun}{{}{Atm}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Atm}}{1}{\mathscr{Atm}}{2}{\mathfrak{Atm}}{3}{\mathbb{Atm}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Atm}}{1}{\mathsf{Atm}}{2}{\mathbb{Atm}}{3}{\mathbf{Atm}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Atm}}{1}{\mathrm{Atm}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Atm}}{1}{\mathtt{Atm}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Atm}}{1}{\mathbf{Atm}}}[\clubsuit]}{Elm}{\mathnormal{Atm}}}[\clubsuit]}}=\\{(\operatorname{fix},\mu),(\operatorname{add},\mu),\operatorname{del}\mid\mu\text{
is an ABox-modification}\\}$ be the set of _atomic TKB-modifications_.
Intuitively, $(\operatorname{fix},\mu)$ stands for the modification of an ABox
through the application of $\mu$, $(\operatorname{add},\mu)$ for the addition
of the empty ABox followed by the application of $\mu$, and
$\operatorname{del}$ for ABox deletion.

A _TKB-modification_ is a finite sequence $\eta$ of atomic TKB-modifications,
with $\varepsilon$ denoting the empty TKB-modification. Notice that, by a
slight abuse of notation, we use $\varepsilon$ to denote both the empty ABox-
modification and the empty TKB-modification; the intended meaning is clear
from the context.

The result of applying a TKB-modification $\eta$ to a sequence
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$ is the sequence
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Lambda)$,
inductively defined as follows, where $\Lambda_{\epsilon}$ denotes the empty
sequence of ABoxes, $\mathcal{A}_{\emptyset}$ the empty ABox, and
$\mathcal{A}|\Lambda=\mathcal{A}\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$:

  * •

${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\varepsilon,\Lambda)=\Lambda$;

  * •

${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}((\operatorname{fix},\mu),\Lambda_{\epsilon})=\Lambda_{\epsilon}$;

  * •

${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}((\operatorname{fix},\mu)\operatorname{\cdot}\eta,\mathcal{A}|\Lambda)={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A})|{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Lambda)$;

  * •

${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}((\operatorname{add},\mu)\operatorname{\cdot}\eta,\Lambda)={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A}_{\emptyset})|{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Lambda)$;

  * •

${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\operatorname{del}\operatorname{\cdot}\eta,\Lambda_{\epsilon}))={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Lambda_{\epsilon})$;

  * •

${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\operatorname{del}\operatorname{\cdot}\eta,\mathcal{A}|\Lambda)={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Lambda)$.

For a given TKB $\Gamma=(\mathcal{T},\Lambda)$ and a TKB-modification $\eta$,
we define
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)=(\mathcal{T},{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Lambda))$.
The cost function naturally extends to TKB-modifications and ABox sequences:

  * •

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\varepsilon,\Lambda)=0$;

  * •

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}((\operatorname{fix},\mu)\operatorname{\cdot}\eta,\Lambda_{\epsilon})={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Lambda_{\epsilon})$;

  * •

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}((\operatorname{fix},\mu)\operatorname{\cdot}\eta,\mathcal{A}|\Lambda)={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu)+{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Lambda)$;

  * •

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}((\operatorname{add},\mu)\operatorname{\cdot}\eta,\Lambda)=1+{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu)+{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Lambda)$;

  * •

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\operatorname{del}\operatorname{\cdot}\eta,\Lambda_{\epsilon})={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Lambda_{\epsilon})$;

  * •

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\operatorname{del}\operatorname{\cdot}\eta,\mathcal{A}|\Lambda)=\big{(}\sum_{\alpha\in\mathcal{A}}{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}($.

The cost of $(\operatorname{add},\mu)$ is that of adding the empty ABox (taken
as 1) and applying $\mu$ to it; similarly, the cost of $\operatorname{del}$ is
that of emptying the ABox, by removing all of its assertions, and removing the
resulting empty ABox (i.e., 1). For a TKB $\Gamma=(\mathcal{T},\Lambda)$ and a
TKB-modification $\eta$, we let
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Gamma)={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Lambda)$.

We can now introduce the TKB-alignment problem.

######  Definition 3.1 (TKB Alignment).

Given a TKB $\Gamma$ and a TCQ $\varphi$, the _TKB-alignment_ problem consists
in finding a minimal-cost TKB-modification $\eta^{*}$ (if any) s.t.
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta^{*},\Gamma)\models\varphi$.

Observe that, for every TKB-modification $\eta$ and TKB $\Gamma$, it holds
that
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta\cdot(\operatorname{fix},\epsilon),\Gamma)$
and
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Gamma)={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta\cdot(\operatorname{fix},\epsilon),\Gamma)$.
That is, appending a sequence of $(\operatorname{fix},\epsilon)$ to $\eta$
does not affect the result or the cost of modifying $\Gamma$. Thus, we can
always extend $\eta$ to guarantee that the combined number of occurrences of
deletions $\operatorname{del}$ and fixes $(\operatorname{fix},\mu)$ in $\eta$
equals at least the number of ABoxes in $\Lambda$. For technical convenience,
from now on, we assume this is the case for every $\eta$.

###  3.1 Solving TKB Alignment

Our solution approach consists in reducing TKB Alignment to Shortest Path. To
this end, we construct a graph, called _Minimal-instantiation Graph_ , with
each edge labelled by an atomic TKB-modification and its corresponding cost,
s.t. every shortest path from a suitably defined _initial_ node to one node
from a (suitably defined) _target_ set, represents an optimal solution to the
original TKB Alignment instance. The construction of such a graph is based on
several intermediate structures, which we present and discuss next.

Consider a TKB $\Gamma=(\mathcal{T},\Lambda)$ and a TCQ $\varphi$. We start
with the construction of a DPA intended to accept the set of models of
$\varphi$. To this end, we adopt an approach similar to that of [4], which
uses the _propositional abstraction_ of $\varphi$. If we view every BCQ
$\phi\in\textsc{pbcq}$ as a proposition $\hat{\phi}$, then $\varphi$ can be
viewed as an ltl formula. This is called the _propositional abstraction_ of
$\varphi$, denoted $\hat{\varphi}$. Obviously,
${{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})$
is the set of all propositions $\hat{\phi}$ occurring in $\hat{\varphi}$, each
corresponding to exactly one BCQ $\phi\in\textsc{pbcq}$.

Since $\hat{\varphi}\in\textsc{ltl}$, we can now use the Büchi automaton (BA)
construction of [24], to obtain a BA that recognizes
$\mathcal{L}(\hat{\varphi})$ and then use the BA-to-DPA construction of [21]
to obtain the DPA
$P_{\hat{\varphi}}=(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})},Q,q_{0},\delta,{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$
of $\hat{\varphi}$. The importance of $P_{\hat{\varphi}}$ lies in the fact
that, although it reads input words
$\Psi=\Phi_{0}\Phi_{1}\cdots\in{(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})})}^{\omega}$
and not FO traces $\mathfrak{I}=\mathcal{I}_{0}\mathcal{I}_{1}\cdots$, it
fully characterizes $\mathcal{L}(\varphi)$, as discussed below.

For $\Phi\in
2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})}$,
let
$\chi(\Phi)=\bigwedge_{\hat{\phi}\in\Phi}\phi\wedge\bigwedge_{\hat{\phi}\in{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})\setminus\Phi}\neg\phi$.
Since the conjuncts in $\chi(\Phi)$ are possibly negated BCQs from pbcq, and
not propositional abstractions, $\chi(\Phi)\in\mathcal{B}(\textsc{bcq})$. If
$\chi(\Phi)$ is consistent, i.e., admits at least one model, $\Phi$ is called
a _type_. When $\mathcal{I}\models\chi(\Phi)$, we call $\Phi$ the _type_ of
$\mathcal{I}$. This notion naturally extends to traces by defining the _trace
type_ of a FO trace $\mathfrak{I}=\mathcal{I}_{0}\mathcal{I}_{1}\cdots$ as the
word
$\Psi=\Phi_{0}\Phi_{1}\cdots\in{(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})})}^{\omega}$
s.t. $\Phi_{i}$ is the type of $\mathcal{I}_{i}$, for all $i\geq 0$. We have
the following result.

######  Lemma 3.2.

Every FO interpretation has a unique type and every type admits an FO
interpretation. Moreover, every FO trace has a unique trace type and every
trace type admits an FO trace.

The following result relates $\mathcal{L}(P_{\hat{\varphi}})$ and
$\mathcal{L}(\varphi)$.

######  Theorem 3.3.

Consider a TCQ $\varphi$. For every FO trace $\mathfrak{I}$ of type $\Psi$, it
holds that $\mathfrak{I}\in\mathcal{L}(\varphi)$ iff
$\,\Psi\in\mathcal{L}(P_{\hat{\varphi}})$.

Since $P_{\hat{\varphi}}$ is independent of $\Gamma$, it cannot be used to
search for the desired minimal-cost modification. For this, we can use a
deterministic finite-state automaton (DFA) $D$, called the _repair-template_
DFA for $\Gamma$ and $\varphi$. The definition of $D$ requires an auxiliary
DPA, called the $\mathcal{T}$-_reduct_ of $P_{\hat{\varphi}}$, to define the
final states of $D$.

######  Definition 3.4 ($\mathcal{T}$-reduct of $P_{\hat{\varphi}}$).

Given a TBox $\mathcal{T}$ and a TCQ $\varphi$, let
$P_{\hat{\varphi}}=(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})},Q,\delta,q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$.
The $\mathcal{T}$-reduct of $P_{\hat{\varphi}}$ is the DPA
$P_{\hat{\varphi}}^{\mathcal{T}}=(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})},Q^{\mathcal{T}},\delta^{\mathcal{T}},q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}^{\mathcal{T}})$
s.t.:

  * •

$Q^{\mathcal{T}}=Q\cup\\{q^{*}\\}$, with $q^{*}\notin Q$;

  * •

$\delta^{\mathcal{T}}(q,\Phi)=q^{\prime}$, iff either:

    * –

$\chi(\Phi)$ is satisfiable wrt $\mathcal{T}$ and $\delta(q,\Phi)=q^{\prime}$;
or

    * –

$\chi(\Phi)$ is not satisfiable wrt $\mathcal{T}$ and $q^{\prime}=q^{*}$; or

    * –

$q=q^{\prime}=q^{*}$;

  * •

${{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}^{\mathcal{T}}(q^{*})=1$
and
${{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}^{\mathcal{T}}(q)={{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}(q)+1$,
for all $q\in Q$.

######  Lemma 3.5.

The $\mathcal{T}$-reduct of $P_{\hat{\varphi}}$ can be computed in doubly
exponential time and has doubly exponential size wrt $\varphi$.

Intuitively, the $\mathcal{T}$-reduct of $P_{\hat{\varphi}}$ accepts a trace
type $\Psi$ iff there exists a FO trace $\mathfrak{I}$ of type $\Psi$ that
does not satisfy $\varphi$ and contains only interpretations satisfying
$\mathcal{T}$. Let
${{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P^{\mathcal{T}}_{\hat{\varphi}})$
be the acceptance set of $P^{\mathcal{T}}_{\hat{\varphi}}$. We have the
following.

######  Lemma 3.6.

Consider a finite sequence $\Psi^{\prime}=\Phi_{0}\cdots\Phi_{k-1}$ of types
and the finite run
$\rho=q_{0}\stackrel{{\scriptstyle\Phi_{0}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle\Phi_{k-1}}}{{\rightarrow}}q_{k}$
induced in $P_{\hat{\varphi}}$. Then,
$q_{k}\notin{{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P^{\mathcal{T}}_{\hat{\varphi}})$
iff for every type $\Psi=\Phi_{0}\cdots\Phi_{k-1}\Phi_{k}\Phi_{k+1}\cdots$,
having $\Psi^{\prime}$ as a prefix, and for all traces
$\mathfrak{I}=\mathcal{I}_{0}\mathcal{I}_{1}\cdots$ of type $\Psi$, if, for
all $i\geq k$, it holds that $\mathcal{I}_{i}\models\mathcal{T}$, then
$\mathfrak{I}\models\varphi$.

Recall that we are looking for a TKB
$\Gamma^{\prime}=(\mathcal{T},\Lambda^{\prime}=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell^{\prime}})$,
obtained as modification of $\Gamma=(\mathcal{T},\Lambda)$, s.t.
$\Gamma^{\prime}\models\varphi$, i.e., all models $\mathfrak{I}$ of
$\Gamma^{\prime}$ (Def. 2.3) are s.t. $\mathfrak{I}\models\varphi$ (Def. 2.5).
Lemma 3.6 implies that every model $\mathfrak{I}$ of $\Gamma^{\prime}$ must
belong to some trace type $\Psi_{\mathfrak{I}}$ whose induced run in
$P_{\hat{\varphi}}$ touches some
$q_{k}\notin{{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P^{\mathcal{T}}_{\hat{\varphi}})$,
for $k=\ell^{\prime}+1$. Based on this, we next define the _repair-template_
DFA.

######  Definition 3.7 (Repair-template DFA).

Given a TKB $\Gamma=(\mathcal{T},\Lambda)$ with
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$ and a TCQ $\varphi$, let
$P_{\hat{\varphi}}^{\mathcal{T}}=(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})},Q^{\mathcal{T}},\delta^{\mathcal{T}},q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}^{\mathcal{T}})$
be the $\mathcal{T}$-reduct of
$P_{\hat{\varphi}}=(2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})},Q,\delta,q_{0},{{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}})$.

The _repair-template DFA (RT-DFA) for $\Gamma$ and $\varphi$_ is the DFA
$D=(Al,S,s_{0},\gamma,F)$ s.t.:

  * •

$Al=(\\{\operatorname{fix},\operatorname{add}\\}\times
2^{2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})}})\cup\\{\operatorname{del}\\}$
is the alphabet;

  * •

$S=2^{Q}\times\\{0,\ldots,\ell+1\\}$ is the set of states;

  * •

$s_{0}=(\\{q_{0}\\},0)$ is the initial state;

  * •

$\gamma:S\times Al\rightarrow S$ is the transition function s.t.
$\gamma((Z,i),X)=(Z^{\prime},i^{\prime})$ iff either:

    1. 1.

$X=\operatorname{del}$, $Z=Z^{\prime}$, and $i^{\prime}=\min\\{i+1,\ell+1\\}$;
or

    2. 2.

all of the following hold:

      1. (a)

$X=(\sigma,\Upsilon)$, with
$\sigma\in\\{\operatorname{fix},\operatorname{add}\\}$;

      2. (b)

$q^{\prime}\in Z^{\prime}$ iff $\delta(q,\Phi)=q^{\prime}$, for $q\in Z$ and
$\Phi\in\Upsilon$;

      3. (c)

there exists an ABox $\mathcal{A}$ consistent with $\mathcal{T}$ s.t.:
$(\mathcal{T},\mathcal{A})\models\bigvee_{\Phi\in\Upsilon}\chi(\Phi)\land\bigwedge_{\Phi\not\in\Upsilon}\lnot\chi(\Phi)$;

      4. (d)

$i^{\prime}=\begin{cases}\min\\{i+1,\ell+1\\},\text{ if
}\sigma=\operatorname{fix}\\\ i,\text{ if
}\sigma=\operatorname{add}\end{cases}$

  * •

$F=\\{(Z,\ell+1)\in S\mid
Z\cap{{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P_{\hat{\varphi}}^{\mathcal{T}})=\emptyset\\}$
is the set of final states.

######  Lemma 3.8.

The RT-DFA for a TKB $\Gamma$ and a TCQ $\varphi$ can be computed in triply
exponential time and has triply exponential size wrt $\varphi$.

Observe that the right-hand side expression of the entailment ($\models$) in
Item 2c above is a Boolean combination of BCQs. The purpose of the RT-DFA is
to capture the solution space of TKB Alignment for $(\mathcal{T},\Lambda)$ and
$\varphi$, in the following sense:  (i) from every accepted word $w$, some TKB
modification $\eta$ can be derived s.t.
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)\models\varphi$,
and  (ii) every TKB modification $\eta$ s.t.
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)\models\varphi$
can be derived from some accepted word $w$.  This is formalized next, by the
notion of TKB-modification _abstraction_ and the subsequent result.

######  Definition 3.9 (TKB-modification abstraction).

Consider a TKB $\Gamma=(\mathcal{T},\Lambda)$, with
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$, a TCQ $\varphi$, and let
$D=(Al,S,s_{0},\gamma,F)$ be the RT-DFA for $\Gamma$ and $\varphi$. A word
$w=w_{0}\cdots w_{m}\in Al^{*}$, inducing a finite run
$\rho=s_{0}\stackrel{{\scriptstyle
w_{0}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle
w_{m}}}{{\rightarrow}}s_{m+1}$ in $D$, is an _abstraction_ of (or _abstracts_)
a TKB-modification $\eta=\eta_{0}\cdots\eta_{m}$ iff, for $j=0,\ldots,m$:

  * •

$w_{j}=\operatorname{del}$ and $\eta_{j}=\operatorname{del}$; or

  * •

$w_{j}=(\operatorname{fix},\Upsilon)$ and, for $s_{j}=(Z,i)$,
$\eta_{j}=(\operatorname{fix},\mu)$, with
$(\mathcal{T},{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A}_{i}))\models\bigvee_{\Phi\in\Upsilon}\chi(\Phi)\land\bigwedge_{\Phi\not\in\Upsilon}\lnot\chi(\Phi)$;
or

  * •

$w_{j}=(\operatorname{add},\Upsilon)$ and $\eta_{j}=(\operatorname{add},\mu)$,
with
$(\mathcal{T},{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A}_{\emptyset}))\models\bigvee_{\Phi\in\Upsilon}\chi(\Phi)\land\bigwedge_{\Phi\not\in\Upsilon}\lnot\chi(\Phi)$.

When this holds, $\eta$ is an _instantiation_ of (or _instantiates_) $w$.

######  Theorem 3.10.

Consider a TKB $\Gamma=(\mathcal{T},\Lambda)$, with
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$, a TCQ $\varphi$, and let
$D=(Al,S,s_{0},\gamma,F)$ be the RT-DFA for $\Gamma$ and $\varphi$. Then:

  1. 1.

for every word $w\in Al^{*}$, there exists an instantiation $\eta$ s.t.
$w\in\mathcal{L}(D)$ iff
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)\models\varphi$;

  2. 2.

for every word $w\in Al^{*}$ and every instantiation $\eta$ of $w$, it holds
that $w\in\mathcal{L}(D)$ iff
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)\models\varphi$;

  3. 3.

for every TKB-modification $\eta$ there exists a unique abstraction $w_{\eta}$
s.t. $w_{\eta}\in\mathcal{L}(D)$ iff
${{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\eta,\Gamma)\models\varphi$.

Thm. 3.10 states that the language of $D$ characterizes the set of solutions
for the TKB-alignment of $\Gamma$ against the specification $\varphi$; in
particular, Item 2 ensures that every instantiation of some TKB-modification
abstraction $w\in\mathcal{L}(D)$ is a solution to TKB Alignment. Then, every
optimal solution $\eta^{*}$ is s.t.:

$\eta^{*}=\mathop{\mathrm{argmin}}_{\eta}\\{{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\Gamma)\mid\eta\text{
instantiates some }w\in\mathcal{L}(D)\\}$.

Based on this, we can reduce the problem of finding $\eta^{*}$ to that of
finding a minimal path in a suitably weighted graph.

######  Definition 3.11 (Minimal-instantiation Graph).

Consider a TKB $\Gamma=(\mathcal{T},\Lambda)$, with
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$, a TCQ $\varphi$, and let
$D=(Al,S,s_{0},\gamma,F)$ be the RT-DFA for $\Gamma$ and $\varphi$. The
_minimal-instantiation graph_ for $\Gamma$ and $\varphi$ is the weighted graph
$G=(N,E,\mathop{{{\IfStrEqCase{Fun}{{}{w}{Name}{\IfStrEqCase{0}{{0}{\mathcal{w}}{1}{\mathscr{w}}{2}{\mathfrak{w}}{3}{\mathbb{w}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{w}}{1}{\mathsf{w}}{2}{\mathbb{w}}{3}{\mathbf{w}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{w}}{1}{\mathrm{w}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{w}}{1}{\mathtt{w}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{w}}{1}{\mathbf{w}}}[\clubsuit]}{Elm}{\mathnormal{w}}}[\clubsuit]}}})$,
where:

  1. 1.

$N=S$ is the finite set of nodes;

  2. 2.

$E\subseteq
N\times{{\IfStrEqCase{Fun}{{}{Atm}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Atm}}{1}{\mathscr{Atm}}{2}{\mathfrak{Atm}}{3}{\mathbb{Atm}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Atm}}{1}{\mathsf{Atm}}{2}{\mathbb{Atm}}{3}{\mathbf{Atm}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Atm}}{1}{\mathrm{Atm}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Atm}}{1}{\mathtt{Atm}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Atm}}{1}{\mathbf{Atm}}}[\clubsuit]}{Elm}{\mathnormal{Atm}}}[\clubsuit]}}\times
N$, is the finite set of edges, labelled by atomic TKB-modifications;

  3. 3.

$\mathop{{{\IfStrEqCase{Fun}{{}{w}{Name}{\IfStrEqCase{0}{{0}{\mathcal{w}}{1}{\mathscr{w}}{2}{\mathfrak{w}}{3}{\mathbb{w}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{w}}{1}{\mathsf{w}}{2}{\mathbb{w}}{3}{\mathbf{w}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{w}}{1}{\mathrm{w}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{w}}{1}{\mathtt{w}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{w}}{1}{\mathbf{w}}}[\clubsuit]}{Elm}{\mathnormal{w}}}[\clubsuit]}}}:E\rightarrow\mathbb{R}^{+}$
is the edge weight function;

  4. 4.

it holds that $e=((Z,i),\eta,(Z^{\prime},i^{\prime}))\in E$ and
$\mathop{{{\IfStrEqCase{Fun}{{}{w}{Name}{\IfStrEqCase{0}{{0}{\mathcal{w}}{1}{\mathscr{w}}{2}{\mathfrak{w}}{3}{\mathbb{w}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{w}}{1}{\mathsf{w}}{2}{\mathbb{w}}{3}{\mathbf{w}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{w}}{1}{\mathrm{w}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{w}}{1}{\mathtt{w}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{w}}{1}{\mathbf{w}}}[\clubsuit]}{Elm}{\mathnormal{w}}}[\clubsuit]}}}(e)=c$
iff, for some $X$, $(Z^{\prime},i^{\prime})=\gamma((Z,i),X)$, and:

     * -

if $X=\operatorname{del}$ then $\eta=\operatorname{del}$ and
$c={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\operatorname{del},\mathcal{A}_{i})$;

     * -

if $X=(\operatorname{fix},\Upsilon)$ then $\eta=\\\
\mathop{\mathrm{argmin}}_{(\operatorname{fix},\mu)}\big{\\{}{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}((\operatorname{fix},\mu),\mathcal{A}_{i})\mid(\mathcal{T},{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A}_{i}))\models\bigvee_{\Phi\in\Upsilon}\chi(\Phi)\land\bigwedge_{\Phi\not\in\Upsilon}\lnot\chi(\Phi)\big{\\}}$
and
$c={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\mathcal{A}_{i})$;

     * -

if $X=(\operatorname{add},\Upsilon)$ then $\eta=\\\
\mathop{\mathrm{argmin}}_{(\operatorname{add},\mu)}\big{\\{}{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}((\operatorname{add},\mu),\Lambda_{\epsilon})\mid\\\
(\mathcal{T},{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A}_{\emptyset}))\models\bigvee_{\Phi\in\Upsilon}\chi(\Phi)\land\bigwedge_{\Phi\not\in\Upsilon}\lnot\chi(\Phi)\big{\\}}$
and
$c={{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\eta,\mathcal{A}_{\emptyset})$.

######  Lemma 3.12.

The Minimal-instantiation Graph for a TKB $\Gamma$ and a TCQ $\varphi$ can be
computed in triply exponential time and has triply exponential size wrt
$\varphi$.

The minimal-instantiation graph $G$ is a graph whose edges are labelled with
atomic TKB-modifications and weighted with the corresponding cost. Through its
labels, every finite path
$s_{0}\stackrel{{\scriptstyle\eta_{0}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle\eta_{m-1}}}{{\rightarrow}}s_{m}$
of $G$ defines an instantiation $\eta=\eta_{0}\cdots\eta_{m}$ of some input
word (not necessarily accepted) $w=w_{0}\cdots w_{m}$ of $D$. Also the
viceversa holds, i.e., every input word $w$ of $D$ is an abstraction of the
TKB-modification $\eta$ defined by some path of $G$.

Observe that, by Item 4 of Def. 3.11, $\eta$ includes only minimal-cost atomic
TKB-modifications $\eta_{i}$, thus it is a minimal-cost TKB-modification among
all those that instantiate the same $w$. Moreover, recall that, by Theorem
3.10, every solution to TKB Alignment is associated to an abstraction
$w\in\mathcal{L}(D)$. Thus, since every such $w$ has a minimal-cost
instantiation in some path of $G$, we can search for the minimal-cost solution
by exploring the paths of $G$. Indeed, it is enough to search for the minimal-
cost paths of $G$ which correspond to the words $w$ accepted by $D$; since the
nodes of $G$ correspond to the states of $D$, this corresponds to searching
for a minimal-path of $G$ starting in $s_{0}$ and ending in some node that is
an accepting state for $D$.

######  Theorem 3.13.

Consider a TKB $\Gamma=(\mathcal{T},\Lambda)$, with
$\Lambda=\mathcal{A}_{0}\cdots\mathcal{A}_{\ell}$, a TCQ $\varphi$, and let
$D=(Al,S,s_{0},\gamma,F)$ be the RT-DFA for $\Gamma$ and $\varphi$. A TKB-
modification $\eta=\eta_{0}\cdots\eta_{m}$ is an optimal solution of TKB
Alignment for $\Gamma$ and $\varphi$ iff there exists a minimum-cost path
$\pi=n_{0}\stackrel{{\scriptstyle\eta_{0}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle\eta_{m-1}}}{{\rightarrow}}n_{m}$
in $G$, s.t. $n_{0}=s_{0}$ and $n_{m}\in F$.

Thus, with $G$ at hand, the search can easily be performed by, e.g.,
Dijkstra’s algorithm. However, in order to state the effective solvability of
TKB Alignment, we must still guarantee that $G$ is actually computable. In
this respect, observe that we still need to explain how the labels and the
weights of $G$ can be obtained.

By Def. 3.11 (Item 4), computing the labels and the weights of $G$ requires to
solve, for every edge, one _local minimization problem_ of the form
$\mathop{\mathrm{argmin}}_{(\sigma,\mu)}\\{{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}((\sigma,\mu),\Lambda)\\}$,
subject to a constraint of the form
$(\mathcal{T},{{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A}))\models\phi$,
with $\phi\in\mathcal{B}(\textsc{bcq})$. This is the _KB-alignment_ problem,
which we formally define and solve in Section 4. We report here that the
problem can be solved in doubly exponential time. This, together with the
complexity results reported above, leads to the following.

######  Theorem 3.14.

TKB Alignment is solvable in triply exponential time.

As mentioned above, one might consider the semantics on TCQs given in [4] and
instantiate TKB alignment with it. Such variation on the semantics has minimal
impact on the solution technique, which can be adapted to that setting with
minimal changes. Details are omitted, due to space constraints.

##  4 The KB-Alignment Problem

In this section, we define the _knowledge base alignment problem (KB
Alignment)_ , and show how to solve it for the query language
$\mathcal{B}(\textsc{bcq})$ and the DL $\mathcal{ALC}$.

######  Definition 4.1 (KB Alignment).

Given a KB $\mathcal{K}=(\mathcal{T},\mathcal{A})$ and a query
$\phi\in\mathcal{B}(\textsc{bcq})$, the problem of KB Alignment consists in
finding an ABox-modification $\mu$ such that for
$\mathcal{A}^{\prime}={{\IfStrEqCase{Fun}{{}{mod}{Name}{\IfStrEqCase{0}{{0}{\mathcal{mod}}{1}{\mathscr{mod}}{2}{\mathfrak{mod}}{3}{\mathbb{mod}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{mod}}{1}{\mathsf{mod}}{2}{\mathbb{mod}}{3}{\mathbf{mod}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{mod}}{1}{\mathrm{mod}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{mod}}{1}{\mathtt{mod}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{mod}}{1}{\mathbf{mod}}}[\clubsuit]}{Elm}{\mathnormal{mod}}}[\clubsuit]}}(\mu,\mathcal{A})$:

  1. 1.

$(\mathcal{T},\mathcal{A}^{\prime})$ is consistent;

  2. 2.

$(\mathcal{T},\mathcal{A}^{\prime})\models\phi$; and

  3. 3.

${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu)\leq{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu^{\prime})$
for all ABox-modifications $\mu^{\prime}$ satisfying Conditions 1 and 2.

An ABox-modification $\mu$ satisfying Condition 1 and 2 is a _solution to KB
Alignment_ for $(\mathcal{K},\phi)$; if it also satisfies 3, it is an
_optimal_ solution.

To solve an instance of KB Alignment, it is sufficient to consider ABox-
modifications with operations defined using concept and role names from the
input KB and query, i.e., using names from their signature. A _signature_ is a
finite subset of $\mathsf{N_{C}}\cup\mathsf{N_{R}}$. We use $\mathsf{sig}(X)$
to denote the set of concept and role names occurring in $X$, where $X$ can be
a KB or a query.

######  Lemma 4.2.

Let $\mathcal{K}$ be a KB and $\phi\in\mathcal{B}(\textsc{bcq})$. If KB
Alignment has a solution for $(\mathcal{K},\phi)$, then it has an optimal
solution $\mu$ where all ABox-operations $\operatorname{ins}(\alpha)$ and in
$\mu$ are such that $\alpha$ is an assertion defined over
$\mathsf{sig}(\mathcal{K})\cup\mathsf{sig}(\phi)$.

An algorithm that solves KB Alignment for $\mathcal{ALC}$ KBs and queries in
$\mathcal{B}(\textsc{bcq})$ is introduced next.

###  4.1 Solving KB-Alignment

Algorithm 1 describes our method to solve KB Alignment. The approach is to (1)
compute an upper bound on the cost of optimal solutions (if any), (2) iterate
over all ABox-modifications of decreasing cost starting from the upper bound,
and finally output a modification that satisfies Condition 1 to 3 from
Definition 4.1, i.e., which is optimal.

More precisely, for the input TBox $\mathcal{T}$ and query $\phi$, the
algorithm first computes an ABox $\mathcal{A}^{\prime}$ such that
$(\mathcal{T},\mathcal{A}^{\prime})$ is consistent and
$(\mathcal{T},\mathcal{A}^{\prime})\models\phi$. Then, a modification
$\mu^{*}$ from the input ABox $\mathcal{A}$ into $\mathcal{A}^{\prime}$ is
obtained which always exists: given two ABoxes $\mathcal{A}$ and
$\mathcal{A}^{\prime}$, a _trivial modification from $\mathcal{A}$ into
$\mathcal{A}^{\prime}$_ is defined as a sequence $\mu=m_{1}\cdots m_{k}\cdots
m_{n}$, where $m_{1}\cdots m_{k}$ consists of the removal of all assertions in
$\mathcal{A}$ and $m_{k+1}\cdots m_{n}$ consists of the insertion of all
assertions occurring in $\mathcal{A}^{\prime}$.

The algorithm computes one trivial modification, which, by Definition 4.1, is
a (possibly non-optimal) solution, thus
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu^{*})$
realizes the first step of the approach as it is an upper bound on the cost of
optimal solutions. Then, the _for-loop_ enumerates all ABox-modifications with
cost smaller than
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu^{*})$,
that satisfy Condition 1 and 2 of Definition 4.1, and returns one ABox
modification of minimal cost.

By using Lemma 4.2, it is not hard to show that the output of Algorithm 1 is
always an optimal solution.

######  Lemma 4.3.

If Algorithm 1 returns $\mu^{*}$ on input $\mathcal{K}$ and $\phi$, then
$\mu^{*}$ is an optimal solution to KB Alignment for $(\mathcal{K},\phi)$. If
Algorithm 1 returns “no solution”, then KB Alignment has no solution for
$(\mathcal{K},\phi)$.

Algorithm 1 KB Alignment.

Input: An $\mathcal{ALC}$ KB $\mathcal{K}=(\mathcal{T},\mathcal{A})$ and a
query $\phi\in\mathcal{B}(\textsc{bcq})$.

Output: An optimal solution of KB Alignment for $(\mathcal{K},\phi)$, if a
solution exists; or “no solution”, otherwise.

1: Compute an ABox $\mathcal{A}^{\prime}$ s.t.
$(\mathcal{T},\mathcal{A}^{\prime})$ is consistent,
$(\mathcal{T},\mathcal{A}^{\prime})\models\phi$ and
$\mathsf{sig}(\mathcal{A}^{\prime})\subseteq\mathsf{sig}(\mathcal{K})\cup\mathsf{sig}(\phi)$.
If no such ABox exists, return “no solution”;

2: Define a trivial modification $\mu^{*}$ from $\mathcal{A}$ into
$\mathcal{A}^{\prime}$;

3: Let $M$ be the set of ABox-modifications $\mu$ defined over
$\mathsf{sig}(\mathcal{K})\cup\mathsf{sig}(\phi)$ s.t.
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu)<{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu^{*})$;

4: for all $\mu\in M$ do

5: if ($\mu$ satisfies conditions 1 and 2 in Definition 4.1) and
(${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu)<{{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu^{*})$)
then

6: $\mu^{*}:=\mu$;

7: return $\mu^{*}$;

Hence, to see that Algorithm 1 solves the KB-alignment problem, it remains to
show that it terminates, i.e., all its steps can _effectively_ be computed.
The following arguments show this for most of the steps:

  * •

Since $\mathcal{A}$ and $\mathcal{A}^{\prime}$ are finite sets, a trivial
modification $\mu^{*}$ can easily be computed from the ABox
$\mathcal{A}^{\prime}$.

  * •

Consistency of $\mathcal{ALC}$ KBs is a decidable problem ([5]), as well as
entailment of $\mathcal{B}(\textsc{bcq})$-queries in $\mathcal{ALC}$ (see Sec.
2.2), hence the conditions at line 5 can be effectively verified for each
$\mu\in M$.

  * •

The set $M$ contains only ABox-modifications defined over the finite signature
$\mathsf{sig}(\mathcal{K})\cup\mathsf{sig}(\phi)$. Hence, given $n>0$, $M$
contains finitely many $\mu$ with $n$ ABox-operations, and each such $\mu$ has
cost of at least $c\cdot n$, where $c$ is the minimal cost of an ABox
operation defined over $\mathsf{sig}(\mathcal{K})\cup\mathsf{sig}(\phi)$. This
implies that $M$ is a finite set and contains only modifications with no more
than
${{\IfStrEqCase{Fun}{{}{c}{Name}{\IfStrEqCase{0}{{0}{\mathcal{c}}{1}{\mathscr{c}}{2}{\mathfrak{c}}{3}{\mathbb{c}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{c}}{1}{\mathsf{c}}{2}{\mathbb{c}}{3}{\mathbf{c}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{c}}{1}{\mathrm{c}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{c}}{1}{\mathtt{c}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{c}}{1}{\mathbf{c}}}[\clubsuit]}{Elm}{\mathnormal{c}}}[\clubsuit]}}(\mu^{*})/c$
operations. Thus, $M$ can be visited in finite time.

It remains to specify how to compute the initial ABox $\mathcal{A}^{\prime}$
(or to determine that it does not exist). This requires a more involved
argument presented in the following.

####  4.1.1 Computing the initial ABox $\mathcal{A}^{\prime}$

The computation of the initial ABox $\mathcal{A}^{\prime}$ in our algorithm is
closely related to the _query emptiness problem_ in ontology-mediated query
answering. This problem was introduced and investigated in [2] for various DLs
(including $\mathcal{ALC}$) and the query language cq. We define this problem
here for the more general query language $\mathcal{B}(\textsc{cq})$. It uses
the notion of $\Sigma$-ABox, which refers to ABoxes that use only names from a
signature $\Sigma$.

######  Definition 4.4 ($\mathcal{B}(\textsc{cq})$-query Emptiness).

Let $\mathcal{T}$ be a TBox, $\Sigma$ a signature and
$\phi\in\mathcal{B}(\textsc{cq})$. The query $\phi$ is called _empty for
$\Sigma$ given $\mathcal{T}$_ if for all $\Sigma$-ABoxes $\mathcal{A}$ such
that $(\mathcal{T},\mathcal{A})$ is consistent, we have
$cert_{(\mathcal{T},\mathcal{A})}(\phi)=\emptyset$.

_$\mathcal{B}(\textsc{cq})$ -query Emptiness_ is the problem of deciding,
given a TBox $\mathcal{T}$, a signature $\Sigma$, and
$\phi\in\mathcal{B}(\textsc{cq})$, whether $\phi$ is empty for $\Sigma$ wrt
$\mathcal{T}$.

In [2], it is shown that to decide cq-query Emptiness in $\mathcal{ALC}$, it
suffices to consider a single $\Sigma$-ABox
$\mathcal{A}_{\mathcal{T},\Sigma}$. This ABox is of exponential size and can
be computed (from a given satisfiable TBox $\mathcal{T}$ and a signature
$\Sigma$) in exponential time, in the size of $\mathcal{T}$ and the
cardinality of $\Sigma$. Moreover, it satisfies the following:

  * •

the KB $(\mathcal{T},\mathcal{A}_{\mathcal{T},\Sigma})$ is consistent, and

  * •

given a pure CQ $\phi$, $\phi$ is empty for $\Sigma$ wrt $\mathcal{T}$ iff
$cert_{(\mathcal{T},\mathcal{A}_{\mathcal{T},\Sigma})}(\phi)=\emptyset$.

The arguments used to prove the second property can be easily extended to pure
${\mathcal{B}(\textsc{cq})}$-queries, as the following result shows.

######  Lemma 4.5.

Let $\mathcal{T}$ be a satisfiable $\mathcal{ALC}$ TBox, $\Sigma$ a signature
and $\phi\in\mathcal{B}(\textsc{cq})$ a pure query. Then, $\phi$ is empty for
$\Sigma$ wrt $\mathcal{T}$ iff
$cert_{(\mathcal{T},\mathcal{A}_{\mathcal{T},\Sigma})}(\phi)=\emptyset$.

For _non-pure_ queries, query emptiness can be reduced to the case of pure
queries. This can be done as follows. Let $\mathcal{T}$ be an $\mathcal{ALC}$
TBox, $\Sigma$ a signature, and $\phi\in\mathcal{B}(\textsc{cq})$ a _non-pure_
query with $\mathsf{Ind}(\phi)=\\{a_{1},\ldots,a_{m}\\}$. We select $m$
_fresh_ concept names $A_{1},\ldots,A_{m}$, i.e., concept names neither
occurring in $\mathcal{T},\phi$ nor $\Sigma$. Then, we define an
$\mathcal{ALC}$ TBox $\mathcal{T}_{p}$, a signature $\Sigma_{p}$ and a query
$\phi_{p}\in\mathcal{B}(\textsc{cq})$, as follows:

  * •

$\mathcal{T}_{p}=\mathcal{T}\cup\mathcal{T}_{d}$, where
$\mathcal{T}_{d}=\\{A_{i}\sqcap A_{j}\sqsubseteq\bot\mid 1\leq i<j\leq m\\}$,

  * •

$\phi_{p}=\phi_{x}\land\phi_{d}$, where $\phi_{x}$ is obtained from $\phi$ by
replacing each $a\in\mathsf{Ind}(\phi)$ by a fresh free variable $x_{a}$,
whereas $\phi_{d}$ is the CQ $\phi_{d}=A_{1}(x_{a_{1}})\land\ldots\land
A_{m}(x_{a_{m}})$, and

  * •

$\Sigma_{p}=\Sigma\cup\\{A_{1},\ldots,A_{m}\\}$.

The following lemma shows that testing whether $\phi$ is empty for $\Sigma$
wrt $\mathcal{T}$ reduces to checking emptiness of $\phi_{p}$ for $\Sigma_{p}$
wrt $\mathcal{T}_{p}$. Since $\phi_{p}$ is a pure query, this yields a
reduction from query emptiness of _non-pure_ queries to the case of pure
queries.

######  Lemma 4.6.

Let $\mathcal{T}$ be an $\mathcal{ALC}$ TBox, $\Sigma$ a signature, and $\phi$
a query in $\mathcal{B}(\textsc{cq})$. The following holds:

  1. 1.

$\phi$ is empty for $\Sigma$ wrt $\mathcal{T}$ iff $\phi_{p}$ is empty for
$\Sigma_{p}$ wrt $\mathcal{T}_{p}$.

  2. 2.

If there is a $\Sigma_{p}$-ABox $\mathcal{A}_{p}$ that witnesses non-emptiness
of $\phi_{p}$ for $\Sigma_{p}$ wrt $\mathcal{T}_{p}$, then, given $t\in
cert_{(\mathcal{T}_{p},\mathcal{A}_{p})}(\phi_{p})$, $\mathcal{A}_{p}$ can be
transformed in polynomial time (in the size of $\mathcal{A}_{p}$ and $t$) into
a $\Sigma$-ABox $\mathcal{A}$ witnessing non-emptiness of $\phi$ for $\Sigma$
wrt $\mathcal{T}$.

Hence, if the input query $\phi$ of Algorithm 1 is pure, by Lemma 4.5 the
search space for the ABox $\mathcal{A}^{\prime}$ can simply be restricted to
$\\{\mathcal{A}_{\mathcal{T},\Sigma}\\}$ where
$\Sigma=\mathsf{sig}(\mathcal{K})\cup\mathsf{sig}(\phi)$. Otherwise, Lemma 4.6
tells us how to obtain $\mathcal{A}^{\prime}$ (if it exists). Namely, the
algorithm first constructs $\mathcal{T}_{p},\phi_{p}$ and $\Sigma_{p}$ from
$\mathcal{T},\phi$ and $\Sigma$. It then checks whether $\phi_{p}$ is non-
empty for $\Sigma_{p}$ wrt $\mathcal{T}_{p}$, by using
$\mathcal{A}_{\mathcal{T}_{p},\Sigma_{p}}$. If the latter is true, then
$\mathcal{A}^{\prime}$ is selected as the ABox obtained from applying to
$\mathcal{A}_{\mathcal{T}_{p},\Sigma_{p}}$ the transformation from the second
statement in Lemma 4.6. Overall, this provides a way to compute
$\mathcal{A}^{\prime}$ whenever it exists.

Hence, Algorithm 1 always terminates. This, together with Lemma 4.3, yields
solvability of KB Alignment. A closer look at Algorithm 1 reveals that it runs
in _double exponential time_ in the size of the input KB and query. Thus, we
obtain the following result.

######  Theorem 4.7.

KB Alignment is solvable for $\mathcal{ALC}$ and $\mathcal{B}(\textsc{bcq})$
in _double exponential time_.

##  5 Discussion and Future Work

TKB Alignment is a new variant of the alignment problem that admits richer
state and property descriptions. Our setting uses $\mathcal{ALC}$-TKBs, CQs
with ltl operators, and a cost function for the edit operations. We have shown
that TKB Alignment wrt temporal CQs is solvable, by developing computation
methods for both TKB and KB Alignment.

The TKB-alignment problem is closely related to abduction and to computing
repairs of KBs, as these tasks also change a KB to either gain a desired
consequence or remove an unwanted one. However, although being active research
topics, neither of the two has yet been investigated for the temporalized
setting and entailment of TCQs. Furthermore, TKB Alignment requires a cost-
optimal solution, which is not very common in the context of abduction or
repairs.

Interestingly, TKB Alignment can also be used for relaxing temporal CQ
answering. Given a tuple of individuals $\bar{a}$ which is not a certain
answer of a TCQ $\phi$, solve TKB Alignment for the Boolean TCQ obtained from
$\phi^{\prime}$ by assigning $\bar{a}$ to the answer variables of $\phi$. The
costs computed during TKB Alignment for $\phi^{\prime}$ then measure the
“distance” to a certain answer of the query.

Our initial investigation on TKB Alignment uses a unitary cost measure for the
edit operations mostly to ease presentation, as our approach can handle other
cost measures easily. In this work, we did not regard rigid symbols, which are
left for future work.

The work of Giuseppe Perelli was partially funded by MUR under the PRIN
programme, grant B87G22000450001 (PINPOINT), and by the PNRR MUR project
PE0000013-FAIR. The work of Fabio Patrizi was partially funded by MUR under
the PNRR MUR project PE0000013-FAIR, the ERC Advanced Grant WhiteMech (No.
834228), and the Sapienza Project MARLeN.

## References

  * [1] Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev, ‘First-order rewritability of ontology-mediated queries in linear temporal logic’, Artif. Intell., 299, 103536, (2021).
  * [2] Franz Baader, Meghyn Bienvenu, Carsten Lutz, and Frank Wolter, ‘Query and predicate emptiness in ontology-based data access’, J. Artif. Intell. Res., 56, 1–59, (2016).
  * [3] Franz Baader, Stefan Borgwardt, Patrick Koopmann, Veronika Thost, and Anni-Yasmin Turhan, ‘Semantic technologies for situation awareness’, Künstliche Intell., 34(4), 543–550, (2020).
  * [4] Franz Baader, Stefan Borgwardt, and Marcel Lippmann, ‘Temporal query entailment in the description logic SHQ’, J. Web Semant., 33, 71–93, (2015).
  * [5] The Description Logic Handbook: Theory, Implementation, and Applications, eds., Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, Cambridge University Press, 2003.
  * [6] Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler, An Introduction to Description Logic, Cambridge University Press, 2017.
  * [7] Meghyn Bienvenu, ‘A short survey on inconsistency handling in ontology-mediated query answering’, Künstliche Intell., 34(4), 443–451, (2020).
  * [8] Meghyn Bienvenu and Magdalena Ortiz, ‘Ontology-mediated query answering with data-tractable description logics’, in Reasoning Web. Web Logic Rules - 11th International Summer School, eds., Wolfgang Faber and Adrian Paschke, volume 9203 of Lecture Notes in Computer Science, pp. 218–307. Springer, (2015).
  * [9] Stefan Borgwardt, Marcel Lippmann, and Veronika Thost, ‘Temporalizing rewritable query languages over knowledge bases’, Journal of Web Semantics, 33, 50–70, (2015).
  * [10] Camille Bourgaux, Patrick Koopmann, and Anni-Yasmin Turhan, ‘Ontology-mediated query answering over temporal and inconsistent data’, Semantic Web, 10(3), 475–521, (2019).
  * [11] Giuseppe De Giacomo, Fabrizio Maria Maggi, Andrea Marrella, and Fabio Patrizi, ‘On the disruptive effectiveness of automated planning for LTL _f_ -based trace alignment’, in AAAI, pp. 3555–3561, (2017).
  * [12] Massimiliano de Leoni, Fabrizio Maria Maggi, and Wil van der Aalst, ‘An alignment-based framework to check the conformance of declarative process models and to preprocess event-log data’, Inf. Syst., 47, 258–277, (2015).
  * [13] Massimiliano de Leoni, Fabrizio Maria Maggi, and Wil M. P. van der Aalst, ‘Aligning event logs and declarative process models for conformance checking’, in BPM, (2012).
  * [14] Warren Del-Pinto and Renate A. Schmidt, ‘Abox abduction via forgetting in $\mathcal{ALC}$’, in The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, pp. 2768–2775. AAAI Press, (2019).
  * [15] Dov M. Gabbay, ‘The declarative past and imperative future: Executable temporal logic for interactive systems’, in Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings, volume 398 of Lecture Notes in Computer Science, pp. 409–448. Springer, (1987).
  * [16] Valerie King, Orna Kupferman, and Moshe Y. Vardi, ‘On the complexity of parity word automata’, in Proc. of FOSSACS, eds., Furio Honsell and Marino Miculan, volume 2030 of Lecture Notes in Computer Science, pp. 276–286. Springer, (2001).
  * [17] Patrick Koopmann, Warren Del-Pinto, Sophie Tourret, and Renate Schmidt, ‘Signature-based abduction for expressive description logics’, in Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), (2020).
  * [18] Orna Kupferman, Nir Piterman, and Moshe Y. Vardi, ‘Extended temporal logic revisited’, in CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, eds., Kim Guldstrand Larsen and Mogens Nielsen, volume 2154 of Lecture Notes in Computer Science, pp. 519–535. Springer, (2001).
  * [19] Carsten Lutz, ‘The complexity of conjunctive query answering in expressive description logics’, in Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pp. 179–193. Springer, (2008).
  * [20] Magdalena Ortiz, Mantas Simkus, and Thomas Eiter, ‘Worst-case optimal conjunctive query answering for an expressive description logic without inverses’, in Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, eds., Dieter Fox and Carla P. Gomes, pp. 504–510. AAAI Press, (2008).
  * [21] Nir Piterman, ‘From nondeterministic büchi and streett automata to deterministic parity automata’, Log. Methods Comput. Sci., 3(3), (2007).
  * [22] Manfred Schmidt-Schauß and Gert Smolka, ‘Attributive concept descriptions with complements’, Artif. Intell., 48(1), 1–26, (1991).
  * [23] Ahmet Soylu, Martin Giese, Rudolf Schlatte, Ernesto Jiménez-Ruiz, Evgeny Kharlamov, Özgür L. Özçep, Christian Neuenstadt, and Sebastian Brandt, ‘Querying industrial stream-temporal data: An ontology-based visual approach’, J. Ambient Intell. Smart Environ., 9(1), 77–95, (2017).
  * [24] Moshe Y. Vardi, ‘An automata-theoretic approach to linear temporal logic’, in Logics for Concurrency - Structure versus Automata (8th Banff Higher Order Workshop, Banff, Canada, August 27 - September 3, 1995, Proceedings), volume 1043 of Lecture Notes in Computer Science, pp. 238–266. Springer, (1995).
  * [25] Thomas Wilke, ‘Classifying discrete temporal properties’, in STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, eds., Christoph Meinel and Sophie Tison, volume 1563 of Lecture Notes in Computer Science, pp. 32–46. Springer, (1999).

##  Appendix A Proofs

###  A.1 Proofs from Section 3

See 3.2

######  Proof A.1.

Consider a FO interpretation $\mathcal{I}$ and the type defined as
$\Phi_{\mathcal{I}}=\\{\hat{\phi}\in{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})\mid\mathcal{I}\models\phi\\}$.
Clearly, we have $\mathcal{I}\models\chi(\Phi_{I})$ and
$\mathcal{I}\not\models\chi(\Phi)$ for every other type $\Phi$.

On the other hand, note that every type $\Phi\in
2^{{{\IfStrEqCase{Fun}{{}{props}{Name}{\IfStrEqCase{0}{{0}{\mathcal{props}}{1}{\mathscr{props}}{2}{\mathfrak{props}}{3}{\mathbb{props}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{props}}{1}{\mathsf{props}}{2}{\mathbb{props}}{3}{\mathbf{props}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{props}}{1}{\mathrm{props}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{props}}{1}{\mathtt{props}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{props}}{1}{\mathbf{props}}}[\clubsuit]}{Elm}{\mathnormal{props}}}[\clubsuit]}}(\hat{\varphi})}$
identifies a combination of positive and negative boolean BCQs that are
consistent by construction, and therefore admit a model $\mathcal{I}$ for all
of them, which means that $\mathcal{I}\models\chi(\Phi)$, and so that
$\mathcal{I}$ is of type $\Phi$.

The proof easily lifts to (infinite) sequences of FO traces and types.

See 3.3

######  Proof A.2.

Observe that from Theorem 2.1, we obtain that
$\Psi\in\mathcal{L}(P_{\hat{\varphi}})$ iff $\Psi\models\hat{\varphi}$,
regarded as propositional ltl. Therefore, we need to prove that, for every
$\mathfrak{I}$, it holds that $\mathfrak{I}\models\varphi$ iff
$\Psi\models\hat{\varphi}$, with $\Psi$ being the trace type of
$\mathfrak{I}$. We do it by induction on the structure of $\varphi$.

  * •

Assume $\varphi=\psi\in\textsc{bcq}$ being a boolean conjunctive query. It
holds that $\mathfrak{I}\models\psi$ iff $\mathfrak{I}_{0}\models\psi$, which,
from Lemma 3.2, is true iff $\hat{\psi}\in\Psi_{0}$, being $\Psi_{0}$ the type
of $\mathfrak{I}_{0}$. The latter holds iff $\Psi\models\hat{\psi}$ and so iff
$\Psi\in\mathcal{L}(P_{\hat{\varphi}})$.

All the other (boolean and temporal) cases are standard proofs that build on
top of the semantics of tcq and of propositional ltl.

See 3.5

######  Proof A.3.

Direct consequence of Thm. 2.1, which states that the state space of
$P_{\varphi}$ has doubly exponential size in $\varphi$, and the EXPTIME-
completeness of deciding satisfiability of $\chi(\Phi)$ wrt $\mathcal{T}$
[19].

See 3.6

######  Proof A.4.

We prove the two implications separately. First, assume that
$q_{k}\notin{{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P^{\mathcal{T}}_{\hat{\varphi}})$
and let $\Psi^{k}=\Phi_{k}\Phi_{k+1}\cdots$ be a type trace and
$\mathfrak{I}^{k}=\mathcal{I}_{k}\mathcal{I}_{k+1}$ a corresponding FO-trace.
If $\mathcal{I}_{i}\not\models\mathcal{T}$ for some $i\geq k$ then the trace
type $\Psi$ already satisfies the statement. Assume instead that
$\mathcal{I}_{i}\models\mathcal{T}$ fore every $i\geq k$ and consider the run

$\rho^{\mathcal{T}}=q_{k}\stackrel{{\scriptstyle\Phi_{k}}}{{\rightarrow}}q_{k+1}\stackrel{{\scriptstyle\Phi_{k+1}}}{{\rightarrow}}\cdots$

of $\Psi^{k}$ in $P^{\mathcal{T}}_{\hat{\varphi}}$. First, observe that, since
$\mathcal{I}_{i}\models\mathcal{T}$ for every $i\geq k$, we have that
$\chi(\Phi_{i})$ is consistent with $\mathcal{T}$ for every $i\geq k$. This
means that the extra state $q^{*}$ in $P^{\mathcal{T}}_{\hat{\varphi}}$ does
not occur in $\rho^{\mathcal{T}}$, which implies that $\rho^{\mathcal{T}}$ is
also the run of $\Psi^{k}$ in $P_{\hat{\varphi}}$. By concatenation, we obtain
that

$\rho^{\prime}=q_{0}\stackrel{{\scriptstyle\Phi_{0}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle\Phi_{k-1}}}{{\rightarrow}}q_{k}\stackrel{{\scriptstyle\Phi_{k}}}{{\rightarrow}}q_{k+1}\stackrel{{\scriptstyle\Phi_{k+1}}}{{\rightarrow}}\cdots$

is the run in $P_{\hat{\varphi}}$ of the word $\Psi$. Now, since
$q_{k}\notin{{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P^{\mathcal{T}}_{\hat{\varphi}})$,
we obtain that
$\min\\{{{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}(\rho^{\mathcal{T}},P^{\mathcal{T}}_{\hat{\varphi}})\\}$
is odd. Therefore, by the definition of
${{\IfStrEqCase{Fun}{{}{col}{Name}{\IfStrEqCase{0}{{0}{\mathcal{col}}{1}{\mathscr{col}}{2}{\mathfrak{col}}{3}{\mathbb{col}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{col}}{1}{\mathsf{col}}{2}{\mathbb{col}}{3}{\mathbf{col}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{col}}{1}{\mathrm{col}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{col}}{1}{\mathtt{col}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{col}}{1}{\mathbf{col}}}[\clubsuit]}{Elm}{\mathnormal{col}}}[\clubsuit]}}^{\mathcal{T}}$,
we obtain that
$\min\\{{{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}(\rho^{\prime},P_{\hat{\varphi}})\\}=\min\\{{{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}(\rho^{\mathcal{T}},P_{\hat{\varphi}})\\}=\min\\{{{\IfStrEqCase{Fun}{{}{inf}{Name}{\IfStrEqCase{0}{{0}{\mathcal{inf}}{1}{\mathscr{inf}}{2}{\mathfrak{inf}}{3}{\mathbb{inf}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{inf}}{1}{\mathsf{inf}}{2}{\mathbb{inf}}{3}{\mathbf{inf}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{inf}}{1}{\mathrm{inf}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{inf}}{1}{\mathtt{inf}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{inf}}{1}{\mathbf{inf}}}[\clubsuit]}{Elm}{\mathnormal{inf}}}[\clubsuit]}}(\rho^{\mathcal{T}},P^{\mathcal{T}}_{\hat{\varphi}})\\}-1$
is even and then that $\Psi\in\mathcal{L}(P_{\hat{\varphi}})$. By Theorem 3.3
we derive that the FO trace $\mathfrak{I}$, being of type $\Psi$, is such that
$\mathfrak{I}\models\varphi$.

We now prove the other direction by counter-nominal argument. Assume
$q_{k}\in{{\IfStrEqCase{Fun}{{}{Acc}{Name}{\IfStrEqCase{0}{{0}{\mathcal{Acc}}{1}{\mathscr{Acc}}{2}{\mathfrak{Acc}}{3}{\mathbb{Acc}}}[\clubsuit]}{Set}{\IfStrEqCase{0}{{0}{\mathrm{Acc}}{1}{\mathsf{Acc}}{2}{\mathbb{Acc}}{3}{\mathbf{Acc}}}[\clubsuit]}{Fun}{\IfStrEqCase{0}{{0}{\mathsf{Acc}}{1}{\mathrm{Acc}}}[\clubsuit]}{Rel}{\IfStrEqCase{0}{{0}{\mathit{Acc}}{1}{\mathtt{Acc}}}[\clubsuit]}{Sym}{\IfStrEqCase{0}{{0}{\mathtt{Acc}}{1}{\mathbf{Acc}}}[\clubsuit]}{Elm}{\mathnormal{Acc}}}[\clubsuit]}}(P^{\mathcal{T}}_{\hat{\varphi}})$.
This means that there exists a word $\Psi^{k}=\Phi_{k}\Phi_{k+1}\ldots$ whose
run

$\rho^{\mathcal{T}}=q_{k}\stackrel{{\scriptstyle\Phi_{k}}}{{\rightarrow}}q_{k+1}\stackrel{{\scriptstyle\Phi_{k+1}}}{{\rightarrow}}\cdots$

of $\Psi^{k}$ in $P^{\mathcal{T}}_{\hat{\varphi}}$ starting from $q_{k}$ is
accepting. This implies that $q^{*}$ never appears in $\rho^{\mathcal{T}}$,
which means that $\chi(\Phi_{i})$ is consistent with $\mathcal{T}$, for every
$i\geq k$, and that

$\rho^{\prime}=q_{0}\stackrel{{\scriptstyle\Phi_{0}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle\Phi_{k-1}}}{{\rightarrow}}q_{k}\stackrel{{\scriptstyle\Phi_{k}}}{{\rightarrow}}q_{k+1}\stackrel{{\scriptstyle\Phi_{k+1}}}{{\rightarrow}}\cdots$

is the run in $P_{\hat{\varphi}}$ of the word
$\Psi=\Phi_{0}\cdots\Phi_{k-1}\Phi_{k}\Phi_{k+1}\cdots$. Being that
$\rho^{\mathcal{T}}$ is accepting in $P^{\mathcal{T}}_{\hat{\varphi}}$, we
have that