Probabilistic synthesis against GR(1) winning condition

Abstract

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(1) 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.

Graphical abstract

Keywords

reactive system / probabilistic synthesis / GR(1)

References

[1] Pneuli A, Rosner R. On the synthesis of a reactive module. In: Proceedings of the 16th ACM International Colloquium. ICALP89, 1989, 179–190

[2] Wallmeier N, Hütten P, Thomas W. Symbolic synthesis of finite-state controllers for request-response specifications. In: Proceedings of the 8th International Conference on Implementation and Application of Automata. 2003, 113–22

[3] Alur R , Torre S L . Deterministic generators and games for LTL fragments. ACM Transactions on Computational Logic (TOCL), 2004, 5( 1): 1– 25

[4] Jobstmann B, Griesmayer A, Bloem R. Program repair as a game. In: Proceedings of the 17th International Conference on Computer Aided Verification. 2005, 226–238

[5] Harding A, Ryan M, Schobbens P Y. A new algorithm for strategy synthesis in LTL games. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 477–492

[6] Asarin E , Maler O , Pnueli A , Sifakis J . Controller synthesis for timed automata. IFAC Proceedings Volumes, 1998, 31( 18): 447– 452

[7] Bloem R , Jobstmann B , Piterman N , Pnueli A . Synthesis of reactive(1) designs. Journal of Computer and System Sciences, 2012, 78( 3): 911– 938

[8] Wasowski A , Dingel J , Rudie K . Controller synthesis for dynamic hierarchical real-time plants using timed automata. Discrete Event Dynamic Systems, 2017, 27( 12): 1– 35

[9] Shapley . Stochastic games. Proceedings of the National Academy of Sciences, 1953, 39( 10): 1095– 1100

[10] Chatterjee K, Henzinger T A, Jobstmann B. Environment assumptions for synthesis. In: Proceedings of the 19th International Conference on Concurrency Theory. 2008, 147–161

[11] Kwiatkowska M, Parker D. Automated verification and strategy synthesis for probabilistic systems. In: Proceedings of the 11th international Symposium, Automated Technology for Verification and Analysis. 2013, 53–22

[12] Neyman A, Sorin S. Stochastic games and applications. Kluwer Academic Publishers, 2003

[13] Nilim A , Ghaoui L . Robust control of markov decision processes with uncertain transition matrices. Operations Research, 2005, 53( 5): 780– 798

[14] Svoreňová M , Kwiatkowska M . Quantitative verification and strategy synthesis for stochastic games. European Journal of Control, 2016, 30 : 15– 30

[15] Chatterjee K, Jurdziński M, Henzinger T A. Simple stochastic parity games. In: Proceedings of the 12th International Workshop on Computer Science Logic. 2003, 100–113

[16] Buchi J R, Landweber L H. Solving Sequential Conditions by Finite-State Strategies. New York, Springer, 1990

[17] Alur R , Moarref S , Topcu U . Counter-strategy guided refinement of GR(1) temporal logic specifications. Formal Methods in Computer-Aided Design, 2013, 26– 33

[18] Koenighofer R , Hofferek G , Bloem R . Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. International Journal on Software Tools for Technology Transfer, 2013, 15( 5–6): 563– 583

[19] Kuvent A, Maoz S, Ringert J O. A symbolic justice violations transition system for unrealizable GR(1) specifications. In: Proceedings of the 11th Joint Meeting on Foundations of Software Engineering. 2017, 362–372

[20] Maoz S, Ringert J O, Shalom R. Symbolic repairs for GR (1) specifications. In: Proceedings of the 41st International Conference on Software Engineering (ICSE). 2019, 1016–1026

[21] Alfaro L D , Henzinger T A , Kupferman O . Concurrent reachability games. Theoretical Computer Science, 2007, 386( 3): 188– 217

[22] Emerson E A. Temporal and Modal Logic. Elsevier and MIT Press, 1990, 995–1072

[23] Baier C, Katoen J P. Principles of model checking. MIT Press, 2008

[24] Kesten Y, Piterman N, Pnueli A. Bridging the gap between fair simulation and trace inclusion. In: Proceedings of the 15th International Conference Computer Aided Verification. 2003, 381–393

RIGHTS & PERMISSIONS

Higher Education Press