skip to main content
research-article

In memory of Oded Maler: automatic reachability analysis of hybrid-state automata

Published: 19 February 2019 Publication History

Abstract

Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with automata capturing switching behavior. Since the introduction of the computational model more than a quarter of a century ago [Maler et al. 1992], its algorithmic verification has been an area of intense research. Within this note, which is dedicated to Oded Maler (1957--2018) as one of the inventors of the model, we are trying to delineate major lines of attack to the reachability problem for hybrid automata. Due to its relation to system safety, the reachability problem is a prototypical verification problem for hybrid discrete-continuous system dynamics.

References

[1]
Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. 2017. Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. Sci. Comput. Program. 148 (2017), 123--160.
[2]
Matthias Althoff. 2013. 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, HSCC 2013, April 8--11, 2013, Philadelphia, PA, USA, Calin Belta and Franjo Ivancic (Eds.). ACM, 173--182.
[3]
Matthias Althoff, Dmitry Grebenyuk, and Niklas Kochdumper. 2018. Implementation of Taylor models in CORA 2018. In ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH@ADHS 2018, Oxford, UK, July 13, 2018 (EPiC Series in Computing), Goran Frehse, Matthias Althoff, Sergiy Bogomolov, and Taylor T. Johnson (Eds.), Vol. 54. EasyChair, 145--173.
[4]
Matthias Althoff, Olaf Stursberg, and Martin Buss. 2008. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In Proceedings of the 47th IEEE Conference on Decision and Control, CDC 2008, December 9--11, 2008, Cancún, Mexico. IEEE, 4042--4048.
[5]
Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. 1993. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel (Eds.). Lecture Notes in Computer Science, Vol. 736. Springer Berlin Heidelberg, 209--229.
[6]
Rajeev Alur and David L. Dill. 1990. Automata for modeling real-time systems. In Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16--20, 1990, Proceedings (Lecture Notes in Computer Science), Mike Paterson (Ed.), Vol. 443. Springer, 322--335.
[7]
Hirokazu Anai and Volker Weispfenning. 2001. Reach set computations using real quantifier elimination. In Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28--30, 2001, Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, 63--76.
[8]
Eugene Asarin and Ahmed Bouajjani. 2001. Perturbed turing machines and hybrid systems. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16--19, 2001, Proceedings. IEEE Computer Society, 269--278.
[9]
Eugene Asarin, Thao Dang, and Antoine Girard. 2003. Reachability analysis of nonlinear systems using conservative approximation. In Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3--5, 2003, Proceedings (Lecture Notes in Computer Science), Oded Maler and Amir Pnueli (Eds.), Vol. 2623. Springer, 20--35.
[10]
Eugene Asarin, Oded Maler, and Amir Pnueli. 1995. Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science 138, 1 (1995), 35 -- 65. Hybrid Systems.
[11]
Gilles Audemard, Marco Bozzano, Alessandro Cimatti, and Roberto Sebastiani. 2005. Verifying industrial hybrid systems with MathSAT. Electronic Notes in Theoretical Computer Science 119, 2 (2005), 17 -- 32. Proceedings of the 2nd International Workshop on Bounded Model Checking (BMC 2004).
[12]
Thomas Becker, Volker Weispfenning, and Heinz Kredel. 1993. Gröbner Bases: A Computational Approach to Commutative Algebra. Springer-Verlag.
[13]
Gerd Behrmann, Alexandre David, Kim G. Larsen, Paul Pettersson, and Wang Yi. 2011. Developing UPPAAL over 15 years. Softw., Pract. Exper. 41, 2 (2011), 133--142.
[14]
Alberto Bemporad and Manfred Morari. 1999. Verification of hybrid systems via mathematical programming (Lecture Notes in Computer Science), Frits W. Vaandrager and Jan H. van Schuppen (Eds.), Vol. 1569. Springer, 31--45.
[15]
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22--28, 1999, Proceedings (Lecture Notes in Computer Science), Rance Cleaveland (Ed.), Vol. 1579. Springer, 193--207.
[16]
Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2012. Taylor model flowpipe construction for non-linear hybrid systems. In Proceedings of the 33rd IEEE Real-Time Systems Symposium, RTSS 2012, San Juan, PR, USA, December 4--7, 2012. IEEE Computer Society, 183--192.
[17]
Xin Chen, Sriram Sankaranarayanan, and Erika Ábrahám. 2014. Under-approximate flowpipes for non-linear continuous systems. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21--24, 2014. IEEE, 59--66.
[18]
Xin Chen, Sriram Sankaranarayanan, and Erika Ábrahám. 2015. Flow* 1.2: more effective to play with hybrid systems. In 1st and 2nd International Workshop on Applied Verification for Continuous and Hybrid Systems, ARCH@CPSWeek 2014, Berlin, Germany, April 14, 2014 / ARCH@CPSWeek 2015, Seattle, WA, USA, April 13, 2015. (EPiC Series in Computing), Goran Frehse and Matthias Althoff (Eds.), Vol. 34. EasyChair, 152--159.
[19]
Hubert Comon and Yan Jurski. 1999. Timed automata and the theory of real numbers. In CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24--27, 1999, Proceedings (Lecture Notes in Computer Science), Jos C. M. Baeten and Sjouke Mauw (Eds.), Vol. 1664. Springer, 242--257.
[20]
Werner Damm, Guilherme Pinto, and Stefan Ratschan. 2005. Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. In Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4--7, 2005, Proceedings (Lecture Notes in Computer Science), Doron A. Peled and Yih-Kuen Tsay (Eds.), Vol. 3707. Springer, 99--113.
[21]
Thao Dang, Oded Maler, and Romain Testylier. 2010. Accurate hybridization of nonlinear systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12--15, 2010, Karl Henrik Johansson and Wang Yi (Eds.). ACM, 11--20.
[22]
Alexandre Donzé and Oded Maler. 2007. Systematic simulation using sensitivity analysis. In Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3--5, 2007, Proceedings (Lecture Notes in Computer Science), Alberto Bemporad, Antonio Bicchi, and Giorgio C. Buttazzo (Eds.), Vol. 4416. Springer, 174--189.
[23]
Parasara S. Duggirala, Sayan Mitra, and Mahesh Viswanathan. 2013. Verification of annotated models from executions. In Proceedings of the International Conference on Embedded Software, EMSOFT 2013, Montreal, QC, Canada, September 29 - Oct. 4, 2013. IEEE, 26:1--26:10.
[24]
Andreas Eggers, Martin Fränzle, and Christian Herde. 2008. SAT modulo ODE: A direct SAT approach to hybrid systems. In Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20--23, 2008. Proceedings (Lecture Notes in Computer Science), Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan (Eds.), Vol. 5311. Springer, 171--185.
[25]
Andreas Eggers, Nacim Ramdani, Nedialko S. Nedialkov, and Martin Fränzle. 2015. Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods. Software and System Modeling 14, 1 (2015), 121--148.
[26]
Georgios E. Fainekos, Antoine Girard, and George J. Pappas. 2006. Temporal logic verification using simulation. In Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25--27, 2006, Proceedings (Lecture Notes in Computer Science), Eugene Asarin and Patricia Bouyer (Eds.), Vol. 4202. Springer, 171--186.
[27]
Martin Fränzle. 1999. Analysis of hybrid systems: an ounce of realism can save an infinity of states. In Computer Science Logic: 13th International Workshop, CSL'99 8th Annual Conference of the EACSL Madrid, Spain, September 20--25, 1999 Proceedings, Jörg Flum and Mario Rodriguez-Artalejo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 126--139.
[28]
Martin Fränzle, Mahsa Shirmohammadi, Mani Swaminathan, and James Worrell. 2018. Costs and rewards in priced timed automata. In 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9--13, 2018, Prague, Czech Republic (LIPIcs), Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella (Eds.), Vol. 107. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 125:1--125:14.
[29]
Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 379--395.
[30]
Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, and Naijun Zhan. 2015. Decidability of the reachability for a family of linear vector fields. In Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12--15, 2015, Proceedings. Springer International Publishing, Cham, 482--499.
[31]
Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan. 2016. Computing reachable sets of linear vector fields revisited. In 2016 European Control Conference, ECC 2016, Aalborg, Denmark, June 29 - July 1, 2016. IEEE, 419--426.
[32]
Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan. 2018. Reachability analysis for solvable dynamical systems. IEEE Trans. Automat. Contr. 63, 7 (2018), 2003--2018.
[33]
Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. 2012. Δ-complete decision procedures for satisfiability over the reals. In Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings (Lecture Notes in Computer Science), Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.), Vol. 7364. Springer, 286--300.
[34]
Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. Satisfiability modulo ODEs. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20--23, 2013. IEEE, 105--112.
[35]
Antoine Girard, Colas Le Guernic, and Oded Maler. 2006. Efficient computation of reachable sets of linear time-invariant systems with inputs. In Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29--31, 2006, Proceedings (Lecture Notes in Computer Science), João P. Hespanha and Ashish Tiwari (Eds.), Vol. 3927. Springer, 257--271.
[36]
Antoine Girard and Colas Le Guernic. 2008. Zonotope/hyperplane intersection for hybrid systems reachability analysis. In Hybrid Systems: Computation and Control, Magnus Egerstedt and Bud Mishra (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 215--228.
[37]
Eric Goubault, Olivier Mullier, Sylvie Putot, and Michel Kieffer. 2014. Inner approximated reachability analysis. In 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, Berlin, Germany, April 15--17, 2014, Martin Fränzle and John Lygeros (Eds.). ACM, 163--172.
[38]
Eric Goubault and Sylvie Putot. 2017. Forward inner-approximated reachability of non-linear continuous systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18--20, 2017, Goran Frehse and Sayan Mitra (Eds.). ACM, 1--10.
[39]
Eric Goubault, Sylvie Putot, and Lorenz Sahlmann. 2018. Inner and outer approximating flowpipes for delay differential equations. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14--17, 2018, Proceedings, Part II (Lecture Notes in Computer Science), Hana Chockler and Georg Weissenbacher (Eds.), Vol. 10982. Springer, 523--541.
[40]
Jan F. Groote, J. W. C. Koorn, and Sebastiaan F. M. van Vlijmen. 1995. The safety guaranteeing system at station Hoorn-Kersenboogerd. In Compass '95: 10th Annual Conference on Computer Assurance. National Institute of Standards and Technology, Gaithersburg, Maryland, 57--68.
[41]
Vineet Gupta, Thomas A. Henzinger, and Radha Jagadeesan. 1997. Robust timed automata (Lecture Notes in Computer Science), Oded Maler (Ed.), Vol. 1201. Springer, 331--345.
[42]
Godfrey H. Hardy, Edward M. Wright, and E.W. Wright. 1979. An Introduction to the Theory of Numbers. Clarendon Press.
[43]
Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. 1997. HYTECH: A model checker for hybrid systems. STTT 1, 1--2 (1997), 110--122.
[44]
Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. 1998. What's decidable about hybrid automata? J. Comput. System Sci. 57, 1 (1998), 94 -- 124.
[45]
Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. 1992. Symbolic model checking for real-time systems. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22--25, 1992. IEEE Computer Society, 394--406.
[46]
Zhenqi Huang and Sayan Mitra. 2012. Computing bounded reach sets from sampled simulation traces. In Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC'12, Beijing, China, April 17--19, 2012, Thao Dang and Ian M. Mitchell (Eds.). ACM, 291--294.
[47]
A. Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee, and George J. Pappas. 2007. Robust test generation and coverage for hybrid systems. In Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3--5, 2007, Proceedings (Lecture Notes in Computer Science), Alberto Bemporad, Antonio Bicchi, and Giorgio C. Buttazzo (Eds.), Vol. 4416. Springer, 329--342.
[48]
Deepak Kapur. 2017. Nonlinear polynomials, interpolants and invariant generation for system analysis. In Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), Kaiserslautern, Germany, July 29, 2017. (CEUR Workshop Proceedings), Matthew England and Vijay Ganesh (Eds.), Vol. 1974. CEUR-WS.org.
[49]
Alexander B. Kurzhanski and Pravin Varaiya. 2000. Ellipsoidal techniques for reachability analysis: internal approximation. Systems & Control Letters 41, 3 (2000), 201 -- 211.
[50]
Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. 1999. A new class of decidable hybrid systems. In Hybrid Systems: Computation and Control, Frits W. Vaandrager and Jan H. van Schuppen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 137--151.
[51]
Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. 2001. Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32, 3 (2001), 231--253.
[52]
Kim G. Larsen, Paul Pettersson, and Wang Yi. 1995. Compositional and symbolic model-checking of real-time systems. In Proceedings 16th IEEE Real-Time Systems Symposium(RTSS). IEEE Computer Society, 76--87.
[53]
Kim G. Larsen and Jacob I. Rasmussen. 2008. Optimal reachability for multi-priced timed automata. Theoretical Computer Science 390, 2 (2008), 197 -- 213. Foundations of Software Science and Computational Structures.
[54]
Meilun Li, Peter Nazier Mosaad, Martin Fränzle, Zhikun She, and Bai Xue. 2018. Safe over- and under-approximation of reachable sets for autonomous dynamical systems. In Formal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Beijing, China, September 4--6, 2018, Proceedings (Lecture Notes in Computer Science), David N. Jansen and Pavithra Prabhakar (Eds.), Vol. 11022. Springer, 252--270.
[55]
Jiang Liu, Naijun Zhan, and Hengjun Zhao. 2011. Computing semi-algebraic invariants for polynomial dynamical systems. In 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, Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah, and Sebastian Fischmeister (Eds.). ACM, 97--106.
[56]
Oded Maler, Zohar Manna, and Amir Pnueli. 1992. From timed to hybrid systems. In Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 3--7, 1991, Proceedings (Lecture Notes in Computer Science), J. W. de Bakker, Cornelis Huizing, Willem P. de Roever, and Grzegorz Rozenberg (Eds.), Vol. 600. Springer, 447--484.
[57]
Dinesh Manocha and John F. Canny. 1992. Algorithm for implicitizing rational parametric surfaces. Comput. Aided Geom. Des. 9, 1 (May 1992), 25--50.
[58]
Nedialko S. Nedialkov, Kenneth R. Jackson, and George F. Corliss. 1999. Validated solutions of initial value problems for ordinary differential equations. Appl. Math. Comput. 105, 1 (1999), 21--68.
[59]
Markus Neher, Kenneth R. Jackson, and Nedialko S. Nedialkov. 2007. On Taylor model based integration of ODEs. SIAM J. Numerical Analysis 45, 1 (2007), 236--262.
[60]
Jens Oehlerking and Oliver E. Theel. 2009. A decompositional proof scheme for automated convergence proofs of stochastic hybrid systems. In Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14--16, 2009. Proceedings (Lecture Notes in Computer Science), Zhiming Liu and Anders P. Ravn (Eds.), Vol. 5799. Springer, 151--165.
[61]
André Platzer and Edmund M. Clarke. 2007. The image computation problem in hybrid systems model checking. In Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3--5, 2007, Proceedings (Lecture Notes in Computer Science), Alberto Bemporad, Antonio Bicchi, and Giorgio C. Buttazzo (Eds.), Vol. 4416. Springer, 473--486.
[62]
Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, and Geir Dullerud. 2015. A decidable class of planar linear hybrid systems. Theoretical Computer Science 574, Supplement C (2015), 1 -- 17.
[63]
Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2007. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Automat. Contr. 52, 8 (2007), 1415--1428.
[64]
Anuj Puri. 1998. Dynamical properties of timed automata (Lecture Notes in Computer Science), Anders P. Ravn and Hans Rischel (Eds.), Vol. 1486. Springer, 210--227.
[65]
Anuj Puri, Vivek Borkar, and Pravin Varaiya. 1996. ϵ-Approximation of differential inclusions. In Hybrid Systems III, Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 362--376.
[66]
Karin Quaas, Mahsa Shirmohammadi, and James Worrell. 2017. Revisiting reachability in timed automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20--23, 2017. IEEE Computer Society, 1--12.
[67]
Nacim Ramdani, Nacim Meslem, and Yves Candau. 2009. A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems. IEEE Trans. Automat. Contr. 54, 10 (2009), 2352--2364.
[68]
Nacim Ramdani and Nedialko S. Nedialkov. 2011. Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Analysis: Hybrid Systems 5, 2 (2011), 149 -- 162. Special Issue related to IFAC Conference on Analysis and Design of Hybrid Systems (ADHS09).
[69]
Stefan Ratschan. 2014. Safety verification of non-linear hybrid systems is quasi-decidable. Formal Methods in System Design 44, 1 (2014), 71--90.
[70]
Stefan Ratschan. 2017. Simulation based computation of certificates for safety of dynamical systems. In Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5--7, 2017, Proceedings (Lecture Notes in Computer Science), Alessandro Abate and Gilles Geeraerts (Eds.), Vol. 10419. Springer, 303--317.
[71]
Stefan Ratschan and Zhikun She. 2005. Safety verification of hybrid systems by constraint propagation based abstraction refinement. In Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9--11, 2005, Proceedings (Lecture Notes in Computer Science), Manfred Morari and Lothar Thiele (Eds.), Vol. 3414. Springer, 573--589.
[72]
Hao Ren and Ratnesh Kumar. 2015. Step simulation/overapproximation-based verification of nonlinear deterministic hybrid system with inputs. In 5th IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2015, Atlanta, GA, USA, October 14--16, 2015 (IFAC-PapersOnLine), Magnus Egerstedt and Yorai Wardi (Eds.), Vol. 48. Elsevier, 21--26.
[73]
Enric Rodríguez-Carbonell and Deepak Kapur. 2007. Generating all polynomial invariants in simple loops. J. Symb. Comput. 42, 4 (2007), 443--476.
[74]
Sriram Sankaranarayanan. 2011. Automatic abstraction of non-linear systems using change of bases transformations. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12--14, 2011, Marco Caccamo, Emilio Frazzoli, and Radu Grosu (Eds.). ACM, 143--152.
[75]
Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. 2004. Constructing invariants for hybrid systems. In Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25--27, 2004, Proceedings (Lecture Notes in Computer Science), Rajeev Alur and George J. Pappas (Eds.), Vol. 2993. Springer, 539--554.
[76]
Warren D. Smith. 2006. Church's thesis meets the N-body problem. Appl. Math. Comput. 178, 1 (2006), 154--183.
[77]
Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley.
[78]
Thomas Wilke. 1994. Automaten und Logiken zur Beschreibung zeitabhängiger Systeme. Ph.D. Dissertation. University of Kiel, Germany.
[79]
Ming Xu, Jiaqi Zhu, and Zhi-bin Li. 2013. Some decidable results on reachability of solvable systems. Int. J. General Systems 42, 4 (2013), 405--425.
[80]
Bai Xue. 2013. Computing Rigor Quadratic Lyapunov Functions and Under-approximate Reachable Sets for Ordinary Differential Equations. Ph.D. Dissertation. Beihang University.
[81]
Aditya Zutshi, Jyotirmoy V. Deshmukh, Sriram Sankaranarayanan, and James Kapinski. 2014. Multiple shooting, CEGAR-based falsification for hybrid systems. In 2014 International Conference on Embedded Software, EMSOFT 2014, New Delhi, India, October 12--17, 2014, Tulika Mitra and Jan Reineke (Eds.). ACM, 5:1--5:10.

