Contracts and games in controller synthesis for discrete systems

This study proposes a method for constructing reliable controllers for arbitrarily large discrete systems. The controller is synthesized by finding a winning strategy for specific games defined by contracts. The discrete system model is an action system, and the requirement is a temporal property. We use the extended action system notation that allows both angelic and demonic nondeterminism, such that the game reduces to a competition between the angel, that is, the controller, and the demon, that is, the plant, which try to prevent each other from achieving their respective goals. If the synthesis is possible, that is, if the angel has a way to enforce the required property, the process ends with finding the winning strategy of the angel, by propagating backwards the computed precondition of the demon, with respect to that property. This technique guarantees the correctness of the derived program. We illustrate our method on a producer-consumer application.