In this work, we address the problem of control synthesis for a homogeneous team of robots given a global temporal logic specification and formal user preferences for relaxation in case of infeasibility. The relaxation preferences are represented as a Weighted Finite-state Edit System and are used to compute a relaxed specification automaton that captures all allowable relaxations of the mission specification and their costs. For synthesis, we introduce a Mixed Integer Linear Programming (MILP) formulation that combines the motion of the team of robots with the relaxed specification automaton. Our approach combines automata-based and MILP-based methods and leverages the strengths of both approaches, while avoiding their shortcomings. Specifically, the relaxed specification automaton explicitly accounts for the progress towards satisfaction, and the MILP-based optimization approach avoids the state-space explosion associated with explicit product-automata construction, thereby efficiently solving the problem. The case studies highlight the efficiency of the proposed approach.

This work presents an optimization-based control synthesis approach for an extension of Signal Temporal Logic (STL) called weighted Signal Temporal Logic (wSTL). wSTL was proposed to accommodate user preferences for importance and priorities over concurrent and sequential tasks as well as satisfaction times denoted by weights over the logical and temporal operators, respectively. We propose a Mixed Integer Linear Programming (MILP) based approach for synthesis with wSTL specifications. These specifications have the same qualitative semantics as STL but differ in their quantitative semantics, which is recursively modulated with weights. Additionally, we extend the formal definition of wSTL to include the semantics for until and release temporal operators and present an efficient encoding for these operators in the MILP formulation. As opposed to the original implementation of wSTL, where the arithmetic-geometric mean robustness was used with gradient-based methods prone to local optima, our encoding allows the use of a weighted version of traditional robustness and efficient global MILP solvers. We demonstrate the operational performance of the proposed formulation using multiple case studies, showcasing the distinct functionalities over Boolean and temporal operators. Moreover, we elaborate on multiple case studies for synthesizing controllers for an agent navigating a non-convex environment under different constraints highlighting the difference in synthesized control plans for STL and wSTL. Finally, we compare the time and complexity performance of encodings for STL and wSTL.

This work presents a step towards utilizing incrementally-improving symbolic perception knowledge of the robot's surroundings for provably correct reactive control synthesis applied to an autonomous driving problem. Combining abstract models of motion control and information gathering, we show that assume-guarantee specifications (a subclass of Linear Temporal Logic) can be used to define and resolve traffic rules for cautious planning. We propose a novel representation called symbolic refinement tree for perception that captures the incremental knowledge about the environment and embodies the relationships between various symbolic perception inputs. The incremental knowledge is leveraged for synthesizing verified reactive plans for the robot. The case studies demonstrate the efficacy of the proposed approach in synthesizing control inputs even in case of partially occluded environments.

In this paper, we introduce an automata-based framework for planning with relaxed specifications. User relaxation preferences are represented as weighted finite state edit systems that capture permissible operations on the specification, substitution and deletion of tasks, with complex constraints on ordering and grouping. We propose a three-way product automaton construction method that allows us to compute minimal relaxation policies for the robots using shortest path algorithms. The three-way product automaton captures the robot’s motion, specification satisfaction, and available relaxations at the same time. Additionally, we consider a bi-objective problem that balances temporal relaxation of deadlines within specifications with changing and deleting tasks. Finally, we present the runtime performance and a case study that highlights different modalities of our framework.