11institutetext:  Institute for IS Research, University of Koblenz-Landau,
Koblenz, Germany
11email<EMAIL_ADDRESS>
22institutetext: University of Maryland, College Park, USA
22email<EMAIL_ADDRESS>
33institutetext: Artificial Intelligence Group, University of Hagen, Hagen,
Germany
33email<EMAIL_ADDRESS>
# Measuring Inconsistency in
Declarative Process Specifications††thanks: This work has been accepted for
publication at the 20th International Conference on Business Process
Management (BPM 2022). This work has been partially supported by the Deutsche
Forschungsgemeinschaft (Grant DE 1983/9-1).

Carl Corea 11 John Grant 22 Matthias Thimm 33

###### Abstract

We address the problem of measuring inconsistency in declarative process
specifications, with an emphasis on linear temporal logic on fixed traces
(LTL${}_{\text{ff}}$). As we will show, existing inconsistency measures for
classical logic cannot provide a meaningful assessment of inconsistency in LTL
in general, as they cannot adequately handle the temporal operators. We
therefore propose a novel paraconsistent semantics as a framework for
inconsistency measurement. We then present two new inconsistency measures
based on these semantics and show that they satisfy important desirable
properties. We show how these measures can be applied to declarative process
models and investigate the computational complexity of the introduced
approach.

###### Keywords:

Inconsistency Measurement LTL Declare.

##  1 Introduction

Linear temporal logic (LTL) is an important logic for specifying the
(temporal) behavior of business processes in the form of _declarative process
specifications_ [20, 1]. The underlying idea is that time is represented as a
linear sequence of states $T=(t_{0},...,t_{m})$, where $t_{0}$ is the
designated starting point. At every state, some statements may be true.
Temporal operators specify properties that must hold over the sequence of
states. For example, the operator X (_next_) means that a certain formula
holds at the next state. Likewise, the operator G (_globally_) means that a
certain formula will hold for all following states. Note that we interpret
over finite traces, i.e., we consider a linear temporal logic over finite
traces (LTL${}_{\text{f}}$) [20, 6].

Traditionally, model checking has been used to verify that a particular
model—that is, the assignment of truth values for statements over the time
sequence—satisfies the requirements. However, a problem in this use case
arises if the set of formulas is _inconsistent_ , i. e., contains
contradictory specifications. In such a case, the set of specifications cannot
be applied for its intended purpose of process verification. For example,
consider the two sets of formulas $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$ (we
will formalize syntax and semantics later):

$\displaystyle\mathcal{K}_{1}=\\{\textbf{X}a,\textbf{X}\neg a\\}$
$\displaystyle\mathcal{K}_{2}=\\{\textbf{G}a,\textbf{G}\neg a\\}$

Both $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$ are inconsistent, as they demand
that both $a$ and $\neg a$ hold in (some) following state, which is
unsatisfiable. This calls for the analysis of such inconsistencies, to provide
insights for inconsistency resolution.

In classical logic, all inconsistent sets are equally bad [14]. However,
considering again the two sets, intuitively, $\mathcal{K}_{2}$ is “more”
inconsistent than $\mathcal{K}_{1}$: The inconsistency in $\mathcal{K}_{1}$
only affects the next state, while the inconsistency in $\mathcal{K}_{2}$
affects all following states. This is an important insight that could prove
useful for debugging or re-modelling LTL${}_{\text{f}}$ specifications or
LTL${}_{\text{f}}$-based constraint sets in general such as Declare. While
there have been some recent works that can _identify_ inconsistent sets in
declarative process specifications [4, 2, 22], those works cannot look “into”
those sets or compare them. In this work, we therefore show how to distinguish
the _severity_ of inconsistencies in LTL${}_{\text{f}}$, specifically,
LTL${}_{\text{ff}}$.

A scientific field geared towards the quantitative assessment of inconsistency
in knowledge representation formalisms is _inconsistency measurement_ [9, 25],
and therefore represents a good candidate for this endeavour. Inconsistency
measurement studies measures that aim to assess a _degree_ of inconsistency
with a numerical value. The intuition here is that a higher value represents a
higher degree of inconsistency. Such measures can provide valuable insights
for debugging inconsistent specifications, e. g., to determine whether certain
sets of formulas are more inconsistent than others. As we will show, existing
measures are currently not geared towards LTL${}_{\text{f}}$ and temporal
operators, and therefore cannot provide a meaningful analysis. Therefore, the
main goal of this paper is to develop a new approach for measuring
inconsistency in linear temporal logic. To frame this problem, we introduce a
variant of LTL${}_{\text{f}}$, which we coin linear temporal logic on _fixed_
traces LTL${}_{\text{ff}}$ (cf. Section 2.2).

Our contributions are as follows. We formalise the problem of measuring
inconsistency in LTL${}_{\text{ff}}$ and propose a rationality postulate that
should be met by quantitative measures applied to this setting (Section 2). We
show that existing inconsistency measures do not satisfy this property, and
propose an approach for measuring inconsistency based on a novel
paraconsistent semantics for LTL${}_{\text{ff}}$ (Section 3). We then show how
our approach can be applied for measuring inconsistency in declarative process
models (Section 4). For evaluation, we investigate the computational
complexity of central aspects regarding inconsistency measurement in
LTL${}_{\text{ff}}$ (Section 5). A conclusion is provided in Section 6. Proofs
for technical results can be found in the Appendix.

##  2 Preliminaries

The traditional setting for inconsistency measurement is that of propositional
logic. For that, let $\mathsf{At}$ be some fixed propositional signature, i.
e., a (possibly infinite) set of propositions, and let
$\mathcal{L}(\mathsf{At})$ be the corresponding propositional language
constructed using the usual connectives $\wedge$ (_conjunction_), $\vee$
(_disjunction_), and $\neg$ (_negation_). A literal is a proposition $p$ or
negated proposition $\neg p$.

###### Definition 1

A knowledge base $\mathcal{K}$ is a finite set of formulas
$\mathcal{K}\subseteq\mathcal{L}(\mathsf{At})$. Let $\mathbb{K}$ be the set of
all knowledge bases.

For a set of formulas $X$ we denote the set of propositions in $X$ by
$\mathsf{At}(X)$.

Semantics for a propositional language is given by _interpretations_ where an
interpretation $\omega$ on $\mathsf{At}$ is a function
$\omega:\mathsf{At}\rightarrow\\{0,1\\}$ (where $0$ stands for false and $1$
stands for true). Let $\Omega(\mathsf{At})$ denote the set of all
interpretations for $\mathsf{At}$. An interpretation $\omega$ _satisfies_ (or
is a _model_ of) an atom $a\in\mathsf{At}$, denoted by $\omega\models a$, if
and only if $\omega(a)=1$. The satisfaction relation $\models$ is extended to
formulas in the usual way. For $\Phi\subseteq\mathcal{L}(\mathsf{At})$ we also
define $\omega\models\Phi$ if and only if $\omega\models\phi$ for every
$\phi\in\Phi$. Furthermore, for every set of formulas $X$, the set of models
is $\mathsf{Mod}(X)=\\{\omega\in\Omega(\mathsf{At})\mid\omega\models X\\}$.
Define $X\models Y$ for (sets of) formulas $X$ and $Y$ if $\omega\models X$
implies $\omega\models Y$ for all $\omega$.

Let $\top$ denote any tautology and $\perp$ any contradiction. If
$\mathsf{Mod}(X)=\emptyset$ we write $X\models\perp$ and say that $X$ is
_inconsistent_.

###  2.1 Inconsistency Measurement

Inconsistency as defined above is a binary concept. To provide more fine-
grained insights on inconsistency beyond such a binary classification, the
field of inconsistency measurement [25] has evolved. The main objects of study
in this field are _inconsistency measures_ , which are quantitative measures
that assess the degree of inconsistency for a knowledge base $\mathcal{K}$
with a non-negative numerical value. Intuitively, a higher value reflects a
higher degree, or severity, of inconsistency. This can be useful for
determining if one set of formulas is “more” inconsistent than another. Let
$\mathbb{R}^{\infty}_{\geq 0}$ be the set of non-negative real values
including $\infty$. Then, an inconsistency measure is defined as follows.

###### Definition 2

An inconsistency measure $\mathcal{I}$ is any function
$\mathcal{I}:\mathbb{K}\rightarrow\mathbb{R}^{\infty}_{\geq 0}$.

To constrain the desired behavior of concrete inconsistency measures, several
properties, called rationality postulates, have been proposed. A well-agreed
upon property is that of _consistency_ , which states that an inconsistency
measure should return a value of 0 iff there is no inconsistency.

_Consistency_ (CO)

$\mathcal{I}(\mathcal{K})=0$ if and only if $\mathcal{K}$ is consistent.

Further important postulates introduced in [12] are _monotony, dominance_ and
_free-formula independence_ , which we will define below. For that, we need
some further notation.

First, a set $M\subseteq\mathcal{K}$ is called a _minimal inconsistent subset_
(MIS) of $\mathcal{K}$ if $M\models\perp$ and there is no $M^{\prime}\subset
M$ with $M^{\prime}\models\perp$. Let $\textsf{MI}(\mathcal{K})$ be the set of
all MISs of $\mathcal{K}$. Second, a formula $\alpha\in\mathcal{K}$ is called
a _free formula_ if $\alpha\notin\bigcup\textsf{MI}(\mathcal{K})$. Let
$\textsf{Free}(\mathcal{K})$ be the set of all free formulas of $\mathcal{K}$.

For the remainder of this section, let $\mathcal{I}$ be an inconsistency
measure, $\mathcal{K},\mathcal{K}^{\prime}\in\mathbb{K}$, and
$\alpha,\beta\in\mathcal{L}(\mathsf{At})$. Then, the basic postulates from
[12] are defined as follows.

_Monotony_ (MO)

If $\mathcal{K}\subseteq\mathcal{K}^{\prime}$ then
$\mathcal{I}(\mathcal{K})\leq\mathcal{I}(\mathcal{K}^{\prime})$.

_Free-formula independence_ (IN)

If $\alpha\in\textsf{Free}(\mathcal{K})$ then
$\mathcal{I}(\mathcal{K})=\mathcal{I}(\mathcal{K}\setminus\\{\alpha\\})$.

_Dominance_ (DO)

If $\alpha\not\models\perp$ and $\alpha\models\beta$ then
$\mathcal{I}(\mathcal{K}\cup\\{\alpha\\})\geq\mathcal{I}(\mathcal{K}\cup\\{\beta\\})$.

