Verification of Knowledge-Based Programs over Description Logic Actions

Zarrieß, Benjamin; Claßen, Jens

Verification of Knowledge-Based Programs over Description Logic Actions

Download BibTeX Cite

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Special Track on Knowledge Representation and Reasoning. 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.

Benjamin Zarrieß, and Jens Claßen. 2015. Verification of Knowledge-Based Programs over Description Logic Actions. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15. IJCAI, 3278–3283. https://ijcai.org/proceedings/2015/462

@inproceedings{ijcai2015p462,
  title     = {Verification of Knowledge-Based Programs over Description Logic Actions},
  author    = {Zarrieß, Benjamin and Claßen, Jens},
  booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
               Artificial Intelligence, {IJCAI-15}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Qiang Yang and Michael Wooldridge},
  pages     = {3278--3283},
  year      = {2015},
  month     = {7},
  note      = {Special Track on Knowledge Representation and Reasoning},
  url       = {https://ijcai.org/proceedings/2015/462},
}

TY  - CPAPER
TI  - Verification of Knowledge-Based Programs over Description Logic Actions
AU  - Zarrieß, Benjamin
AU  - Claßen, Jens
T2  - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15
PB  - International Joint Conferences on Artificial Intelligence
PY  - 2015
SP  - 3278
EP  - 3283
UR  - https://ijcai.org/proceedings/2015/462
ER  -