We address the problem of modeling and
analyzing 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. We
introduce the notion of Resource Timed
Automata (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 special
kind of parallel composition of such au-
tomata, and the balancing problem can
be formalized as reachability problems on
an observer automaton. Finally, we illus-
trate how these reachability problems can
be solved using established methods from
model checking, and discuss why we sus-
pect these methods will scale well in prac-
tice for this type of problem.