Formal Methods for Adaptive Control of Dynamical Systems

TL;DR

This paper presents a formal, correct-by-design method for controlling discrete-time systems with unknown parameters using linear temporal logic, applicable to both finite and infinite systems through abstractions.

Contribution

It introduces parametric and adaptive transition systems and develops a formal approach to synthesize control strategies without relying on reference models.

Findings

Method successfully controls systems with unknown parameters.

Applicable to both finite and infinite systems via abstractions.

Demonstrated effectiveness through case studies.

Abstract

We develop a method to control discrete-time systems with constant but initially unknown parameters from linear temporal logic (LTL) specifications. We introduce the notions of (non-deterministic) parametric and adaptive transition systems and show how to use tools from formal methods to compute adaptive control strategies for finite systems. For infinite systems, we first compute abstractions in the form of parametric finite quotient transition systems and then apply the techniques for finite systems. Unlike traditional adaptive control methods, our approach is correct by design, does not require a reference model, and can deal with a much wider range of systems and specifications. Illustrative case studies are included.