Synthesising Features by Games

We describe an algorithmic method for the synthesis of features. The method takes as input a base system, a triggering condition for the feature, a set of system variables which the feature is allowed to update, and a requirement on the result of integrating it. It computes whether a feature of the given form and with the desired property exists and, if so, a construction of it. The method is based on the theory of infinite parity games.