Abstract—Hybrid systems are mathematical models of control systems whose safety verification is critical for many applications. In practice, a rigorous tool is still not available for verifying every class of hybrid systems. HyTech was the first attempt in this direction followed by PHaver, both restricted to Linear Hybrid Automata (LHA). HSolver is another successful contribution for verification of nonlinear systems. PHaver can efficiently verify safety properties with the help of piecewise constant bounds on derivatives. Its use is greatly motivated by on-the-fly over approximations of piecewise affine dynamics with various user-specified parameters. HSolver verifies safety of nonlinear systems using constraint propagation based abstraction refinement. We have evaluated a few examples and shown that both tools have their strengths and weaknesses. In all the examples, the approximation of nonlinear systems by linear systems is performed by the rate translation.
Index Terms—HSolver, Hybrid systems, rate translation, reachability analysis, PHAVer.
The author is with Indian Institute of Technology Guwahati, India. (e-mail: g.manish@alumni.iitg.ernet.in).
Cite: Manish Goyal, "Reachability Analysis of Hybrid Systems an Experience Report," International Journal of Modeling and Optimization vol. 2, no. 6, pp. 681-686, 2012.
Copyright © 2008-2024. International Journal of Modeling and Optimization. All rights reserved.
E-mail: ijmo@iacsitp.com