Goal specification using temporal logic in presence of non-deterministic actions
Chitta Baral and Matt Barry.
Abstract
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.