Since the Golog [5, 10] 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 received increasing attention [4, 7]. Both the Golog language itself and the underlying Situation Calculus [11, 13] 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 [6, 15]. In this extended abstract 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 in the epistemic Situation Calculus were proposed by Reiter [14] and later by Claßen and Lakemeyer [3]. Here we review our work on a new epistemic action formalism based on the basic Description Logic (DL) ALC obtained by combining and extending earlier proposals for DL action formalisms [1] and epistemic DLs [8]. 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. More precisely, in our setting a knowledge-based programs for the control of a single agent consists of the following ingredients: 1. an (objective) ALC-TBox and ABox representing the initial static knowledge of the agent about the world.; 2. a set of primitive actions describing the basic abilities of an agent to change the world and to gain new information from the environment and 3. a program expression defining the possible courses of action by combining primitive actions and subjective conditions formulated in the epistemic DL ALCOK (an extension of ALC with nominals (O) and an epistemic constructor (K)) using programming constructs ? Supported by DFG Research Unit FOR 1513, (http://www.hybrid-reasoning.org) ?? See [2] for the long versions of the paper and [16] for the technical report.
for sequencing, iteration and nondeterministic choice. Desired properties of such a program can be expressed in LTL over ALC-concept inclusions and ALCOKABox assertions - a logic we call ALCOK-LTL. The verification problem asks whether or not all runs of a given knowledge-based program satisfy a given ALCOK-LTL formula.
Verifying knowledge-based programs with this language yields multiple
advantages. First, under reasonable restrictions 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 [
As an example consider a mobile robot in a factory whose task it is to detect faulty gears and do the necessary repairs before turning them on. The agent is equipped with the following KB K = (T ; A) representing its initial knowledge about the world:
T = fFault v CritFault t UncritFault; 9has-f:> v System; System v 8has-f:Faultg; A = fSystem(gear); :On(gear); Fault(blocked)g: The first concept inclusion (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.
To represent conditional effects of primitive actions and axioms whose truth can be sensed we use boolean combinations of atoms, i.e. ABox assertions where in place of individuals also variables are allowed. An effect is of the form '= , where ' is a boolean combination of atoms and is a literal of the form A(z); :A(z); r(z; z0) and :r(z; z0). A primitive action is a pair of the finite sets e and sense, where e is a set of effects and sense a finite set of boolean combinations of atoms. For example consider the following actions: turn-on(x) : (e = f(:9has-f:CritFault(x))=On(x)g; sense = ;); sense-on(x) : (e = ;; sense = fOn(x)g): turn-on(x) with variable 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. No sensing result is provided. sense-on(x) is a pure sensing action that represents the agent’s ability to perceive whether On(x) is true in the real world.
Semantically, a primitive ground action induces a binary relation on epistemic interpretations (I; W) which allow us to explicitly distinguish changes affecting the real world, represented by the interpretation I, and changes to the knowledge state W, which is a set of interpretations (i.e., possible worlds) over a common countably infinite domain. In our semantics we also assume that the agent knows the physical effects of its primitive actions. For instance, assume K as given above is all the agent knows initially about the world. Thus, it is initially known that gear is not on, but the effect condition :9has-f:CritFault(gear) of turn-on(gear) is unknown, i.e. there is a least one possible world satisfying K where gear is an instance of 9has-f:CritFault and one where this is not the case. Consequently, the actual outcome of executing turn-on(gear) in K is also unknown. This can be expressed by the epistemic ABox assertion :KOn u :K:On(gear), where the K is used here as a concept constructor, intuitively denoting the known instances. 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 epistemic ABox assertions K9has-f:CritFault t K:9has-f:CritFault(gear) and KOn t K:On(gear) come to hold. A knowledge-based program describing the behaviour of an agent is then given as follows, where sense-f(gear; x) is an additional sensing action for checking if gear has fault x and repair(gear; x) an action for removing fault x of gear.
while :K(8has-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) 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 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. 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. This can be expressed by the following ALCOK-LTL formula: 9has-f:(CritFault u :KFault)(gear) ! 3K9has-f:(CritFault u :KFault)(gear): In our semantics of actions it is not guaranteed that the TBox given in the initial KB always holds. However persistence of a TBox T in a program can be verified by checking validity of the ALCOK-LTL formula 2 V%2T % : 3
Unfortunately, it turns out that the verification problem is undecidable for an already quite small subset of our formalism. In our setting a state of the program consists of an epistemic interpretation and a program expression representing the program that remains to be executed. Thus, we end up with an infinite state transition system. As the source of undecidability we have identified the pick-operator for non-deterministic choice of argument, which may range over the whole countably infinite domain. However, we also have the positive result that decidability of the verification problem can be retained for a syntactically restricted fragment of the formalism where pick operators are extended with epistemic guards such that the agent is only allowed to choose an argument among the known individuals. We have devised an algorithm with a 2ExpSpace upper bound.