Superposition Principle in Composable Hybrid Automata

• Autorzy: Akhundov J. , Tröger P. , Werner M.

Identyfikatory

DOI

10.3233/FI-2018-1630

• Języki publikacji: EN

Abstrakty

EN

Hybrid automata are a well-established modelling approach. The formalism is used in many real-time and control systems engineering projects, which makes model composition an increasingly relevant topic. A well-defined composition support allows concurrent engineering activities and the validation of larger systems. However, many existing publications seldom consider it or make unrealistic assumptions on the model design. The article discusses the common problems with hybrid automata composition and presents a new formalism, called linear time-invariant hybrid automata (LTI-HA), which targets specifically these issues. Our approach considers the superposition principle for flow functions, which makes it specifically useful for practical modelling purposes in the spacecraft and control domain. We compare the approach to well-known related ideas, such as hybrid I/O automata. Several properties of composition, such as commutativity, are proven.

Słowa kluczowe

EN

composition; hybrid automata; hybrid systems; linear systems; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 157, nr 4
• Strony: 321--339
• Opis fizyczny: Bibliogr. 37 poz., rys., tab.

Twórcy

autor

Akhundov J.

• Operating Systems Group, TU Chemnitz, Germany

autor

Tröger P.

• Operating Systems Group, TU Chemnitz, Germany

autor

Werner M.

• Operating Systems Group, TU Chemnitz, Germany

Bibliografia

