Hybrid automata models can capture observed phenomena in protein networks: the protein concentration dynamics inside each cell are modeled using linear differential equations; inputs activate or deactivate these continuous dynamics through discrete switches, which themselves are controlled by protein concentrations reaching given thresholds. The compelling reason to adopt this paradigm is that we are now capable of performing completely symbolic computation on certain classes of hybrid automata. That is, instead of numerical parameters, we can compute symbolic ranges for parameters such as switching thresholds and chemical rates necessary for a given process. More importantly, we are able to compute symbolic reachable sets for experimentally observed biological steady states. This gives us a set of the initial conditions (i.e. protein concentration/activation levels) that leads to a particular steady state, which can be used to predict which initial conditions will lead to that steady state, and to suggest experiments to study those.