Verification of Knowledge-Based Programs over Description Logic Actions
Aus International Center for Computational Logic
Verification of Knowledge-Based Programs over Description Logic Actions
Vortrag von Benjamin Zarrieß
- Veranstaltungsort: APB 3027
- Beginn: 7. September 2015 um 14:50
- Ende: 7. September 2015 um 15:50
- Forschungsgruppe: Automatentheorie
- Event series: KBS Seminar
- iCal
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.