Residential thermostatically controlled loads (TCLs) have potential for participation in electricity markets. This is because we can control a large group of these loads to achieve aggregate system behavior such as providing frequency reserves while ensuring the control actions are non-disruptive to the end users. A main challenge in controlling aggregations of TCLs is developing dynamical system models that are simple enough for optimization and control, but rich enough to capture the behavior of the loads. In this work, we propose three classes of models that approximate aggregate TCL dynamics. We analyze these models in terms of their accuracy and computational tractability. The models demonstrate a progression from models that help us analyze and predict TCL population behavior to those that help us develop large-scale automatic control strategies. Specifically, we demonstrate how formal methods from computer science and optimal control can be used to derive bounds on model error, guarantees for trajectory tracking, and algorithms for price arbitrage. We find that the accuracy of the analytic results decreases as TCL parameter heterogeneity is introduced. Thus, we motivate further development of analytical tools and modeling approaches to investigate realistic TCL behavior in power systems.