Probabilistic synthesis against GR(1) winning condition

Reactive synthesis is a technique for automatic generation of a reactive system from a high level specification.The system is reactive in the sense that it reacts to the inputs from the environment.The specification is in general given as a linear temporal logic(LTL)formula.The behaviour of the system interacting with the environment can be represented as a game in which the system plays against the environment.Thus,a problem of reactive synthesis is commonly treated as solving such a game with the specification as the winning condition.Reactive synthesis has been thoroughly investigated for more two decades.A well-known challenge is to deal with the complex uncertainty of the environment.We understand that a major issue is due to the lack of a sufficient treatment of probabilistic properties in the traditional models.For example,a two-player game defined by a standard Kriple structure does not consider probabilistic transitions in reaction to the uncertain physical environment;and a Markov Decision Process(MDP)in general does not explicitly separate the system from its environment and it does not describe the interaction between system and the environment.In this paper,we propose a new and more general model which combines the two-player game and the MDP.Furthermore,we study probabilistic reactive synthesis for the games of General Reactivity of Rank 1(i.e.,GR(1))defined in this model.More specifically,we present an algorithm,which for given model,a location and a GR(1)specification,determines the strategy for each player how to maximize/minimize the probabilities of the satisfaction of at location.We use an example to describe the model of probabilistic games and demonstrate our algorithm.