Verification of Knowledge-Based Programs over Description Logic Actions

Benjamin ZarrießBenjamin Zarrieß, Jens ClaßenJens Claßen

Benjamin Zarrieß, Jens Claßen
Verification of Knowledge-Based Programs over Description Logic Actions
In Qiang Yang, Michael Wooldridge, eds., Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15), 3278-3284, 2015. AAAI Press

Details
Bibtex

KurzfassungAbstract
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, that we then use to build knowledge-based programs with test conditions expressed in an 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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ZC2015,
  author    = {Benjamin Zarrie{\ss} and Jens Cla{\ss}en},
  title     = {Verification of Knowledge-Based Programs over Description Logic
               Actions},
  editor    = {Qiang Yang and Michael Wooldridge},
  booktitle = {Proceedings of the 24th International Joint Conference on
               Artificial Intelligence (IJCAI'15)},
  publisher = {AAAI Press},
  year      = {2015},
  pages     = {3278-3284}
}