nach oben

vorheriger Artikel Selected Extended Papers of NFM 2017: Preface

nächster Artikel Compositional Falsification of Cyber-Physical S...

Tipp

Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants

Zeitschrift:: Journal of Automated Reasoning > Ausgabe 4/2019

Autoren:: Andrew Sogokon, Paul B. Jackson, Taylor T. Johnson

Wichtige Hinweise

This material is based upon work supported by the UK Engineering and Physical Sciences Research Council under Grants EPSRC EP/I010335/1 and EP/J001058/1, the National Science Foundation (NSF) under Grant Numbers CNS 1464311 and CCF 1527398, the Air Force Research Laboratory (AFRL) through Contract Number FA8750-15-1-0105, and the Air Force Office of Scientific Research (AFOSR) under Contract Number FA9550-15-1-0258.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

We describe a method for verifying the temporal property of persistence in non-linear hybrid systems. Given some system and an initial set of states, the method establishes that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flowpipe computation with deductive reasoning about invariants and is more general than each technique alone. We illustrate the method with a case study showing that potentially destructive stick-slip oscillations of an oil-well drill eventually die away for a certain choice of drill control parameters. The case study demonstrates how just using flowpipes or just reasoning about invariants alone can be insufficient and shows the richness of systems that one can handle with the proposed method, since the systems features modes with non-polynomial ODEs. We also propose an alternative method for proving persistence that relies solely on flowpipe computation.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175–205 (2010) MathSciNetMATHCrossRef

Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems, Volume 736 of LNCS, pp. 209–229. Springer, Berlin (1992)

Baier, C., Tinelli, C. (eds.): Tools and Algorithms for the Construction and Analysis of Systems—21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings, volume 9035 of LNCS. Springer (2015)

Bemporad, A., Bicchi, A., Buttazzo, G.C. (eds.): Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3–5, 2007, Proceedings, Volume 4416 of LNCS. Springer (2007)

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) MathSciNetMATHCrossRef

Blanchini, F.: Set invariance in control. Automatica 35(11), 1747–1767 (1999) MathSciNetMATHCrossRef

Carter, R.A:. Verification of liveness properties on hybrid dynamical systems. Ph.D. thesis, University of Manchester, School of Computer Science (2013)

Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina and Veith [69], pp. 258–263 CrossRef

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) MathSciNetMATHCrossRef

10.

Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1), 1–40 (2012) MathSciNetMATH

11.

Collins, G.E.: Hauptvortrag: quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Automata Theory and Formal Languages, 2nd GI Conference, Kaiserslautern, May 20–23, 1975, Volume 33 of LNCS, pp. 134–183. Springer, Berlin (1975)

12.

Davenport, J.H., England, M.: Recent advances in real geometric reasoning. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry—10th International Workshop, ADG 2014, Coimbra, Portugal, July 9–11, 2014, Revised Selected Papers, Volume 9201 of LNCS, pp. 37–52. Springer (2014)

13.

Davison, E., Kurak, E.: A computational method for determining quadratic Lyapunov functions for non-linear systems. Automatica 7(5), 627–636 (1971) MathSciNetMATHCrossRef

14.

Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad et al. [4], pp. 174–189

15.

Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: 2011 IEEE/ACM International Conference on Cyber-Physical Systems, ICCPS 2011, Chicago, Illinois, USA, 12–14 April, 2011, pp. 22–31. IEEE Computer Society (2011)

16.

Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: Dang, T., Mitchell, I.M. (eds.) Hybrid Systems: Computation and Control (Part of CPS Week 2012), HSCC’12, Beijing, China, April 17–19, 2012, pp. 115–124. ACM (2012)

17.

Eggers, A., Ramdani, N., Nedialkov, N.S., Fränzle, M.: Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Softw. Syst. Model. 14(1), 121–148 (2015) MATHCrossRef

18.

Fan, C., Kapinski, J., Jin, X., Mitra, S.: Locally optimal reach set over-approximation for nonlinear systems. In: 2016 International Conference on Embedded Software, EMSOFT 2016, Pittsburgh, Pennsylvania, USA, October 1–7, 2016, pp. 6:1–6:10. ACM (2016)

19.

Fan, C., Kapinski, J., Jin, X., Mitra, S.: Simulation-driven reachability using matrix measures. ACM Trans. Embed. Comput. Syst. 17(1):21:1–21, 28 (2018)

20.

Forsman, K.: Construction of Lyapunov functions using Gröbner bases, Vol. 1, pp. 798–799. IEEE(1991)

21.

Frehse, G., Guernic, C.L., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification—23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011. Proceedings, Volume 6806 of LNCS, pp. 379–395. Springer (2011) CrossRef

22.

Fulton, N., Mitsch, S., Quesel, J., 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—25th International Conference on Automated Deduction, Berlin, Germany, August 1–7, 2015, Proceedings, Volume 9195 of LNCS, pp. 527–538. Springer (2015) CrossRef

23.

Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, Volume 8413 of LNCS, pp. 279–294. Springer (2014)

