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 often referred to as goal specification. Temporal logics such as LTL, and CTL* have been used to specify goals of cognitive 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 existing temporal logics such as LTL, CTL*, and π-CTL*. We then propose the language, P-CTL*, which includes the quantifiers, exist a policy and for all policies. We show that this language allows for the specification of richer goals, including many intuitive and useful goals mentioned in the literature which cannot be expressed in existing temporal languages. We generalize our approach of showing the limitations of Tr-CTL* to develop a framework to compare expressiveness of goal languages.