SpaceEx

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 spaceex.imag.fr. 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 25 articles )

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

1 2 next

  1. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  2. 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)
  3. Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
  4. Hagemann, Willem: Efficient geometric operations on convex polyhedra, with an application to reachability analysis of hybrid systems (2015)
  5. Matsumoto, Shota; Kono, Fumihiko; Kobayashi, Teruya; Ueda, Kazunori: HyLaGi: symbolic implementation of a hybrid constraint language HydLa (2015) ioport
  6. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  7. Casagrande, A.; Dreossi, T.; Fabriková, J.; Piazza, C.: $\epsilon$-semantics computations on biological systems (2014)
  8. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  9. Minopoli, Stefano; Frehse, Goran: Non-convex invariants and urgency conditions on linear hybrid automata (2014)
  10. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014) ioport
  11. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  12. Zamani, Majid; Abate, Alessandro: Approximately bisimilar symbolic models for randomly switched stochastic systems (2014)
  13. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  14. Mitchell, Ian M.; Kaynama, Shahab; Chen, Mo; Oishi, Meeko: Safety preserving control synthesis for sampled data systems (2013)
  15. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2013)
  16. Seladji, Yassamine; Bouissou, Olivier: Fixpoint computation in the polyhedra abstract domain using convex and numerical analysis tools (2013)
  17. Testylier, Romain; Dang, Thao: NLTOOLBOX: a library for reachability computation of nonlinear dynamical systems (2013)
  18. Ben Sassi, Mohamed Amin; Testylier, Romain; Dang, Thao; Girard, Antoine: Reachability analysis of polynomial systems using linear programming relaxations (2012)
  19. Goubault, Eric; Le Gall, Tristan; Putot, Sylvie: An accurate join for zonotopes, preserving affine input/output relations (2012)
  20. Johnson, Taylor T.; Green, Jeremy; Mitra, Sayan; Dudley, Rachel; Erwin, Richard Scott: Satellite rendezvous and conjunction avoidance: case studies in verification of nonlinear hybrid systems (2012)

1 2 next


Further publications can be found at: http://spaceex.imag.fr/documentation/publications