A planner agent that tries its best in presence of nondeterminism

In many nondeterministic planning domains, an agent whose goal is to achieve φ may not succeed in finding a policy that can guarantee that all paths from the initial state lead to a final state where φ holds (strong solution). Nevertheless, if the agent is trying its best to achieve φ, it cannot give up. Instead, it may be inclined to accept weaker guarantees, such as having a path leading to φ from any intermediate state reached by the policy (strong-cyclic solution), or even less, such as having at least one path leading to φ from the initial state (weak solution). But the agent should choose among such different options based on their availability in each situation. Although the specification of this type of goal has been addressed before, in this paper we show how a planner based on the branching time temporal logic α-ctl can be used to plan for intuitive and useful goals of the form “try your best to achieve φ”.