Specification Verification and Controller Synthesis Using (γ, δ)-Similarity

We address the problems of specification verification and controller synthesis in the context of (γ,δ) -similarity, a notion of approximate system comparison that measures to what extent the external behaviors of two potentially non-deterministic systems are similar in an L2 sense. Expressing specifications in terms of input-output trajectories of a dynamical system, we use (γ, δ)-similarity to verify whether the external behavior of a system satisfies such specifications in an approximate sense. We characterize this problem as a linear matrix inequality feasibility problem. In case a control system fails to satisfy specifications with a desired accuracy, we synthesize a dynamic controller that enforces specification satisfaction. We characterize the synthesis problem in terms of a bilinear matrix inequality feasibility problem. Aware of the computational costs for solving such problem, we obtain a sufficient condition for the existence of the controller that can be expressed in terms of a linear matrix inequality. Based on this, we propose an algorithm to construct the controller.