Hyrose: A symbolic simulator of the hybrid constraint language HydLa

Hybrid systems are dynamical systems with continuous changes of states and discrete changes of states and governing equations. Hybrid systems are appliable to diverse fields including physics. HydLa is a declarative language for describing hybrid systems using constraints, and we have developed a symbolic simulator of HydLa named Hyrose. Hyrose is our first publicly available implementation of HydLa. Features of Hyrose include the simulation of systems with parameters, search based on automatic case analysis and bounded model checking. In this paper, we first describe the architecture and features of Hyrose, as well as semantical issues that had to be clarified to implement Hyrose. Then, in order to demonstrate the power of symbolic execution, we show several examples of the analysis of systems whose behavior exhibits quantitative and qualitative changes depending on parameters.