24.

Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47, 19–43 (2017) MATH

25.

Goubault, E., Jourdan, J., Putot, S., Sankaranarayanan, S.: Finding non-polynomial positive invariants and Lyapunov functions for polynomial systems through Darboux polynomials. In: American Control Conference, ACC 2014, Portland, OR, USA, June 4–6, 2014, pp. 3571–3578. IEEE (2014)

26.

Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Frehse, G., Mitra, S. (eds.) Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18–20, 2017, pp. 1–10. ACM (2017)

27.

Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta and Malik [28], pp. 190–203

28.

Gupta, A., Malik, S. (eds.): Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008, Proceedings, Volume 5123 of LNCS. Springer (2008)

29.

Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27–30, 1996, pp. 278–292. IEEE Computer Society (1996)

30.

Immler, F.: Verified reachability analysis of continuous systems. In: Baier and Tinelli [3], pp. 37–51

31.

Jirstrand, M.: Cylindrical algebraic decomposition—an introduction. Technical Report 1807, Linköping University, Automatic Control (1995)

32.

Kapela, T., Mrozek, M., Pilarczyk, P., Wilczak, D., Zgliczyński, P.: CAPD—a rigorous toolbox for computer assisted proofs in dynamics. Technical report, Jagiellonian University, Krakow, Poland (2010). http://capd.ii.uj.edu.pl/. Accessed 20 Nov 2018

33.

Khalil, H.K.: Nonlinear Systems, 3rd edn. Prentice Hall, Upper Saddle River (2002) MATH

34.

Kong, S., Gao, S., Chen, W., Clarke, E.M.: dreach: \({\delta }\)-reachability analysis for hybrid systems. In: Baier and Tinelli [3], pp. 200–205

35.

Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255–299 (1990) CrossRef

36.

Lin, Y., Stadtherr, M.A.: Validated solutions of initial value problems for parametric ODEs. Appl. Numer. Math. 57(10), 1145–1162 (2007) MathSciNetMATHCrossRef

37.

Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed) Programming Languages and Systems—8th Asian Symposium, APLAS 2010, Shanghai, China, November 28–December 1, 2010. Proceedings, Volume 6461 of LNCS, pp. 1–15. Springer (2010)

38.

Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: 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, pp. 97–106. ACM (2011)

39.

Lygeros, J., Johansson, K.H., Simić, S.N., Zhang, J., Sastry, S.S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2–17 (2003) MathSciNetMATHCrossRef

40.

Mahboubi, A.: Programming and certifying a CAD algorithm in the Coq system. In: Coquand, T., Lombardi, H., Roy, M. (eds.) Mathematics, Algorithms, Proofs, 9–14. January 2005, Volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2005)

41.

Maidens, J.N., Arcak, M.: Trajectory-based reachability analysis of switched nonlinear systems using matrix measures. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15–17, 2014, pp. 6358–6364. IEEE (2014)

42.

Maidens, J.N., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265–270 (2015) MathSciNetMATHCrossRef

43.

Makino, K., Berz, M.: COSY INFINITY version 9. Nucl. Instrum. Methods Phys. Res. Sect. A 558(1), 346–350 (2006) CrossRef

44.

Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Dwork, C. (ed) Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, Quebec City, Quebec, Canada, August 22–24, 1990, pp. 377–410. ACM (1990)

45.

Martin-Dorel, É., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16–17, 2017, pp. 90–99. ACM (2017)

46.

Mitrohin, C., Podelski, A.: Composing stability proofs for hybrid systems. In: Fahrenberg, U., Tripakis, S. (eds.) Formal Modeling and Analysis of Timed Systems—9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings, Volume 6919 of LNCS, pp. 286–300. Springer (2011)

47.

Möhlmann, E., Hagemann, W., Theel, O.E.: Hybrid tools for hybrid systems—proving stability and safety at once. In: Sankaranarayanan, S., Vicario, E. (eds.) Formal Modeling and Analysis of Timed Systems—13th International Conference, FORMATS 2015, Madrid, Spain, September 2–4, 2015, Proceedings, Volume 9268 of LNCS, pp. 222–239. Springer (2015)

48.

Möhlmann, E., Theel, O.E.: Stabhyli: a tool for automatic stability verification of non-linear hybrid systems. In: Belta, C., Ivančić, F. (eds.) Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, April 8–11, 2013, Philadelphia, PA, USA, pp. 107–112. ACM (2013)

49.

Navarro-López, E.M., Carter, R.: Hybrid automata: an insight into the discrete abstraction of discontinuous systems. Int. J. Syst. Sci. 42(11), 1883–1898 (2011) MathSciNetMATHCrossRef

50.

Navarro-López, E.M., Carter, R.: Deadness and how to disprove liveness in hybrid dynamical systems. Theor. Comput. Sci. 642(C), 1–23 (2016) MathSciNetMATHCrossRef

51.

Navarro-López, E.M., Suárez, R.: Practical approach to modelling and controlling stick-slip oscillations in oilwell drillstrings, Vol. 2, pp. 1454–1460. IEEE (2004)

