We present a framework of answer set programming-based solutions for various problems related to declarative process specifications. Specifically, the framework ofers implementations for conformance checking, satisfiability checking, and two diferent inconsistency measures. Since the aforementioned problems are represented in a fragment of linear temporal logic, the framework could also prove useful for a broader range of applications beyond process specifications.
uct is empty) [
For conformance checking, existing algorithmic ap- to automata [
Regarding the analysis of inconsistency in declarative Section 2 and present an overview of our framework in specifications, virtually all existing approaches also rely Section 3. on the mentioned automata representation (and verify inconsistency by checking whether the automata prod
sequence of temporal states. In this work we consider
CC is actually closer to the definition of the problem of
sequences of finite [
In inconsistency measurement (IM) [
¬F¬ .
declarative process specifications. In [
Problems Related to Declarative Process Specifica- constraint, and if () = ∅, is called a fact. We further i.e., ˆ(, ) = 1 if is assigned 1 at . A formula is satisfied
by an interpretation ˆ, denoted ˆ |= , if ˆ, 0 |= . Further, ˆ, |= is inductively defined as ˆ, |= if ˆ(, ) = 1 for ∈ At ˆ, |= ¬ if ˆ, ̸|= ˆ, |= 1 ∧ 2 if ˆ, |= 1 and ˆ, |= 2 ˆ, |= 1 ∨ 2 if ˆ, |= 1 or ˆ, |= 2 ˆ, |= X if < and ˆ, +1 |= ˆ, |= 1U 2 if ˆ, |= 2 with ∈ { + 1, . . . , } and ˆ, |= 1 ∀ ∈ {, . . . , − 1
} interpretation ˆ satisfies a set of formulas w.r.t. any interpretation ˆ, and ∈ {0, . . . , }. An if ∀
∈ : ˆ |= . We also refer to a satisfiable set of formulas as consistent, and to an unsatisfiable set of formulas as inconsistent. tions
Conformance checking (CC) is the task of deciding whether a given trace = ⟨0, . . . , ⟩, consisting of a sequence of activities or actions, conforms to a given specification
. Note that, following the literature in
business process modeling, only the atom indicated by
( ∈ {0, . . . , }) is set to 1 in state , while all other
atoms are set to 0 in [
formulas can be vacuously satisfied. satisfiability checking (SC) as the task of deciding whether there exists a trace of length , and a corresponding interpretation ˆ, s.t. ˆ |= , for a given specification . Again, only atom is set to true in state , and
ative process specifications, we additionally provide implementations for the “general” problems of CC and SC in LTLf . To be precise, we lift the restriction that only atom is allowed to be true in state , and we prohibit formulas to be vacuously satisfied. We denote the correAnswer Set Programming
ming (ASP) [
An extended logic program is comprised of rules of the form “ = 0:- 1, . . . , , not +1, . . . , not .” with (0 ≤ ≤ ≤
) being atoms, and “not”
indicating default negation [
An ASP rule (as illustrated above) is comprised of
a head () = 0 and a body () = {1, . . . , ,
not +1, . . . , not }. If () is empty, is called a
is called an answer set of .
+() ⊆
divide the elements of () into +() = {1, . . . , }
and − () = {+1, . . . , }. A set of ground
atoms is a model of a ground logic program if for
all ∈ , () ∈ whenever − () ∩ = ∅ and
. The reduct [
The framework2 we present combines ASP-based
implementations of all problems defined in the preceding
section (namely, CC, MC, SC, SCLTLf , and IM w.r.t. the
two measures defined in [
Note that the implementations for CC and SC have been
introduced in a recent work by the authors [
Since due to page limitations, we cannot explain the true per state (instead of a single atom). Furthermore, the
ASP encodings for each problem in detail, we take CC approach can be easily modified to solve SC and SCLTLf .
as an example to demonstrate our overall approach. Our Intuitively, for SCLTLf we merely need to add a rule that
framework takes as input for CC (i) a file containing a “guesses” an interpretation which is then checked to be
specification (i.e., a set of LTL formulas), and (ii) a file satisfiable, and for SC we additionally need to handle
containing a set of traces . For each trace ∈ , we vacuous satisfiability directly within ASP.
encode CC in ASP, and if an answer set can be derived, The ASP encodings for the two inconsistency
meathe given problem instance (, ) is satisfiable, otherwise sures from [
In order to encode a given problem instance (, ) in to model only the “true” case w.r.t. the diferent operaASP, we begin by representing each atom ∈ At() as a tors. Instead, we use truthValue(, , ) to explicitly fact “atom().”. In the same manner, each formula ∈ represent a truth value for a formula in . However, is modeled as kbElement( ). Next, we represent the the overall approach is still the same—we directly model “type” of each (sub-)formula; e.g., a conjunction = logical entailment. 1 ∧ 2 is represented as conjunction(, 1, 2).
The remaining operators (disjunction, negation, next, until, eventually, and globally) are modeled analogously. 4. Conclusions and Future Work If a formula consists of a single atom , it is repre- We introduced a framework that provides ASP-based sosented by formulaIsAtom(, ). To represent a trace lutions for multiple problems related to LTL, targeted at in ASP, we first define || states, where the final state the field of declarative process specifications. Our ap = || − 1 is represented as finalState(). The proach does not require any preprocessing (such as the states {0, . . . , } are then modeled by adding the rule computation of automata), and can be used in other LTL“state(0..M) :- finalState(M).” to the encoding. related domains as well. In terms of future work, we aim Further, we model that ( ∈ {0, . . . , }) is true in to extend our set of implementations, e.g., by considerstate by adding “true(, ).”. ing culpability measures (which indicate a level of blame
An overview of our encoding of logical entailment is for the inconsistency of a knowledge base w.r.t. a given given in Listing 1. Essentially, we can directly follow the formula or atom). Also, we aim to apply our framework definition of each operator (see Section 2)—e.g., a formula to more non-monotonic settings, e.g., inconsistency meaX is true in if < and is true in +1 (line surement in the presence of superiority relations between 5). Moreover, lines 2–4 describe the classical operators, LTL formulas. lines 6–8 the remaining LTL-specific ones, and line 1 the case if a formula is in fact an atom. Finally, we add an integrity constraint (line 9) which ensures that no answer References set can be derived if any formula ∈ evaluates to “not true” in state 0, i.e., every formula must be satisfied. 3Note that in the case of CC, vacuously satisfied formulas are simply not encoded in ASP; in the case of MC, every formula is encoded.