SpaceEx State Space Explorer

Will Lake Mead go dry? An introduction to hybrid automata and reachability

The water level of the Lake Mead/Lake Powell system is decreasing every year, and it could completely dry up with the next two decades (cf. Barnett and Pierce. When will Lake Mead run dry? J. Water Resources Research, 2008). This exercise takes a (grossly simplified) look at the problem and compares a worst-case estimate based on constant rates with an estimate based on a hybrid model with switching rates. For solutions and model files, see here.

Lake Mead is fed by the Colorado River at an average rate of rin=15 million acre feet per year (maf/yr), a figure which is expected to decrease by up to 30% over a time span of tdec=50 years. Water is taken out of the lake at a rate of 14 maf/yr, plus 1.7 maf/yr due to evaporation and infiltration, resulting in a constant loss of rout=15.7 maf/yr.

Constant Rate Model

Let x be the water level. As of June 2007, the reservoir contains xini=25.7 maf. For conservative estimate, assume that the fill rate can be anywhere between today’s rate rin, and its predicted reduced value of 70% of rin. The net rate is therefore :

(1) 0.7rin - rout ≤ x' ≤ rin-rout

This constraint belongs to the general class of linear differential inclusions, which are conjunctions of constraints of the form :

(2) a1x1' + a2x2' + . . . + anxn' ≤ b, 

where the xare real-valued variables and the ai are real-valued constants. Equalities can be captured in this form by using two inequalities, one of them having both sides multiplied with -1. The xi are referred to as continuous variables since they change continuously over time. Continuous dynamics of this form are referred to as piecewise constant dynamics (PCD). Hybrid automata with these dynamics are called Linear Hybrid Automata, or LHA for short.

Model this system with an automaton that has a single location and no transitions. Use (1) as flow equation, and impose the invariant:

(3) x ≥ 0

to restrict the model to behaviors in which the lake level is nonnegative. To measure time elapse, introduce a variable t with rate:

(4) t’ = 1. 

Compute the reachable states of this system, starting from the initial states :

(5) x = 25.7

a)  In what time frame could Lake Mead be dry according to this model? What is the largest reachable value of t, and why is it finite?

Switched Rate Model

Let’s make a more precise model in order to get a better estimate than with the assumption of a constant feed. The feed from the Colorado River varies strongly with the seasons, see here for tables from 1906 to 2006. In the rainy season, April to June, rin,r=30 maf/yr, while in the rest of the year, dry season, rin,d=10 maf/yr. This variation in feed causes a corresponding seasonal variation in Lake Mead's water level, so Lake Mead might actually dry up sooner than the constant-rate estimate suggests.

We now construct a hybrid automaton model that includes the seasonal switch in dynamics. For clarity, we proceed systematically without trying to minimize the number of variables or locations used.

Introduce a location each for the dry and the rainy season. In each location the dynamics are given by a differential inclusion, which models the net rate to be in the interval between today's rate and the rate with inflow reduced to 70%:

(6) 0.7rin,r - rout ≤ x' ≤ rin,r - rout

(7) 0.7rin,d - rout ≤ x' ≤ rin,d - rout

Since the change of season depends on the time of year, introduce another clock variable c, i.e., a variable with

(8) c’ = 1/yr.

The system may remain in location “dry” only during the first nine months, so as long as

(9) c ≤ 9/12. 

Similarly, it may remain in location “rainy” until the last month of the year, which means

(10) c ≤ 12/12.

Include (9) in the invariant of location “dry” and (10) in the invariant of location “rainy”. Model the change from dry to rainy season with a transition from location “dry” to location “rainy” with label “rd” and whose guard is

(11) c ≥ 9/12. 

Guard and invariant of location “dry” overlap only on c=9/12. Since the derivative c’ ≠ 0, c takes this value only at a single instant in time, and the system transitions immediately from dry to rainy when the clock reaches this boundary.

Model the change from rainy to dry season with a similar transition “dr”, except that it resets the clock c to zero in order to restart the cycle when a full year has elapsed. This reset is denoted with the assignment

(12) c' = 0.

Note that the prime (as in c’) in a transition assignment denotes the new value of a variable after the transition, not its derivative.

b)   In what time frame could Lake Mead be dry according to this model?

c)  At what values of t can transition rd take place?

d)  How can one model the transition from dry to rainy without a guard?

 Computing the image of a reset like c’=0 is quite costly, as it corresponds to existential quantification over the old value of c, and then adding c=0 as a new constraint. Existential quantification is of exponential complexity in the number of variables for sets of linear constraints. Resets belong to the more general class of affine assignments, which have the form

(13) x' = ax + b. 

Affine assignments are called resets (or singular) if a = 0 and regular if a ≠ 0. The image of regular assignments can be computed by substituting x with a-1(x’-b), which is of only cubic complexity, and therefore much easier to compute.

e)  How can one model the transition from rainy to dry with a regular affine assignment instead of a reset?


Model with Affine Continuous Dynamics

In the LHA model of Lake Mead, we assumed that the feed of the Colorado river has a constant lower bound corresponding to a feed rate rin reduced by 30%. In their report, Barnett and Pierce assume that the reduction actually takes place gradually over tdec=50 years. Let’s refine the estimate by replacing the constant rate rin with a new continuous variable v that decreases linearly over time so that it is reduced by 30% after tdec years:

(14) x' = v - rout

(15) v' = -0.3 rin / tdec

Note that (14) is not a constant bound differential inclusion, since the derivative of x depends on another continuous variable, v. The resulting hybrid automaton is not a LHA, but called a piecewise affine automaton.

Create a piecewise affine model of the Lake Mead water level: Copy the automaton of the switched rate model and modify its dynamics according to (14) and (15), using rin,r or rin,d according to the location.

f)  In what time frame could Lake Mead be dry according to this model?


In their study, Barnett and Pierce use probabilistic instead of worst-case estimates, and of course their analysis is infinitely more sophisticated than the models used in this exercise. Based on this analysis, Barnett and Pierce conclude that there is a 10% chance that Lake Mead could be dry in 2013, and a 50% chance that it is dry by 2021. There will be chances for vacationing at beautiful Lake Mead for a little while longer.


For solutions and model files, see here.