We address the problem of modeling andanalyzing the flexible behavior of Pro-sumer systems for the purpose of balanc-ing production and consumption of en-ergy in, for example, an energy grid. Weintroduce the notion of Resource TimedAutomata (RTA) and show how pro-sumers can be modeled using these au-tomata. Furthermore, we show that ag-geregation of prosumers in a smart elec-tricity grid can be modeled as a specialkind of parallel composition of such au-tomata, and the balancing problem canbe formalized as reachability problems onan observer automaton. Finally, we illus-trate how these reachability problems canbe solved using established methods frommodel checking, and discuss why we sus-pect these methods will scale well in prac-tice for this type of problem.