SCO Seminar - Armin Pirastehzad, University of Groningen

Title: From Modular Verification and Design to Hierarchical Synthesis: A (γ,δ)-Similarity Approach

Abstract:

We express specifications in terms of the input-output trajectories of a dynamical ‘specification’ system, which allows the formulation of complex behaviors. We then introduce the notion of (γ,δ)-similarity to verify whether the input-output behavior of a non-deterministic continuous-time stable linear system satisfies these specifications in an approximate sense. Our study on the compositional properties of (γ,δ)-similarity shows that the notion is preserved through series interconnections, which makes it a suitable framework for modular verification. We accordingly utilize (γ,δ)-similarity to conduct modular verification and design for interconnected systems with series architecture. In modular verification, we make use of our prior knowledge of local specifications on components to replace each high-dimensional component by its low-dimensional specification and then conduct verification on the basis of these local specifications. In modular design of such series interconnections, for a given high-dimensional component and its associated low-dimensional specification, we design the other component such that the resulting series interconnection satisfies the global specification. For this purpose, we replace the given component by its corresponding local specification and then design the other component on the basis of this local specification.

We then consider the situation where a system fails to satisfy specifications with the desired accuracy imposed by (γ,δ)-similarity. We therefore synthesize controllers to enforce specification satisfaction within the framework of (γ,δ)-similarity. Aware of the scalability issues in the synthesis of such controllers, we synthesize them according to a hierarchical scheme. This scheme synthesizes a controller for a non-deterministic ‘concrete’ system in three consecutive steps. First, an ‘abstract’ system, which is a low-dimensional model of the concrete system, is obtained. Then, a controller is designed for the abstract system. At last, the abstract controller is refined into the concrete controller through an ‘interface’. To enable this, we extend the notion of (γ,δ)-similarity to control systems and conceive the notion of (γ,δ)-abstraction, which utilizes an L2 approximation metric to measure the behavioral similarity of the concrete system and its abstraction. This induces a hierarchical framework that is compatible with many design methods in control theory as they typically employ the L2 signal norm. We accordingly synthesize the abstract controller and refine it into the concrete one.