Compositional analysis for linear systems

Compositional analysis techniques such as assume-guarantee reasoning are frequently used in computer science to validate the design of complex process models. Since many engineering systems are built modularly from interconnections of components, the resulting mathematical models can be arbitrarily complex, which makes their analysis equally challenging. This paper presents a framework of how to apply compositional and assume-guarantee reasoning to linear time-invariant (LTI) systems. A key tool are simulation relations which are used to relate systems models with their specifications as well as to determine abstractions of given system behaviors. First, complex systems defined by standard feedback interconnections are considered. Parallel composition of LTI systems, the second type of interconnections, introduces algebraic constraints but allows for decomposition of a global specification.

Research highlights
► Compositional reasoning techniques simplify verification tasks for control systems.
► Circular assume-guarantee reasoning is always sound for feedback interconnections of linear control systems.
► Specifications can be decomposed for parallel compositions of linear systems.