• [1] Maler O, Manna Z, Pnueli A. From Timed to Hybrid Systems. In: Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 3-7, 1991, Proceedings. 1991 pp. 447-484.
• [2] Nise N. Control Systems Engineering. Wiley, 2011. ISBN: 9780470646120.
• [3] Henzinger TA. The Theory of Hybrid Automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS ’96. IEEE Computer Society, Washington, DC, USA. 1996 pp. 278. ISBN: 0-8186-7463-6.
• [4] Raskin JF. An Introduction to Hybrid Automata, pp. 491-517. Birkhäuser Boston, Boston, MA. 2005. ISBN: 978-0-8176-4404-8.
• [5] Lunze J, Lamnabhi-Lagarrigue F (eds.). Handbook of Hybrid Systems Control: Theory, Tools, Applications. Cambridge University Press, Cambridge, UK, New York, 2009. ISBN: 978-0-521-76505-3.
• [6] Lynch N, Segala R, Vaandrager F. Hybrid I/O Automata. Inf. Comput., 2003;185(1):105-157. URL https://doi.org/10.1016/S0890-5401(03)00067-1.
• [7] Akhundov J, Reißner M, Werner M. Using Hybrid Automata for Early Spacecraft Design Evaluation. In: To appear in: Proceedings of the 26th International Workshop on Concurrency, Specification and Programming. Warsaw, Poland, 2017.
• [8] Akhundov J, Schaus V, Gerndt A, Werner M. Using Timed Automata to Check Space Mission Feasibility in the Early Design Phases. In: IEEE Aerospace 2016 Proceedings. Big Sky, Montana, USA, 2016. doi:10.1109/AERO.2016.7500572.
• [9] Akhundov J, Tröger P, Werner M. Considering Concurrency in Early Spacecraft Design Studies. In: CS&P 2015 Proceedings. Rzeszow, Poland. 2015 pp. 22-30. ISBN: 978-83-7996-181-8.
• [10] Schaus V, Tiede M, Fischer PM, Lüdtke D, Gerndt A. A Continuous Verification Process in Concurrent Engineering. In: AIAA SPACE 2013. Conference and Exposition San Diego, CA 2013. URL https://doi.org/10.2514/6.2013-5429.
• [11] Ábrahám E. Modeling and Analysis of Hybrid Systems: Lecture Notes, 2012.
• [12] Alur R, Dill DL. A Theory of Timed Automata. Theoretical Computer Science, 1994;126(2):183-235. URL https://doi.org/10.1016/0304-3975(94)90010-8.
• [13] Henzinger TA, Kopke PW, Puri A, Varaiya P. What’s Decidable about Hybrid Automata? Journal of Computer and System Sciences, 1998;57(1):94-124. URL https://doi.org/10.1006/jcss.1998.1581.
• [14] Abraham E, Hannemann U, Steffen M. Verification of Hybrid Systems: Formalization and Proof Rules in PVS. Technical Report TR-ST-01-1, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, 2001. doi:10.1109/ICECCS.2001.930163.
• [15] Baier C, Katoen JP. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. ISBN: 026202649X, 9780262026499.
• [16] Daws C, Yovine S. Two Examples of Verification of Multirate Timed Automata with Kronos. In: Proceedings 16th IEEE Real-Time Systems Symposium. 1995 pp. 66-75. doi:10.1109/REAL.1995.495197.
• [17] Alur R, Henzinger T, Lafferriere G, George, Pappas GJ. Discrete Abstractions of Hybrid Systems. In: Proceedings of the IEEE. 2000 pp. 971-984. doi:10.1109/5.871304.
• [18] Alur R. Principles of Cyber-Physical Systems. MIT Press, 2015. ISBN: 9780262029117.
• [19] Alur R, Courcoubetis C, Henzinger T, Ho P, Nicollin X, Olivero A, Sifakis J, Yovine S. The Algorithmic Analysis of Hybrid Systems. In: Cohen G, Quadrat JP (eds.), 11th International Conference on Analysis and Optimization of Systems Discrete Event Systems: Sophia-Antipolis, June 151617, 1994, pp. 329-351. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN: 978-3-540-39345-0, 1994.
• [20] Lynch N, Segala R, Vaandrager F, Weinberg HB. Hybrid I/O Automata, pp. 496-510. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN: 978-3-540-68334-6, 1996.
• [21] Cassez BBF. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: In Proc. FORMATS05, vol. 3829 of LNCS. Springer, 2005 pp. 211-225. URL https://doi.org/10.1007/11603009_17.
• [22] Branicky MS. Introduction to Hybrid Systems, pp. 91-116. Birkhäuser Boston, Boston, MA. ISBN: 978-0-8176-4404-8, 2005. doi:10.1007/0-8176-4404-0 5. URL https://doi.org/10.1007/0-8176-4404-0_5.
• [23] Maler O. Algorithmic Verification of Continuous and Hybrid Systems. In: Proceedings 15th International Workshop on Verification of Infinite-State Systems, INFINITY 2013, Hanoi, Vietnam, 14th October 2013 pp. 48-69. doi:10.4204/EPTCS.140.4.
• [24] Alur R, Courcoubetis C, Henzinger TA, Ho PH. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Springer-Verlag, 1992 pp. 209-229.
• [25] Henzinger TA. The Theory of Hybrid Automata. In: Inan M, Kurshan R (eds.), Verification of Digital and Hybrid Systems, volume 170 of NATO ASI Series, pp. 265-292. Springer Berlin Heidelberg 2000. ISBN:978-3-642-64052-0.
• [26] Lygeros J, Tomlin C, Sastry S. Controllers for Reachability Specifications for Hybrid Systems. Automatica, 1999;35(3):349-370. URL https://doi.org/10.1016/S0005-1098(98)00193-9.
• [27] Platzer A. A Temporal Dynamic Logic for Verifying Hybrid System Invariants. Springer Berlin Heidelberg, Berlin, Heidelberg 2007 pp. 457-471. ISBN: 978-3-540-72734-7. doi:10.1007/978-3-540-72734-7_32. URL http://dx.doi.org/10.1007/978-3-540-72734-7_32.
• [28] Platzer A, Clarke EM. Computing Differential Invariants of Hybrid Systems as Fixedpoints, Springer Berlin Heidelberg, Berlin, Heidelberg, 2008 pp. 176-189. ISBN: 978-3-540-70545-1. doi:10.1007/978-3-540-70545-1_17. URL http://dx.doi.org/10.1007/978-3-540-70545-1_17.
• [29] Lygeros J, Johansson KH, Simic SN, Zhang J, Sastry S. Continuity and Invariance in Hybrid Automata. In: Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228), volume 1. 2001 pp. 340-345. doi:10.1109/.2001.980123.
• [30] Zhang J, Johansson KH, Lygeros J, Sastry S. Zeno hybrid systems. International Journal of Robust and Nonlinear Control, 2001;11(5):435-451. doi:10.1002/rnc.592.
• [31] Ye H, Michel AN, Hou L. Stability Theory for Hybrid Dynamical Systems. Automatic Control, IEEE Transactions on, 1998;43(4):461-474. doi:10.1109/9.664149.
• [32] Branicky MS. Multiple Lyapunov Functions and other Analysis Tools for Switched and Hybrid Systems. Automatic Control, IEEE Transactions on, 1998;43(4):475-482. doi:10.1109/9.664150.
• [33] Ames AD, Abate A, Sastry S. Sufficient Conditions for the Existence of Zeno Behavior. In: Proceedings of the 44th IEEE Conference on Decision and Control and European Control Conference. 2005 pp. 696-701.
• [34] Higham NJ, Dennis MR, Glendinning P, Martin PA, Santosa F, Tanner J (eds.). The Princeton Companion to Applied Mathematics. Princeton University Press, Princeton, NJ, USA, 2015. ISBN: 978-0-691-15039-0.
• [35] Johansson M, Rantzer A. Computation of piecewise quadratic Lyapunov functions for hybrid systems. Automatic Control, IEEE Transactions on, 1998;43(4):555-559. doi:10.1109/9.664157.
• [36] Liberzon D, Morse AS. Basic Problems in Stability and Design of Switched Systems. IEEE Control Systems, 1999;19(5):59-70. doi:10.1109/37.793443.
• [37] Bemporad A, Ferrari-Trecate G, Morari M. Observability and Controllability of Piecewise Affine and Hybrid Systems. IEEE Transactions on Automatic Control, 2000;45(10):1864-1876. doi:10.1109/TAC.2000.880987.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).