MO states that adding formulas to the knowledge base cannot decrease the
inconsistency value. IN means that removing free formulas from the knowledge
base does not change the inconsistency value. DO consists of several cases,
depending on the presence or absence of $\alpha$ or $\beta$ in $\mathcal{K}$:
the idea is that substituting a consistent formula $\alpha$ by a weaker
formula $\beta$ cannot increase the inconsistency.

Numerous inconsistency measures have been proposed (see [26] for a survey),
many of which differ in regard to their compliance w.r.t. the introduced
postulates. In this work, we will consider six measures as defined below. In
order to define the _contension measure_ $\mathcal{I}_{c}$ [8] we need some
additional background on Priest’s three-valued semantics [21]. A three-valued
interpretation is a function $\nu:\mathsf{At}\rightarrow\\{0,1,\text{B}\\}$,
which assigns to every atom either $0$, $1$ or B, where $0$ and $1$ correspond
to $false$ and $true$, respectively, and B (standing for _both_) denotes a
conflict. Assuming the _truth order_ $\prec_{T}$ with $0\prec_{T}B\prec_{T}1$,
the function $\nu$ can be extended to arbitrary formulas as follows:
$\nu(\alpha\wedge\beta)=\min_{\prec_{T}}(\nu(\alpha),\nu(\beta))$,
$\nu(\alpha\vee\beta)=\max_{\prec_{T}}(\nu(\alpha),\nu(\beta))$,
$\nu(\neg\alpha)=1$ if $\nu(\alpha)=0$, $\nu(\neg\alpha)=0$ if
$\nu(\alpha)=1$, and $\nu(\neg\alpha)=B$ if $\nu(\alpha)=B$. We say that an
interpretation $\nu$ satisfies a formula $\alpha$, denoted by
$\nu\models^{3}\alpha$, iff $\nu(\alpha)=1$ or $\nu(\alpha)=\text{B}$.

We will now define the measures used in this work.

###### Definition 3

Let the measures $\mathcal{I}_{d}$, $\mathcal{I}_{\mathsf{MI}}$,
$\mathcal{I}_{p}$, $\mathcal{I}_{r}$, $\mathcal{I}_{c}$, and
$\mathcal{I}_{at}$ be defined as follows:

