=Paper=
{{Paper
|id=Vol-2663/paper-9
|storemode=property
|title=Give Inconsistency a Chance: Semantics for Ontology-Mediated Verification
|pdfUrl=https://ceur-ws.org/Vol-2663/paper-9.pdf
|volume=Vol-2663
|authors=Clemens Dubslaff,Patrick Koopmann,Anni-Yasmin Turhan
|dblpUrl=https://dblp.org/rec/conf/dlog/DubslaffKT20
}}
==Give Inconsistency a Chance: Semantics for Ontology-Mediated Verification==
https://ceur-ws.org/Vol-2663/paper-9.pdf
Give Inconsistency a Chance:
Semantics for Ontology-Mediated Verification
Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
Technische Universität Dresden, Dresden, Germany
{clemens.dubslaff,patrick.koopmann,anni-yasmin.turhan}@tu-dresden.de
Abstract. Recently, we have introduced ontologized programs as a for-
malism to link description logic ontologies with programs specified in
the guarded command language, the de-facto standard input formalism
for probabilistic model checking tools such as Prism, to allow for an
ontology-mediated verification of stochastic systems. Central to our ap-
proach is a complete separation of the two formalisms involved: guarded
command language to describe the dynamics of the stochastic system
and description logics are used to model background knowledge about
the system in an ontology. In ontologized programs, these two languages
are loosely coupled by an interface that mediates between these two
worlds. Under the original semantics defined for ontologized programs, a
program may enter a state that is inconsistent with the ontology, which
limits the capabilities of the description logic component. We approach
this issue in different ways by introducing consistency notions, and dis-
cuss two alternative semantics for ontologized programs. Furthermore,
we present complexity results for checking whether a program is consis-
tent under the different semantics.
Keywords: Description Logics, Inconsistency, Probabilistic Model Checking,
Ontology-Mediated Verification
1 Introduction
Probabilistic model checking (PMC, see, e.g., [2,7] for surveys) is an automated
technique for the quantitative analysis of dynamic systems. PMC has been suc-
cessfully applied in many areas, e.g., to ensure that the system meets quality
requirements such as low error probabilities or an energy consumption within
a given bound. The de-facto standard specification language for dynamic sys-
tems in PMC is given by stochastic programs, a probabilistic variant of Dijk-
stra’s guarded command language [5,9] used within many PMC tools such as
Prism [10]. Usually, the behavior described by a stochastic program is part of
a bigger system, or might be even used within a collection of systems that have
an impact on the operational behavior as well. There are different ways how to
Copyright © 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
2 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
model this by using stochastic programs. First, one could integrate additional
knowledge about the surrounding system directly into the stochastic program.
While this approach provides accurate PMC results, it has the disadvantage that
the guarded command language is not well-suited for describing complex static
knowledge. Alternatively, one can use non-determinism to over-approximate the
possible behaviors of the surrounding system. This approach has the disadvan-
tage that a best- and worst-case PMC analysis might lead to many possible
results that do not allow for a meaningful interpretation. As third option, one
can use ontology-mediated PMC, an approach to integrate knowledge described
by a description logic (DL) ontology into the PMC process, which we recently
proposed in [6]. The core of this approach are ontologized (stochastic) programs
which can be subject of PMC.
A central idea of ontologized programs is the complete separation of concerns
and formalisms: the operational behavior is described using a program component
expressed by guarded commands. Static knowledge about the system is described
in an ontology using DL formalisms. An interface mediates between these two
worlds by providing mappings from statements in guarded command language
to DL and vice versa. The loose coupling achieved in this way allows to reuse and
replace both components easily, so that the same behavior can be analyzed with
different ontologies (to describe different system configurations), and the same
ontology can be used with different programs (e.g., to describe different strategies
of behavior to be analyzed within the same system). This approach distinguishes
our work from other approaches that use DLs for the verification of dynamic
systems, in which DL constructs are used directly within the program [1,4,8,14].
To be able to analyze ontologized programs practically, we developed a two-
step procedure in [6]. First, the ontologized program and the property to be
analyzed are rewritten into a plain stochastic program and a modified property.
Then, these are evaluated using the PMC tool Prism. This way, essentially
all model-checking tasks supported by Prism can be performed on ontologized
programs, ranging from verification of standard properties (like the probability
or the expected time for reaching a failure state) to more advanced quantitative
analysis (cf. [7,3]). Our approach was implemented and evaluated in [6].
Under the original semantics of ontologized programs in [6], program com-
ponents are allowed to enter states that are inconsistent with the ontology. This
leaves the task of resolving the inconsistency to the program component by im-
plementing a sort of exception handling. However, inconsistent states may also
stand for situations that never can arise in practice. In this case, a semantics
that avoids inconsistent states when possible is favorable, leading to a consis-
tency notion of ontologized programs. In this paper, we answer the following
open questions: 1) how to handle inconsistent states in a meaningful way and
2) what does it mean for an ontologized program to be inconsistent. We approach
these questions by presenting three possible semantics of ontologized programs:
consistency-independent, probability-normalizing, and probability-preserving se-
mantics. Each semantics specifies the behavior of the program in a different way,
Semantics for Ontology-Mediated Verification 3
and additionally comes with its own notion of consistency. For each of these no-
tions, we give tight complexity bounds for deciding consistency of programs.
2 Preliminaries
We assume familiarity of the reader with the basics of description logics. The
results in this paper apply to different DLs, on which we make some basic as-
sumptions: 1) they are fragments of SROIQ, and 2) they use unary encoding
for numbers. This was done for convenience in our proofs, and we conjecture
that our results can be lifted to a more general class of DLs.
We briefly address relevant preliminaries on probabilistic operational mod-
els and their verification.
P A probability distribution over S is a function µ : S →
[0, 1]∩Q with s∈S µ(s) = 1, denoting the set of distributions over S by Distr (S).
Markov decision processes (MDPs) are tuples M = hQ, Act, P, q0 , Λ, λi
where Q and Act are countable sets of states and actions, respectively, P is a
partial probabilistic transition function P : Q × Act * Distr (Q) and q0 ∈ Q an
initial state, Λ is a set of labels assigned to states via a labeling function λ : Q →
℘(Λ). For convenience, for q1 , q2 ∈ Q, α ∈ Act, we abbreviate P (q1 , α)(q2 ) by
P (q1 , α, q2 ). An action α ∈ Act is enabled in a state q ∈ Q if P (q, α) is defined.
We assume that M does not have final states, i.e., in each state at least one
action is enabled. A finite path in M is a sequence π = q0 α0 q1 α1 . . . αk−1 qk
where pi = P (qi , αi , qi+1 ) > 0 for all i < k. The probability of π is Pr(π) =
p0 · p1 · . . . · pk−1 . Intuitively, the behavior of M in state q is to select an enabled
action α and move to a successor state q 0 with probability P (q, α, q 0 ). Such a
selection is done via (randomized) schedulers, i.e., functions S that map a finite
paths to a distribution over actions. For schedulers, we require that for each
finite path π in M with last state q, we have P (q, α) is defined for any α ∈ Act
with S(π)(α) > 0. Then, a probability measure PrS M over maximal S-paths, i.e.,
infinite paths that follow S, is defined in the standard way (cf. [13]).
Probabilistic model checking (PMC, cf. [2]) is used in this paper for a
quantitative analysis of MDPs. Usually one has given a temporal logical property
φ over the set of labels Λ that defines sets of maximal paths in the MDP that
fulfill φ. For instance, linear temporal logic (LTL, [12]) can be used to specify
the set of paths reaching states labeled by an ` ∈ Λ, formally φ1 = ♦`, or where
always when such a state is reached, within two time steps
a state not labeled by
` is reached again, formally φ2 = ` → (X¬` ∨ XX¬`) . For a scheduler S, any
LTL property constitutes a measurable set of S-paths such that we can reason
about the probability PrS M (φ) of M satisfying an LTL property φ w.r.t. S. By
ranging over all possible schedulers, this enables a best- and worst-case analysis.
A stochastic property is an expression Φ = Pex (φ) ./ τ where φ is an LTL
formula, τ ∈ Q a threshold, ./ ∈ {<, ≤, ≥, >} a relation, and ex ∈ {min, max}.
Then, M satisfies Φ, denoted M |= Φ, iff ex = min and inf S PrS M (φ) ./ τ or
4 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
ex = max and supS PrS M (φ) ./ τ . The PMC problem for Φ and M amounts
to decide whether M |= Φ. For more details on MDPs and PMC, we refer to
standard textbooks such as [13,2,7]. Note that in [6] we considered weighted
MDP for ontology-mediated PMC over expected accumulated costs. For brevity,
we consider only plain MDPs in this paper.
Arithmetic Constraints and Boolean Expressions are defined over a
countable set V of variables. An evaluation over V is a function η that assigns
to each v ∈ V a value in {−δ(v), −δ(v) + 1, . . . , δ(v)} where δ : V → N defines
bounds of each variable. The set of evaluations is denoted by Eval (V). Let z
range over Z and v range over V. The set of arithmetic expressions E(V) is de-
fined by the grammar α ::= z | v | (α + α) | (α · α) . Evaluations naturally
extend to arithmetic expressions, e.g., η(α1 + α2 ) = η(α1 ) + η(α2 ). C(V) denotes
the set of arithmetic constraints over V, which are terms of the form (α ./ z)
with α ∈ E(V), ./ ∈ {>, =, <}, and z ∈ Z. For a given evaluation η ∈ Eval (V)
and constraint γ ∈ C(V), we write η |= γ iff γ holds in η. We denote by C(η)
the constraints entailed by η, i.e., C(η) = {c ∈ C(V) | η |= c}. B(V) denotes
the set of Boolean expressions over C(V), i.e., the set of propositional formulas
where arithmetic constrains over V are used as atoms. Entailment of Boolean
expressions B(V) from evaluations is defined in the usual way.
Stochastic programs provide in the area of PMC the de-facto standard to con-
cisely describe MDPs. They are essentially a probabilistic variant of Dijkstra’s
guarded command language [5,9]. We call a function u : V → E(V) update, and a
distribution σ ∈ Distr (Upd ) over a given finite set Upd of updates stochastic up-
date. The effect of an update u : V → E(V) on an evaluation η ∈ Eval (V) is their
composition η ◦ u ∈ Eval (V), i.e., (η ◦ u)(v) = max{−δ(v), min{η(u(v)), δ(v)}}
for all v ∈ V. This notion naturally extends to stochastic updates σ ∈ Distr (Upd )
where for any η, η 0 ∈ Eval (V) we have that (η ◦ σ)(η 0 ) is the sum over all σ(u)
for which η ◦ u = η 0 . A stochastic guarded command over a finite set of updates
Upd , briefly called command, is a pair hg, σi where g ∈ B(V) is a guard and
σ ∈ Distr (Upd ) is a stochastic update, which we write in the following form:
1/2 : server proc1 := 1
(server proc1 = 2 ∧ server proc2 = 2) 7→ (1)
1/2 : server proc1 := 3
A stochastic program over V is a tuple P = hV, C, η0 i where C is a finite set
of commands and η0 ∈ Eval (V) is an initial variable evaluation. For brevity, we
write Upd (P) for the set of all updates in C. The MDP induced by P is defined
as M[P] = hS, Act, P, η0 , Λ, λi where
– S = Eval (V), – λ(η) = C(η) for all η ∈ S, and
– Act = Distr (Upd (P)), – P (η, σ, η 0 ) = (η◦σ)(η 0 ) for η, η 0 ∈ S
– Λ = C(V), and hg, σi ∈ C with λ(η) |= g.
Semantics for Ontology-Mediated Verification 5
Ontologized Program State q1
Command Perspective DL Perspective
OverloadServer ≡ Server u ≥3runs.Process
migrateServer2 Server(s1 ) Server(s2 ) Server(s3 )
Process(p1 ) Process(p2 ) Process(p3 )
server proc1 = 2 runs(s2 , p1 )
server proc2 = 2 runs(s2 , p2 )
server proc3 = 2 runs(s2 , p3 )
Fig. 1. Perspectives on the ontologized program state q1 : the command perspective
(left) and DL perspective (right), linked by the interface (arrows).
3 Ontologized Stochastic Programs
In general, an ontologized program comprises the following three components [6]:
The Program is a specification of the operational behavior.
The Description Logic Ontology contains static background knowledge that
may influence the behavior of the program.
The Interface links program and ontology by providing mappings between the
languages used for the program and the ontology.
Ontologized programs combine the two formalisms guarded command lan-
guage and description logics (DLs). To achieve maximum division of concerns,
the behaviors and the static knowledge about the context of the program are
specified separately and are only loosely coupled by an interface. This allows
for specifying operational behavior in the usual way and to extend and reuse
existing program specifications, and similarly, to easily link established or even
standardized ontologies to a program.
Before we formally define ontologized programs, we explain how global states
of ontologized programs are represented. Both formalisms, guarded command
language and DL, may represent abstracted versions of global states in different
ways. For the guarded command language a state is described as an evaluation of
variables, while in DL a state is described using a set of axioms. Both formalisms
require different degrees of abstraction and detail, depending on their dedicated
purpose. Consequently, global states of ontologized programs are composed of
two components, which we call the command perspective and the DL perspective
on the global system state (see Figure 1). As can be seen in the figure, there
are some elements in the two perspectives that correspond to each other, while
others have no direct correspondence. The correspondence, depicted by arrows in
6 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
the figure, is defined in the interface component of the ontologized program via
a function Dc (DL to command ), mapping DL axioms to command expressions.
The part of the DL perspective inside the box is not mapped to anything on the
command side – this is the static part, and contains the background knowledge
about the system that is independent of the current state of the system. In
contrast, the mapped axioms in the ontology perspective can change, which is
why we call them fluents. Note that we also allow the command perspective to
use variables that have no correspondence in the DL perspective.
So far, our description of global states does not depend on any DL reason-
ing, which is, however, required by the DL component to provide background
knowledge for the operational component of the program. To invoke a reasoning
task from the command side of ontologized programs, we have introduced the
notion of hooks in [6]. A hook is a propositional variable in the program com-
ponent that is linked by the interface to a Boolean query on the DL component
of the ontologized program state. The result of the query determines the value
of the propositional variable using the function cD (command to DL). In our
example, we would for each server i ∈ {1, 2, 3} define one hook migrateServeri
that stands for the knowledge that processes should be migrated from Server i:
cD(migrateServeri) = {OverloadedServer(si )}.
In the ontologized state shown in Figure 1, the hook migrateServer2 is active
because the ontology in DL perspective entails OverloadedServer(s2 ).
To enable the actual use of hooks in the guarded command language, we have
to slightly extend the definition of commands. Specifically, we define abstract
stochastic programs as stochastic programs where guards are Boolean expressions
over arithmetic expressions and hooks. For example a command in an abstract
stochastic program looks like the following:
1/2 : server proc1 := 1
(migrateServer2 ∧ server proc1 = 2) 7→ (2)
1/2 : server proc1 := 3
While the intention of this command is similar to the command (1), this version
omits the specification of the condition under which Server 2 needs to migrate.
Specifying and testing this condition is now delegated to the DL component.
Now we are ready to formally define ontologized programs. Given an abstract
stochastic program P, we denote by HP the hooks used in P.
Definition 1. An ontologized program is a tuple P = hP, K, Ii where
– P = hVP , CP , WP , ηP,0 i is an abstract stochastic program,
– K is a DL ontology called the static DL knowledge,
– I = hVI , HI , F, Dc, cDi is a tuple describing the interface, where VI is a set
of public variables, HI is a set interface hooks, F is a set of DL axioms
called fluents, and two mappings cD : HI → ℘(A) and Dc : F → B(VI ), and
P is compliant with I, i.e., HP ⊆ HI and VI ⊆ VP . If for a DL L every axiom
in K ∪ F is an L axiom, we call P an L-ontologized program.
Semantics for Ontology-Mediated Verification 7
4 Three Semantics of Ontologized Programs
Stochastic programs are used as concise representations of MDPs that can be
subject of a quantitative analysis. Analogously, ontologized programs are con-
cise representations of ontologized MDPs, where a quantitative analysis on these
MDPs can further rely on information provided by the ontology. Since there
is an additional logical component in ontologized programs, there are differ-
ent meaningful ways in which ontologized MDPs can be defined to represent
the operational behavior of ontologized programs. We present three semantics
for ontologized programs that differ in their treatment of inconsistencies. Such
inconsistencies arise when variable evaluations in the stochastic program have
an inconsistent meaning in the ontology. Choosing an appropriate semantics is
a modeling decision to be made when constructing the ontologized program.
Therefore we analyze the impact of this choice on the computational complex-
ity of deciding consistency w.r.t. each of the different semantics. First we define
formally that ontologized states comprise a command perspective and a DL
perspective (see Figure 1).
Definition 2. Let P = hP, K, Ii be an ontologized program as in Definition 1.
An ontologized state in P is a tuple q = hηq , Kq i, with command perspective ηq
and DL perspective Kq , where
– K ⊆ Kq , – ηq ∈ Eval (VP ), and
– Kq ⊆ K ∪ F, – α ∈ Kq iff ηq |= Dc(α) for every α ∈ F.
We call an ontologized state q inconsistent if Kq is inconsistent.
For every evaluation η ∈ Eval (VP ), there is always a unique KB Kη s.t.
hη, Kη i is an ontologized state in P. We denote this state by s(P, η). To de-
fine updates on ontologized states, we exploit the fact that 1) updates can only
directly modify the command perspective of ontologized states, and 2) the DL
perspective of ontologized states is fully determined by the command perspec-
tive. Thus, we can easily lift the effect of updates on evaluations to updates
on ontologized states. For an update u ∈ Upd (VP ) and an ontologized state
q, we define u(q) = s(P, u(ηq )). Correspondingly, we extend stochastic updates
σ : Upd (VP ) → [0, 1] to ontologized states q by setting σ(q, u(q)) = σ(u) for all
u ∈ Upd (VP ). To illustrate how commands are executed on ontologized states,
we consider the ontologized state q1 shown in Figure 1 and the abstract com-
mand in (2). First, we note that the guard in the command is active, since
the hook migrateServer2 is active in q1 . The command can thus be executed
on the state, and executes each of its updates with a 50% chance. For the
first update, server proc1 := 1, we obtain the ontologized state q2 in which
server proc1 = 2 is replaced by server proc1 = 1, and runs(s2 , p2 ) is replaced
by runs(s1 , p2 ). Consequently, the hook migrateServer2 becomes inactive in q2 ,
since cD(migrateServer2) = {OverloadedServer(s2 )} and OverloadedServer(s2 )
is not entailed by the DL perspective on q2 .
8 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
4.1 Consistency-Independent Semantics
We first present the semantics for ontologized programs originally introduced
in [6]. This semantics does not give inconsistent ontologized states a priori a spe-
cial meaning, therefore named consistency-independent semantics. The definition
of the MDP induced by an ontologized program under consistency-independent
semantics closely follows the one for MDPs induced by plain stochastic programs.
Definition 3. Let P = hP, K, Ii be an ontologized program as in Definition 1.
The MDP induced by P under consistency-independent semantics is given by
Mci [P] = hQ, Act, P, q0 , Λ, λi, where
– Q = {s(P, η) | η ∈ Eval (VP )}, – λ(q) = C(ηq ) ∪ {` ∈ HP |
– Act = Distr (Upd (P)), Kq |= cD(`)} for every q ∈ Q, and
– q0 = s(P, η0 ), – P (q, σ) = σ(q) for all hg, σi ∈ C
– Λ = HP ∪ C(VP ), with λ(q) |= g.
P is inconsistent if there exists an inconsistent q ∈ Q reachable from q0 .
We can test consistency of ontologized programs using a reachability analysis
on the state space. For this, we generate states one after the other, using DL
reasoner calls for each state to determine their active hooks and their consis-
tency. As each state requires polynomial space, this can be done in polynomial
space with a k-oracle, where k is the complexity of entailment in the DL. A cor-
responding lower bound can be obtained by reduction of the word problem for
polynomially space-bounded Turing machines with k-oracle. The construction
used here shows a close relationship between Turing machines with k-oracle and
L-ontologized programs, provided that L is k-hard. This relationship is also used
for later complexity results presented in this paper.
Theorem 1. Let L be a DL such that deciding entailment in L is k-complete.
Then, deciding consistency of L-ontologized programs is PSpacek -complete, even
for non-stochastic programs.
4.2 Probability-Normalizing Semantics
If a stochastic program is inconsistent, consistency-independent semantics relies
on the program specification to deal with inconsistent states. On the one hand,
this can offer flexibility. On the other hand, it can be desirable to let the seman-
tics handle the situation by definition. Since inconsistent states have no corre-
spondence to states of the modeled system, they could stand for undesired states
that should not occur in the MDP at all. The idea of probability-normalizing
semantics is to remove all states of paths that can lead to an inconsistent state
and locally normalize probabilistic choices accordingly. Under this semantics, the
ontology serves an additional purpose: not only does it assign meaning to the
hooks, it also specifies which program states are possible, and thus restricts the
Semantics for Ontology-Mediated Verification 9
transitions from a given state. This allows for a further separation of concerns,
and thus for reusability of the behavioral and the DL component of the program:
we may use the same behavioral component with different ontologies that put
different constraints on the state space. In the running server example, we may
want to analyze a system in which the servers have different software and/or
hardware configurations, such that some processes cannot run on all servers. For
instance, we might use a different ontology that specifies that Process 1 cannot
run on Server 3. This restricts the possible outcomes of applying the command
in (2) on the state in Figure 1 (with the modified ontology). It can now only move
Process 1 to Server 1, so that this migration is performed with 100% probability.
To achieve this behavior under consistent-independent semantics, we would
have to extend the commands of the program with a case distinction over all
possible successors to inconsistent states, which is clearly undesired in the above
example. Instead, we capture the restriction to possible states of the MDP by
defining probability-normalizing semantics for ontologized programs. Intuitively,
under probability-normalizing semantics, the induced MDP can be obtained from
the corresponding consistency-independent semantics by removing inconsistent
states and then normalizing the resulting probabilities. It is possible that for
some state q and command hg, σi with λ(q) |= g such a normalization is not
possible, since all successor states that should have a positive probability lead
to an inconsistent state. In this case, the command cannot be applied on q. If
no command can be applied anymore on a state, this state is removed from the
MDP as well.
Definition 4. Let Mci [P] = hQ, Act, P, q0 , Λ, λi for an ontologized program P.
An MDP M is probability-normalizing w.r.t. P if q0 is consistent and M =
hQ0 , Act, P 0 , q0 , Λ, λ0 i, where
1. Q0 ⊆ Q contains only consistent states,
2. λ0 is obtained from λ by restricting its domain to Q0 ,
3. for all q ∈ Q and σ ∈ Act s.t. P (q, σ) is defined, we have for all q 0 ∈ Q0 :
X
P (q, σ, q 0 ) = P 0 (q, σ, q 0 ) · 0
P (q, σ, q̂).
q̂∈Q
P is called probability-normalizable if there exists a probability-normalizing MDP
w.r.t. by P. In case Q0 and P 0 are subset-maximal, M is the called the MDP
induced by P under probability-normalizing semantics, denoted Mpn [P].
Recall that according to our definition, MDPs cannot have final states. There-
fore, to obtain the probability probability-normalizing MDP, it does not suffice
to remove inconsistent state, but also states that would only lead to inconsistent
states would have to be removed. As this operation might lead to a removal
of the initial state, not every ontologized program is probability-normalizable.
While for consistency-independent semantics consistency of a program can be
decided by determining reachability of inconsistent states, we have to solve a
complementary task for probability-normalizability. Specifically, we have to de-
cide whether one can find an unbounded path that never enters an inconsistent
10 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
state, for which again polynomial space and an oracle for the reasoner is suffi-
cient. As a result, deciding probability-normalizability has the same complexity
as deciding consistency under consistency-independent semantics.
Theorem 2. Let L be a DL for which deciding entailment has complexity k.
Then, deciding whether an L-ontologized program is probability-normalizable is
PSpacek -complete, even for non-stochastic programs.
4.3 Probability-Preserving Semantics
If we use probability-normalizing semantics, it is possible that the probabilities
specified in the commands change. This is the right choice if the program uses
probabilities to model randomized behavior as in our running example: the pro-
gram migrates a process as soon as this becomes necessary, and it does so by
choosing each possible server with equal probability. If the ontology restricts the
number of possible choices, then consequently the probabilities need to change
as well. However, there are other scenarios where a change of probabilities is not
desired: rather than using stochastic commands to model randomized behavior,
the program component may use stochastic commands to describe probabilistic
outcomes of the simulated system that are based on measured probabilities. For
instance, we might know that at any point in time the server has a probability
of 1% of becoming disfunct and needs a restart. This probability should not be
affected by the specifications: there might be a program state in which a disfunct
server would necessarily lead to an inconsistency in the future. This should not
mean that the server cannot become disfunct and that the current program state
should be possible by definition. To capture such phenomena in a semantics, we
introduce probability-preserving semantics.
Definition 5. Let Mci [P] = hQ, Act, P, q0 , Λ, λi for an ontologized program P.
An MDP M is probability-preserving w.r.t. P if q0 is consistent and M =
hQ0 , Act, P 0 , q0 , Λ, λ0 i where
1. Q0 ⊆ Q contains only consistent states,
2. λ0 is obtained from λ by restricting its domain to Q0 , and
3. for all P 0 (q, σ, q 0 ) > 0 we have that P 0 (q, σ, q 0 ) = P (q, σ, q 0 ).
P is called probability-preservable if there exists a probability-preserving MDP
w.r.t. P. In case Q0 and P 0 are subset-maximal, M is the called the MDP
induced by P under probability-preserving semantics, denoted Mpp [P].
Note that Definition 5 requires M to be an MDP and hence, P 0 is a probability
transition function. Hence, Condition 3 implies that any transition that reaches
an inconsistent state with positive probability w.r.t. P has no corresponding
transition in P 0 .
To verify whether a program is probability-preservable, we have to take the
non-deterministic and the probabilistic choices of the program differently into ac-
count. This is different to the other notions of consistency discussed here, because
Semantics for Ontology-Mediated Verification 11
only a single path, going over non-deterministic and probabilistic choices indif-
ferently, is sufficient to witness inconsistency or probability-normalizability. We
can characterize probability-preservability as follows: a program is probability-
preservable iff there exists a resolution of the non-deterministic choices in the
program such that for all probabilistic choices an inconsistent state is never
reached. Thus, testing this property requires both existential and universal ex-
plorations of the state space, which is why we can use alternating Turing ma-
chines with polynomial space to solve the corresponding problem.
Theorem 3. Let L be a DL for which deciding entailment has complexity k.
Then, deciding whether an L-ontologized program is probability-preservable is
APSpacek -complete. For non-stochastic programs, it is PSpacek -complete.
Recall that APSpace = ExpTime (see for example Corollary 2 to Theorem
16.5 and Corollary 3 to Theorem 2.20 in [11]). However, as an exponential Turing
machine may also write exponentially long queries to the oracle, we may not
always have APSpacek = ExpTimek .
4.4 Ontology-mediated PMC
In [6] we presented a technique to apply PMC techniques to ontologized pro-
grams to perform quantitative analysis tasks on knowledge-intensive systems. For
this, we treated inconsistent states as consistent ones, following the consistency-
independent semantics presented in Section 4.1. Inconsistencies in ontologized
programs is not as bad as usually in other logic-based formalisms, as stochastic
properties can also be evaluated on MDPs with inconsistent states. In fact, they
can even have a designated meaning, e.g., modeling exceptions the program has
to face. An advantage of ontologized programs is that commands could be used
to detect when a program is in an inconsistent state. To this end, a guard employ-
ing a hook inc that is satisfied in exactly those states that are inconsistent, e.g.,
with cD(inc) = (> v ⊥), can invoke the actions to undertake when an exception
has occurred. Note that while all inconsistent states agree on the hooks that are
active (it is always the complete set of hooks), the command perspective of states
can still be different. Here, private variables may encode additional information
about the current state that can be used to decide how to react to inconsistencies.
An example for ontology-mediated PMC on consistency-independent semantics,
is to decide whether
Pmin (inc → (X¬inc ∨ XX¬inc)) > 95%
Intuitively, this states that an exception is always successfully handled with
high probability of at least 95% in the sense that whenever an inconsistent state
is reached, a consistent state is reached again within at most two steps. Such
a stochastic property can be checked using our method in [6] and the PMC
tool Prism [10].
Ontology-mediated PMC for probability-normalizing and -preserving seman-
tics is not as straight forward as under consistency-independent semantics. While
12 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
we could achieve a stochastic program that disallows to reach inconsistent states
also under consistency-independent semantics, this requires an explicit handling
of inconsistencies and modifications in the program that “provisions” the pos-
sible variable evaluations. More specifically, we then need a the possibility to
decide for each update in the command whether it would lead to an inconsistent
state or not. However, while this would work out well in our running example,
we cannot expect such an encoding for any ontologized program. Fortunately,
Definitions 4 and 5 are defined in a constructive way, i.e., these consistency-
dependent semantics are defined based on the consistency-independent one by
manipulating the state space and probabilistic transition function. Hence, we
could restrict the state space to consistent states and adjust further states and
probabilities on-the-fly during the construction process of the MDP.
5 Outlook
We are currently implementing a scenario to evaluate our implementation for
ontology-mediated PMC under the different semantics we presented in this pa-
per. Here, we can benefit from the constructive definition of our semantics that
evaluates inconsistent states beforehand and could hence directly included into
the model building process, e.g., in the probabilistic model checker Prism [10].
There are some theoretical results that are still left open but should be easy
to obtain: the complexity of the actual model-checking tasks, or the size of the
rewritings that our practical method produces. Furthermore, there are some ex-
tensions and modifications worth investigating: our semantics offer two possible
ways of treating probabilities occurring in the program to “restore” consistency.
The choice of which one to select depends on the kind of stochastic phenomena
actually modeled. It is easy to think of scenarios where both kinds of stochastics
occur. This would require a more flexible type of ontologized programs. In such
a program, some distributions may be marked as “fixed”, while others could
be subject to normalization. In our framework, modifications of program states
happen on the level of DL axioms and thus affect all models similarly to [4,8].
Another approach are DL action-based programs [1,14], where modifications of
states affect the level of interpretations. So, a variant of ontologized programs
where states are associated not with ontologies, but with interpretations, similar
to [1,14] is certainly an interesting direction for future research.
Acknowledgements
The authors are supported by the DFG through the Collaborative Research
Center TRR 248 (see https://perspicuous-computing.science, project ID
389792660), the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704,
as part of Germany’s Excellence Strategy), and the Research Training Groups
QuantLA (GRK 1763) and RoSI (GRK 1907).
Semantics for Ontology-Mediated Verification 13
References
1. Baader, F., Zarrieß, B.: Verification of Golog programs over description logic ac-
tions. In: Proceedings of FroCos 2013. LNCS, vol. 8152, pp. 181–196. Springer
(2013)
2. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
3. Baier, C., Dubslaff, C., Klüppelholz, S.: Trade-off analysis meets probabilistic
model checking. In: Proc. of the 23rd Conference on Computer Science Logic and
the 29th Symposium on Logic In Computer Science (CSL-LICS). pp. 1:1–1:10.
ACM (2014)
4. Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: Actions and programs
over description logic knowledge bases: A functional approach. In: Knowing, Rea-
soning, and Acting: Essays in Honour of H. J. Levesque. College Publications (2011)
5. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)
6. Dubslaff, C., Koopmann, P., Turhan, A.: Ontology-mediated probabilistic model
checking. In: Ahrendt, W., Tarifa, S.L.T. (eds.) Integrated Formal Methods - 15th
International Conference, IFM 2019. Lecture Notes in Computer Science, vol.
11918, pp. 194–211. Springer (2019). https://doi.org/10.1007/978-3-0u30-34968-
4 11
7. Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification
techniques for probabilistic systems. In: Proc. of the School on Formal Methods for
the Design of Computer, Communication and Software Systems, Formal Methods
for Eternal Networked Software Systems (SFM’11). LNCS, vol. 6659, pp. 53–113.
Springer (2011)
8. Hariri, B.B., Calvanese, D., Montali, M., De Giacomo, G., De Masellis, R., Felli,
P.: Description logic knowledge and action bases. J. Artif. Intell. Res. 46, 651–686
(2013)
9. Jifeng, H., Seidel, K., McIver, A.: Probabilistic models for the guarded command
language. Science of Computer Programming 28(2), 171 – 192 (1997)
10. Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of proba-
bilistic real-time systems. In: Proc. of the 23rd Intern. Conf. on Computer Aided
Verification (CAV’11). LNCS, vol. 6806, pp. 585–591 (2011)
11. Papadimitriou, C.H.: Computational complexity. Academic Internet Publ. (2007)
12. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foun-
dations of Computer Science, Providence, Rhode Island, USA, 31 October - 1
November 1977. pp. 46–57 (1977). https://doi.org/10.1109/SFCS.1977.32
13. Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Program-
ming. John Wiley & Sons, Inc., New York, NY (1994)
14. Zarrieß, B., Claßen, J.: Verification of knowledge-based programs over description
logic actions. In: IJCAI. pp. 3278–3284. AAAI Press (2015)
14 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
A Appendix
We provide here the proofs of our results that have been omitted due to space
constraints in the main paper.
A.1 Auxiliary Lemmas for the Hardness Results
We define the size of a concept/axiom/ontology in the usual way as its string
length, that is, the number of symbols needed to write it down, where concept,
role and individual names count as one, as do logical operators, and number
restrictions are encoded using unary encoding.
The following auxiliary lemma will be helpful for the hardness results, as it
shows how to represent ontologies based on a polynomially bounded enumeration
of DL axioms. We first need a more liberal definition of conservative extensions.
Definition 6. A renaming is a bijective function σ : NC ∪NR ∪NI → NC ∪NR ∪NI
s.t. σ(X) ∈ NC iff X ∈ NC , σ(X) ∈ NR iff X ∈ NR and σ(X) ∈ NI iff X ∈ NI .
Given an ontology O and a renaming σ, we denote by Oσ the result of replacing
every name X in O by σ(X).
Let O1 and O2 be two ontologies. Then, O1 is a conservative extension of O2
modulo renaming iff there exists some renaming σ s.t. for every axiom α using
only names in O2 , O1 σ |= α iff O2 |= α.
Lemma 1. There exists a polynomial function p s.t. for every n ∈ N, there exists
a polynomially computable function π from indices {0, . . . , p(n)} to SROIQ
axioms s.t. for every ontology O of size at most n, we can compute in time
polynomial in O a set I ⊆ {0, . . . , p(n)} s.t. {π(i) | i ∈ I} is a conservative
extension of O modulo renaming.
Proof. Let n ∈ N be our bound on ontology sizes. Using standard structural
transformations, we can compute for every SROIQ ontology O in polynomial
time a normalized ontology that is a conservative of O and in which every axiom
is of one of the following forms:
1. A1 v {a1 }, 5. ≤ir1 .A1 v A2 , 9. r1 (a1 , a2 ),
2. A1 u A2 v A3 , 6. A1 v ∃r.Self, 10. r1 v r2 ,
3. A1 v A2 t A3 , 7. ∃r.Self. v A1 , 11. r1 ◦ r2 v r3 ,
4. A1 v ≤ir1 .A2 , 8. A1 (a1 ), 12. Disj(r1 , r2 ),
where A1 , A2 , A3 ∈ NC ∪ {>, ⊥}, r1 , r2 , r3 ∈ NR , i ∈ N and a1 , a2 ∈ NI .
Let m be the maximal size of any ontology that is the result of normalizing
an ontology of size n. Note that m is polynomial in n. The number of concept
names, role names and individuals occurring in any normalized ontology O of
size m is bounded by m, and every number occurring in O is bounded by m as
well. This means, we can pick a set
X = {X1 , . . . , Xm } ⊆ NC ∪ {>, ⊥} ∪ NR ∪ NI
Semantics for Ontology-Mediated Verification 15
s.t. for every any normalized ontology O of size m there exists a renaming σ s.t.
Oσ uses only names from X. As the resulting ontology is still normalized, every
such ontology uses only axioms from the set
A = {α | α is normalized and uses only names from X and numbers ≤ m}
As there are 12 axiom types, and each uses at most 3 names from X and one
number, the number of axioms in A is bounded by p(n) = 12 · |X|3 · m = 12m4 ,
which is polynomial in n because m is polynomial in n.
The function π is required can then for example defined as follows: for i ∈
{0, . . . , p(n)}, we define π(i) = α, where
1. α is of the form (i mod 12) as above,
2. for a ∈ {1, 3}, Xj is the ath name occurring in α, where j = b 12mia−1 c
mod m, and
3. if α is of the form (4) or (5), i.e. it contains a number, then this number is
i
j = b 12m 3 c mod m
For every ontology O, we obtain the index set I as required by first normal-
izing O, renaming it accordingly, and then assigning the indices. t
u
Using an index function π as in Lemma 1, we can define a special type of
oracle Turing machines called (alternating) Turing machines with DL oracles.
Such a Turing machine uses an oracle tape with tape alphabet {0, 1, b} (b being
the blank symbol), and is specified using an enumeration π of DL axioms as
above, and some axiom α. Based on the current oracle tape content, we obtain
an index set I that contains the number i iff the oracle tape contains a 1 at
position i. The oracle then answers yes if {π(i) | i ∈ I} |= α, and no otherwise.
For a given DL L, we may additionally require that the oracle only accepts
inputs for which the corresponding ontology is in L, in which case we call the
Turing machine a Turing machine with L-oracle for π, α.
Lemma 2. Let k be a complexity class and L a DL for which deciding entailment
is k-hard. Then, for every Turing machine T with k-oracle and bound n on the
size of the oracle tape, we can construct in time polynomial in n and T a Turing
machine T 0 with L-oracle for some axiom enumeration π and CI α that accepts
the same set of words with at most polynomial overhead.
Proof. We first argue that it suffices to focus on entailment of axioms of the
form α = A(a), since entailment of CIs can be reduced to it. Specifically, for any
ontology O and CI C v D, we have O |= C v D iff O ∪ {C(a), D v A} |= A(a),
where a and A do not occur in O. Because entailment in L is k-hard, we can
construct for every query to the k-oracle in polynomial time an ontology O that
entails α iff the query should return true. Because the oracle tape is bounded,
we can use Lemma 1 to translate that ontology into a corresponding index set
to serve as input for the L-oracle. T 0 thus proceeds as T , but before sending
a query to the oracle, it reduces it to the entailment of the axiom α from an
ontology O, which it then translates to a query to the L-oracle. t
u
16 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
A.2 Consistency-Independent Semantics
Theorem 1. Let L be a DL such that deciding entailment in L is k-complete.
Then, deciding consistency of L-ontologized programs is PSpacek -complete, even
for non-stochastic programs.
Proof. Let M[P] be the MDP induced by some ontologized program P as in
Definition 3 where K is expressed in L. For the upper bound, we specify a
non-deterministic PSpace algorithm that, starting from the initial state, ex-
plores all reachable states in M[P] and decides in k whether the current state
is inconsistent. Specifically, for each current variable evaluation in P, we non-
deterministically select a command in PP whose guard is satisfied. Then, we
non-deterministically select an update that has a positive probability in the dis-
tribution of the command and apply this update on the current evaluation. In
each step, we use a k-oracle to determine whether the current state is consistent,
and which hooks are active. As each state can be stored in polynomial space,
the algorithm runs in PSpacek .
For the lower bound, we provide a polynomial reduction of the acceptance
problem for polynomially space bounded, deterministic Turing machines T with
k-oracle. Let
T = hQ, Γ, γ0 , Γi , Γo , q0 , F, δ, q? , q+ , q− i
be such a Turing machine, where
– Q are the states,
– Γ = {γ0 , . . . γm } is the tape alphabet,
– γ0 is the blank symbol,
– Γi ⊆ Γ is the input alphabet,
– Γo is the oracle tape alphabet,
– q0 is the initial state,
– F ⊆ Q is the set of accepting states,
– δ : (Q \ (F ∪ {q? })) × Γ × Γo → Q × Γ × {−1, 0, +1} × Γo × {−1, 0, +1}
is the transition relation, (which works on two tapes, the standard tape and
the oracle tape),
– q? ∈ Q \ F is the query state to query the oracle, and
– q+ , q− ∈ Q \ F are the query answer states.
The Turing machine uses two polynomially bounded tapes: one standard tape
and one oracle tape. In every state that is non-final and not the query state, δ
defines the successor state of T . Whenever the current state is q? , the oracle is
invoked, leading to T entering q+ in the next step if the oracle accepts the content
of the oracle tape, and entering q− otherwise. Based on T and the input word
w = σ0 . . . σl , we build an ontologized program PT,w s.t. PT,w is inconsistent iff
T accepts w.
Since entailment in L is k-hard, we can use Lemma 2 to construct a polyno-
mially space-bounded Turing machine T 0 with L-oracle for π, A(a) that accepts
Semantics for Ontology-Mediated Verification 17
w iff so does T . Specifically, we obtain a set Fq of DL axioms, polynomially
bounded in |w|, a mapping π : {0, . . . , r(|w|)} 7→ Fq , where r is a polynomial,
T 0 = hQ0 , Γ, γ0 , Γi , {0, 1}, q0 , F 0 , δ 0 , q? , q+ , q− i,
where Q0 = {q0 , . . . , qn }, and T 0 accepts the same language as T , is still poly-
nomially space-bounded, but uses a different oracle. If T 0 is in state q? , and the
oracle tape contains the word σ0 . . . σr(|w|) , the Turing machine moves into the
state q+ iff {π(i) | 0 ≤ i ≤ r(|w|), σi = 1} |= A(a), and otherwise moves to q− .
Based on this Turing machine, we construct the ontologized program PT,w .
Let p be a polynomial s.t. T 0 uses at most p(|w|) tape cells on input w. The
program uses the following variables:
– state ∈ {0, . . . , n} stores the state of the Turing machine,
– for 0 ≤ i ≤ p(|w|), dtape i ∈ {0, . . . , m} stores the letter on the default tape
position i,
– for 0 ≤ i ≤ r(|w|), otape i ∈ {0, 1} stores the letter on the oracle tape at
position i,
– dpos ∈ {0, . . . , p(|w|)} stores the current position on the default tape,
– opos ∈ {0, . . . , r(|w|)} stores the current position on the oracle tape.
We use a single hook H = {oracle yes} standing for the positive oracle answer.
For every
hhqi1 , γi2 , γi3 i, hqi4 , γi5 , Dird , γi6 , Diro ii ∈ δ 0 ,
every i ∈ {0, . . . , p(|w|)} and every j ∈ {0, . . . , r(|w|)}, we use the following
non-stochastic command:
state=i1 state := i4
∧dpos=i ∧ dtape i=i2 7→ dtape i := i5 , dpos := dpos + Dird , (3)
∧opos=j ∧ otape j=i3 otape j := i6 , opos := opos + Diro
To handle the behavior of the oracle, we further add the following commands,
where q? = qi1 , q+ = qi2 and q− = qi3
state = i1 ∧ oracle yes 7→ state := i2 (4)
state = i1 ∧ ¬oracle yes 7→ state := i3 (5)
The initial state ηP,0 of the program is the evaluation state = 0, dtape i =
wi for i ∈ {0, . . . , l}, dtape i = 0 for i ∈ {l, . . . , p(|w|)}, otape i = 0 for
i ∈ {0, . . . , r(|w|)}, dpos = otape = 0. This completes the definition of the
program component P in PT,w .
As DL axioms, we set for the static DL knowledge K = ∅ and for the fluents
F = Fq ∪ {> v ⊥}. It remains to specify the interface functions Dc and cD. For
Dc, we set for every i ∈ {0, . . . , r(|w|)},
Dc(π(i)) = otape i = 1
18 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
to translate the oracle calls, and
_
Dc(> v ⊥) = state = i ,
qi ∈F
to encode that the ontologized states that correspond to accepting states in the
Turing machine are inconsistent. Finally, we specify cD by setting
cD(oracle yes) = {A(a)}.
It is standard to verify that the Turing machine T 0 accepts w iff the ontologized
program PT,w is inconsistent, i.e., can reach an inconsistent state. Since T ac-
cepts w iff so does T 0 , this completes the reduction. t
u
A.3 Probability-Normalizing Semantics
Theorem 2. Let L be a DL for which deciding entailment has complexity k.
Then, deciding whether an L-ontologized program is probability-normalizable is
PSpacek -complete, even for non-stochastic programs.
Proof. For the upper bound, note that the only way for P to be inconsistent un-
der probability-normalizing semantics is if all probabilistic choices would lead to
an inconsistent state in the M[P]. We can thus use a non-deterministic PSpacek -
algorithm similar to the one described in the proof for Theorem 1 to determine
whether a program is probability-normalizable: instead of testing for inconsis-
tency of the current state, we here test for consistency. Note that it is sufficient
to find a single execution path that never reaches an inconsistent state for an on-
tologized program to be probability-normalizable. This execution path might be
infinite, however, because the state space is bounded, any infinite execution path
would need to visit a state twice. We use a counter to put an exponential bound
on the states to be visited, and store a non-deterministically selected state for
later comparison. If this state repeats, we found an unbounded execution path
that never visits an inconsistent state, and accept. If we reach the bound, such
a loop was not found and we reject.
For the lower bound, we note that the reduction used in the proof for Theo-
rem 1 can also be used for probability-normalizability. In that reduction, we re-
duce the word-problem of deterministic polynomially-space bounded Turing ma-
chines with k-oracle to consistency of ontologized programs under consistency-
independent semantics. Inspection of the construction reveals that the con-
structed program PT,w is not only non-stochastic, but even deterministic, by
which we mean that in every ontologized state, there is at most one command
that can be executed. Specifically, there is exactly one Command (3) in the proof
of Theorem 1 for each assignment to the variables state, dpos, opos, dtape -
i and otape j, which means that in each ontologized state, at most one of
these commands is executable. Moreover, for the assignment state = i1 , where
qi1 = q? denotes the oracle query state, there is no such command, as there
Semantics for Ontology-Mediated Verification 19
is no transition in the Turing machine for those states, and exactly one of the
commands (4) and (5) is executable if state = i1 , unless if the state is incon-
sistent. We obtain that, if some path in M[PT,w ] leads from the initial state to
an inconsistent state, then all paths lead to an inconsistent state, in which case
the program is not probability-normalizable. Consequently, PT,w is probability-
normalizable iff PT,w is consistent, which is the case iff T does not accept w. Since
non-acceptance of words in polynomially space-bounded Turing-machines with
k-oracle is also PSpacek -complete, we obtain that probability-normalizability is
PSpacek -hard. tu
A.4 Probability-Preserving Semantics
Theorem 3. Let L be a DL for which deciding entailment has complexity k.
Then, deciding whether an L-ontologized program is probability-preservable is
APSpacek -complete. For non-stochastic programs, it is PSpacek -complete.
Proof. Both bounds are via reductions from and to alternating Turing machines.
In an alternating Turing machine, we switch between ∃-non-determinism and ∀-
non-determinism, meaning that the Turing machine can switch between ∃-non-
deterministic choices and ∀-non-deterministic transitions. Acceptance is then
defined inductively according to the choices involved: a configuration is accepting
if 1) it is in an accepting state, 2) there exists an ∃-non-deterministic transition
to a configuration that is accepting, or 3) all ∀-non-deterministic transitions lead
to an accepting configuration.
For the upper bounds, we use a modification of the algorithm used in the
proof for Theorem 1 that runs in alternating polynomial space and decides
probability-preservability of ontologized programs. Let P be an ontologized pro-
gram as in Definition 1, and Mci [P] = hQ, Act, P, ι, Λ, λ, wgti the MDP induced
by P under consistency-independent semantics. The algorithm guesses the states
q ∈ Q to be included in the probability-preserving MDP one after the other,
starting from ι, where we use alternation to switch between the non-deterministic
and the probabilistic choices of the program. Specifically, we have to guess a set
of states Q0 s.t.: 1) no state in Q0 is inconsistent, 2) for every Q0 there is always
some guarded command that can be executed on the current state, and 3) all
successor-states into which this command would bring us with a positive prob-
ability are included in Q0 . Our algorithm thus proceeds as follows based on the
currently guessed state. If the current state is inconsistent, we reject. Otherwise,
we non-deterministically select a guarded command hg, σi ∈ CP s.t. q |= g (∃-
non-determinism) and continue on all states q 0 ∈ Q such that P (q, σ, q 0 ) > 0,
q 0 ∈ Q0 (∀-non-determinism). Each state takes polynomial space, and we use a
k-oracle to determine which hooks are active and whether the state is consistent.
Since this procedure can be implemented by an alternating Turing machine with
k-oracle that uses polynomial space, probability-preservability can be decided
in APSpacek . If the program is non-stochastic, the ∀-non-determinism is not
needed, and the algorithm runs in PSpacek .
20 Clemens Dubslaff, Patrick Koopmann, and Anni-Yasmin Turhan
For the lower bound, we adapt the reduction used in the proof for Theorem 1.
However, this time, we reduce the word acceptance problem for polynomially
space bounded alternating Turing machines with k-oracle. Specifically, let
T = hQ, Γ, γ0 , Γi , Γo , q0 , F, δ, q? , q+ , q− , gi,
be such a Turing machine, where Q = {q0 , . . . , qn }, Γ = {γ0 , . . . γn } is the
standard tape alphabet, γ0 ∈ Γi is the blank symbol, Γi ⊆ Γ is the input
alphabet, Γo is the oracle alphabet, q0 is the initial state, F ⊆ Q∧ ∪ Q∨ is the
set of accepting states,
δ : (Q \ (F ∪ {q? })) × Γ × Γo → ℘(Q × Γ × {−1, +1} × Γo ∪ {−1, +1})
is the transition function, the states q? , q+ q− ∈ Q manage the querying of the
oracle, and g : Q → {∀, ∃, accept, reject} partitions the states Q into four cat-
egories of universal and existential quantified states, and accepting and rejecting
states, respectively. The definition of acceptance is standard, specifically, the
oracle works as in the proof for Theorem 1, and a configuration with state q is
accepting 1) if g(q) = accept, 2) g(q) = ∃ and one of the successor configurations
is accepting, or 3) g(q) = ∀ and all successor configurations are accepting.
Again, we use Lemma 2 to construct, based on T and the input word w, a
polynomially bounded set Fq of DL axioms, a mapping π : Fq → {0, . . . , r(|w|)},
where r is a polynomial, and an alternating Turing machine
T 0 = hQ0 , Γ, γ0 , Γi , {0, 1, b}, q0 , F 0 , δ 0 , q? , q+ , q− , g 0 i
with an L-oracle for π, A v B, that is polynomially space-bounded, and accepts
w iff so does T 0 . If T 0 is in state q? , and the oracle tape contains the word
σ0 . . . σr(|w|) , the Turing machines moves into the state q+ iff
π(i) | 0 ≤ i ≤ r(|w|), σi = 1 |= A(a),
and otherwise moves to q− . Based on this Turing machine, we construct the
ontologized program PT,w in the same way as in the proof for Theorem 1, but
with a different set CP of commands.
We first model the ∀-transitions. For every
t = hqi1 , γi2 , γi3 i ∈ (Q \ (F ∪ {q? , q+ , q− })) × Γ × Γo ,
where g 0 (qi1 ) = ∀, every hqi4 , γi5 , Dird , γi6 , Diro i ∈ δ 0 (t), every i ∈ {0, . . . , p(|w|)}
and every j ∈ {0, . . . , r(|w|)}, we use the command
state = i1 state := i4
∧ dpos = i ∧ dtape i = i2 7→ dtape i := i5 , dpos := dpos + Dird ,
∧ opos = j ∧ otape j = i3 otape j := i6 , opos := opos + Diro
Note that for the program to be not probability preservable, every command
that we can execute in an ontologized state leads to an inconsistency, which is
Semantics for Ontology-Mediated Verification 21
why we model ∀-transitions in this way. For the ∃-transitions, we make use of
the stochastic component. Let
t1 = hqi1 , γi2 , γi3 i ∈ (Q \ (F ∪ {q? , q+ , q− })) × Γ × Γo ,
where g 0 (qi1 ) = ∃. For every i ∈ {0, . . . , p(|w|)} and j ∈ {0, . . . , r(|w|)}, we add
the stochastic command
state = i1
∧ dpos = i ∧ dtape i = i2 7→ σ
∧ opos = j ∧ otape j = i3
where σ is the stochastic update such that for every
t2 = hqi4 , γi5 , Dird , γi6 , Diro i ∈ δ 0 (t1 ),
we have
state := i4
1
σ dtape i := i5 , dpos := dpos + Dird , = 0 .
|δ (t1 )|
otape j := i6 , opos := opos + Diro
The corresponding transitions are excluded from the probability-preserving MDP
if there is a positive probability of getting into an inconsistent state. To this end,
we can model ∃-transitions in this way.
The stochastic commands that handle the use of the oracle are as in the proof
for Theorem 1. It is standard to show that the resulting program is probability-
preserving iff w is accepted by the Turing machine, so that we obtain that
probability-preservability is APSpacek -hard.
Now assume that for no state q ∈ Q, g 0 (q) = ∃. T then corresponds to
a coNPSpacek -machine, and the ontologized program PT,w is non-stochastic.
As a consequence, deciding whether non-stochastic programs are probability-
preserving is coNPSpacek = PSpacek -hard. t
u