Deductive planning with inductive loops
Martin Magnusson, Patrick Doherty · 2008
Agents plan to achieve and maintain goals. Maintenance that requires continuous action excludes the representation of plans as finite sequences of actions. If there is no upper bound on the number of actions, a simple list of actions would be infinitely long. Instead, a compact representation requires some form of looping construct. We look at a specific tem-porally extended maintenance goal, multiple target video sur-veillance, and formalize it in Temporal Action Logic. The logic’s representation of time as the natural numbers suggests using mathematical induction to deductively plan to satisfy temporally extended goals. Such planning makes use of a sound and useful, but incomplete, induction rule that com-pactly represents the solution as a recursive fixpoint formula. Two heuristic rules overcome the problem of identifying a sufficiently strong induction hypothesis and enable an auto-mated solution to the surveillance problem that satisfies the goal indefinitely.