Simulation and verification of hybrid systems using Chi

The hybrid Χ (Chi) formalism integrates concepts from dynamics and control theory with concepts from computer science. It integrates ease of modeling with a straightforward, structured operational semantics based on S-functions. Both simulators are defined in terms of a so-called stepper, which computes the set of possible transitions for given a Χ process. The stepper consists of three main functions: a function, Sa which returns the set of action steps for given a Χ process, a function Sd which returns the set of time steps for given a Χ process, and a function Tr which returns the reduced set of transitions. Action steps and time steps can be seen as symbolic transitions. They contain all information that is needed to determine the transitions that the process from which they are derived can perform without solving predicates. An action step represents zero or more action transitions and a time step represents zero or more time transitions.