Research

This page lists recent projects that I have been involved in, acknowledging all the amazing researchers that I had the pleasure to cooperate with on these projects.

All projects are truly interdisciplinary efforts at the intersection of control theory and formal methods from computer science, involving experts from both domains and appearing in publishing venues of both communities.

A full publication list is available here.

 

D – Symbolic Output-Feedback Control Design

The problem of correctly controlling a dynamical system through a digital interface has gained substantial attention in recent years due to its relevance in cyber-physical systems (CPS) design. Here, physical (dynamical) system components interact with cyber (digital) decision units, naturally leading to symbolic interfaces between them. Given a particular specification over the variables of this interface, a relevant question is whether there exists a digital control device only interacting with the physical system (i.e., the plant) via its symbolic interface, such that this specification always holds.

Our work develops fully automated and scalable abstraction and controller synthesis techniques for this important class of output-feedback control problems within CPS.

C – Contract-Based Digital Control Design

C.2 – Negotiating Assumptions for Distributed Contract-based Control Design

Distributed controller synthesis is the problem of algorithmically constructing controllers of distributed, communicating systems so that each closed-loop system satisfies a given temporal specification. Our work focuses on developing algorithms, called negotiation, which automatically and iteratively construct assumptions and guarantees for each system. In each iteration, each system attempts to fulfill its specification and its guarantee (from the previous round), under the current assumption on the other systems. If no controller exists for this synthesis problem, the algorithm computes a sufficient assumption on the other systems that ensures the existence of a local controller. This additional assumption further constrains the control design problem of other systems, leading to the next round in the negotiation. The process terminates when a compatible assumption-guarantee pair is found for each system.

Our work has established automated negotiation algorithms for simple distributed digital system architectures and is currently expanded towards more realistic designs.

C.1 – Digital Controller Synthesis under Assumptions

Many problems in reactive synthesis are stated using two formulas —an environment assumption and a system guarantee— and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools often produce strategies that formally satisfy such specifications by actively preventing an environment assumption from holding. While formally correct, such strategies do not capture the intention of the designer.

Our work focuses on developing new, efficient synthesis algorithms that produce indented strategies when existing plant properties are modeled as environment assumptions in the context of symbolic control design. These algorithms are inspired by ideas from supervisory control (see B).

B – Bridging the Gap between Reactive Synthesis and Supervisory Control

Reactive synthesis and supervisory control theory both provide a design methodology for the automatic and algorithmic design of digital systems from declarative specifications. The reactive synthesis approach originates in computer science, and seeks to synthesize a system that interacts with its environment over time and that, doing so, satisfies a prescribed specification. Supervisory control originates in control theory and seeks to synthesize a controller that – in closed-loop configuration with a plant – enforces a prescribed specification over time. While both methods apparently are closely related, the technical details differ significantly.

Our research aims at understanding the fundamental connection between both disciplines to enable fruitful collaborations between the discrete control and the computer science community in the context of reliable CPS design.

A – Abstraction-Based Control Design (ABCD)

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.

A.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.

A.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.

A.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.