Cited By

View all
  • (2024)A Reference Architecture of Human Cyber-Physical Systems – Part III: Semantic FoundationsACM Transactions on Cyber-Physical Systems10.1145/36228818:1(1-23)Online publication date: 14-Jan-2024
  • (2024)Reach-Avoid Verification Based on Convex OptimizationIEEE Transactions on Automatic Control10.1109/TAC.2023.327482169:1(598-605)Online publication date: Jan-2024
  • (2024)Towards Probabilistic Contracts for Intelligent Cyber-Physical SystemsLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_3(26-47)Online publication date: 27-Oct-2024
  • Show More Cited By
  1. In memory of Oded Maler: automatic reachability analysis of hybrid-state automata

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM SIGLOG News
    ACM SIGLOG News  Volume 6, Issue 1
    January 2019
    39 pages
    EISSN:2372-3491
    DOI:10.1145/3313909
    Issue’s Table of Contents

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 19 February 2019
    Published in SIGLOG Volume 6, Issue 1

    Check for updates

    Qualifiers

    • Research-article

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)11
    • Downloads (Last 6 weeks)1
    Reflects downloads up to 27 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2024)A Reference Architecture of Human Cyber-Physical Systems – Part III: Semantic FoundationsACM Transactions on Cyber-Physical Systems10.1145/36228818:1(1-23)Online publication date: 14-Jan-2024
    • (2024)Reach-Avoid Verification Based on Convex OptimizationIEEE Transactions on Automatic Control10.1109/TAC.2023.327482169:1(598-605)Online publication date: Jan-2024
    • (2024)Towards Probabilistic Contracts for Intelligent Cyber-Physical SystemsLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_3(26-47)Online publication date: 27-Oct-2024
    • (2024)Switching Controller Synthesis for Hybrid Systems Against STL FormulasFormal Methods10.1007/978-3-031-71177-0_15(229-247)Online publication date: 9-Sep-2024
    • (2023)Inner Approximating Robust Reach-Avoid Sets for Discrete-Time Polynomial Dynamical SystemsIEEE Transactions on Automatic Control10.1109/TAC.2022.321198268:8(4682-4694)Online publication date: Aug-2023
    • (2023)Safety guarantee for time-delay systems with disturbancesScience China Information Sciences10.1007/s11432-020-3266-666:3Online publication date: 18-Jan-2023
    • (2023)Verification of Quantum Systems Using Barrier CertificatesQuantitative Evaluation of Systems10.1007/978-3-031-43835-6_24(346-362)Online publication date: 20-Sep-2023
    • (2022)Encoding inductive invariants as barrier certificatesInformation and Computation10.1016/j.ic.2022.104965289:PAOnline publication date: 1-Nov-2022
    • (2021)Reach-Avoid Analysis for Delay Differential Equations2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9683555(1301-1307)Online publication date: 14-Dec-2021
    • (2021)Synthesizing Invariant Barrier Certificates via Difference-of-Convex ProgrammingComputer Aided Verification10.1007/978-3-030-81685-8_21(443-466)Online publication date: 20-Jul-2021
    • Show More Cited By

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media