Platform-Aware Mission Planning with Task-Level Contracts

Abstract

Automated temporal planning is used to synthesize courses of action for a deterministic abstraction of a system; the produced plans are often modeled as schedules of tasks to be executed on the real system under control. A key problem with adopting this architecture is how to ensure the plan is executable and goal-reaching on the real system, which can be arbitrarily complex and possibly non-deterministic. In this paper, we propose a framework to exploit task-level contracts, expressed as assumptions and guarantees at the beginning and end of tasks, to automatically synthesize plans that are guaranteed to be correct on any system satisfying the contracts. Our framework combines a temporal planner to generate candidate plans and a contract reasoner to instantiate and verify the contracts associated with the plan. If the plan is found invalid, we refine the planning problem until a valid plan is found. We present an experimental evaluation on a realistic case-study and on several synthetic problems, showing the applicability of the approach.