A formal semantics for multiple vehicle task and motion planning

The application of autonomous guided vehicles to well-structured industrial sites requires considerably more than a path planning algorithm onboard each vehicle. Issues such as task planning, vehicle routing and vehicle-vehicle interactions predominate in determining the overall system ability. We exhibit a mathematical model of a multiple vehicle system, which has similarities to the Timed Traces models developed to reason about parallel processes. A denotational semantics is derived from this model, ascribing meaning to a simple language of service operations and concurrent path planning. This semantics captures a complete description of vehicles´ behaviour, which can provide a global planning strategy guaranteeing both satisfiability and liveness