Hybrid Systems in TLA+

In the early 90s, hybrid systems became a fashionable topic in formal methods. Theoreticians typically respond to a new problem domain by inventing new formalisms. Physicists don’t have to revise the theory of differential equations every time they study a new kind of system, and computer scientists shouldn’t have to change their formalisms when they encounter a new kind of system. Abadi and I showed in [106] that TLA can handle real-time specifications by simply introducing a variable to represent the current time. It’s just as obvious that it can handle hybrid systems by introducing variables to represent other physical quantities. It is often necessary to demonstrate the obvious to people, and the opportunity to do this arose when there was a workshop in Denmark devoted to a toy problem of specifying a simple gas burner and proving the correctness of a simple implementation. I was unable to attend the workshop, but I did write this TLA+ solution. (The version of TLA+ used here is slightly different from the more current version that is described in [127].)

The correctness conditions given in the problem statement included an ad hoc set of rules about how long the gas could be on if the flame was off. The purpose of those conditions was obviously to prevent a dangerous build-up of unburned gas. To demonstrate the power of TLA+, and because it made the problem more fun, I wrote a higher-level requirement stating that the concentration of gas should be less than a certain value. Assuming that the dissipation of unburned gas satisfied a simple differential equation, I proved that their conditions implied my higher-level specification–under suitable assumptions about the rate of diffusion of the gas. This required, among other things, formally specifying the Riemann integral, which took about 15 lines. I also sketched a proof of the correctness of the next implementation level. All of this was done completely in TLA+. The introduction to the volume says that I “extend[ed] … TLA+ with explicit variables that denote continuous states and clocks.” That, of course, is nonsense. Apparently, by their logic, you have extended C if you write a C program with variables named time and flame instead of t and f.