  Storm water detention ponds are used to manage the discharge of rainfall
runoff from urban areas to nearby streams. Their purpose is to reduce the
hydraulic impact and sediment loads of the receiving waters. Detention ponds
are currently designed based on static controls: the output flow of a pond is
capped at a fixed value. This is not optimal with respect to the current
infrastructure capacity and for some detention ponds it might even violate
current regulations set by the European Water Framework Directive. We apply
formal methods to synthesize (i.e., derive automatically) a safe and optimal
active controller. We model the storm water detention pond, including the urban
catchment area and the rain forecasts, as a hybrid Markov decision process.
Subsequently, we use the tool Uppaal Stratego to synthesize a control strategy
minimizing the cost related to pollution (optimality) while guaranteeing no
emergency overflow of the detention pond (safety). Simulation results for an
existing pond show that Uppaal Stratego can learn optimal strategies that
prevent emergency overflows, where the current static control is not always
able to prevent it. At the same time, our approach can improve sedimentation
during low rain periods.
