LTL Templates for Play-Calling Supervisory Control

摘要

A Playbook allows operators to design sets of tasks for a team of vehicles to perform in an abstract way before the mission begins, and then call the plays much like a coach of a human sports team during the mission. We extend this Playbook concept to include a set of assertions that must be true on each vehicle to ensure successful completion of a play, provide a means of specifying contingency plans, and then translate this extended Playbook into a linear temporal logic specification that can be used to synthesize a correct-by-construction controller. We provide a demonstration of this concept and discuss its implications for autonomous systems safety and reliability.