A New Algorithm for Strategy Synthesis in LTL Games

Abstract. The automatic synthesis of programs from their specifications has been a dream of many researchers for decades. If we restrict to open finite-state reactive systems, the specification is often presented as an ATL or LTL formula interpreted over a finite-state game. The required program is then a strategy for winning this game. A theoretically optimal solution to this problem was proposed by Pnueli and Rosner, but has never given good results in practice. This is due to the 2EXPTIMEcomplete complexity of the problem, and the intricate nature of Pnueli and Rosner’s solution. A key difficulty in their procedure is the determinisation of B¨uchi automata. In this paper we look at an alternative approach which avoids determinisation, using instead a procedure that is amenable to symbolic methods. Using an implementation based on the BDD package CuDD, we demonstrate its scalability in a number of examples. Furthermore, we show a class of problems for which our algorithm is si...

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Aidan Harding, Mark Ryan, Pierre-Yves Schobbens
• Keywords: Algorithms, Bdd Package Cudd, Rosner’s Solution, TACAS 2005, finite-state Reactive Systems