Plan Validation for Extended Goals under Partial Observability (preliminary report)

The increasing interest in planning in nondeterministic domains by model checking has seen the recent development of two complementary research lines. In the first, planning is carried out considering extended goals, expressed in the CTL temporal logic, but has been developed under the simplifying hypothesis of full observability. In the second, simple reachability goals have been tackled under the more general hypothesis of partial observability. The combination of extended goals and partial observability for nondeterministic domains is, to the best of our knowledge, an open problem, whose solution turns out to be by no means trivial. This paper is a first step towards a full, principled merging of the two research lines, in order to be able to describe complex and significant goals over realistic domains. We make the following contributions. First, we define a general framework,encompassing both partial observability and temporally extended goals. Second, we define the K-CTL goal language, that extends CTL with a knowledge operator that allows to reason about the information that can be acquired at run-time. This is necessary to deal with partially observable domains, where limited ``knowledge`` about the domain state is a key issue. Then, we define a general mechanism for plan validation for K-CTL goals, based on the idea of monitor. A monitor plays the role of evaluating the truth of knowledge predicates, and allows us to fully exploit the CTL model checking machinery. This paper restricts to plan validation of K-CTL goals. However, it provides a solid basis for tackling the problem of planning for K-CTL goals under partial observability