52.

Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM—IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), Duisburg (2006)

53.

Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236–262 (2007) MathSciNetMATHCrossRef

54.

Nishida, T., Mizutani, K., Kubota, A., Doshita, S.: Automated phase portrait analysis by integrating qualitative and quantitative analysis. In: Dean, T.L., McKeown, K.R. (eds.) Proceedings of the 9th National Conference on Artificial Intelligence, Anaheim, CA, USA, July 14–19, 1991, Vol. 2, pp. 811–816. AAAI Press/The MIT Press (1991)

55.

Paulson, L.C.: MetiTarski: Past and future. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving—Third International Conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings, Volume 7406 of LNCS, pp. 1–10. Springer (2012)

56.

Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008) MathSciNetMATHCrossRef

57.

Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta and Malik [28], pp. 176–189

58.

Platzer, A., Quesel, J.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008, Proceedings, Volume 5195 of LNCS, pp. 171–178. Springer (2008)

59.

Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29–31, 2006, Proceedings, Volume 3927 of LNCS, pp. 507–521. Springer (2006)

60.

Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3–5, 2007, Proceedings, Volume 4763 of LNCS, pp. 320–335. Springer (2007)

61.

Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad et al. [4], pp. 750–753

62.

Prabhakar, P., Soto, M.G.: Abstraction based model-checking of stability of hybrid systems. In: Sharygina and Veith [69], pp. 280–295 CrossRef

63.

Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25–27, 2004, Proceedings, Volume 2993 of LNCS, pp. 477–492. Springer (2004)

64.

Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM J. Control Optim. 48(7), 4377–4394 (2010) MathSciNetMATHCrossRef

65.

Rebiha, R., Moura, A.V., Matringe, N.: Generating invariants for non-linear hybrid systems. Theor. Comput. Sci. 594, 180–200 (2015) MathSciNetMATHCrossRef

66.

Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Logic 33(4), 514–520, 12 (1968) MathSciNetMATH

67.

Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12–15, 2010, pp. 221–230. ACM (2010)

68.

Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods Syst. Des. 32(1), 25–55 (2008) MATHCrossRef

69.

Sharygina, N., Veith, H. (eds.): Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, Volume 8044 of LNCS. Springer (2013)

70.

Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation—17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings, Volume 9583 of LNCS, pp. 268–288. Springer (2016)

71.

Sogokon, A., Ghorbal, K., Johnson, T.T.: Operational models for piecewise-smooth systems. ACM Trans. Embed. Comput. Syst. 16(5), 185:1–185:19 (2017)

72.

Sogokon, A., Jackson, P.B.: Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In: Bjørner, N., de Boer, F.S. (eds.) FM 2015: Formal Methods—20th International Symposium, Oslo, Norway, June 24–26, 2015, Proceedings, Volume 9109 of LNCS, pp. 514–531. Springer (2015)

73.

Strzeboński, A.W.: Cylindrical decomposition for systems transcendental in the first variable. J. Symb. Comput. 46(11), 1284–1290 (2011) MathSciNetMATHCrossRef

74.

Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: Kannan, R., Kumar, K.N. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009, December 15–17, 2009, IIT Kanpur, India, Volume 4 of LIPIcs, pp. 383–394. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

75.

Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) Hybrid Systems: Computation and Control, 11th International Workshop, HSCC 2008, St. Louis, MO, USA, April 22–24, 2008. Proceedings, Volume 4981 of LNCS, pp. 658–661. Springer (2008)

76.

Vannelli, A., Vidyasagar, M.: Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems. Automatica 21(1), 69–80 (1985) MathSciNetMATHCrossRef

77.

Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M.J., Conchon, S., Zaïdi, F. (eds.) Formal Methods and Software Engineering—17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3–5, 2015, Proceedings, Volume 9407 of LNCS, pp. 382–399. Springer (2015)

78.

Xue, B., Easwaran, A., Cho, N., Fränzle, M.: Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control 62(7), 3518–3523 (2017) MathSciNetMATHCrossRef

79.

Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods—19th International Symposium, Singapore, May 12–16, 2014. Proceedings, Volume 8442 of LNCS, pp. 733–748. Springer (2014)

80.

Zhao, H., Zhan, N., Kapur, D.: Synthesizing switching controllers for hybrid systems by generating invariants. In: Theories of Programming and Formal Methods—Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pp. 354–373 (2013) CrossRef

Titel: Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants
Autoren:: Andrew Sogokon
Paul B. Jackson
Taylor T. Johnson
Publikationsdatum: 24.11.2018
DOI: https://doi.org/10.1007/s10817-018-9497-x
Verlag: Springer Netherlands
Zeitschrift: Journal of Automated Reasoning
Ausgabe 4/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670

Premium Partner

Bildnachweise

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Publisher's Note

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2019

Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

Selected Extended Papers of NFM 2017: Preface

Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

QPCF: Higher-Order Languages and Quantum Circuits

Efficient Active Automata Learning via Mutation Testing

Premium Partner