Recent work has shown that Dynamic Epistemic Logic (DEL) offers a solid foundation for automated planning under partial observability and non-determinism. Under such circumstances, a plan must branch if it is to guarantee achieving the goal under all contingencies (strong planning). Without branching, plans can offer only the possibility of achieving the goal (weak planning). We show how to formulate planning in uncertain domains using DEL and give a language of conditional plans. Translating this language to standard DEL gives verification of both strong and weak plans via model checking. In addition to plan verification, we provide a tableau-inspired algorithm for synthesising plans, and show this algorithm to be terminating, sound and complete.
|Title of host publication||Logics in Artificial Intelligence : 13th European Conference, JELIA 2012, Toulouse, France, September 26-28, 2012. Proceedings|
|Publication status||Published - 2012|
|Event||13th European Conference on Logics in Artificial Intelligence (JELIA 2012) - Toulouse, France|
Duration: 26 Sep 2012 → 28 Sep 2012
|Conference||13th European Conference on Logics in Artificial Intelligence (JELIA 2012)|
|Period||26/09/2012 → 28/09/2012|
|Series||Lecture Notes in Computer Science|