doi: 10.7763/IJMO.2012.V2.209
Reachability Analysis of Hybrid Systems an Experience Report
Manish Goyal
- Indian Institute of Technology Guwahati, India.
Abstract
Hybrid systems are mathematical models ofcontrol systems whose safety verification is critical for manyapplications. In practice, a rigorous tool is still not available forverifying every class of hybrid systems. HyTech was the firstattempt in this direction followed by PHaver, both restricted toLinear Hybrid Automata (LHA). HSolver is another successfulcontribution for verification of nonlinear systems. PHaver canefficiently verify safety properties with the help of piecewiseconstant bounds on derivatives. Its use is greatly motivated byon-the-fly over approximations of piecewise affine dynamics withvarious user-specified parameters. HSolver verifies safety ofnonlinear systems using constraint propagation based abstractionrefinement. We have evaluated a few examples and shown thatboth tools have their strengths and weaknesses. In all theexamples, the approximation of nonlinear systems by linearsystems is performed by the rate translation.
Keywords
- HSolver
- Hybrid systems
- rate translation
- reachability analysis
- PHAVer
How to 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. https://doi.org/ 10.7763/IJMO.2012.V2.209
Copyright & License
Copyright © 2012 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).