Goal specification, non-determinism and quantifying over policies

摘要

One important aspect in directing cognitive robots or agents is to formally specify what is expected of them. This is of-ten referred to as goal specification. Temporal logics such as LTL, and CTL ∗ have been used to specify goals of cogni-tive robots and agents when their actions have deterministic consequences. It has been suggested that in domains where actions have non-deterministic effects, temporal logics may not be able to express many intuitive and useful goals. In this paper we first show that this is indeed true with respect to ex-isting temporal logics such as LTL, CTL∗, and pi-CTL∗. We then propose the language, P-CTL∗, which includes the quan-tifiers, exist a policy and for all policies. We show that this language allows for the specification of richer goals, includ-ing many intuitive and useful goals mentioned in the literature