Decidable Verification of Knowledge-Based Programs over Description Logic Actions with Sensing.
Benjamin Zarrieß, Jens Claßen · RWTH Publications (RWTH Aachen) · 2015
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 Clasen 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