Simple synthesis of reactive systems with tolerance for unexpected environmental behavior

During the synthesis of reactive systems, if we assume some behavioral property of an environment, any specification must include the environmental constraint in their conditions. In general, the behavior of a synthesized reactive system from such specifications only tends to satisfy the specification for the case where the environmental behavior follows these conditions; however, in a real-world setting it is desirable that the behavior of the reactive system satisfies the specification, even in the case of unexpected environmental behavior. We call tolerance for such a case environmental tolerance. In this paper, we give a simple definition of environmental tolerance, and propose a method for synthesizing a reactive system with environmental tolerance. In our method, the winning region of a safety game is computed using the Safraless synthesis method, and this is converted to a mean-payoff game such that a payoff is earned if the specification is satisfied. The optimal strategy for the game is then computed and the resulting reactive system is synthesized. The method is implemented and applied to specifications as an experiment, and it is confirmed that the obtained reactive systems have environmental tolerance.