Control Barrier Functions for Abstraction-Free Control Synthesis under Temporal Logic Constraints

TL;DR

This paper introduces a novel control barrier function-based method for synthesizing controllers that satisfy linear temporal logic specifications in cyber-physical systems without the need for system abstraction, improving scalability.

Contribution

The paper proposes an abstraction-free control synthesis method using control barrier functions for LTL constraints, avoiding the computational complexity of traditional abstraction-based approaches.

Findings

Guarantees satisfaction of LTL specifications under feasible quadratic programs.

Demonstrates effectiveness through a numerical case study.

Provides a scalable alternative to existing abstraction-based methods.

Abstract

Temporal logic has been widely used to express complex task specifications for cyber-physical systems (CPSs). One way to synthesize a controller for CPS under temporal logic constraints is to first abstract the CPS as a discrete transition system, and then apply formal methods. This approach, however, is computationally demanding and its scalability suffers due to the curse of dimensionality. In this paper, we propose a control barrier function (CBF) approach to abstraction-free control synthesis under a linear temporal logic (LTL) constraint. We first construct the deterministic Rabin automaton of the specification and compute an accepting run. We then compute a sequence of LTL formulae, each of which must be satisfied during a particular time interval, and prove that satisfying the sequence of formulae is sufficient to satisfy the LTL specification. Finally, we compute a control policy for satisfying each formula by constructing an appropriate CBF. We present a quadratic program to compute the controllers, and show the controllers synthesized using the proposed approach guarantees the system to satisfy the LTL specification, provided the quadratic program is feasible at each time step. A numerical case study is presented to demonstrate the proposed approach.