Formal verification and controller synthesis for discrete-time systems.

摘要

Temporal logics, such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL), are customarily used to specify the correctness of computer programs and digital circuits modeled as finite-state transition systems. In recent years, due to their expressivity and resemblance to natural language, temporal logics gained increasing popularity as specification languages for more realistic system models, such as dynamical systems. Most of the work approaching the problem of verifying and controlling non-trivial dynamical systems from rich specifications are centered on the concept of abstraction. This dissertation proposes theoretical frameworks and computational tools for the verification and control of infinite-state discrete-time systems from temporal logic specifications.;The focus of this dissertation is on three particular classes of discrete-time systems, with widespread use in several areas: linear, switched linear, and piecewise affine systems. For switched linear systems, the existence of equivalent finite models is shown under stability constraints. Efficient algorithms to compute such finite models are developed. Moreover, algorithms for solving verification and synthesis problems from formulae of a particular fragment of LTL are designed, and are applied to equivalent finite models of stable switched linear systems. For linear and piecewise affine systems, a novel language-guided procedure to design control strategies from temporal logic specifications is developed. The language-guided procedure combines the abstraction and temporal logic control of the finite model, and restricts the search for control strategies in such a way that the satisfaction of the specifications is guaranteed at all times. Furthermore, this procedure generates a characterization of all satisfying system trajectories in the form of sequences of polytopic sets, which allows synthesizing optimal control strategies from temporal logic specifications. In particular, a model predictive control (MPC) approach for optimal control of piecewise affine systems from temporal logic specifications is proposed. The MPC controller minimizes a cost over the trajectories of the system, while guaranteeing correctness with respect to a temporal logic formula. As an application, a computational framework for formal verification of synthetic gene networks from given experimental data is presented.