Verification of Knowledge-Based Programs over Description Logic Actions

1 Introduction

Since the GOLOG [Levesque et al., 1997; De Giacomo et al., 2000] family of action programming languages has become a popular means for control of high-level agents, the verification of temporal properties of GOLOG programs has recently received increasing attention [Claßen and Lakemeyer, 2008; De Giacomo et al., 2010]. Both the GOLOG language itself and the underlying Situation Calculus [McCarthy and Hayes, 1969; Reiter, 2001a] are of high (first-order) expressivity, which renders the general problem undecidable. Identifying non-trivial fragments where decidability is given is therefore a worthwhile endeavour [De Giacomo et al., 2012; Zarrieß and Claßen, 2014].

Here we consider the class of so-called knowledge-based programs, which are suited for more realistic scenarios where the agent possesses only incomplete information about its surroundings and has to use sensing in order to acquire additional knowledge at run-time. As opposed to classical GOLOG, knowledge-based programs contain explicit references to the agent's knowledge, thus enabling it to choose its course of action based on what it knows and does not know. Formalizations of knowledge-based programs were

Jens Claßen

Knowledge-Based Systems Group RWTH Aachen University, Germany classen@kbsg.rwth-aachen.de

proposed by Reiter [2001b] and later by Claßen and Lakemeyer [2006] based on Scherl and Levesque's [2003] account of an epistemic Situation Calculus and Lakemeyer and Levesque's [2004; 2010] modal variant ES, respectively. Common to these approaches is that conditions in the program are evaluated by reducing reasoning about both knowledge and action to standard first-order theorem proving.

In this paper, we propose a new epistemic action formalism based on the basic Description Logic (DL) ALC by combining and extending earlier proposals for DL action formalisms [Baader et al., 2005] and epistemic DLs [Donini et al., 1998]. From the latter we use a concept constructor for knowledge to formulate test conditions within programs and desired properties thereof, while we extend the former by not only including physical, but also sensing actions. As will become apparent, representing and verifying knowledge-based programs with this language yields multiple advantages. First, we obtain decidability of verification for a formalism whose expressiveness goes far beyond propositional logic. Moreover, it enables us to resort to powerful DL reasoning systems. Finally, the new formalism also inherits many useful properties of the epistemic Situation Calculus and ES such as Reiter's [1991] solution to the frame problem, a variant of Levesque's [1990] notion of only-knowing, and a reasoning mechanism resembling Levesque and Lakemeyer's [2001] Representation Theorem where reasoning about knowledge is reduced to standard DL reasoning.

As a motivating example, consider a mobile robot in a factory whose task it is to detect faults in gears and do the necessary repairs before turning them on. The agent is equipped with an (objective) DL knowledge base consisting of a TBox and an ABox, as usual. The TBox defines basic terminology such as the role name has-f that relates a system to its faults. The ABox gives an incomplete description of the initial situation and provides some properties of possible faults. Assume that the agent has two pure sensing actions at its disposal, namely sense-f(gear, x) to sense whether the individual gear has fault x and sense-on(gear) to check if gear is on or not. Furthermore, the physical action repair(gear, x) is available to remove a fault. An example for a knowledgebased program for this agent is given in Figure 1. As long as the agent does not know that gear has no known fault, a known fault x is chosen non-deterministically for which it is unknown whether gear has it or not. The agent then senses

while ¬K(∀has-f.¬KFault)(gear) pick(x) : KFault(x) ∧ ¬Khas-f(gear, x) ∧ ¬K¬has-f(gear, x)?. sense-f(gear, x); if Khas-f(gear, x) then repair(gear, x) else continue; end turn-on(gear); sense-on(gear); if K¬On(gear) then raise-alarm else continue;

whether gear has this fault and repairs it if necessary. After completing the loop the agent turns on the gear system and checks if this was successful. If not, then there must be an unknown fault and an alarm is raised. An example for a property of this program to be verified is if a gear initially has an unknown critical fault, then the agent will eventually come to know it.

