Goal specification using temporal logic in presence of non-deterministic actions

Chitta Baral and Matt Barry.


In this paper we show that despite a past claim goals such as `try your best to make $p$ true' in presence of non-deterministic actions can be expressed in the framework of branching time temporal logic. We analyze the ${\sf A}$ and ${\sf E}$ operators in CTL$^*$ and point out why it was thought that the above mentioned goal can not be expressed using CTL$^*$. We then introduce the operators ${\sf A}_\pi$ and ${\sf E}_\pi$ (and present a temporal logic $\pi$-CTL$^*$) which take into account the policy being followed by the agent and show that using these operators we can indeed specify the above mentioned goal.