Safety verification of hybrid systems by constraint propagation based abstraction refinement This paper deals with the problem of safety verification of non-linear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method into an abstraction refinement framework and improve it by developing an additional refinement step that employs constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allows switching conditions, initial states and unsafe states to be described by complex constraints instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented since it is based on a well-defined set of constraints, on which one can run any constraint propagation based solver. First tests of such an implementation are promising.

References in zbMATH (referenced in 25 articles , 1 standard article )

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

1 2 next

  1. Zhao, Hengjun; Zeng, Xia; Chen, Taolue; Liu, Zhiming; Woodcock, Jim: Learning safe neural network controllers with barrier certificates (2021)
  2. Yang, Zhengfeng; Wu, Min; Lin, Wang: An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems (2020)
  3. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  4. Zhang, Hui; Wu, Jinzhao: Formal verification and quantitative metrics of MPSoC data dynamics (2018)
  5. Dai, Liyun; Gan, Ting; Xia, Bican; Zhan, Naijun: Barrier certificates revisited (2017)
  6. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  7. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  8. Dzetkulič, Tomáš: Rigorous integration of non-linear ordinary differential equations in Chebyshev basis (2015)
  9. Lin, Wang; Wu, Min; Yang, Zhengfeng; Zeng, Zhenbing: Exact safety verification of hybrid systems using sums-of-squares representation (2014)
  10. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  11. Hiraishi, Kunihiko; Kobayashi, Koich: An approximation algorithm for box abstraction of transition systems on real state spaces (2013)
  12. She, Zhikun; Li, Haoyang; Xue, Bai; Zheng, Zhiming; Xia, Bican: Discovering polynomial Lyapunov functions for continuous dynamical systems (2013)
  13. Zhang, Lijun; She, Zhikun; Ratschan, Stefan; Hermanns, Holger; Hahn, Ernst Moritz: Safety verification for probabilistic hybrid systems (2012)
  14. Ramdani, Nacim; Nedialkov, Nedialko S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques (2011)
  15. Geuvers, Herman; Koprowski, Adam; Synek, Dan; van der Weegen, Eelis: Automated machine-checked hybrid system safety proofs (2010)
  16. Ratschan, Stefan; She, Zhikun: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions (2010)
  17. Akbarpour, Behzad; Paulson, Lawrence C.: Applications of \textttMetiTarskiin the verification of control and hybrid systems (2009)
  18. Plaku, Erion; Kavraki, Lydia E.; Vardi, Moshe Y.: Hybrid systems: From verification to falsification by combining motion planning and discrete search (2009)
  19. Sankaranarayanan, Sriram; Dang, Thao; Ivančić, Franjo: Symbolic model checking of hybrid systems using template polyhedra (2008)
  20. She, Zhikun; Zheng, Zhiming: Tightened reachability constraints for the verification of linear hybrid systems (2008)

1 2 next