×

Compositional analysis for linear systems. (English) Zbl 1205.93068

Summary: 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 the given system behavior. 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 decomposing of a global specification.

MSC:

93C15 Control/observation systems governed by ordinary differential equations
93C05 Linear systems in control theory
34H05 Control problems involving ordinary differential equations
93B52 Feedback control
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Berezin, S.; Campos, S. V.A.; Clarke, E. M., Compositional reasoning in model checking, (COMPOS’97: Revised Lectures from the International Symposium on Compositionality: The Significant Difference (1998), Springer-Verlag: Springer-Verlag London, UK), 81-102
[2] H. Peng, S. Tahar, A Survey on Compositional Verification, Tech. rep., Concordia University, Montreal, 1998.; H. Peng, S. Tahar, A Survey on Compositional Verification, Tech. rep., Concordia University, Montreal, 1998.
[3] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[4] Alur, R.; Henziger, T. A.; Lafferriere, G.; Pappas, G. J., Discrete abstractions of hybrid systems, Proceedings of the IEEE, 88, 971-984 (2000)
[5] Pappas, G. J., Bisimilar linear systems, Automatica, 39, 2035-2047 (2003) · Zbl 1045.93033
[6] van der Schaft, A. J., Equivalence of dynamical systems by bisimulation, IEEE Transactions on Automatic Control, 49, 12, 2160-2172 (2004) · Zbl 1365.93212
[7] Pappas, G. J.; Lafferriere, G.; Sastry, S., Hierarchically consistent control systems, IEEE Transactions on Automatic Control, 45, 6, 1144-1160 (2000) · Zbl 0971.93004
[8] Tabuada, P., Controller synthesis for bisimulation equivalence, Systems and Control Letters, 57, 6, 443-452 (2008) · Zbl 1154.93324
[9] Misra, J.; Chandy, K. M., Proofs of networks of processes, IEEE Transactions on Software Engineering, 7, 4, 417-426 (1981) · Zbl 0468.68030
[10] T.A. Henzinger, S. Qadeer, S.K. Rajamani, You assume, we guarantee: methodology and case studies, in: CAV 1998, 1998, pp. 440-451.; T.A. Henzinger, S. Qadeer, S.K. Rajamani, You assume, we guarantee: methodology and case studies, in: CAV 1998, 1998, pp. 440-451.
[11] G. Frehse, Compositional Verification of Hybrid Systems using Simulation Relations, Ph.D. Thesis, Radboud Universiteit Nijmegen, 2005.; G. Frehse, Compositional Verification of Hybrid Systems using Simulation Relations, Ph.D. Thesis, Radboud Universiteit Nijmegen, 2005.
[12] F. Kerber, A.J. van der Schaft, Assume-guarantee reasoning for linear dynamical systems, in: European Control Conference, August 2009.; F. Kerber, A.J. van der Schaft, Assume-guarantee reasoning for linear dynamical systems, in: European Control Conference, August 2009.
[13] F. Kerber, A. van der Schaft, Compositional and assume-guarantee reasoning for switching linear systems, in: Preprints of the Conference on Analysis and Design of Hybrid Systems, 2009, pp. 328-333.; F. Kerber, A. van der Schaft, Compositional and assume-guarantee reasoning for switching linear systems, in: Preprints of the Conference on Analysis and Design of Hybrid Systems, 2009, pp. 328-333.
[14] Kerber, F.; van der Schaft, A. J., Compositional analysis for linear control systems, Hybrid Systems: Control and Computation (2010) · Zbl 1360.93279
[15] A.J. vander Schaft, Equivalence of hybrid dynamical systems, in: Proceedings of the Mathematical Theory of Networks and Systems, Leuven, July 2004.; A.J. vander Schaft, Equivalence of hybrid dynamical systems, in: Proceedings of the Mathematical Theory of Networks and Systems, Leuven, July 2004. · Zbl 1365.93212
[16] van der Schaft, A. J., \(L_2\)-Gain and passivity techniques in nonlinear control, (Communications and Control Engineering (2000), Springer-Verlag: Springer-Verlag New York) · Zbl 1410.93004
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.