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 M,a location s and a GR(l)specification P,determines the strategy for each player how to maximize/minimize the probabilities of the satisfaction of P at location s.We use an example to describe the model of probabilistic games and demonstrate our algorithm.

Wei ZHAO;Rui LI;Wanwei LIU;Wei DONG;Zhiming LIU

College of Computer Science&Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;College of Computer&Information Science,Southwest University,Chongqing 400715,China;School of Computer,National University of Defense Technology,Changsha 410073,China

计算机科学前沿

[1]Wei ZHAO;Rui LI;Wanwei LIU;Wei DONG;Zhiming LIU-.Probabilistic synthesis against GR(1)winning condition)[J].计算机科学前沿,2022(02):16-24

Kriple

Probabilistic,synthesis,against,GR,winning,condition,Reactive,technique,automatic,generation,reactive,system,from,high,level,specification,sense,that,reacts,inputs,environment,general,given,linear,temporal,logic,LTL,formula,behaviour,interacting,can,represented,which,plays,Thus,problem,commonly,treated,solving,such,has,been,thoroughly,investigated,two,decades,well,known,challenge,deal,complex,uncertainty,We,understand,major,issue,due,lack,sufficient,treatment,probabilistic,properties,traditional,models,For,example,player,defined,by,standard,structure,does,not,consider,transitions,reaction,physical,Markov,Decision,Process,MDP,explicitly,separate,its,describe,interaction,between,In,this,paper,propose,new,combines,Furthermore,study,games,General,Reactivity,Rank,More,specifically,algorithm,location,determines,strategy,each,how,maximize,minimize,probabilities,satisfaction,use,demonstrate

0.499506