---
title: "Verification of Knowledge-Based Programs over Description Logic Actions"
authors:
  - "Benjamin Zarrieß"
  - "Jens Claßen"
doi: ""
url: "https://ijcai.org/proceedings/2015/462"
pdf: "https://ijcai.org/proceedings/2015/0462.pdf"
venue: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence"
year: 2015
pages: "3278-3283"
track: "Special Track on Knowledge Representation and Reasoning"
keywords:
---

# Verification of Knowledge-Based Programs over Description Logic Actions

Benjamin Zarrieß, Jens Claßen

*Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence*, pages 3278-3283.

## Abstract

A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent's knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, and that we then use to build knowledge-based programs with test conditions expressed in the epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure's complexity.