The remainder of this paper starts with recalling basic notion of DLs for representing initial knowledge, effect conditions of primitive actions, sensing properties, tests in programs and temporal properties of programs. In Section 3 we present our new action formalism that allows us to model both sensing and acting and consider the projection problem as a basic reasoning task. Section 4 then is about the verification of programs. We define syntax and semantics of the programming language and show how to specify temporal properties of programs. Afterwards, we discuss a restricted fragment where verification becomes decidable and that in some respect even goes beyond earlier work on nonepistemic programs [Zarrieß and Claßen, 2014], namely by re-introducing a limited variant of the operator for the nondeterministic choice of arguments ("pick operator"). We provide a constructive proof (along with an upper bound on the procedure's complexity) in which our variant of the Representation Theorem is used to build a finite abstraction of a program's transition system by means of DL reasoning, after which standard propositional model checking can be applied.

Due to space constraints all detailed proofs must be omitted. They can be found in the accompanying technical report [Zarrieß and Claßen, 2015].

2 The Epistemic Description Logic ALCOK

Here we introduce the syntax and semantics of the epistemic DL ALCOK following [Donini et al., 1998]. It extends the basic DL ALC by singleton concepts called nominals (O), and by an epistemic role and concept constructor (K). Although we sometimes only use the objective sublogics ALC and ALCO, we present all basic notions here for full ALCOK.

Let NR, NC, NI be countably infinite sets of role names, concept names and individual names, respectively. A generalized ALCOK-role P is built from role names using the epistemic role constructor and role negation (see Table 1). A simple ALCOK-role (role for short) is a generalized role without role negation. ALCOK-concept descriptions (concepts for short) are built from (simple) roles, concept names and the concept constructors shown in the lower part of Table 1 where a ∈ NI. The following concept constructors are defined as abbreviations: C⊔D := ¬(¬C⊓¬D), KwC := KC⊔K¬C and ∀R.C := ¬∃R.¬C. Intuitively, an object belongs to the concept KwC if it is known whether it belongs to C or to ¬C. In the following we often use the symbols r for a role name, R for a role, P for a generalized role, A for a concept name, C,D for possibly complex concepts, and a, b for individual names (individuals).

The different kinds of ALCOK-axioms are shown in Table 2. A TBox T is a finite set of concept inclusions (CIs for short) and an ABox A is a finite set of concept and role assertions (also called ABox assertions), where assertions of the form A(a), ¬A(a), r(a, b), ¬r(a, b) are called literals. A knowl-

edge base (KB) K = (T , A) consists of a TBox and an ABox. ALCOK uses a possible world semantics defined in terms of interpretations. An interpretation I = (∆I , ·I ) consists of a non-empty domain ∆I and a mapping ·I with AI ⊆ ∆I for all A ∈ NC, rI ⊆ ∆I ×∆I for all r ∈ NR and aI ∈ ∆I for all a ∈ NI. Here we adopt the so called standard name assumption (SNA): all interpretations are defined over a fixed countably infinite domain of standard names, denoted by ∆, with a fixed interpretation of individuals: We define ∆ := NI and we assume that for any interpretation I, ∆I = ∆ and aI = a for all a ∈ NI. An epistemic interpretation is a pair (I,W) consisting of an interpretation I and a set of interpretations W. The interpretation function ·I,W maps concepts and roles to subsets of ∆ and ∆×∆, respectively, as given in Table 1. Satisfaction of an axiom ϱ in (I,W), denoted by (I,W) ||= ϱ, is defined as given in Table 2, and translates to ABoxes, TBoxes and KBs in the obvious way.

An epistemic model of a KB K is a non-empty set of interpretations M such that for all I ∈ M it holds that

(I,M) ||= K and for all sets of interpretations M′ with M⊊M′ there exists J ∈M′ such that (J ,M′ ) ̸||= K.

An axiom ϱ is epistemically entailed by K, written as K ||= ϱ, iff for all epistemic models M of K and for all I ∈ M it holds that (I,M) ||= ϱ. K is called consistent if K has an epistemic model.

A concept, axiom, TBox, ABox or KB without any occurrences of K is called objective, and subjective if all occurring concept and role names occur within the scope of a K.

In case of an objective concept C we sometimes write C I instead of C I,W and I |= X instead of (I,W) ||= X for an objective axiom, KB, TBox or ABox X. Likewise, for an objective KB K and objective axiom ϱ we write K |= ϱ instead of K ||= ϱ. We also sometimes omit I if we deal with subjective concepts, roles and axioms.

For an objective KB K there exists a unique epistemic model. This unique epistemic model of K is given by M(K) = {I | I |= K}.

3 Actions with Sensing

We introduce a simple notion of primitive actions describing the basic abilities of an agent to change the world and to gain new information from the environment. Primitive actions are defined as syntactical objects composed of (parametrized) ABox assertions representing effects, effect conditions and properties of the environment that can be sensed, and are equipped with a purely model-theoretic semantics.

To define the syntax of actions, let NV be a countably infinite set of variables. An atom is an ABox assertion where in place of individuals also variables are allowed, i.e. atoms are of the form C(z) or P(z, z′ ) with z, z′ ∈ NV ∪NI. Primitive atoms are of the form A(z), ¬A(z), r(z, z′ ) or ¬r(z, z′ ). A formula is a boolean combination of atoms. The set of all variables occurring in a formula ψ is denoted by Var(ψ). A formula without variables is called ground formula. Subjectivity and objectivity of formulas is defined in the obvious way. We will use the symbols ϕ for atoms, γ for primitive atoms and ψ for formulas.

Definition 1. An effect is either of the formψ/γ (conditional effect) or of the form γ (unconditional effect), where ψ is an objective formula called effect condition and γ a primitive atom. A primitive action α is a pair α : (eff, sense) where eff is a finite set of effects and sense a finite set of objective formulas. We often write α(x1, . . . , xn) where x1, . . . , xn are the variables occurring in α. An action without variables is called ground action.

turn-on(x) : (eff = {(¬∃has-f.CritFault(x))/On(x)}) sense-on(x) : (sense = {On(x)}).

Figure 2 shows an example of a pure physical action and a pure sensing action where the sets sense and eff, respectively, are omitted. turn-on(x) has a single conditional effect that causes x to be On after the action is executed only if x previously has no critical fault. Note that here effects and their conditions are restricted to be objective since eff is supposed to only encode physical effects. sense-on(x) is a sensing action that represents the agent's ability to perceive whether On(x) is true in the real world. Again, formulas in sense are objective since sensors only provide information about the outside world.

Semantically, a primitive action induces a binary relation on epistemic interpretations (I,W) which allows us to explicitly distinguish changes affecting the real world represented by I and changes to the knowledge state W.

To execute an action we first need to instantiate it. A variable mapping ν is a total function of the form ν : NV →∆. We write ψν to denote the ground formula that is obtained from the formula ψ by replacing each variable x ∈ Var(ψ) by ν(x). Similarly, given a primitive action α : (eff, sense), αν : (eff ν , senseν ) denotes the corresponding ground action.

Next we define how a single interpretation I is affected by a set of literals L. The update of I with L is an interpretation I L that is defined as follows:

for all A ∈ NC and all r ∈ NR. For a given set of ground effects E and an interpretation I we define an effect function E that maps E and I to a set of literals given by:

To define how sensing affects the knowledge of the agent we introduce the notion of sensing compatibility of interpretations. Two interpretations I and J are sensing compatible w.r.t. a primitive ground action β : (eff, sense), written as I ∼β J , if for all ψ ∈ sense it holds that I |= ψ iff J |= ψ.

Now we are ready to define the execution semantics of a primitive ground action.

Definition 2. Let β : (eff, sense) be a primitive ground action, (I,W) an epistemic interpretation with I ∈ W and (I ′ ,W′ ) an epistemic interpretation. We write (I,W) =⇒β (I ′ ,W′ ), if the following conditions are satisfied:

• I ′ = I L with L = E(eff, I) and
• W′ = {J L | J ∈W,J ∼β I, L = E(eff,J)}.

Let σ = β0, . . . , βn-1 be a sequence of primitive ground actions. We write (I0,W0) =⇒σ (In,Wn) as an abbreviation for (I0,W0) =⇒β0 (I1,W1) =⇒β1 · · · =⇒βn-1 (In,Wn). The real world I of an epistemic interpretation (I,W) is updated according to the physical effects eff. Intuitively, from I the agent receives information about the truth of each formula in sense. Interpretations in W contradicting this information are discarded, while those that agree with I are updated as well, yielding the new knowledge state. Thus, in our semantics the agent is fully aware of all effects of an action.

As a basic reasoning task we consider projection.

Definition 3 (projection). Let K = (T ,A) be an objective KB, σ a sequence of primitive ground actions and ψ an ALCOK-ground formula or ALC-CI. We say that ψ is valid after executing σ in K iff for all I ∈ M(K) it holds that (I ′ ,W′ ) ||= ψ where (I,M(K)) =⇒σ (I ′ ,W′ ).

Note that the TBox T is only required to hold and to be known in the initial state, and that later states resulting from the execution of actions may violate it. While the persistence of T is thus not enforced in our formalization, checking this property is simply a special case of the projection problem.

Figure 3: Example initial knowledge base K = (T , A)

Example 4. Figure 3 shows an initial KB K for our example domain. The first CI in T states that faults are critical faults or uncritical ones, the last two CIs define the domain System and range Fault for the role has-f. A describes a simple initial situation. Assume K is all the agent knows initially about the world. Thus, it is known that gear is not on, but the effect condition ¬∃has-f.CritFault(gear) of turn-on(gear) is unknown (there is a least one possible world inM(K) satisfying it and one that does not). Consequently, after executing turn-on(gear) in K, we get that ¬KwOn(gear) is valid. If the agent now in turn executes sense-on(gear), it will also come to know whether gear has a critical fault or not, i.e. both Kw∃has-f.CritFault(gear) and KwOn(gear) are valid.

The correctness of our action semantics can be shown by an embedding into the epistemic Situation Calculus based on the modal first-order logic ES [Lakemeyer and Levesque, 2004; 2010]. The embedding is done by translating the initial KB and the primitive actions into a Reiter-style basic action theory (BAT) formulated in ES. The definition of our action semantics and the projection problem cause the initial KB and the (possibly conditional) effects of primitive actions to be everything the agent knows about the world and its dynamics. We have shown in [Zarrieß and Claßen, 2015] that the projection problem in our formalism thus exactly corresponds to an entailment problem in ES formulated by means of the onlyknowing modality and the translated BAT.

4 Verification of Knowledge-Based Programs

We are now ready to assemble complex programs for describing the behavior of a knowledge-based agent. To specify desired properties of such programs we use a temporal extension of ALCOK. Our main objective is to identify fragments of the programming language such that the verification problem, i.e. the problem of deciding whether all runs of a program satisfy the specified property, is decidable.

4.1 ALCOK-Golog Programs

In this section we define the syntax and semantics of a Gologlike action programming language [Levesque et al., 1997] that uses the action formalism introduced in the previous section. It allows to define complex behaviour through program expressions which are constructed from primitive actions, programming constructs, and tests formulated in ALCOK.

A program expression δ is built according to the following grammar:

A program can thus be the empty program [], a primitive action α, a test ψ?, where ψ is an ALCOK-formula, or constructed from subprograms by means of sequence δ; δ, nondeterministic iteration δ∗ (meaning execute δ zero or more times), non-deterministic choice δ|δ, and the guarded pick constructor pick(⃗x) : ψ?.δ, where ψ is a ALCOK-formula and ⃗x are free variables in ψ and δ. Intuitively, the agent executes a guarded pick by non-deterministically choosing a binding ⃗a from ∆ for the ⃗x such that ψ with ⃗x replaced by ⃗a is satisfied, after which it executes δ using the same bindings. An expression pick(⃗x) : ψ? is called guarded pick. Conditionals and while-loops can be defined in terms of the above, namely by if ψ then δ else δ′ end := (ψ?; δ)|(¬ψ?; δ′ ) and while ψ do δ end := (ψ?; δ)∗ ; ¬ψ?.

Definition 5 (ALCOK-Golog Program). Let K = (T ,A) be a consistent ALC-KB, Σ a finite set of primitive actions, and δ a program expression such that all primitive actions in δ are from Σ. An ALCOK-Golog program is of the form P = (K,Σ, δ), where we require that Σ contains two predefined purely physical actions ϵ : (eff = {Term(p)}) and f : (eff = {Fail(p)}) for indicating termination and failure of a program, respectively. Both special actions do not occur in δ and also the names Term and Fail are not used in T or in any other action or test. Furthermore, we require that {¬Term(p), ¬Fail(p)} ⊆ A and δ is closed, i.e. all variables in δ are bound by a guarded pick. P is called knowledgebased if all tests in δ are subjective.

For the execution of a program we split up the program expression into its atomic programs and then execute these atomic programs step by step. An atomic program, denoted by a, is either a primitive action, a test or a guarded pick. We introduce two functions head(·) and tail(·, ·). Intuitively, head(δ) contains those atomic programs that can be executed first when executing the program expression δ. It is defined by induction on the structure of δ. For instance, we have head([]) := {ϵ}, head(δ∗ ) := {ϵ} ∪ head(δ) and

For a ∈ head(δ), tail(a, δ) yields the remainder of the program, i.e., the part that still needs to be executed after a has been executed. For instance we have

The complete definitions of head and tail can be found in [Zarrieß and Claßen, 2015]. Note that if a program is "eaten up" completely, the termination action ϵ can be found in the head. We call a program expression that can be reached by a sequence of such head and tail applications a reachable subprogram. The set of all reachable subprograms for an expression δ is denoted by sub(δ). For a program expression ρ and a variable mapping ν, ρν denotes the program expression obtained by replacing each occurrence of a free variable x in ρ by ν(x). We define subg(ρ) := {ζ ν | ζ ∈ sub(ρ), ν is a variable mapping}.

Given these auxiliary notions, we can define the semantics of a program P = (K,Σ, δ) as a transition system TP = (Q,→, I) with a set of states Q, a transition relation → and a set of initial states I ⊆ Q. A state is a pair 〈(I,W), ρ〉 ∈ Q consisting of an epistemic interpretation (I,W) with I ∈ W and ρ ∈ subg(δ).

There is a transition 〈(I,W), ρ〉 → 〈(I ′ ,W′ ), ρ′ 〉, iff

• there exists a primitive action α ∈ head(ρ) such that (I,W) =⇒α (I ′ ,W′ ) and ρ′ ∈ tail(α, ρ) or
• there exists a test ψ? ∈ head(ρ) such that (I,W) ||= ψ, (I ′ ,W′ ) = (I,W) and ρ′ ∈ tail(ψ?, ρ) or
• there exists pick(⃗x) : ψ? ∈ head(ρ) and a variable map ν such that (I,W) ||= ψν , (I ′ ,W′ ) = (I,W) and there is ζ ∈ tail(pick(⃗x) : ψ?, ρ) with ρ′ = ζ ν ,
• or, if no atomic program in the head of ρ is applicable, then the failure action f is executed in (I,W) by leaving ρ unchanged.

Due to the distinguished actions ϵ and f, a successor state is always guaranteed to exist. The initial states are of the form 〈(I,M(K)), δ〉 with I ∈ M(K). A run π of a program P is an infinite path in TP = (Q,→, I) starting in an initial state. The infinite sequence of epistemic interpretations occurring in the states along a run π is denoted by I(π).

4.2 Specifying Temporal Properties of Programs

To specify temporal properties of a given program we use the logic ALCOK-LTL that generalizes ALC-LTL [Baader et al., 2008]. ALCOK-LTL formulas are built according to the following grammar:

where ϱ stands for an ALCOK-ABox assertion or ALC-CI. We use the following usual abbreviations: ✸Φ := ⊤(a) U Φ (eventually), ✷Φ := ¬✸¬Φ (globally) and Φ1 → Φ2 := ¬Φ1 ∨ Φ2.

The semantics of ALCOK-LTL is based on the notion of an ALCOK-LTL structure, which is an infinite sequence of epistemic interpretations I = (Ii,Wi)i=0,1,2,.... Let Φ be an ALCOK-LTL formula, I an ALCOK-LTL structure, and i ∈ {0, 1, 2, . . .} a time point. Validity of Φ in I at time i, denoted by I, i |= Φ, is defined as follows:

Now, we are ready to define the verification problem.

Definition 6. Let P = (K, Σ, δ) be an ALCOK-Golog program and Φ an ALCOK-LTL formula. The formula Φ is valid in P iff for all runs π of P it holds that I(π), 0 |= Φ.

Example 7. In a program that uses the program expression given in Figure 1 and the initial KB in Figure 3 the following property is valid:

saying that if gear has an unknown critical fault initially, then the agent will eventually recognize it. We can also verify executability and whether the TBox T is preserved along each run by checking validity of ✷(∧ϱ∈T ϱ ∧ ¬Fail(p)).

4.3 Verifying Restricted Programs

Unfortunately, it turns out that in the general case the verification problem is undecidable. The main source of undecidability is the high degree of non-determinism introduced by the guarded pick operator that allows to quantify arguments ranging over the whole countably infinite domain ∆. We get undecidability even in an already quite restricted subset of our language by a straightforward reduction of the halting problem of two-counter machines [Minsky, 1967].

Theorem 8. The verification problem is undecidable even if no CIs are used, the initial TBox is empty and the primitive actions have only unconditional effects, at most one argument, and provide no sensing result.

In order to retain decidability of the verification problem we restrict the syntax of the guards allowed in the pick-operators.

Definition 9. Let P = (K, Σ, δ) be an ALCOK-Golog program. P is called restricted if all guarded picks occurring in δ are of the form

with m ≥ 1 and for each ψi with 1 ≤ i ≤ m it holds that {x1, . . . , xn} ⊆ Var(ψi) and ψi is a conjunction of concept and role atoms of the form KC(z) and Kr(z, z′ ), respectively, where C is an ALC-concept with K ̸|= ⊤ ⊑ C. There are no restrictions on the formula ψ′ .

Note that the example program in Figure 1 is restricted. The restricted atoms in the guard of the pick-operator can also be viewed as objective instance queries posed to the current KB of the agent. The agent then chooses a binding for the variables among the retrieved answers. As a consequence of the restriction we obtain the following property for the transition system. From now on let Ind ⊆ ∆ be a fixed finite set of individuals, including all individuals occurring in P.

Lemma 10. Let P = (K,Σ, δ) be a restricted program, 〈(I,W), ρ〉 a state in TP reachable from an initial state, C an ALC-concept with K ̸|= ⊤ ⊑ C and r a role name. It holds that (Kr)W ⊆ Ind × Ind and (KC)W ⊆ Ind.

Consequently, the concepts and roles we use as qualifiers for objects chosen in the guards of a pick-operator have finite extensions under knowledge states reachable from an initial state. Thus, the range of the pick operator is limited to objects mentioned in P. Intuitively, the agent won't be able to directly cope with unknown individuals. As seen in our running example, the agent is able to recognize whether or not there is some unknown fault, but there is no possibility to directly access it.

However, even in this restricted setting the transition system has still infinitely many states. Since the epistemic model M(K) is infinite, there also infinitely many initial states, namely one initial state for each I ∈M(K).

To show decidability of the verification problem for restricted programs, we basically proceed as in [Baader and Zarrieß, 2013; Zarrieß and Claßen, 2014]: We show that a finite bisimilar abstraction of the transition system of the program can be constructed such that the verification problem boils down to a propositional model checking problem of the finite abstraction against the propositional abstraction of the ALCOK-LTL formula. In the following we briefly outline the main steps of the construction of the abstraction.

Recall that a state in the transition system is of the form 〈(I, W), ρ〉 where ρ ∈ subg(δ). As a consequence of Lemma 10 we only need to consider possible instantiations with objects from the finite set Ind. Therefore, we are able to show that there are only polynomially many (in the size of δ) reachable program expressions in the transition system. Our focus now is on how to partition the epistemic interpretations that appear in the transition system into finitely many equivalence classes such that the satisfaction of temporal properties is preserved. First, we use Lemma 10 to identify a finite set of relevant axioms. By considering all axioms in the initial KB, in the temporal property, all groundings of atoms appearing as tests in the program and primitive actions, we obtain a finite set of relevant ALCOK-axioms that we call context of P, denoted by CK(P). This set is the basis for constructing types, i.e. equivalence classes, of single interpretations. To do this we need to deal with the references to knowledge in the axioms of the context. We make use of the following simple structure of the reachable knowledge states.

Lemma 11. Let KD be anALCOK-concept mentioning only individuals from Ind and 〈(I,W), ρ〉 a reachable state in the transition system of a restricted program. If there exists d ∈ ∆ \ Ind such that d ∈ (KD)W , then ∆ \ Ind ⊆ (KD)W .

Consequently, (KD)W is a finite subset of Ind, or a finite subset of Ind plus all unnamed elements from ∆ \ Ind. This result together with the property of epistemic roles shown in Lemma 10 gives rise to a rewriting of epistemic sub-concepts by non-epistemic ones. We define the notion of an instance function κ that maps concepts of the form KD to a subset of {{a} | a ∈ Ind} ∪ {¬N} where N := ⊔a∈Ind{a}, and a given role name r and an individual a to a subset of {{a} | a ∈ Ind}. Intuitively, an instance function represents an abstraction of a possible knowledge state. Given an ALCOK-concept C and an instance function κ we have defined a rewriting that yields an objective concept C κ . The rewriting technique is very similar to the one used in the Representation Theorem [Levesque and Lakemeyer, 2001], where the idea is to replace each knowledge subformula by a description of its instances.

Clearly, the context CK(P) contains only finitely many epistemic roles and epistemic subconcepts. Therefore there are only finitely many relevant instance functions we need to consider. Using the rewriting operator we can close up the context under all possible rewritings of epistemic subconcepts and roles, which yields the so-called knowledge closure of the context. Let ̂ C(P) be the set of all non-epistemic axioms contained in the knowledge closure and 2Lit denote the set of all sets of literals occurring in the context, used for representing accumulated physical effects. The dynamic type of an interpretation I is then given by:

Obviously, there are only finitely many different dynamic types. We showed that the problem whether a given subset of ̂ C(P) × 2Lit represents the dynamic type of an interpretation I ∈M(K) is reducible to a consistency check in ALCO.

The knowledge closure and the dynamic types are the main technical notions used to construct the abstract transition system. The abstraction of a state is given by the dynamic type of the real world, the set of dynamic types for the possible worlds in the knowledge state, and the program expression. Given this finite abstract transition system which preserves satisfaction of temporal properties, we can treat axioms in the ALCOK-LTL property as propositional atoms and apply LTL model checking to solve the verification problem.

Theorem 12. Let P be a restricted ALCOK-Golog program and Φ an ALCOK-LTL formula. The problem whether Φ is valid in P or not is decidable in 2EXPSPACE.

Since the size of ̂ C(P) and 2Lit is exponential in the size of the input, there are at most double-exponentially many dynamic types and at most triple-exponentially many states in the abstract transition system, which can be constructed onthe-fly. We thus obtain a 2EXPSPACE upper bound.

The presented decidable fragment is also maximal in the sense that relaxing any of the restrictions leads to undecidability. For instance it can be shown that this happens if the restricted conjunct of the guard is allowed to contain nominals or nested K operators within concept atoms, or role atoms of the form K¬r(z, z′ ). The problem is that such extensions may open the domain of the pick-operator for anonymous objects, which immediately causes undecidability.

Finally note that although the projection problem (see Definition 3) can be viewed as a special case of the verification problem, it is worth special consideration as it is also the basic reasoning task for executing a knowledge-based program. We have the following result:

Theorem13. The projection problem is EXPTIME-complete, and PSPACE-complete if the initial TBox is empty.

The proofs of the results presented in this section can be found in the technical report [Zarrieß and Claßen, 2015].

5 Conclusion

So far, little work has been done on decidable verification of knowledge-based Golog programs. De Giacomo, Lesp´erance and Patrizi [2013] present a class of epistemic Situation Calculus action theories for which they show decidability of µcalculus properties, however they do not consider Golog and rely on a purely semantical definition of this class. On the propositional level, Lang and Zanuttini [2012] have investigated the complexity of verifying post-conditions of a class of modal logic knowledge-based programs that could be viewed as a (deterministic) subset of Golog.

Finally, alternative approaches for reasoning about actions and programs using DLs were proposed. The formalization presented in [Calvanese et al., 2011] for example adopts Levesque's functional view on knowledge bases, where all interactions with the agent's KB to happen through the two operations ASK (test evaluation) and TELL (update after action execution). While this allows for tractable solutions to the executability and projection problems for certain light-weight DLs, this non-declarative representation makes no distinction between world-changing and sensing actions as we do. Also, verification of temporal properties is not considered.

In this paper, we introduced an action language for both physical and sensing actions based on the epistemic DL ALCOK. We showed that under suitable restrictions, verifying LTL properties over possibly epistemic ALCOK-axioms of knowledge-based Golog programs based on our action language is decidable. The main idea to obtain decidability is to syntactically limit the domain of the guarded pick operator to contain named objects only.

Furthermore, we investigated the complexity of projection as the basic reasoning task for executing knowledge-based programs. As future work, among other things, we want to investigate whether the obtained upper complexity bound of the verification problem can be improved, or it is actually tight.

Acknowledgments This work was supported by the German Research Foundation (DFG) research unit FOR 1513 on Hybrid Reasoning for Intelligent Systems (http://www. hybrid-reasoning.org).