Ghosts & Differential Ghosts

Synopsis

While working toward yet another fundamental reasoning technique for differential equations, this chapter describes somewhat surprising uses of additional auxiliary variables, called ghosts, in the modeling of and reasoning about cyberphysical systems. A discrete ghost is an extra variable introduced with an assignment into the proof (or model) for the sake of analyzing the model. A differential ghost is an extra variable that is added into the dynamics of a system with a quite arbitrarily made-up differential equation for the purposes of analyzing the system. What might at first sound counterproductive, because it increases the dimension of the system, will, upon closer inspection, turn out to be helpful for proving purposes, because the differential ghost variables provide additional quantities relative to whose (arbitrarily chosen) continuous evolution the behavior of the system can be understood. With a clever choice of the new differential equations for the differential ghosts, it can also become easier to understand the evolution of the original variables, because there is something else to relate to. Differential ghosts can make quite a surprising difference in our understanding of differential equations and can even explain how differential equations can be solved as part of an ordinary differential invariants proof.