$\displaystyle\mathcal{I}_{d}(\mathcal{K})$
$\displaystyle=\left\\{\begin{array}[]{cc}1&\text{if~{}}\mathcal{K}\models\perp\\\
0&\text{otherwise}\end{array}\right.$
$\displaystyle\mathcal{I}_{\mathsf{MI}}(\mathcal{K})$
$\displaystyle=|\textsf{MI}(\mathcal{K})|$
$\displaystyle\mathcal{I}_{p}(\mathcal{K})$
$\displaystyle=|\bigcup_{M\in\textsf{MI}(\mathcal{K})}M|$
$\displaystyle\mathcal{I}_{r}(\mathcal{K})$ $\displaystyle=\min\\{|X|\mid
X\subseteq\mathcal{K}\text{~{}and }\mathcal{K}\setminus X\not\models\perp\\}$
$\displaystyle\mathcal{I}_{c}(\mathcal{K})$
$\displaystyle=\min\\{|\nu^{-1}(B)\cap\mathsf{At}|\mid\nu\models^{3}\mathcal{K}\\}$
$\displaystyle\mathcal{I}_{at}(\mathcal{K})$
$\displaystyle=|\bigcup_{M\in\textsf{MI}(\mathcal{K})}\mathsf{At}(M)|$

A baseline approach is the drastic inconsistency measure $\mathcal{I}_{d}$
[13], which only differentiates between inconsistent and consistent knowledge
bases. The MI-inconsistency measure $\mathcal{I}_{\mathsf{MI}}$ [13] counts
the number of minimal inconsistent subsets. A similar version is the
problematic inconsistency measure $\mathcal{I}_{p}$ [8], which counts the
number of distinct formulas appearing in any inconsistent subset. The repair
measure $\mathcal{I}_{r}$ counts the smallest number of formulas that must be
removed in order to restore consistency. The contension measure
$\mathcal{I}_{c}$ [8] quantifies inconsistency by seeking a three-valued
interpretation that assigns B to a minimal number of propositions. Finally,
the $\mathcal{I}_{at}$ measure counts the number of atoms in the non-free
formulas.

We conclude this section with a small example illustrating the behavior of the
considered inconsistency measures.

###### Example 1

Consider $\mathcal{K}_{3}$, defined via

$\displaystyle\mathcal{K}_{3}$ $\displaystyle=\\{a,\neg a,b,\neg b\wedge
c\wedge d,\neg a\vee\neg b\\}$

Then we have that

$\displaystyle\textsf{MI}(\mathcal{K}_{3})$ $\displaystyle=\\{\\{a,\neg
a\\},\\{b,\neg b\wedge c\wedge d\\},\\{a,\neg a\vee\neg b,b\\}\\}$

Thus

$\displaystyle\mathcal{I}_{d}(\mathcal{K}_{3})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{\mathsf{MI}}(\mathcal{K}_{3})$ $\displaystyle=3$
$\displaystyle\mathcal{I}_{p}(\mathcal{K}_{3})$ $\displaystyle=5$
$\displaystyle\mathcal{I}_{r}(\mathcal{K}_{3})$ $\displaystyle=2$
$\displaystyle\mathcal{I}_{c}(\mathcal{K}_{3})$ $\displaystyle=2$
$\displaystyle\mathcal{I}_{at}(\mathcal{K}_{3})$ $\displaystyle=4$

The main focus of study in inconsistency measurement, and the introduced
measures, has been on propositional logic. In this work, our aim is to apply
inconsistency measures for linear time logic, which we introduce now.

###  2.2 Linear Temporal Logic on Fixed Traces

In this work, we consider a specific variant of LTL${}_{\text{f}}$ that we
coin linear temporal logic on _fixed_ traces (LTL${}_{\text{ff}}$). We
consider a linear sequence of states $t_{0},\ldots,t_{m}$, where every $t_{i}$
is the state at instant $i$. We assume that $m>1$ to avoid the trivial case.
Note that the difference with LTL${}_{\text{f}}$—where interpretations can
vary in their length as long as they are finite—is that we keep the length of
this sequence finite and fixed across all interpretations. This variant of
LTL${}_{\text{f}}$ is introduced mainly to discuss matters of inconsistency
measurement, as here, the inconsistency value is computed in regard to a
comparable length for all formulas. However, the ideas presented in the next
sections can be extended to LTL${}_{\text{f}}$ [5] in a straightforward
manner: In the unbounded case we can use a parameter N and then proceed as in
the bounded case. This also means that $m$ must not necessarily be known or
provided a priori, as a parameter N can be selected.

The syntax of LTL${}_{\text{ff}}$ is the same as the syntax of LTL and
LTL${}_{\text{f}}$ [6]. Formulas are built from a set of propositional symbols
$\mathsf{At}$ and are closed under the Boolean connectives, the unary operator
X (_next_), and the binary operator U (_until_). Formally, any formula
$\varphi$ of LTL${}_{\text{ff}}$ is built using the grammar rule

$\displaystyle\varphi::=a|(\neg\varphi)|(\varphi_{1}\wedge\varphi_{2})|(\varphi_{1}\vee\varphi_{2})|(\textbf{X}\varphi)|(\varphi_{1}\textbf{U}\varphi_{2}).$

with $a\in\mathsf{At}$. Intuitively, $\textbf{X}\varphi$ denotes that
$\varphi$ will hold at the next state and $(\varphi_{1}\textbf{U}\varphi_{2})$
denotes that $\varphi_{1}$ will hold until the state when $\varphi_{2}$ holds.
Let $d(\varphi)\in\mathbb{N}$ denote the maximal number of nested temporal
operators in $\varphi$.-2-2-2$d(\varphi)$ is inductively defined via $d(a)=0$
for $a\in\mathsf{At}$, $d(\neg\phi)=d(\phi)$,
$d(\phi_{1}\wedge\phi_{2})=d(\phi_{1}\vee\phi_{2})=\max\\{d(\phi_{1}),d(\phi_{2})\\}$,
$d(\textbf{X}\phi)=1+d(\phi)$, and
$d(\phi_{1}\textbf{U}\phi_{2})=1+\max\\{d(\phi_{1}),d(\phi_{2})\\}$.

From the basic operators, some useful abbreviations can be derived, including
$\textbf{F}\varphi$ (defined as $\top\textbf{U}\varphi$), which denotes that
$\varphi$ will hold (eventually) in the future and $\textbf{G}\varphi$
(defined as $\neg\textbf{F}\neg\varphi$), which denotes that $\varphi$ will
hold for all following states. Again, let $\top$ be any tautology and $\bot$
any contradiction.

An LTL${}_{\text{ff}}$-interpretation $\hat{\omega}$ w.r.t. $\mathsf{At}$ is a
function mapping each state and proposition to $0$ or $1$, meaning that
$\hat{\omega}(t,a)=1$ if proposition $a$ is assigned $1$ (true) in state
$t$.-1-1-1Recall that we assume time of a fixed length $t_{0},\ldots,t_{m}$
and interpretations only vary in what is true at each state. Then the
satisfaction of a formula $\phi$ by an interpretation $\hat{\omega}$, denoted
by $\hat{\omega}\models\phi$, is defined via

$\displaystyle\hat{\omega}\models\phi\quad\Leftrightarrow\quad\hat{\omega},t_{0}\models\phi$

where $\hat{\omega},t_{i}\models\phi$ for any interpretation $\hat{\omega}$ as
above and for every $t_{i}\in\\{t_{0},…,t_{m}\\}$ is inductively defined as
follows:

$\displaystyle\hat{\omega},t_{i}\models a\text{ iff
}\hat{\omega}(t_{i},a)=1\text{~{}for~{}}a\in\mathsf{At}$
$\displaystyle\hat{\omega},t_{i}\models\neg\varphi\text{ iff
}\hat{\omega},t_{i}\not\models\varphi$
$\displaystyle\hat{\omega},t_{i}\models\varphi_{1}\wedge\varphi_{2}\text{ iff
}\hat{\omega},t_{i}\models\varphi_{1}\text{ and
}\hat{\omega},t_{i}\models\varphi_{2}$
$\displaystyle\hat{\omega},t_{i}\models\varphi_{1}\vee\varphi_{2}\text{ iff
}\hat{\omega},t_{i}\models\varphi_{1}\text{ or
}\hat{\omega},t_{i}\models\varphi_{2}$
$\displaystyle\hat{\omega},t_{i}\models\textbf{X}\varphi\text{ iff
}i<m\text{~{}and~{}}\hat{\omega},t_{i+1}\models\varphi$
$\displaystyle\hat{\omega},t_{i}\models\varphi_{1}\textbf{U}\varphi_{2}\text{
iff }\hat{\omega},t_{j}\models\varphi_{2}\text{ for some
}j\in\\{i+1,\ldots,m\\}$ $\displaystyle\qquad\quad\quad\quad\quad\text{ and
}\hat{\omega},t_{k}\models\varphi_{1}\text{ for all }k\in\\{i,\ldots,j-1\\}$

An interpretation $\hat{\omega}$ satisfies a set of formulas $K$ iff
$\hat{\omega}\models\phi$ for all $\phi\in K$. A set $K$ is consistent iff
there exists $\hat{\omega}$ such that $\hat{\omega}\models K$. Define
$X\models Y$ for (sets of) formulas $X$ and $Y$ if $\hat{\omega}\models X$
implies $\hat{\omega}\models Y$ for all $\hat{\omega}$.

###  2.3 Related Work and Contributions

This work is related to consistency- and model checking in declarative process
specifications, see e.g. [23, 10, 19]. In particular, our approach extends
recent works [4, 2, 22, 19] on the identification of inconsistent sets in
declarative process specifications by allowing to look “into” those sets and
leverage inconsistency resolution with quantitative insights. For example,
existing resolution approaches mainly try to minimize the _number_ of deleted
formulas [4, 2, 16]. This however completely leaves aside the semantics of
those formulas or their impact on any corresponding process. Given this
motivation, it is useful to consider also the degree to which certain formulas
affect the following behavior, which is why we propose time sensitive
inconsistency measures.

This paper is related to [7] which presents several, what we call time
sensitive, inconsistency measures for branching time logics (BTL). However, in
this work we are able to avoid the complicated overload of branching time as
the process specifications are provided in linear time logic. Using branching
time logic adds a layer of complexity that is unnecessary when dealing with a
linear time situation. Just to take one example, consider the set
$\\{\textbf{X}a,\textbf{X}\neg a\\}$. In linear time logic this gives one
inconsistency at the next state. But in the case of branching time logic what
does X mean? There may be many “next” states. If X means “some next state”
then the set is consistent because $a$ and $\neg a$ may hold in different next
states. If X means “all next states” then it is inconsistent but how
inconsistent depends on the number of next states. We avoid such issues by
dealing only with linear temporal logic. Note also that BTL takes a different
view on time than LTL${}_{\text{f}}$ as studied in this paper and is therefore
expressively incomparable (cf. [27]).

##  3 Inconsistency Measurement in LTL${}_{\text{ff}}$

In this section, we address the issue of measuring inconsistency in
LTL${}_{\text{ff}}$. As we will show, existing inconsistency measures cannot
provide meaningful insights when dealing with temporal logic. Therefore, we
develop a novel paraconsistent semantics as a framework for handling
inconsistency and propose two concrete inconsistency measures for
LTL${}_{\text{ff}}$.

###  3.1 Motivation for Inconsistency Measures for LTL${}_{\text{ff}}$

We recall the sets of LTL${}_{\text{ff}}$ formulas $\mathcal{K}_{1}$ and
$\mathcal{K}_{2}$:

$\displaystyle\mathcal{K}_{1}=\\{\textbf{X}a,\textbf{X}\neg a\\}$
$\displaystyle\mathcal{K}_{2}=\\{\textbf{G}a,\textbf{G}\neg a\\}$

The knowledge base $\mathcal{K}_{1}$ states that $a$ is both true and false in
the next state while $\mathcal{K}_{2}$ states that $a$ is both true and false
in all future states. Obviously, both knowledge bases are inconsistent. Yet,
the inconsistencies are different in regard to the number of states they
affect. For $\mathcal{K}_{1}$ the number is $1$ and for $\mathcal{K}_{2}$ the
number is $m>1$. It would therefore be desirable for an inconsistency measure
to take this information into account and assign $\mathcal{K}_{2}$ a larger
inconsistency value.

In order to capture LTL${}_{\text{ff}}$ by the inconsistency measurement
framework of Section 2.1, from now on a knowledge base $\mathcal{K}$
(Definition 1) will be a finite set of LTL${}_{\text{ff}}$ formulas and
$\mathbb{K}$ is the set of all LTL${}_{\text{ff}}$ knowledge bases. So we can
apply the inconsistency measures for $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$
in a straightforward manner.

###### Example 2

Consider $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$. Then we have that

$\displaystyle\mathcal{I}_{d}(\mathcal{K}_{1})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{d}(\mathcal{K}_{2})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{\mathsf{MI}}(\mathcal{K}_{1})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{\mathsf{MI}}(\mathcal{K}_{2})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{p}(\mathcal{K}_{1})$ $\displaystyle=2$
$\displaystyle\mathcal{I}_{p}(\mathcal{K}_{2})$ $\displaystyle=2$
$\displaystyle\mathcal{I}_{r}(\mathcal{K}_{1})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{r}(\mathcal{K}_{2})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{c}(\mathcal{K}_{1})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{c}(\mathcal{K}_{2})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{at}(\mathcal{K}_{1})$ $\displaystyle=1$
$\displaystyle\mathcal{I}_{at}(\mathcal{K}_{2})$ $\displaystyle=1$

Note that all six inconsistency measures give identical values for
$\mathcal{K}_{1}$ and $\mathcal{K}_{2}$, because they, or for that matter, any
other propositional logic inconsistency measure, cannot distinguish between X
and G. But intuitively $\mathcal{K}_{2}$ is more inconsistent than
$\mathcal{K}_{1}$ because the inconsistency persists through all future states
in $\mathcal{K}_{2}$ as opposed to the single state in $\mathcal{K}_{1}$.
Thus, we believe that a proper inconsistency measure for LTL${}_{\text{ff}}$
should distinguish between these operators. Therefore, we propose a new
rationality postulate.

_Time Sensitivity_ (TS)

For all formulas $\varphi$ of propositional logic,
$\mathcal{I}(\\{\textbf{G}\varphi,\textbf{G}\neg\varphi\\})>\mathcal{I}(\\{\textbf{X}\varphi,\textbf{X}\neg\varphi\\})$.

In other words, the number of affected states should be reflected in the
inconsistency value, i.e., inconsistency measures for LTL${}_{\text{ff}}$
should be time sensitive.

###### Proposition 1

$\mathcal{I}_{d},\mathcal{I}_{\mathsf{MI}},\mathcal{I}_{p},\mathcal{I}_{r},\mathcal{I}_{c},\mathcal{I}_{at}$
violate TS.

Following Proposition 1, the existing measures that we have from propositional
logic cannot capture the desired behavior. Therefore, we introduce a novel
approach to measure inconsistency in LTL${}_{\text{ff}}$.

###  3.2 A Paraconsistent Semantics for LTL${}_{\text{ff}}$

Our first contribution towards measuring inconsistency in LTL${}_{\text{ff}}$
is to define an LTL${}_{\text{ff}}$-variant of the three-valued semantics of
[21]. By doing so, we not only develop a means to neatly express inconsistency
measures for LTL${}_{\text{ff}}$, but also define a general applicable
paraconsistent semantics for LTL${}_{\text{ff}}$.

A three-valued interpretation $\hat{\nu}$ for LTL${}_{\text{ff}}$ is a
function mapping each state and proposition to $0$, $1$ or B, that is,
$\hat{\nu}:\\{t_{0},t_{1},\ldots
t_{m}\\}\times\textsf{At}\rightarrow\\{0,1,\text{B}\\}$ where as before $0$
and $1$ correspond to the classic logical false and true, respectively, and B
(standing for _both_) denotes a conflict. We then assign

$\displaystyle\hat{\nu}(\phi)$ $\displaystyle=\hat{\nu}(t_{0},\phi)$

where $\hat{\nu}(t_{i},\phi)$, for any interpretation $\hat{\nu}$ as above and
state $t_{i}\in\\{t_{0},…,t_{m}\\}$, is inductively defined as follows:

$\displaystyle\hat{\nu}(t_{i},a)$
$\displaystyle=\hat{\nu}(t_{i},a)\text{~{}for~{}}a\in\mathsf{At}$
$\displaystyle\hat{\nu}(t_{i},\neg\phi)$
$\displaystyle=\left\\{\begin{array}[]{ll}1&\text{if~{}}\hat{\nu}(t_{i},\phi)=0\\\
0&\text{if~{}}\hat{\nu}(t_{i},\phi)=1\\\
\text{B}&\text{if~{}}\hat{\nu}(t_{i},\phi)=\text{B}\end{array}\right.$
$\displaystyle\hat{\nu}(t_{i},\varphi_{1}\wedge\varphi_{2})$
$\displaystyle=\left\\{\begin{array}[]{ll}1&\text{if~{}}\hat{\nu}(t_{i},\varphi_{1})=\hat{\nu}(t_{i},\varphi_{2})=1\\\
0&\text{if~{}}\hat{\nu}(t_{i},\varphi_{1})=0\text{~{}or~{}}\hat{\nu}(t_{i},\varphi_{2})=0\\\
\text{B}&\text{otherwise}\end{array}\right.$
$\displaystyle\hat{\nu}(t_{i},\varphi_{1}\vee\varphi_{2})$
$\displaystyle=\left\\{\begin{array}[]{ll}1&\text{if~{}}\hat{\nu}(t_{i},\varphi_{1})=1\text{~{}or~{}}\hat{\nu}(t_{i},\varphi_{2})=1\\\
0&\text{if~{}}\hat{\nu}(t_{i},\varphi_{1})=\hat{\nu}(t_{i},\varphi_{2})=0\\\
\text{B}&\text{otherwise}\end{array}\right.$
$\displaystyle\hat{\nu}(t_{i},\textbf{X}\varphi)$
$\displaystyle=\left\\{\begin{array}[]{ll}\hat{\nu}(t_{i+1},\varphi)&\text{if~{}}i<m\\\
0&\text{otherwise}\end{array}\right.$
$\displaystyle\hat{\nu}(t_{i},\varphi_{1}\textbf{U}\varphi_{2})$
$\displaystyle=\left\\{\begin{array}[]{ll}1&\text{if there
is~{}}j\in\\{i+1,\ldots,m\\}\text{ with}\\\
&\hat{\nu}(t_{j},\varphi_{2})=\hat{\nu}(t_{i},\varphi_{1})=\ldots\\\
&=\hat{\nu}(t_{j-1},\varphi_{1})=1\\\ \text{B}&\text{if there
is~{}}j\in\\{i+1,\ldots,m\\}\text{ with}\\\
&\\{\hat{\nu}(t_{j},\varphi_{2}),\hat{\nu}(t_{i},\varphi_{1}),\ldots,\\\
&\hat{\nu}(t_{j-1},\varphi_{1})\\}=\\{1,\text{B}\\}\\\
0&\text{otherwise}\end{array}\right.$

Some comments on the above definition are in order. First, note that the
evaluation of the classical Boolean connectives is the same as for
propositional three-valued semantics (see Section 2.1). Furthermore, the
evaluation of $\textbf{X}\phi$ is simply the truth value of $\phi$ at the next
state, or, if there is no next state, $0$ (as for the classical semantics of
LTL${}_{\text{ff}}$). The main new feature, however, is the three-valued
evaluation of a formula of the form $\varphi_{1}\textbf{U}\varphi_{2}$. This
formula evaluates to $1$ as in the classical case, i. e., if $\phi_{2}$
evaluates to $1$ in some future state and $\phi_{1}$ evaluates to $1$ in
between. We evaluate $\varphi_{1}\textbf{U}\varphi_{2}$ to B if $\phi_{2}$
evaluates to $1$ or B in some future state and $\phi_{1}$ evaluates to $1$ or
B in between (and at least one of these evaluations must be to B). Finally,
$\varphi_{1}\textbf{U}\varphi_{2}$ evaluates to $0$ otherwise, i.e., if either
$\phi_{2}$ always evaluates to $0$ in the future or in-between $\varphi_{1}$
evaluates at least once to $0$.

A three-valued LTL${}_{\text{ff}}$ interpretation $\hat{\nu}$ satisfies a
formula $\phi$, denoted by $\hat{\nu}\models^{3}\phi$, iff
$\hat{\nu}(\phi,t_{0})\in\\{1,\text{B}\\}$. A three-valued interpretation
$\hat{\nu}$ satisfies a set of formulas $\mathcal{K}$ iff
$\hat{\nu}\models^{3}\phi$ for all $\phi\in\mathcal{K}$.

###### Example 3

Let $\mathsf{At}=\\{a,b\\}$ and assume $m=2$. Consider the knowledge base
$\mathcal{K}$ defined via

$\displaystyle\mathcal{K}$ $\displaystyle=\\{\textbf{X}\neg a,a\textbf{U}b\\}$

and the three-valued interpretation $\hat{\nu}$ defined via

$\displaystyle\hat{\nu}(t_{0},a)$ $\displaystyle=1$
$\displaystyle\hat{\nu}(t_{0},b)$ $\displaystyle=0$
$\displaystyle\hat{\nu}(t_{1},a)$ $\displaystyle=\text{B}$
$\displaystyle\hat{\nu}(t_{1},b)$ $\displaystyle=0$
$\displaystyle\hat{\nu}(t_{2},a)$ $\displaystyle=0$
$\displaystyle\hat{\nu}(t_{2},b)$ $\displaystyle=1$

Then we have $\hat{\nu}(t_{0},a\textbf{U}b)=\text{B}$ as $b$ evaluates to $1$
in $t_{2}$ and $a$ evaluates to B in $t_{1}$. Moreover, we have
$\hat{\nu}(t_{0},\textbf{X}\neg a)=\text{B}$ and therefore
$\hat{\nu}\models^{3}\mathcal{K}$.

Define $X\models^{3}Y$ for formulas $X$ and $Y$ if $\hat{\nu}\models X$
implies $\hat{\nu}\models Y$ for all $\hat{\nu}$.

In the propositional logic case, $\models^{3}$ is a faithful extension of
$\models$, meaning that $\omega\models\phi$ if and only if
$\omega\models^{3}\phi$ for every two-valued interpretation $\omega$ and every
$\phi$. Our LTL${}_{\text{ff}}$ extension of the three-valued semantics enjoys
the same property (note that every two-valued interpretation is a also a
three-valued interpretation that does not use the value B).

###### Proposition 2

For every (two-valued) LTL${}_{\text{ff}}$ interpretation $\hat{\omega}$ and
LTL${}_{\text{ff}}$ formula $\phi$, $\hat{\omega}\models\phi$ if and only if
$\hat{\omega}\models^{3}\phi$.

The three-valued semantics of [21] has another nice property in propositional
logic, namely the non-existence of inconsistency: every propositional formula
is trivially satisfiable by the interpretation that assigns B to all
propositions. In general, an LTL${}_{\text{ff}}$ formula may become
unsatisfiable w.r.t. to the three-valued semantics if it affects a state
”beyond“ $t_{m}$. However, for other formulas we obtain the following result
regarding universal satisfiability.

###### Proposition 3

For any LTL${}_{\text{ff}}$ formula $\phi$ with $d(\phi)\leq m$ there is
$\hat{\nu}$ with $\hat{\nu}\models^{3}\phi$.

The semantics presented in this section allows for inconsistency-tolerant
reasoning in LTL${}_{\text{ff}}$ (and it can straightforwardly be adapted for
LTL${}_{\text{f}}$ and LTL). This provides a useful tool for the usual
application scenarios of temporal logics, such as model checking and
verification. While it may be worthwhile to investigate this aspect in more
depth, in the remainder of this work we will focus on the application of this
semantics for inconsistency measurement and postpone that endeavour to future
work.

###  3.3 Time Sensitive Inconsistency Measures for LTL${}_{\text{ff}}$

We will now exploit our three-valued semantics for LTL${}_{\text{ff}}$ to
define some new inconsistency measures. We do this similarly as for
propositional logic by assessing the amount of usage of the paraconsistent
truth value B in models of an LTL${}_{\text{ff}}$ knowledge base $\mathcal{K}$
but refine it by two different levels of granularity. This yields two new
inconsistency measures.

Our first approach measures the number of states affected by inconsistency.
For any three-valued interpretation $\hat{\nu}$, define

$\displaystyle\textsf{AffectedStates}(\hat{\nu})$
$\displaystyle=\\{t\mid\exists a:\hat{\nu}(t,a)=\text{B}\\}$

In other words, $\textsf{AffectedStates}(\hat{\nu})$ is the set of states
where $\hat{\nu}$ assigns B to at least one proposition. We can define an
inconsistency measure by considering those 3-valued models of the knowledge
base that affect the minimal number of states.

######  Definition 4 (LTL time measure)

Let $\mathcal{K}$ be a set of formulas. Then, the LTL time measure is defined
via

$\displaystyle\mathcal{I}^{LTL}_{d}(\mathcal{K})$
$\displaystyle=\min_{\hat{\nu}\models^{3}\mathcal{K}}|\textsf{AffectedStates}(\hat{\nu})|$

if there is $\hat{\nu}$ with $\hat{\nu}\models^{3}\mathcal{K}$ and
$\mathcal{I}^{LTL}_{d}(\mathcal{K})=\infty$ otherwise.

This measure counts the number of states for which the knowledge base is
inconsistent. It is, in fact, the extension of the drastic measure,
$\mathcal{I}_{d}$, in that for each state it adds $1$ if there is an
inconsistency and $0$ otherwise. This measure can be used to distinguish the
knowledge bases $\mathcal{K}_{1}$ and $\mathcal{K}_{2}$, i.e., it is time
sensitive.

###### Example 4

We recall the knowledge bases $\mathcal{K}_{1}=\\{\textbf{X}a,\textbf{X}\neg
a\\}$ and $\mathcal{K}_{2}=\\{\textbf{G}a,\textbf{G}\neg a\\}$. Then we have

$\displaystyle\mathcal{I}^{LTL}_{d}(\mathcal{K}_{1})=1$
$\displaystyle\mathcal{I}^{LTL}_{d}(\mathcal{K}_{2})=m$

As an example where there is no $\hat{\nu}$ s.t.
$\hat{\nu}\models^{3}\mathcal{K}$, consider the formula
$\textbf{X}\textbf{X}\textbf{X}a$. This formula cannot be satisfied for $m=2$,
so $\mathcal{I}^{LTL}_{d}$ would return $\infty$ here.

Example 4 shows that the proposed measure $\mathcal{I}^{LTL}_{d}$ can already
provide meaningful insights for measuring inconsistency in LTL. But a
potential limitation is that it can only distinguish inconsistency in
individual states in a binary manner. For example, $\mathcal{I}^{LTL}_{d}$
cannot distinguish the knowledge base
$\mathcal{K}_{4}=\\{\textbf{X}a,\textbf{X}\neg a,\textbf{X}b,\textbf{X}\neg
b\\}$ from $\mathcal{K}_{1}$ because all inconsistencies occur at one state,
namely $t_{1}$. For this reason we believe it is useful to be able to look
inside states for inconsistency. In order to do so, given a three-valued
interpretation $\hat{\nu}$, define

$\displaystyle\textsf{Conflictbase}(\hat{\nu})$
$\displaystyle=\\{(t,a)\mid\hat{\nu}(t,a)=\text{B}\\}$

Then, define the LTL contension measure as follows.

######  Definition 5 (LTL contension measure)

Let $\mathcal{K}$ be a set of formulas and

$\displaystyle\mathcal{I}^{LTL}_{c}(\mathcal{K})$
$\displaystyle=\min_{\hat{\nu}\models^{3}\mathcal{K}}|\textsf{Conflictbase}(\hat{\nu})|$

if there is $\hat{\nu}$ with $\hat{\nu}\models^{3}\mathcal{K}$ and
$\mathcal{I}^{LTL}_{c}(\mathcal{K})=\infty$ otherwise.

$\mathcal{I}^{LTL}_{c}$ seeks an interpretation that assigns B to a minimal
number of propositions individually over all the states and uses this number
for the inconsistency measure. This is an extension of
$\mathcal{I}^{LTL}_{d}$, and for that matter, of $\mathcal{I}_{c}$ as it
calculates $\mathcal{I}^{LTL}_{c}$ for each state and sums the numbers
obtained this way.

###### Example 5

We recall the knowledge bases $\mathcal{K}_{1}=\\{\textbf{X}a,\textbf{X}\neg
a\\}$, $\mathcal{K}_{4}=\\{\textbf{X}a,\textbf{X}\neg a,$
$\textbf{X}b,\textbf{X}\neg b\\}$, and consider
$\mathcal{K}_{5}=\\{\textbf{G}a,\textbf{G}\neg a,\textbf{G}b,\textbf{G}\neg
b\\}$. If $m=3$, then we have

$\displaystyle\mathcal{I}^{LTL}_{d}(\mathcal{K}_{1})=1$
$\displaystyle\mathcal{I}^{LTL}_{d}(\mathcal{K}_{4})=1$
$\displaystyle\mathcal{I}^{LTL}_{d}(\mathcal{K}_{5})=3$
$\displaystyle\mathcal{I}^{LTL}_{c}(\mathcal{K}_{1})=1$
$\displaystyle\mathcal{I}^{LTL}_{c}(\mathcal{K}_{4})=2$
$\displaystyle\mathcal{I}^{LTL}_{c}(\mathcal{K}_{5})=6$

As can be seen in Example 5, the two inconsistency measures proposed in this
work can, contrary to previously existing measures, be used to provide
meaningful insights into inconsistency in linear temporal logic, i.e., they
are in fact time sensitive. As the two measures have a different granularity
in regard to time, selecting which of the two to use depends on the intended
use case.

Intuitively, it would be possible to devise further time-sensitive
inconsistency measures for LTL${}_{\text{ff}}$. We will however leave this
discussion for future work. Importantly, the aim of this paper is to show that
traditional inconsistency measures cannot be plausibly applied to temporal
logics, and to present means for time sensitive inconsistency measurement. In
this regard, the measures proposed in this work can be used as a baseline for
measuring inconsistency in LTL. Also, they (broadly) satisfy other desirable
properties and can therefore be seen as strictly better (w.r.t. the considered
postulates) than their propositional logic “counterpart”, i.e.,
$\mathcal{I}_{d}$ for $\mathcal{I}^{LTL}_{d}$, respectively $\mathcal{I}_{c}$
for $\mathcal{I}^{LTL}_{c}$ . The results of this section are summarized in
Table 3. Proofs can be found in the Appendix.

$\mathcal{I}$ | CO | MO | IN | DO | TS
---|---|---|---|---|---
$\mathcal{I}_{d}$ | ✓ | ✓ | ✓ | ✓ | ✗
$\mathcal{I}_{\mathsf{MI}}$ | ✓ | ✓ | ✓ | ✗ | ✗
$\mathcal{I}_{p}$ | ✓ | ✓ | ✓ | ✗ | ✗
$\mathcal{I}_{r}$ | ✓ | ✓ | ✓ | ✗ | ✗
$\mathcal{I}_{c}$ | ✓ | ✓ | ✗ | ✓ | ✗
$\mathcal{I}_{at}$ | ✓ | ✗ | ✗ | ✗ | ✗
$\mathcal{I}^{LTL}_{d}$ | ✓ | ✓ | ✓ | ✓ | ✓
$\mathcal{I}^{LTL}_{c}$ | ✓ | ✓ | ✗ | ✓ | ✓
Table 1: Compliance of inconsistency measures with rationality postulates.

Note that only the measures we introduced satisfy TS. Note also that
$\mathcal{I}^{LTL}_{c}$ does not satisfy IN due to the problem of iceberg
inconsistencies, cf. the provided proofs.

##  4 Application to Declarative Process Models

A common application scenario for LTL${}_{\text{f}}$ is that of declarative
process models [18], which are sets of (LTL-based) constraints. For such
declarative process models, the issue of inconsistency is equally as
problematic, as any inconsistencies between the constraints make the
declarative process model unsatisfiable.

There have been a number of works addressing the issue of inconsistency in
declarative process models [4, 16, 2]. However, those works mainly look at
whether a process model is inconsistent at all (in a binary manner), or try to
identify sets of inconsistent constraints. Those works can however not look
“into” those sets or assess their severity. For this use case, our proposed
approach can be extended to declarative process models as follows.

###  4.1 Inconsistency Measurement in Declarative Process Models

A declarative process model consists of a set of constraints. Typically, these
constraints are constructed using predefined templates, i. e., predicates,
that are specified relative to a set of propositions (e. g., company
activities).

######  Definition 6 (Declarative Process Model)

A declarative process model is a tuple
$\textbf{M}=(\textbf{A},\textbf{T},\textbf{C})$, where A is a set of
propositions, T is a set of constraint types, and C is the set of constraints,
which instantiate the template elements in T with activities in A.000For
readability, we will denote declarative process models as a set of constraints
(C)

In this work, we consider the declarative modelling language Declare [18],
which offers a set of “standard” templates. We will use a selection of
templates shown in Table 2. We refer the reader to [4] for an overview of
other Declare template types and corresponding semantics.

Template | LTL${}_{\text{ff}}$ Semantics
---|---
Init(a) | a
End(a) | $\textbf{G}(a\vee\textbf{F}a)$
Response(a,b) | $\textbf{G}(a\rightarrow\textbf{F}b)$
NotResponse(a,b) | $\textbf{G}(a\rightarrow\neg\textbf{F}b)$
ChainResponse(a,b) | $\textbf{G}(a\rightarrow\textbf{X}b)$
NotChainResponse(a,b) | $\textbf{G}(a\rightarrow\neg\textbf{X}b)$
AtLeast(a,_n_) | $\textbf{F}(a\wedge\textbf{X}(\text{atLeast}(a,\text{\emph{n}-1}))),\text{atLeast}(a,1)=a\vee\textbf{F}(a)$
AtMost(a,_n_) | $\textbf{G}(\neg a\vee\textbf{X}(\text{atMost}(a,\text{\emph{n}}-1))),\text{atMost}(a,0)=\textbf{G}(\neg a)$
Table 2: LTL${}_{\text{ff}}$ Semantics for a selection of Declare templates.

By rewriting the constraints of a declarative process model into
LTL${}_{\text{ff}}$ formulas, our approach for measuring inconsistency in
LTL${}_{\text{ff}}$ can be applied to Declare in a straightforward manner.

###### Example 6

Consider the sets of constraints $C_{a}$ and $C_{b}$, defined via

$\displaystyle C_{a}$
$\displaystyle=\\{\textsc{Init}(a),\textsc{Response}(a,b),\textsc{NotResponse}(a,b)\\}$
$\displaystyle(\Leftrightarrow\\{a,\textbf{G}(a\rightarrow\textbf{F}b),\textbf{G}(a\rightarrow\neg\textbf{F}b)\\})$
$\displaystyle C_{b}$
$\displaystyle=\\{\textsc{Init}(a),\textsc{Response}(a,b),\textsc{NotResponse}(a,b),$
$\displaystyle\qquad\textsc{Response}(a,c),\textsc{NotResponse}(a,c)\\}$
$\displaystyle(\Leftrightarrow\\{a,\textbf{G}(a\rightarrow\textbf{F}b),\textbf{G}(a\rightarrow\neg\textbf{F}b),\textbf{G}(a\rightarrow\textbf{F}c),\textbf{G}(a\rightarrow\neg\textbf{F}c)\\})$

then we have that $\mathcal{I}^{LTL}_{c}(C_{a})=1$ and
$\mathcal{I}^{LTL}_{c}(C_{b})=2$.

Due to the recursive definition of some “existence” constraints (cf. Table 2),
note that also inconsistencies concerned with cardinalities can be assessed
correctly.

###### Example 7

Consider $C_{c}=\\{\textsc{AtMost}(a,1)$, $\textsc{AtLeast}(a,2)\\}$ and
$C_{d}=\\{\textsc{AtMost}(a,1)$, $\textsc{AtLeast}(a,100)\\}$, then
$\mathcal{I}^{LTL}_{d}(C_{c})<\mathcal{I}^{LTL}_{d}(C_{d})$.

As a border case, note that any inconsistency referring to a point in time
beyond the assumed sequence of states will return a value of $\infty$ per
definition, as we cannot assess any error that leaves the boundaries of our
logical framework.

###### Example 8

Let $C_{e}=\\{\textsc{End}(a),\textsc{ChainResponse}(a,b)\\}$, then
$\mathcal{I}^{LTL}_{d}(C_{e})=\infty$.

These examples show that our approach can provide detailed insights on the
severity of inconsistency in declarative process models. Such insights can
prove useful for prioritizing or re-modelling different issues of the process
specification. In this context, it seems intuitive that conflicts affecting
only the next state (X) should be considered as less severe than conflicts
affecting multiple following states (G), i. e., for any LTL${}_{\text{ff}}$
formula $\varphi$,
$\mathcal{I}(\\{\textbf{G}\varphi,\textbf{G}\neg\varphi\\})>\mathcal{I}(\\{\textbf{X}\varphi,\textbf{X}\neg\varphi\\})$.
In this regard, there are still open questions on how to distinguish the
operators X and F, in particular: for an LTL${}_{\text{ff}}$ formula
$\varphi$, what is the relation between
$\mathcal{I}(\\{\textbf{X}\varphi,\neg\textbf{X}\varphi\\})$ and
$\mathcal{I}(\\{\textbf{F}\varphi,\neg\textbf{F}\varphi\\})$? We address this
question in the following.

###  4.2 On Potentially Inconsistent States

Consider the following sets of constraints $C_{m}$ and $C_{n}$, defined via

$\displaystyle C_{m}=$ $\displaystyle C_{n}=$
$\displaystyle\\{\textsc{Init}(a)\Leftrightarrow a,$
$\displaystyle\\{\textsc{Init}(a),$
$\displaystyle\textsc{Response}(a,b)\Leftrightarrow\textbf{G}(a\rightarrow\textbf{F}b),$
$\displaystyle\textsc{ChainResponse}(a,b)\Leftrightarrow\textbf{G}(a\rightarrow\textbf{X}b),$
$\displaystyle\textsc{NotResponse}(a,b)\Leftrightarrow\textbf{G}(a\rightarrow\neg\textbf{F}b)\\}$
$\displaystyle\textsc{NotChainResponse}(a,b)\Leftrightarrow\textbf{G}(a\rightarrow\neg\textbf{X}b)\\}$

Both sets are inconsistent, as they demand that $b$ should and should not
follow. However, the point in time at which the actual inconsistency can occur
is different. Naturally, one question arises: which inconsistency is more
severe? Or are they equally severe? We encourage the reader to come up with an
own answer to this question at this point before we continue with our view on
this matter.

Using the measures introduced in this work, the absolute number of affected
states is 1 in both cases. So regarding the minimal number of affected states,
the inconsistencies are equally severe. However, the certainty of where the
inconsistency can occur at is clearly different, as visualized in Figure 1.

_a_?…? (a) Potentially inconsistent states for $C_{m}$

_a_ ↯A… (b) Certainty of inconsistency for $C_{n}$

Figure 1: Visualization of the (un)certainty of where the inconsistency may
occur for $C_{m}$ and $C_{n}$.

In $C_{m}$, there are $m$ different possible states to which a minimal
interpretation could assign the truth value B to the proposition $b$, whereas
the inconsistency can only occur in exactly 1 state for $C_{n}$. This could
entail different severities for the inconsistencies, depending on the
viewpoint:

Consider a running process which is in state $t_{0}$. For $C_{m}$, it is
unclear when the inconsistency will occur. For $C_{n}$, it is directly known
that the next state is inconsistent. Recovery mechanisms for such cases are
well known [15], e. g., it would be possible to just skip the next state and
continue with a consistent process. This is not possible for $C_{m}$ without
skipping all following states until the end of the process. So one might argue
that the inconsistency in $C_{m}$ is more severe. However, for $C_{n}$, this
also means there is in fact no possible continuation as the process is in a
dead-end state, thus, $C_{n}$ needs to be attended to more urgently (So one
might as well argue that the inconsistency in $C_{n}$ is more severe).

In the field of inconsistency measurement, the dominance property states that
substituting a consistent formula by a weaker formula cannot increase the
inconsistency value [12]. However, when moving from $C_{m}$ to $C_{n}$ or
vice-versa, we both replace one constraint with a stronger one and the other
with a weaker one (every ChainResponse is also a Response but every
NotResponse is a NotChainResponse). So the dominance property is not
applicable here and the question remains which inconsistency is more severe.
In this work, we will not give a definitive answer to this question and leave
this discussion for future work. However, based on the two possible views
given above, we will argue that they are, in fact, different. It would
therefore be desirable to be able to distinguish the inconsistency in $C_{m}$
and $C_{n}$. Here, the introduced contension concept can be adapted to
quantify the certainty of _when_ the inconsistency will occur.

The introduced measures quantify inconsistency by seeking an interpretation
that assigns B to a minimal number of states. We denote the set of all such
interpretations that assign B to a minimal number of states (at least to one)
as

$\displaystyle\hat{V}_{\textsf{min}}^{B>0}(\mathcal{K})$
$\displaystyle=\\{\hat{\nu}\models^{3}\mathcal{K}:|\textsf{AffectedStates}(\hat{\nu})|>0\wedge|\textsf{AffectedStates}(\hat{\nu})|=\mathcal{I}^{LTL}_{d}(\mathcal{K})\\}$

Every such (minimal) interpretation also encodes which exact states are
affected by the inconsistency. For $C_{n}$, only one state is necessarily
affected (cf. Fig 1 (b)), thus, there exists only one minimal interpretation.
For $C_{m}$, there are $m$ different interpretations that are all equally
minimal in terms of how many states are affected. So the number of minimal
interpretations relates to the number of distinct (sets of) states that can
potentially be affected.

######  Definition 7 (Number of Minimal Interpretations)

Let $\mathcal{K}$ be a set of formulas. Then, define the number of minimal
interpretations via

$\displaystyle\textsf{\\#minInterpretations}(\mathcal{K})=|\hat{V}_{\textsf{min}}^{B>0}(\mathcal{K})|$

###### Example 9

We recall $C_{m}$ and $C_{n}$. Then we have that
$\textsf{\\#minInterpretations}(C_{m})=m$ and
$\textsf{\\#minInterpretations}(C_{n})=1$ as expected (cf. the above
discussion)

Importantly, the function #minInterpretations is not an inconsistency measure,
i. e., a higher value does not indicate a higher degree of inconsistency. It
therefore also does not matter where the inconsistency in $C_{m}$ eventually
triggers. The value merely expresses the “certainty” of knowing where the
conflict can occur at. The semantics of which is worse depends on the use
case.

##  5 Computational Complexity

We conclude with an investigation of computational complexity in measuring
inconsistency in LTL. We assume familiarity with computational complexity, see
[17] for an introduction. Proofs can be found in the Appendix.

Note that deciding satisfiability is PSPACE-complete for LTL${}_{\text{f}}$
[6] and also intractable for many variants of LTL${}_{\text{f}}$ [5]. For our
variant LTL${}_{\text{ff}}$, as $m$ is fixed, we get NP-completeness (think
for example of a non-deterministic algorithm that guesses $\hat{\omega}$ and
verifies (in polynomial time) that $\hat{\omega}\models\phi$).

###### Theorem 5.1

Deciding whether a formula $\phi$ is satisfiable in LTL${}_{\text{ff}}$ is NP-
complete.

If the parameter $m$ is given in unary, the complexity result holds as it is.
However, if $m$ is given in binary then the complexity will likely increase
(in the membership proof, we need to guess an interpretation and if m is given
in binary, that interpretation may be exponential in the size of the input).

We continue with an investigation of the computational complexity of measuring
inconsistency in LTL. For this, let $\mathbb{L}$ denote the set of all
LTL${}_{\text{ff}}$ knowledge bases. Following [26], we consider the following
computational problems:

ExactI |  Input: |  $\mathcal{K}\in\mathbb{L}$, $x\in\mathbb{R}^{\infty}_{\geq 0}$
---|---|---
|  Output: |  true iff $\mathcal{I}(\mathcal{K})=x$
UpperI |  Input: |  $\mathcal{K}\in\mathbb{L}$, $x\in\mathbb{R}^{\infty}_{\geq 0}$
|  Output: |  true iff $\mathcal{I}(\mathcal{K})\leq x$
LowerI |  Input: |  $\mathcal{K}\in\mathbb{L}$, $x\in\mathbb{R}^{\infty}_{\geq 0}\setminus\\{0\\}$
|  Output: |  true iff $\mathcal{I}(\mathcal{K})\geq x$
ValueI |  Input: |  $\mathcal{K}\in\mathbb{L}$
|  Output: | The value of $\mathcal{I}(\mathcal{K})$

For UpperI, the same general non-deterministic algorithm can be applied.

###### Theorem 5.2

Upper${}_{\mathcal{I}^{LTL}_{d}}$ and Upper${}_{\mathcal{I}^{LTL}_{c}}$ are
NP-complete.

Using the results in [26] we also get the following results for the other
problems.

###### Corollary 1

Lower${}_{\mathcal{I}^{LTL}_{d}}$ and Lower${}_{\mathcal{I}^{LTL}_{c}}$ are
coNP-complete. Exact${}_{\mathcal{I}^{LTL}_{d}}$ and
Exact${}_{\mathcal{I}^{LTL}_{c}}$ are in DP. Value${}_{\mathcal{I}^{LTL}_{d}}$
and Value${}_{\mathcal{I}^{LTL}_{c}}$ are in $\textsf{FP}^{\textsf{NP}[\log
n]}$.

In regard to the algorithmic implementation of our approach, a general
approach of SAT encodings can be used. Corollary 1 gives a straightforward
implementation for an algorithm to compute the measures by combining binary
search with iterative calls to a SAT solver using an encoding of the problem
Upper (see proof of Corollary 1). This encoding would be based on a SAT
encoding for LTL${}_{\text{ff}}$ satisfiability, which is straightforward.

##  6 Conclusion

In this work, we have presented an approach for measuring the severity of
inconsistencies in declarative process specifications, in particular those
based on linear temporal logic. In this regard, we introduced a paraconsistent
semantics for LTL${}_{\text{ff}}$ and developed two inconsistency measures.
This provides useful insights for debugging or re-modelling LTL${}_{\text{f}}$
specifications, e. g., by allowing to compare or prioritize different
inconsistencies. Here, our approach extends recent works [4, 2, 22] on the
identification of inconsistent sets in declarative process specifications by
allowing a look “into” those sets.

In future work, we aim to investigate the application of our approach to other
languages such as GSM or DCR. Note that this is however not trivial, as the
process models there might not be represented as orthogonal formulas. As a
further limitation of our work, the current approach treats time as discrete
time steps where any number of activities (within the bounds of the
constraints) are allowed to occur at the same time. Real processes may however
contain activities that take real time and may not be parallelizable because
of resource constraints. As a result, a logically equivalent inconsistency may
weigh more than another. In future work, we aim to address this issue with
data-aware versions of LTL${}_{\text{ff}}$.

## References

  * [1] Cecconi, A., De Giacomo, G., Di Ciccio, C., Maggi, F.M., Mendling, J.: A temporal logic-based measurement framework for process mining. In: Proceedings of the 2nd ICPM. pp. 113–120. IEEE (2020)
  * [2] Corea, C., Nagel, S., Mendling, J., Delfmann, P.: Interactive and minimal repair of declarative process models. In: BPM Forum, Rome. pp. 3–19. Springer (2021)
  * [3] De Bona, G., Hunter, A.: Localizing iceberg dependencies. Artificial Intelligence 246, 118–151 (2017)
  * [4] Di Ciccio, C., Maggi, F.M., Montali, M., Mendling, J.: Resolving inconsistencies and redundancies in declarative process models. Inf. Systems 64, 425–446 (2017)
  * [5] Fionda, V., Greco, G.: The compl. of LTL on finite traces: Hard and easy fragments. In: Proc. of the 30th AAAI Conference on AI, Phoenix. pp. 971–977. AAAI (2016)
  * [6] Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the 23rd IJCAI, Beijing. pp. 854–860. AAAI (2013)
  * [7] Grant, J.: Measuring inconsistency in some branching time logics. Journal of Applied Non-Classical Logics 31, 85–107 (2021)
  * [8] Grant, J., Hunter, A.: Measuring consistency gain and inf. loss in stepwise inc. resolution. In: Proc. of the 11th ECSQARU, Belfast. pp. 362–373. Springer (2011)
  * [9] Grant, J., Martinez, M.V.: Measuring Inc. in Information. College Pub. (2018)
  * [10] Hildebrandt, T., Mukkamala, R.R., Slaats, T., Zanitti, F.: Contracts for cross-organizational workflows as timed dynamic condition response graphs. The Journal of Logic and Algebraic Programming 82(5-7), 164–185 (2013)
  * [11] Hunter, A., Konieczny, S.: On the measure of conflicts: Shapley inconsistency values. Artificial Intelligence 174(14), 1007–1026 (2010)
  * [12] Hunter, A., Konieczny, S., et al.: Shapley inc. values. KR 6, 249–259 (2006)
  * [13] Hunter, A., Konieczny, S., et al.: Measuring inconsistency through minimal inconsistent sets. KR 8, 358–366 (2008)
  * [14] Knight, K.: Measuring inconsistency. Journal of Phil. Logic 31(1), 77–98 (2002)
  * [15] Ly, L.T., Maggi, F.M., Montali, M., Rinderle-Ma, S., van der Aalst, W.M.: A framework for the systematic comparison and evaluation of compliance monitoring approaches. In: 17th IEEE EDOC, Vancouver. pp. 7–16. IEEE (2013)
  * [16] Maggi, F.M., Westergaard, M., Montali, M., van der Aalst, W.M.: Runtime verification of ltl-based declarative process models. In: Proceedings of the 2nd RV, San Francisco. pp. 131–146. Springer (2011)
  * [17] Papadimitriou, C.: Computational Complexity. Addison-Wesley (1994)
  * [18] Pesic, M., Schonenberg, H., Van der Aalst, W.M.: Declare: Full support for loosely-structured processes. In: 11th IEEE EDOC, Annapolis. pp. 287–287. IEEE (2007)
  * [19] Pill, I., Quaritsch, T.: Behavioral diagnosis of ltl specifications at operator level. In: 23rd International Joint Conference on Artificial Intelligence. Citeseer (2013)
  * [20] Pnueli, A.: The temporal logic of programs. In: 18th Symposium on Foundations of Computer Science, Rhode Island. pp. 46–57. IEEE Computer Society (1977)
  * [21] Priest, G.: Logic of Paradox. Journal of Phil. Logic 8, 219–241 (1979)
  * [22] Roveri, M., Di Ciccio, C., Di Francescomarino, C., Ghidini, C.: Computing unsatisfiable cores for LTLf specifications (Preprint). arXiv (2022)
  * [23] Solomakhin, D., Montali, M., Tessaris, S., Masellis, R.D.: Verification of artifact-centric systems. In: Proceedings of the 11th ICSOC. pp. 252–266. Springer (2013)
  * [24] Thimm, M.: On the evaluation of inconsistency measures. In: Grant, J., Martinez, M.V. (eds.) Measuring Inconsistency in Information. College Publications (February 2018)
  * [25] Thimm, M.: Inconsistency measurement. In: Proceedings of the 13th International Conference on Scalable Uncertainty Management, Compiègne. Springer (2019)
  * [26] Thimm, M., Wallner, J.P.: On the complexity of inc. meas. AI 275, 411–456 (2019)
  * [27] Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Proceedings of the 7th TACAS, Italy. pp. 1–22. Springer (2001)

##  Appendix: Proofs for Technical Results

###### Proposition 2

For every (two-valued) LTL${}_{\text{ff}}$ interpretation $\hat{\omega}$ and
LTL${}_{\text{ff}}$ formula $\phi$, $\hat{\omega}\models\phi$ if and only if
$\hat{\omega}\models^{3}\phi$.

###### Proof

Let $\hat{\omega}$ be any two-valued LTL${}_{\text{ff}}$ interpretation. First
observe that using three-valued semantics,
$\hat{\omega}(t_{i},\phi)\neq\text{B}$ for every $\phi$ (this can be easily
verified by structural induction since no atom has the value B). We prove now
the more general statement that $\hat{\omega},t_{i}\models\phi$ if and only if
$\hat{\omega}(t_{i},\phi)=1$ for any $t_{i}$ by induction on the structure of
$\phi$:

  * •

$\phi=a$ for $a\in\mathsf{At}$: From $\hat{\omega},t_{i}\models\phi$ it
follows $\hat{\omega}(t_{i},a)=1$ via classical semantics, which is equivalent
to $\hat{\omega}(t_{i},a)=1$ via 3-valued semantics.

  * •

$\phi=\neg\psi$: We have $\hat{\omega},t_{i}\models\neg\psi$ iff
$\hat{\omega},t_{i}\not\models\psi$. By the induction hypothesis, this is
equivalent to $\hat{\omega}(t_{i},\psi)=0$. This is equivalent to
$\hat{\omega}(t_{1},\neg\psi)=1$.

  * •

$\phi=\phi_{1}\wedge\phi_{2}$: We have that
$\hat{\omega},t_{i}\models\phi_{1}\wedge\phi_{2}$ is equivalent to
$\hat{\omega},t_{i}\models\phi_{1}$ and $\hat{\omega},t_{i}\models\phi_{2}$.
By the induction hypothesis, this is equivalent to
$\hat{\omega}(t_{i},\phi_{1})=1$ and $\hat{\omega}(t_{i}\phi_{2})=1$. This is
equivalent to $\hat{\omega}(t_{i},\phi)=1$.

  * •

$\phi=\phi_{1}\vee\phi_{2}$: We have that
$\hat{\omega},t_{i}\models\phi_{1}\vee\phi_{2}$ is equivalent to
$\hat{\omega},t_{i}\models\phi_{1}$ or $\hat{\omega},t_{i}\models\phi_{2}$.
Without loss of generality assume $\hat{\omega},t_{i}\models\phi_{1}$. By the
induction hypothesis, this is equivalent to $\hat{\omega}(t_{i},\phi_{1})=1$
which implies $\hat{\omega}(t_{i},\phi)=1$. This other direction is analogous.

  * •

$\phi=\textbf{X}\psi$: Observe first that for $i\geq m$ both
$\hat{\omega},t_{i}\not\models\phi$ and $\hat{\omega}(t_{i},\phi)=0$ hold. So
assume that $i<m$. Then we have $\hat{\omega},t_{i}\models\textbf{X}\psi$
equivalent to $\hat{\omega},t_{i+1}\models\psi$. By the induction hypothesis,
this is equivalent to $\hat{\omega}(t_{i+1},\psi)=1$ and
$\hat{\omega}(t_{i},\textbf{X}\psi)=1$.

  * •

$\phi=\varphi_{1}\textbf{U}\varphi_{2}$: Assume that
$\hat{\omega},t_{i}\models\varphi_{1}\textbf{U}\varphi_{2}$. Then there is
some $j\in\\{i+1,\ldots,m\\}$ with $\hat{\omega},t_{j}\models\phi_{2}$ and
$\hat{\omega},t_{k}\models\phi_{1}$ for all $k\in\\{i,\ldots,j-1\\}$. By the
induction hypothesis, this amounts to $\hat{\omega}(t_{j},\phi_{2})=1$ and
$\hat{\omega}(t_{k},\phi_{1})=1$ for all $k\in\\{i,\ldots,j-1\\}$. From this
follows $\hat{\omega}(t_{i},\phi_{1}\textbf{U}\phi_{2})=1$. The other
direction is analogous.

###### Proposition 3

For every LTL${}_{\text{ff}}$ formula $\phi$ with $d(\phi)\leq m$ there is a
$\hat{\nu}$ with $\hat{\nu}\models^{3}\phi$.

###### Proof

Let $\hat{\nu}_{b}$ be the three-valued interpretation defined via
$\hat{\nu}_{b}(t_{i},a)=\text{B}$ for all $t_{i}$ and $a$. We prove the more
general statement that $\hat{\nu}_{b}(t_{i},\phi)=\text{B}$ for any $t_{i}$
and $d(\phi)\leq m-i$ by induction on the structure of $\phi$:

  * •

$\phi=a$ for $a\in\mathsf{At}$: $\hat{\nu}_{b}(t_{i},a)=\text{B}$ holds by
definition.

  * •

$\phi=\neg\psi$: $d(\phi)\leq m-i$ implies that $d(\psi)\leq m-i$ as well. By
the induction hypothesis, $\hat{\nu}_{b}(t_{i},\psi)=\text{B}$ and therefore
$\hat{\nu}_{b}(t_{i},\neg\psi)=\text{B}$ as well.

  * •

$\phi=\phi_{1}\wedge\phi_{2}$: $d(\phi)\leq m-i$ implies that $d(\phi_{1})\leq
m-i$ and $d(\phi_{2})\leq m-i$ as well. By the induction hypothesis,
$\hat{\nu}_{b}(t_{i},\phi_{1})=\hat{\nu}_{b}(t_{i},\phi_{2})=\text{B}$ and
therefore $\hat{\nu}_{b}(t_{i},\phi_{1}\wedge\phi_{2})=\text{B}$.

  * •

$\phi=\phi_{1}\vee\phi_{2}$: $d(\phi)\leq m-i$ implies that $d(\phi_{1})\leq
m-i$ and $d(\phi_{2})\leq m-i$ as well. By the induction hypothesis,
$\hat{\nu}_{b}(t_{i},\phi_{1})=\hat{\nu}_{b}(t_{i},\phi_{2})=\text{B}$ and
therefore $\hat{\nu}_{b}(t_{i},\phi_{1}\vee\phi_{2})=\text{B}$.

  * •

$\phi=\textbf{X}\psi$: $d(\phi)\leq m-i$ implies $d(\psi)\leq m-(i+1)$. By the
induction hypothesis $\hat{\nu}_{b}(t_{i+1},\psi)=\text{B}$ which directly
gives $\hat{\nu}_{b}(t_{i},\textbf{X}\psi)=\text{B}$.

  * •

$\phi=\varphi_{1}\textbf{U}\varphi_{2}$: $d(\phi)\leq m-i$ implies that
$d(\phi_{1})\leq m-(i+1)$ and $d(\phi_{2})\leq m-(i+1)$ as well. So, by the
induction hypothesis $\hat{\nu}_{b}(t_{i+1},\phi_{2})=\text{B}$ and therefore
$\hat{\nu}_{b}(t_{i},\varphi_{1}\textbf{U}\varphi_{2})=\text{B}$.

$\mathcal{I}$ | CO | MO | IN | DO | TS
---|---|---|---|---|---
$\mathcal{I}_{d}$ | ✓ | ✓ | ✓ | ✓ | ✗
$\mathcal{I}_{\mathsf{MI}}$ | ✓ | ✓ | ✓ | ✗ | ✗
$\mathcal{I}_{p}$ | ✓ | ✓ | ✓ | ✗ | ✗
$\mathcal{I}_{r}$ | ✓ | ✓ | ✓ | ✗ | ✗
$\mathcal{I}_{c}$ | ✓ | ✓ | ✗ | ✓ | ✗
$\mathcal{I}_{at}$ | ✓ | ✗ | ✗ | ✗ | ✗
$\mathcal{I}^{LTL}_{d}$ | ✓ | ✓ | ✓ | ✓ | ✓
$\mathcal{I}^{LTL}_{c}$ | ✓ | ✓ | ✗ | ✓ | ✓
Table 3: Compliance of the inconsistency measures with the considered
rationality postulates.

###### Proposition 4

The compliance of the inconsistency measures
$\mathcal{I}_{d},\mathcal{I}_{\mathsf{MI}},\mathcal{I}_{p},\mathcal{I}_{r},\mathcal{I}_{c},\mathcal{I}_{at},\mathcal{I}^{LTL}_{d}$
and $\mathcal{I}^{LTL}_{c}$ with the postulates CO, MO, IN, DO and TS is as
shown in Table 3.

###### Proof

The proofs for
$\mathcal{I}_{d},\mathcal{I}_{\mathsf{MI}},\mathcal{I}_{p},\mathcal{I}_{r},\mathcal{I}_{c},\mathcal{I}_{at}$
can be found in [24].111$\mathcal{I}_{r}$ is equivalent to
$\mathcal{I}_{dalal}^{hit}$ from that work. Also, the proofs for
$\mathcal{I}_{at}$ are analogous to $\mathcal{I}_{mv}$. In the process we
corrected one result in [24], based on an earlier error. Actually,
$\mathcal{I}_{c}$ does not satisfy IN because of iceberg inconsistencies (see
[3]). For example, consider a knowledge base $\mathcal{K}_{c}=\\{a\wedge\neg
a\wedge b,\neg b\\}$. Then $\neg b$ is free, but
$\mathcal{I}_{c}(\mathcal{K}_{c})=2$ and
$\mathcal{I}_{c}(\mathcal{K}_{c}\setminus\\{\neg b\\})=1$. Also, for those
measures TS follows from Example 2.

We now consider the remaining measures $\mathcal{I}^{LTL}_{d}$ and
$\mathcal{I}^{LTL}_{c}$ in turn. Recall that the definition of consistency for
LTL${}_{\text{f}}$ requires the existence of a 2-valued interpretation
$\hat{\nu}$ such that $\hat{\nu}\models\mathcal{K}$. Using such an
interpretation we obtain
$|\textsf{AffectedStates}(\hat{\nu})|=|\textsf{ConflictBase}(\hat{\nu})|=0$.
If $\mathcal{K}$ is inconsistent, B is assigned to at least one proposition,
so these values are positive.

We now start with $\mathcal{I}^{LTL}_{d}$. For this, let
$\mathcal{K},\mathcal{K}^{\prime}$ be knowledge bases and $\alpha,\beta$ be
two formulas of LTL${}_{\text{ff}}$. CO follows directly from the definition
of consistency. For MO, if $\mathcal{K}$ is consistent, then
$\mathcal{K}\cup\mathcal{K}^{\prime}$ is either consistent or inconsistent. In
both cases
$\textsf{AffectedStates}(\mathcal{K}\cup\mathcal{K}^{\prime})\geq\textsf{AffectedStates}(\mathcal{K})$.
If $\mathcal{K}$ is inconsistent, so is $\mathcal{K}\cup\mathcal{K}^{\prime}$
and again
$\mathcal{I}^{LTL}_{d}(\mathcal{K})\leq\mathcal{I}^{LTL}_{d}(\mathcal{K}\cup\mathcal{K}^{\prime})$.
For IN, observe that for any free formula $\alpha$, there exists an
interpretation that maps $\alpha$ to $1$; thus, free formulas cannot affect
the size of AffectedStates. In turn, if $\alpha$ is a free formula, for any
interpretation $\hat{\nu}$ that assigns B to a minimal number of propositions
we have that $|\textsf{AffectedStates}(\hat{\nu})|$ is the same for
$\mathcal{K}$ and ($\mathcal{K}\setminus\alpha$). For DO, observe from [11]
that if $\alpha\models\beta$, then
$\\{\hat{\nu}\mid\hat{\nu}\models^{3}(\mathcal{K}\cup\\{\alpha\\})\\}\subseteq\\{\hat{\nu}\mid\hat{\nu}\models^{3}(\mathcal{K}\cup\\{\beta)\\})\\}$.
Therefore
$\min_{\hat{\nu}\models^{3}(\mathcal{K}\cup\\{\alpha\\})}|\textsf{AffectedStates}(\hat{\nu})|\geq\min_{\hat{\nu}\models^{3}(\mathcal{K}\cup\\{\beta\\})}|\textsf{AffectedStates}(\hat{\nu})|$.
For TS let $\mathcal{K}=\\{\textbf{X}\varphi,\textbf{X}\neg\varphi\\}$ and
$\mathcal{K}^{\prime}=\\{\textbf{G}\varphi,\textbf{G}\neg\varphi\\}$. Then
there is an interpretation satisfying $\mathcal{K}$ that only assigns B to
state $t_{1}$. But for $\mathcal{K}^{\prime}$ every interpretation must assign
B to $m$ states. Therefore
$\min_{\hat{\nu}\models^{3}\mathcal{K}}|\textsf{AffectedStates}(\hat{\nu})|<\min_{\hat{\nu}\models^{3}\mathcal{K}^{\prime}}|\textsf{AffectedStates}(\hat{\nu})|$.

The proofs for $\mathcal{I}^{LTL}_{c}$ are analogous to
$\mathcal{I}^{LTL}_{d}$ except that $\mathcal{I}^{LTL}_{c}$ counts the number
of inconsistencies for each state also. VO and MO are immediate as before. For
IN the counterexample for propositional logic can be used. DO follows as for
$\mathcal{I}^{LTL}_{d}$. The only difference in the proof for TS is that now
it is possible to give a formula $\varphi$ for which
$\mathcal{I}^{LTL}_{c}(\mathcal{K})>1$ but then
$\mathcal{I}^{LTL}_{c}(\mathcal{K}^{\prime})=m\times\mathcal{I}^{LTL}_{c}(\mathcal{K})>\mathcal{I}^{LTL}_{c}(\mathcal{K})$.

###### Theorem 6.1

Deciding whether a formula $\phi$ is satisfiable in LTL${}_{\text{ff}}$ is NP-
complete.

###### Proof

For NP-membership consider the following non-deterministic algorithm. Since
$m$ is fixed, we can guess an LTL${}_{\text{ff}}$ interpretation
$\hat{\omega}$ and verify (in polynomial time) that $\hat{\omega}\models\phi$.

NP-hardness follows directly from the fact that satisfiability in
LTL${}_{\text{ff}}$ subsumes propositional satisfiability (as $\phi$ can be a
purely propositional formula).

###### Theorem 6.2

Upper${}_{\mathcal{I}^{LTL}_{d}}$ and Upper${}_{\mathcal{I}^{LTL}_{c}}$ are
NP-complete.

###### Proof

First, observe that given a 3-valued interpretation $\hat{\nu}$, evaluating
$\hat{\nu}(t_{i},\phi)$ for any $t_{i}$ and $\phi$, as well as determining
$\textsf{AffectedStates}(\hat{\nu})$ and $\textsf{Conflictbase}(\hat{\nu})$,
can be done in polynomial time.

For NP-membership consider the following non-deterministic algorithm. Given
$\mathcal{K}$ and $x\in\mathbb{R}^{\infty}_{\geq 0}$, we non-deterministically
guess an interpretation $\hat{\nu}$ and verify
$\hat{\nu}\models^{3}\mathcal{K}$ and
$|\textsf{AffectedStates}(\hat{\nu})|\leq x$ (or
$|\textsf{Conflictbase}(\hat{\nu})|\leq x$).

For NP-hardness, observe that for given $\mathcal{K}$ and $x=0$, both problems
Upper${}_{\mathcal{I}^{LTL}_{d}}$ and Upper${}_{\mathcal{I}^{LTL}_{c}}$ are
equivalent to the problem of deciding whether there is a two-valued
interpretation that satisfies $\mathcal{K}$. Due to Proposition 2 this problem
is equivalent to the classical satisfiability problem in LTL${}_{\text{ff}}$.
Therefore, we can reduce the classical satisfiability problem of propositional
logic to the problem Upper${}_{\mathcal{I}^{LTL}_{d}}$ (or
Upper${}_{\mathcal{I}^{LTL}_{c}}$) with $x=0$, which shows the NP-hardness of
the latter.

###### Corollary 1

Lower${}_{\mathcal{I}^{LTL}_{d}}$ and Lower${}_{\mathcal{I}^{LTL}_{c}}$ are
coNP-complete. Exact${}_{\mathcal{I}^{LTL}_{d}}$ and
Exact${}_{\mathcal{I}^{LTL}_{c}}$ are in DP. Value${}_{\mathcal{I}^{LTL}_{d}}$
and Value${}_{\mathcal{I}^{LTL}_{c}}$ are in $\textsf{FP}^{\textsf{NP}[\log
n]}$.

###### Proof

The coNP-completeness of Lower${}_{\mathcal{I}^{LTL}_{d}}$ and
Lower${}_{\mathcal{I}^{LTL}_{c}}$ and the membership of
Exact${}_{\mathcal{I}^{LTL}_{d}}$ and Exact${}_{\mathcal{I}^{LTL}_{c}}$ in DP
follow from Lemma 6 in [26], Proposition 6.2, and the fact that the measures
$\mathcal{I}^{LTL}_{c}$ and $\mathcal{I}^{LTL}_{d}$ are well-serializable, cf.
Definition 22 in [26], due to their range being equal to
$\\{0,\ldots,m,\infty\\}$ (for $\mathcal{I}^{LTL}_{d}$) and
$\\{0,\ldots,m|\mathsf{At}|,\infty\\}$ (for $\mathcal{I}^{LTL}_{c}$). The
membership of Value${}_{\mathcal{I}^{LTL}_{d}}$ and
Value${}_{\mathcal{I}^{LTL}_{c}}$ in $\textsf{FP}^{\textsf{NP}[\log n]}$
follow likewise from Lemma 4 in [26] and Proposition 6.2.