Discretization-based Abstraction of Non-linear Control Systems

With the advent of digital controllers being increasingly used to control safety-critical cyber-physical systems (CPS), there is a growing need to provide formal correctness guarantees of such controllers. A recent approach to achieve this goal is so-called Abstraction-Based Controller Design (ABCD).

ABCD is a general procedure for automatic synthesis of controllers for continuous-time nonlinear dynamical systems against temporal specifications. ABCD works by abstracting a time-sampled version of the continuous dynamics of the open-loop system by a symbolic finite state model. Then, it automatically computes a finite-state controller for the symbolic model using algorithms from automata-theoretic reactive synthesis. When the time-sampled system and the symbolic model satisfy a certain refinement relation, the abstract controller can be refined to a controller for the original continuous-time system while guaranteeing its time-sampled behavior satisfies the temporal specification.

Below we list past projects in this line of work in reverse chronological order.

4 – ABCD for Stochastic Systems

Controlled Markov processes (CMPs) over continuous state spaces and evolv-
ing in discrete time form a general model for temporal decision making under
stochastic uncertainty. In recent years, the problem of finding or approximating
optimal policies in CMPs for specifications given in temporal logics or automata
has received a lot of attention. This line of work poposes a novel approach towards the handling of nonlinear models for general ω-regular specifications in a symbolic way.

3 – Incremental and Resilient ABCD

Like any other model-based controller synthesis technique, the formal guarantees of ABCD rely on the assumption of an accurate system model including a known upper perturbation bound which captures both modeling inaccuracies and environmental disturbances. In order to ensure hard safety constrains on CPS, very conservative perturbation bounds need to be used. This often leads to an excessively restrictive controller which fails to suit any practical purpose.

We have therefore developed techniques which allow to use a less conservative perturbation bound to improve controller performance without sacrificing safety.

2 – Lazy ABCD

Lazy abstraction is a technique to systematically and efficiently explore large state spaces through abstraction and refinement, and is the basis for successful model checkers for software and hardware. We applied the paradime of lazy abstraction to ABCD – our algorithm selectively chooses which portions of the system to compute abstract transitions for, avoiding doing so for portions that have been already solved by synthesis. This co-dependence of the two major computational components of ABCD is both conceptually appealing and results in significant performance benefits.

1 – Compositional ABCD

The computational bottleneck of ABCD is the expensive abstraction step (typically exponential in the dimension of the state space) that limits its applicability to real systems. To overcome this issue we have developed composition abstraction and synthesis techniques.