Designing controllers for reachability

We propose a deductive method for constructing reliable reachability controllers, with application to fault-tolerant discrete systems. Designing the controller reduces to finding a strategy to win specific games defined by sequential angelic and demonic nondeterministic statements. During the game, the plant (the demon) tries to prevent the controller (the angel) from achieving its respective goal, modeled by a special kind of liveness property. We show that the angel has a way to enforce the required property, provided that adequate invariance and termination properties hold. The control strategy is obtained by propagating certain assertions into the angelic statement. We illustrate our method on a data-processing application.