Abstract—We introduce the notion of asymptotic similarity which compares the asymptotic external behavior of two non-deterministic continuous-time stable linear systems. Describing the asymptotic external behaviors in terms of the solution trajectories of an autonomous exosystem, asymptotic similarity determines the ability of a system in reproducing the asymptotic external behavior of another system. We characterize the notion of asymptotic similarity in terms of the solvability of regulator equations that are solely in terms of system matrices. We accordingly characterize the solvability of these equations as a subspace inclusion which allows one to determine asymptotic similarity through rank computation. We then conceive and characterize the notion of asymptotic bisimilarity which is a symmetric version of asymptotic similarity in the sense that it determines the equivalence of the asymptotic behaviors of systems. By specializing asymptotic similarity to deterministic systems, we give an interpretation of the notion in terms of the transfer matrices of systems. We also propose a technique to extract and compare the transient behavior of asymptotically similar systems. We finally extend the notion of asymptotic similarity to interconnected systems and show that it is preserved through series and feedback interconnections.

Abstract—We develop a modular verification and synthesis framework that utilizes assume-guarantee contracts to express specifications on the asymptotic external behavior of linear dynamical systems. We describe the asymptotic behavior of a system in terms of the solution trajectories of an autonomous exosystem and accordingly construct contracts as pairs of two subspaces of matrices, namely assumptions and guarantees. The assumptions subspace specifies the acceptable asymptotic behavior of external inputs to a system, whereas the guarantees subspace specifies the allowed asymptotic behavior of the system output. We formalize this by introducing the notion of implementation which is then characterized in terms of the solvability of regulator equations. Based on this characterization, we propose a computationally effective technique that verifies contracts by solving a linear matrix equation solely determined by system parameters, the basis of assumptions, and the basis of guarantees. We then construct the series composition of contracts to conduct modular verification for interconnected systems with series architecture. Finally, for systems that fail to implement a contract, we conceive the notion of controlled implementation, which determines the possibility of enforcing a system to implement a contract through control synthesis.

Abstract—We compensate for the scalability issues in controller synthesis by developing a hierarchical control scheme within the framework of (γ,δ)-similarity, which measures to what extent a potentially non-deterministic system satisfies specifications expressed as solution trajectories of a dynamical ‘specification’ system. This scheme synthesizes a controller for a non-deterministic ‘concrete’ system in three hierarchical 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 introduce and characterize the notion of (γ,δ)-abstraction that utilizes an L2 approximation metric to measure the behavioral similarity of the concrete system and its abstraction in the presence of the interface. We utilize this characterization to propose a step-by-step procedure to construct the interface. We then synthesize the abstract controller and refine it into a concrete one.

Abstract—For series interconnection of non-deterministic, continuous-time linear systems, we develop a modular verification and design framework that utilizes the notion of (γ,δ)- similarity to measure to what extent a global specification is satisfied in an approximate sense. We first address the modular verification problem where 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. We therefore derive a condition that guarantees the global specification solely on the basis of local specifications. We characterize this condition as a linear matrix inequality feasibility problem that is only in terms of the parameters of the (global and local) specifications. We then address the modular design problem where for a given component and its associated specification, we design the other component such that the resulting series interconnection satisfies the global specification. We characterize the existence of such component as a linear matrix inequality feasibility problem that is only in terms of the parameters of the (local and global) specifications rather than those of the component. On the basis of this characterization, we propose an algorithm to construct the component.

Abstract—For non-deterministic linear ‘concrete’ systems, we develop a control framework that conducts controller synthesis within three hierarchical steps. First, a low-dimensional ‘abstract’ system is obtained that behaves similarly to the concrete system in an input-output sense. Then, a con- troller is designed for the abstract system. Due to the low-dimensionality of the abstract system, designing such controller is computationally efficient. At last, the synthesized abstract controller is refined into a concrete controller using an ‘interface’. We introduce the notion of (γ,δ,ρ)-abstraction to measure the behavioral similarity of the concrete system and its abstraction in the presence of the interface and the abstract controller. Utilizing an L2 approximation metric to measure behavioral similarity, (γ,δ,ρ)-abstraction induces a hierarchical control framework that is compatible with existing effective methods for analysis and synthesis of control systems, in particular, techniques from robust control and dissipativity theory. We characterize the notion of (γ,δ,ρ)-abstraction as a linear matrix inequality feasibility problem. We then exploit this to characterize the existence of an abstract system in terms of a rank-constrained linear matrix inequality feasibility problem. On the basis of such feasibility problem, we propose an algorithm to construct the abstract system and interface.