×

Verification of hybrid systems. (English) Zbl 1392.68246

Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 1047-1110 (2018).
Summary: Hybrid systems are models which combine discrete and continuous behavior. They occur frequently in safety-critical applications in various domains such as health care, transportation, and robotics, as a result of interactions between a digital controller and a physical environment. They also have relevance in other areas such as systems biology, in which the discrete dynamics arises as an abstraction of fast continuous processes. One of the prominent models is that of hybrid automata, where differential equations are associated with each node, and jump constraints such as guards and resets are associated with each edge.
For the entire collection see [Zbl 1390.68001].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] 1. Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE (2012) · Zbl 1319.03004
[2] 2. Althoff, M., Krogh, B.: Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans. Autom. Control 59, 371-383 (2014) · Zbl 1360.93082
[3] 3. Althoff, M., Krogh, B.H., Stursberg, O.: Analyzing reachability of linear dynamic systems with parametric uncertainties. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Springer, Heidelberg (2011)
[4] 4. Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 173-182. ACM, New York (2013) · Zbl 1362.93011
[5] 5. Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 45-54. ACM, New York (2012) · Zbl 1362.93012
[6] 6. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3-34 (1995) · Zbl 0823.68067
[7] 7. Alur, R.: Formal verification of hybrid systems. In: Chakraborty et al. [8, 34, 35, 91, 132], pp. 273-278
[8] 8. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman et al. [31, 100, 113, 129, 149, 174-177], pp. 209-229
[9] 9. Alur, R., Dang, T., Ivancic, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250-271 (2006) · Zbl 1088.68096
[10] 10. Alur, R., Dang, T., Ivancic, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5(1), 152-199 (2006) · Zbl 1088.68096
[11] 11. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183-235 (1994) · Zbl 0803.68071
[12] 12. Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971-984 (2000)
[13] 13. Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181-201 (1996)
[14] 14. Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: ACM Symposium on Theory of Computing, pp. 592-601 (1993) · Zbl 1310.68139
[15] 15. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Domenica Di Benedetto, M., Sangiovanni-Vincentelli, A.L. (eds.) HSCC. LNCS, vol. 2034, pp. 49-62. Springer, Heidelberg (2001) · Zbl 0991.93076
[16] 16. Alur, R., Pappas, G.J. (eds.): Hybrid Systems: Computation and Control, Proceedings of the 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004. LNCS, vol. 2993. Springer, Heidelberg (2004) · Zbl 1046.93002
[17] 17. Asarin, E., Dang, T.: Abstraction by projection and application to multi-affine systems. In: Alur and Pappas [24, 46, 53, 62, 101, 114, 164, 168], pp. 32-47 · Zbl 1135.93339
[18] 18. Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Inform. 43(7), 451-476 (2007) · Zbl 1134.93026
[19] 19. Asarin, E., Dang, T., Maler, O., Bournez, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Proc. HSCC 00: Hybrid Systems—Computation and Control. LNCS, vol. 1790, pp. 20-31. Springer, Heidelberg (2000) · Zbl 0938.93502
[20] 20. Asarin, E., Dang, T., Maler, O., Testylier, R.: Using redundant constraints for refinement. In: Automated Technology for Verification and Analysis, pp. 37-51. Springer, Heidelberg (2010) · Zbl 1305.68117
[21] 21. Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor. Comput. Sci. 138(1), 35-65 (1995) · Zbl 0884.68050
[22] 22. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1-2), 3-21 (2008)
[23] 23. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: Proc. of LICS, pp. 217-226. IEEE, Piscataway (2008)
[24] 24. Balluchi, A., Di Natale, F., Sangiovanni-Vincentelli, A.L., van Schuppen, J.H.: Synthesis for idle speed control of an automotive engine. In: Alur and Pappas [130, 182], pp. 80-94 · Zbl 1135.93327
[25] 25. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Proc. of HSCC. LNCS, vol. 2034, pp. 147-161. Springer, Heidelberg (2001) · Zbl 0991.68037
[26] 26. Bemporad, A., Bicchi, A., Buttazzo, G. (eds.): Hybrid Systems: Computation and Control, Proceedings of the 10th International Conference, HSCC 2007, Pisa, Italy. LNCS, vol. 4416. Springer, Heidelberg (2007) · Zbl 1116.68001
[27] 27. Bemporad, A., Morari, M.: Verification of hybrid systems via mathematical programming. In: Vaandrager and van Schuppen [104], pp. 31-45 · Zbl 0954.93019
[28] 28. Benerecetti, M., Faella, M., Minopoli, S.: Automatic synthesis of switching controllers for linear hybrid systems: safety control. Theor. Comput. Sci. 493, 116-138 (2013) · Zbl 1294.93041
[29] 29. Bergstra, J.A., Middelburg, C.A.: Process algebra for hybrid systems. Theor. Comput. Sci. 335(2-3), 215-280 (2005) · Zbl 1080.68073
[30] 30. Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliab. Comput. 4(4), 361-369 (1998) · Zbl 0976.65061
[31] 31. Bicchi, A., Pallottino, L.: On optimal cooperative conflict resolution for air traffic management systems. IEEE Trans. Intell. Transp. Syst. 1(4), 221-231 (2000)
[32] 32. Blum, L., Cucker, F., Shub, M., Smale, S.: Complexity and Real Computation. Springer, New York (1998) · Zbl 0872.68036
[33] 33. Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2-3), 291-345 (2004) · Zbl 1070.68063
[34] 34. Branicky, M.S.: General hybrid dynamical systems: modeling, analysis, and control. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems, vol. 1066, pp. 186-200. Springer, Heidelberg (1995)
[35] 35. Branicky, M.S., Borkar, V.S., Mitter, S.K.: A unified framework for hybrid control: model and optimal control theory. IEEE Trans. Autom. Control 43(1), 31-45 (1998) · Zbl 0951.93002
[36] 36. Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: On reachability for hybrid automata over bounded time. In: Proceedings of ICALP 2011: International Colloquium on Automata, Languages and Programming (Part II). LNCS, vol. 6756, pp. 416-427. Springer, Heidelberg (2011) · Zbl 1300.68033
[37] 37. Bu, L., Li, Y., Wang, L., Li, X.: BACH: bounded reachability checker for linear hybrid automata. In: Formal Methods in Computer-Aided Design, 2008. FMCAD’08, pp. 1-4. IEEE, Piscataway (2008)
[38] 38. Buchberger, B.: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. PhD thesis, University of Innsbruck (1965) · Zbl 1245.13020
[39] 39. Carloni, L.P., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1(1/2), 1-193 (2006) · Zbl 1107.68385
[40] 40. Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: CONCUR, pp. 138-152 (2000) · Zbl 0999.68112
[41] 41. Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.): Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, Part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011. ACM, New York (2011)
[42] 42. Chase, C., Serrano, J., Ramadge, P.J.: Periodicity and chaos from switched flow systems: contrasting examples of discretely controlled continuous systems. IEEE Trans. Autom. Control 38(1), 70-83 (1993) · Zbl 0773.93050
[43] 43. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: RTSS, pp. 183-192. IEEE, Piscataway (2012)
[44] 44. Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. USSR Comput. Math. Math. Phys. 8(6), 282-293 (1968) · Zbl 0218.90030
[45] 45. Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager and van Schuppen [8, 27, 29, 35, 52, 91, 118, 120, 131, 132, 134, 135, 143, 167, 179, 180], pp. 76-90 · Zbl 0954.93020
[46] 46. Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583-604 (2003) · Zbl 1101.68678
[47] 47. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. of CAV 2000: Computer Aided Verification. LNCS, vol. 1855, pp. 154-169. Springer, Heidelberg (2000) · Zbl 0974.68517
[48] 48. Collet, P., Eckmann, J.P.: Iterated Maps on the Interval as Dynamical Systems, vol. 1. Springer, Heidelberg (1980) · Zbl 0458.58002
[49] 49. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134-183. Springer, Heidelberg (1975)
[50] 50. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299-328 (1991) · Zbl 0754.68063
[51] 51. Collins, P.: Optimal semicomputable approximations to reachable and invariant sets. Theory Comput. Syst. 41(1), 33-48 (2007) · Zbl 1118.93320
[52] 52. Cuijpers, P.J.L., Reniers, M.A.: Hybrid process algebra. J. Log. Algebraic Program. 62(2), 191-245 (2005) · Zbl 1090.68071
[53] 53. Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating traffic agents. Int. J. Control 79(5), 395-421 (2006) · Zbl 1122.90325
[54] 54. Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliab. Comput. 17(2), 128-152 (2012)
[55] 55. Dantzig, G.B., Eaves, B.C.: Fourier-Motzkin elimination and its dual. J. Comb. Theory 14, 288-297 (1973) · Zbl 0258.15010
[56] 56. Darboux, J.-G.: Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré. Bull. Sci. Math. Astron. 2(1), 151-200 (1878) · JFM 10.0214.01
[57] 57. De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33(1-3), 45-84 (2008) · Zbl 1165.68392
[58] 58. De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: from timed models to timed implementations. Form. Asp. Comput. 17(3), 319-341 (2005) · Zbl 1101.68670
[59] 59. Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208-213 (2007) · Zbl 1184.68337
[60] 60. Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic rectangular refinement of affine hybrid systems. In: Proc. of FORMATS 2005: Formal Modelling and Analysis of Timed Systems. LNCS, vol. 3829, pp. 144-161. Springer, Heidelberg (2005) · Zbl 1175.68243
[61] 61. Fainekos, G.E., Girard, A., Pappas, G.J.: Temporal logic verification using simulation. In: Formal Modeling and Analysis of Timed Systems, pp. 171-186. Springer, Heidelberg (2006) · Zbl 1141.68463
[62] 62. Fehnker, A., Krogh, B.H.: Hybrid system verification is not a sinecure—the electronic throttle control case study. Int. J. Found. Comput. Sci. 17(4), 885-902 (2006) · Zbl 1096.68670
[63] 63. Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69-76 (1975) · Zbl 0294.02022
[64] 64. Fränzle, M.: Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: CSL. LNCS, vol. 1683, pp. 126-140. Springer, Heidelberg (1999) · Zbl 0944.68119
[65] 65. Frazzoli, E., Grosu, R. (eds.): Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, 2011. ACM, New York (2011)
[66] 66. Frehse, G.: Compositional verification of hybrid systems using simulation relations. PhD thesis, Radboud Universiteit Nijmegen (October 2005)
[67] 67. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263-279 (2008)
[68] 68. Frehse, G., Le Guernic, C., Donzé, A., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806. Springer, Heidelberg (2011)
[69] 69. Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 203-212. ACM, New York (2013) · Zbl 1362.93015
[70] 70. Frehse, G., Krogh, B.H., Rutenbar, R.A.: Verifying analog oscillator circuits using forward/backward abstraction refinement. In: Gielen, G.G.E. (ed.) DATE, pp. 257-262. European Design and Automation Association, Leuven (2006)
[71] 71. Freund, R.M., Orlin, J.B.: On the complexity of four polyhedral set containment problems. Math. Program. 33(2), 139-145 (1985) · Zbl 0581.90060
[72] 72. Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction, CADE-25. LNCS, vol. 9195, pp. 527-538. Springer, Heidelberg (2015) · Zbl 1465.68281
[73] 73. Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS. LNCS, vol. 8413, pp. 279-294. Springer, Heidelberg (2014)
[74] 74. Ghosh, P.K., Kumar, K.V.: Support function representation of convex bodies, its application in geometric computing, and some related representations. Comput. Vis. Image Underst. 72(3), 379-403 (1998)
[75] 75. Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC. LNCS, vol. 3414, pp. 291-305. Springer, Heidelberg (2005) · Zbl 1078.93005
[76] 76. Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947-953 (2012) · Zbl 1246.93045
[77] 77. Girard, A., Le Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC. LNCS, vol. 3927, pp. 257-271. Springer, Heidelberg (2006) · Zbl 1178.93024
[78] 78. Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782-798 (2007) · Zbl 1366.93032
[79] 79. Girard, A., Zheng, G.: Verification of safety and liveness properties of metric transition systems. ACM Trans. Embed. Comput. Syst. 11(S2), 54 (2012)
[80] 80. Goebel, R., Sanfelice, R.G., Teel, A.R.: Hybrid dynamical systems. IEEE Control Syst. Mag. 29(2), 28-93 (2009) · Zbl 1395.93001
[81] 81. Greenstreet, M.R.: Verifying safety properties of differential equations. In: Computer Aided Verification. LNCS, vol. 1102, pp. 277-287. Springer, Heidelberg (1996)
[82] 82. Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.): Hybrid Systems. LNCS, vol. 736. Springer, Heidelberg (1993) · Zbl 0825.00044
[83] 83. Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol. 5643, pp. 540-554. Springer, Heidelberg (2009) · Zbl 1242.93059
[84] 84. Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV. LNCS, vol. 5123, pp. 190-203. Springer, Heidelberg (2008) · Zbl 1155.68437
[85] 85. Haghverdi, E., Tabuada, P., Pappas, G.J.: Bisimulation relations for dynamical, control, and hybrid systems. Theor. Comput. Sci. 342(2), 229-261 (2005) · Zbl 1077.68062
[86] 86. Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: International Static Analysis Symposium, SAS’94, Namur (1994)
[87] 87. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: the next generation. In: Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS ’95), p. 56. IEEE, Piscataway (1995)
[88] 88. Henzinger, T.A.: Hybrid automata with finite bisimulations. In: ICALP: Automata, Languages, and Programming. LNCS, vol. 944, pp. 324-335. Springer, Heidelberg (1995) · Zbl 1412.68130
[89] 89. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1, 110-122 (1997) · Zbl 1060.68603
[90] 90. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th Annual Symposium on Principles of Programming Languages, pp. 58-70. ACM, New York (2002) · Zbl 1323.68374
[91] 91. Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol. 170, pp. 265-292. Springer, Heidelberg (2000) · Zbl 0959.68073
[92] 92. Henzinger, T.A., Ho, P.-H.: A note on abstract interpretation strategies for hybrid automata. In: Hybrid Systems II, pp. 252-264. Springer, Heidelberg (1995)
[93] 93. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43, 540-554 (1998) · Zbl 0918.93019
[94] 94. Henzinger, T.A., Kopke, P.W.: State equivalences for rectangular hybrid automata. In: CONCUR: Concurrency Theory. LNCS, vol. 1119, pp. 530-545. Springer, Heidelberg (1996)
[95] 95. Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theor. Comput. Sci. 221, 369-392 (1999) · Zbl 0930.68086
[96] 96. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57, 94-124 (1998) · Zbl 0920.68091
[97] 97. Henzinger, T.A., Raskin, J.-F.: Robust undecidability of timed and hybrid systems. In: Proc. of HSCC 00: Hybrid Systems—Computation and Control. LNCS, vol. 1790, pp. 145-159. Springer, Heidelberg (2000) · Zbl 0944.93018
[98] 98. Henzinger, T.A., Wong-Toi, H.: Using HyTech to synthesize control parameters for a steam boiler. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Formal Methods for Industrial Applications. LNCS, vol. 1165, pp. 265-282. Springer, Heidelberg (1995)
[99] 99. Ho, P.-H., Wong-Toi, H.: Automated analysis of an audio control protocol. In: Wolper, P. (ed.) CAV. LNCS, vol. 939, pp. 381-394. Springer, Heidelberg (1995)
[100] 100. Johnson, T.T., Mitra, S.: Parametrized verification of distributed cyber-physical systems: an aircraft landing protocol case study. In: ICCPS, pp. 161-170. IEEE, Piscataway (2012)
[101] 101. Jula, H., Kosmatopoulos, E.B., Ioannou, P.A.: Collision avoidance analysis for lane changing and merging. PATH Research Report UCB-ITS-PRR-99-13, Institute of Transportation Studies, University of California, Berkeley (1999)
[102] 102. Agung Julius, A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Hybrid Systems: Computation and Control, pp. 329-342. Springer, Heidelberg (2007) · Zbl 1221.93076
[103] 103. Kim, K.-D., Kumar, P.R.: Cyber-physical systems: a perspective at the centennial. Proc. IEEE 100, 1287-1308 (2012). Centennial-Issue
[104] 104. Kouskoulas, Y., Renshaw, D.W., Platzer, A., Kazanzides, P.: Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Belta, C., Ivancic, F. (eds.) HSCC, pp. 263-272. ACM, New York (2013)
[105] 105. Kühn, W.: Rigorously computed orbits of dynamical systems without the wrapping effect. Computing 61(1), 47-67 (1998) · Zbl 0910.65052
[106] 106. Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal toolbox (ET). In: 45th IEEE Conference on Decision and Control, pp. 1498-1503. IEEE, Piscataway (2006)
[107] 107. Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal techniques for reachability analysis of discrete-time linear systems. IEEE Trans. Autom. Control 52(1), 26-38 (2007) · Zbl 1366.93039
[108] 108. Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. Math. Control Signals Syst. 13(1), 1-21 (2000) · Zbl 1059.68073
[109] 109. Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231-253 (2001) · Zbl 0983.93004
[110] 110. Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. PhD thesis, Université Grenoble 1, Joseph Fourier (2009) · Zbl 1242.93059
[111] 111. Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems—A Cyber-Physical Systems Approach (2013). · Zbl 1371.68001
[112] 112. Lerda, F., Kapinski, J., Clarke, E.M., Krogh, B.H.: Verification of supervisory control software using state proximity and merging. In: Hybrid Systems: Computation and Control, pp. 344-357. Springer, Heidelberg (2008) · Zbl 1143.68457
[113] 113. Livadas, C., Lygeros, J., Lynch, N.A.: High-level modeling and analysis of TCAS. Proc. IEEE 88(7), 926-947 (2000)
[114] 114. Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM. LNCS, vol. 6664, pp. 42-56. Springer, Heidelberg (2011)
[115] 115. Loos, S.M., Witmer, D., Steenkiste, P., Platzer, A.: Efficiency analysis of formally verified adaptive cruise controllers. In: Hegyi, A., De Schutter, B. (eds.) ITSC. Springer, Heidelberg (2013)
[116] 116. Lotov, A.V., Bushenkov, V.A., Kamenev, G.K.: Interactive Decision Maps. Applied Optimization, vol. 89. Kluwer Academic, Boston (2004)
[117] 117. Lunze, J., Lamnabhi-Lagarrigue, F.: Handbook of Hybrid Systems Control: Theory, Tools, Applications. Cambridge University Press, Cambridge (2009) · Zbl 1180.93001
[118] 118. Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O automata. Inf. Comput. 185(1), 105-157 (2003)
[119] 119. Maler, O.: Algorithmic verification of continuous and hybrid systems. In: Int. Workshop on Verification of Infinite-State System (Infinity) (2013)
[120] 120. Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop, vol. 600, pp. 447-484. Springer, Heidelberg (1991)
[121] 121. Maler, O., Pnueli, A. (eds.): Hybrid Systems: Computation and Control, Proceedings of the 6th International Workshop, HSCC 2003, Prague, Czech Republic, April 3-5, 2003. LNCS, vol. 2623. Springer, Heidelberg (2003) · Zbl 1017.00053
[122] 122. Marwedel, P.: Embedded System Design: Embedded Systems Foundations of Cyber-Physical Systems. Springer, Heidelberg (2010) · Zbl 1213.68003
[123] 123. Matringe, N., Vieira Moura, A., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS. LNCS, vol. 6337, pp. 373-389. Springer, Heidelberg (2010) · Zbl 1306.68101
[124] 124. Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Proc. of HSCC 00: Hybrid Systems—Computation and Control. LNCS, vol. 1790, pp. 296-309. Springer, Heidelberg (2000) · Zbl 0992.93050
[125] 125. Milner, R.: An algebraic definition of simulation between programs. In: Cooper, D.C. (ed.) Proc. of the 2nd Int. Joint Conference on Artificial Intelligence, London, UK, September 1971. pp. 481-489. William Kaufmann, British Computer Society, London (1971)
[126] 126. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980) · Zbl 0452.68027
[127] 127. Mitchell, I.M., Bayen, A.M., Tomlin, C.J.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50(7), 947-957 (2005) · Zbl 1366.91022
[128] 128. Mitchell, I.M., Templeton, J.A.: A toolbox of Hamilton-Jacobi solvers for analysis of nondeterministic continuous and hybrid systems. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control. LNCS, vol. 3414, pp. 480-494. Springer, Heidelberg (2005) · Zbl 1078.93522
[129] 129. Mitra, S., Wang, Y., Lynch, N.A., Feron, E.: Safety verification of model helicopter controller using hybrid input/output automata. In: Maler and Pnueli [8, 91], pp. 343-358 · Zbl 1032.93535
[130] 130. Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: Robotics: Science and Systems (2013)
[131] 131. Nerode, A., Yakhnis, A.: Modelling hybrid systems as games. In: Proceedings of the 31st IEEE Conference on Decision and Control, vol. 3, pp. 2947-2952 (1992)
[132] 132. Nerode, A., Kohn, W.: Models for hybrid systems: automata, topologies, controllability, observability. In: Grossman et al. [135, 141], pp. 317-356
[133] 133. Neumaier, A.: The wrapping effect, ellipsoid arithmetic, stability and confidence regions. In: Validation Numerics, pp. 175-190. Springer, Heidelberg (1993) · Zbl 0790.65035
[134] 134. Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: An approach to the description and analysis of hybrid systems. In: Grossman et al. [7, 12, 39, 80, 103, 143, 163, 171, 172], pp. 149-178
[135] 135. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143-189 (2008) · Zbl 1181.03035
[136] 136. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309-352 (2010) · Zbl 1191.03024
[137] 137. Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010) · Zbl 1211.68412
[138] 138. Platzer, A.: Quantified differential invariants. In: Frazzoli and Grosu [165], pp. 63-72 · Zbl 1362.93071
[139] 139. Platzer, A.: Stochastic differential dynamic logic for stochastic hybrid programs. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE. LNCS, vol. 6803, pp. 431-445. Springer, Heidelberg (2011) · Zbl 1341.68030
[140] 140. Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. Log. Methods Comput. Sci. 8(4), 1-44 (2012). Special issue for selected papers from CSL’10 · Zbl 1261.03113
[141] 141. Platzer, A.: The complete proof theory of hybrid systems. In: LICS [137], pp. 541-550 · Zbl 1364.03045
[142] 142. Platzer, A.: A differential operator approach to equational differential invariants. In: Beringer, L., Felty, A. (eds.) ITP. LNCS, vol. 7406, pp. 28-48. Springer, Heidelberg (2012) · Zbl 1360.68596
[143] 143. Platzer, A.: Logics of dynamical systems. In: LICS [111, 122], pp. 13-24 · Zbl 1362.68178
[144] 144. Platzer, A.: The structure of differential invariants and differential cut elimination. Log. Methods Comput. Sci. 8(4), 1-38 (2012) · Zbl 1261.03112
[145] 145. Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219-265 (2017) · Zbl 1437.03119
[146] 146. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Heidelberg (2018) · Zbl 1400.93003
[147] 147. Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad et al. [8, 27, 29, 35, 52, 91, 118, 120, 131, 132, 134-136, 167, 179, 180], pp. 473-486 · Zbl 1221.93118
[148] 148. Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Form. Methods Syst. Des. 35(1), 98-120 (2009) · Zbl 1180.93024
[149] 149. Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D. (eds.) FM. LNCS, vol. 5850, pp. 547-562. Springer, Heidelberg (2009)
[150] 150. Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. LNCS, vol. 5195, pp. 171-178. Springer, Heidelberg (2008) · Zbl 1165.68469
[151] 151. Platzer, A., Quesel, J.-D.: European Train Control System: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM. LNCS, vol. 5885, pp. 246-265. Springer, Heidelberg (2009)
[152] 152. Prabhakar, P., Viswanathan, M.: A dynamic algorithm for approximate flow computations. In: Frazzoli and Grosu [22], pp. 133-142 · Zbl 1362.93019
[153] 153. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur and Pappas [55, 63], pp. 477-492 · Zbl 1135.93317
[154] 154. Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415-1429 (2007) · Zbl 1366.93711
[155] 155. Puri, A.: Dynamical properties of timed automata. In: FTRTFT ’98. LNCS, vol. 1486, pp. 210-227. Springer, Heidelberg (1998)
[156] 156. Puri, A., Varaiya, P.: Decidability of hybrid systems with rectangular differential inclusion. In: Proc. of CAV. LNCS, vol. 818, pp. 95-104. Springer, Heidelberg (1994)
[157] 157. Ratschan, S.: Safety verification of non-linear hybrid systems is quasi-semidecidable. In: TAMC 2010: 7th Annual Conference on Theory and Applications of Models of Computation. LNCS, vol. 6108, pp. 397-408. Springer, Heidelberg (2010) · Zbl 1284.68415
[158] 158. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. Trans. Embed. Comput. Syst. 6(1), 8 (2007) · Zbl 1078.93508
[159] 159. Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 221-230. ACM, New York (2010) · Zbl 1360.34082
[160] 160. Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 188-202. Springer, Heidelberg (2008) · Zbl 1134.68419
[161] 161. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods Syst. Des. 32(1), 25-55 (2008) · Zbl 1133.68365
[162] 162. Segelken, M.: Abstraction and counterexample-guided construction of · Zbl 1135.68482
[163] 163. Sokolsky, O., Lee, I., Heimdahl, M.P.E.: Challenges in the regulatory approval of medical cyber-physical systems. In: Chakraborty et al. [44], pp. 227-232
[164] 164. Stursberg, O., Fehnker, A., Han, Z., Krogh, B.H.: Verification of a cruise control system using counterexample-guided search. Control Eng. Pract. 12(10), 1269-1278 (2004)
[165] 165. Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Heidelberg (2009) · Zbl 1195.93001
[166] 166. Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951) · Zbl 0044.25102
[167] 167. Tavernini, L.: Differential automata and their discrete simulators. Nonlinear Anal. 11(6), 665-683 (1987) · Zbl 0666.34005
[168] 168. Tiwari, A.: Approximate reachability for linear systems. In: Maler and Pnueli [6, 96], pp. 514-525 · Zbl 1032.93518
[169] 169. Tiwari, A.: Abstractions for hybrid systems. Form. Methods Syst. Des. 32(1), 57-83 (2008) · Zbl 1133.68368
[170] 170. Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC. LNCS, vol. 4981, pp. 658-661. Springer, Heidelberg (2008) · Zbl 1144.93311
[171] 171. Tiwari, A.: Logic in software, dynamical and biological systems. In: LICS, pp. 9-10. IEEE, Piscataway (2011)
[172] 172. Tiwari, A., Shankar, N., Rushby, J.M.: Invisible formal methods for embedded control systems. Proc. IEEE 91(1), 29-39 (2003)
[173] 173. Tiwary, H.R.: On the hardness of computing intersection, union and Minkowski sum of polytopes. Discrete Comput. Geom. 40(3), 469-479 (2008) · Zbl 1155.52008
[174] 174. Tomlin, C., Pappas, G., Košecká, J., Lygeros, J., Sastry, S.: Advanced air traffic automation: a case study in distributed decentralized control. In: Siciliano, B., Valavanis, K. (eds.) Control Problems in Robotics and Automation. Lecture Notes in Control and Information Sciences, vol. 230, pp. 261-295. Springer, Heidelberg (1998)
[175] 175. Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE Trans. Autom. Control 43(4), 509-521 (1998) · Zbl 0904.90113
[176] 176. Umeno, S., Lynch, N.A.: Proving safety properties of an aircraft landing protocol using I/O automata and the PVS theorem prover: a case study. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM, vol. 4085, pp. 64-80. Springer, Heidelberg (2006)
[177] 177. Umeno, S., Lynch, N.A.: Safety verification of an aircraft landing protocol: a refinement approach. In: Bemporad et al. [136], pp. 557-572
[178] 178. Vaandrager, F.W., van Schuppen, J.H. (eds.) Hybrid Systems: Computation and Control, Proceedings of the Second International Workshop, HSCC’99, Berg en Dal, The Netherlands, March 29-31, 1999. LNCS, vol. 1569, Springer, Heidelberg (1999) · Zbl 0911.00057
[179] 179. van Beek, D.A., Man, K.L., Reniers, M.A., Rooda, J.E., Schiffelers, R.R.H.: Syntax and consistent equation semantics of hybrid Chi. J. Log. Algebraic Program. 68(1-2), 129-210 (2006) · Zbl 1088.68111
[180] 180. van Beek, D.A., Reniers, M.A., Schiffelers, R.R.H., Rooda, J.E.: Concrete syntax and semantics of the compositional interchange format for hybrid systems. In: 17th IFAC World Congress (2008) · Zbl 1221.68152
[181] 181. Wong-Toi, H.: Analysis of slope-parametric rectangular automata. In: Hybrid Systems. LNCS, vol. 1567, pp. 390-413. Springer, Heidelberg (1997) · Zbl 0927.93034
[182] 182. Wongpiromsarn, T., Mitra, S., Murray, R.M., Lamperski, A.G.: Periodically controlled hybrid systems. In: Majumdar, R., Tabuada, P. (eds.) HSCC. LNCS, vol. 5469, pp. 396-410. Springer, Heidelberg (2009) · Zbl 1237.93120
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.