Necessary and Sufficient Conditions for Satisfying Linear Temporal Logic Constraints Using Control Barrier Certificates

Temporal logic specifications have been used to express complex tasks for control systems. Discretization-free approaches, which do not require discretizing the state and input spaces of the system, have been proposed for control synthesis under temporal logic specifications. Among these approaches, control barrier certificate (CBC)-based solutions have attracted increasing attention. The existing CBC-based approaches, however, have no guarantee on always finding control laws to satisfy the specification, and hence are sound but not complete. In this paper, we derive the necessary and sufficient conditions for a control law to satisfy a temporal logic specification over finite traces using CBCs. By leveraging the equivalence between satisfying the specification and violating the negated specification, we first negate the specification and construct the deterministic finite automaton (DFA) as a representation. We then decompose the DFA into a set of safety problems, where each decomposed problem corresponds to a transition in the DFA. We derive the necessary and sufficient conditions for a control law to solve each safety problem via CBC-based approach. We further develop the necessary and sufficient conditions to verify whether the control laws associated with different safety problems are composable or not. The composability captures whether a sequence of transitions in the DFA can be realized by the system or not. If the set of composable control laws does not render an accepting run on the DFA, then the system can satisfy the specification. We illustrate the proposed approach using a numerical case study on a multi-agent system.