Formal Specification and Control Synthesis of Autonomous Robots Using Rulebooks

This paper presents a formal specification framework for planning and control of autonomous robots, focusing on the challenge of managing complex trade-offs among multiple, potentially conflicting objectives. These include hierarchical relationships and non-comparable objectives, some of which may be too complex to be captured by standard additive cost functions. We leverage therulebookformalism to represent such objectives and their relationships and formulate two control synthesis problems: single-strategy synthesis, which seeks one optimal strategy, and complete synthesis, which computes the full set of optimal strategies with respect to a rulebook, analogous to the Pareto front in multi-objective planning. We show that our formulation generalizes existing temporal logic-based and optimization-based planning and control, providing a unifying framework across robotics, formal methods, control theory, and operations research. For single-strategy, we identify tractable subclasses and present a polynomial-time algorithm that accommodates richer combinations of objectives than prior work. For complete synthesis, we introduce an algorithm to compute all optimal solutions and analyze its computational complexity. In both cases, we present case studies that include complex multi-objective planning problems and demonstrate the practical effectiveness of our approach compared to existing methods.