SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.

References in zbMATH (referenced in 37 articles )

Showing results 1 to 20 of 37.
Sorted by year (citations)

1 2 next

  1. Benerecetti, Massimo; Faella, Marco: Tracking smooth trajectories in linear hybrid systems (2017)
  2. Djaballah, Adel; Chapoutot, Alexandre; Kieffer, Michel; Bouissou, Olivier: Construction of parametric barrier functions for dynamical systems using interval analysis (2017)
  3. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  4. Tran, Hoang-Dung; Nguyen, Luan Viet; Xiang, Weiming; Johnson, Taylor T.: Order-reduction abstractions for safety verification of high-dimensional linear systems (2017)
  5. Bak, Stanley; Bogomolov, Sergiy; Henzinger, Thomas A.; Johnson, Taylor T.; Prakash, Pradyot: Scalable static hybridization methods for analysis of nonlinear systems (2016)
  6. Konečný, Michal; Taha, Walid; Bartha, Ferenc A.; Duracz, Jan; Duracz, Adam; Ames, Aaron D.: Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point (2016)
  7. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  8. Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
  9. Bak, Stanley; Bogomolov, Sergiy; Johnson, Taylor T.: HYST: a source transformation and translation tool for hybrid automaton models (2015)
  10. Frehse, Goran; Bogomolov, Sergiy; Greitschus, Marius; Strump, Thomas; Podelski, Andreas: Eliminating spurious transitions in reachability with support functions (2015)
  11. Hagemann, Willem: Efficient geometric operations on convex polyhedra, with an application to reachability analysis of hybrid systems (2015)
  12. Lesser, Kendra; Oishi, Meeko: Finite state approximation for verification of partially observable stochastic hybrid systems (2015)
  13. Matsumoto, Shota; Kono, Fumihiko; Kobayashi, Teruya; Ueda, Kazunori: HyLaGi: symbolic implementation of a hybrid constraint language HydLa (2015) ioport
  14. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  15. Bogomolov, Sergiy; Herrera, Christian; Muñiz, Marco; Westphal, Bernd; Podelski, Andreas: Quasi-dependent variables in hybrid automata (2014)
  16. Casagrande, A.; Dreossi, T.; Fabriková, J.; Piazza, C.: $\epsilon$-semantics computations on biological systems (2014)
  17. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  18. Liberzon, Daniel: Finite data-rate feedback stabilization of switched and hybrid linear systems (2014)
  19. Minopoli, Stefano; Frehse, Goran: Non-convex invariants and urgency conditions on linear hybrid automata (2014)
  20. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014) ioport

1 2 next

Further publications can be found at: