Reachability Analysis of Hybrid Systemsan Experience Report
Manish Goyal · International Journal of Modeling and Optimization · 2012
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.