A New Algorithm for Strategy Synthesis in LTL Games

Aidan Harding, Mark Ryan, P-Y Schobbens

Research output: Contribution to journalArticlepeer-review

25 Citations (Scopus)


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 2EXPTIME-complete 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üchi 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 singly exponential. Our solution, however, is not complete; we prove a condition which guarantees completeness and argue by empirical evidence that examples for which it is not complete are rare enough to make our solution a useful tool.
Original languageEnglish
Pages (from-to)477-492
Number of pages16
JournalLecture Notes in Computer Science
Publication statusPublished - 1 Jan 2005
EventEleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05) -
Duration: 1 Jan 2005 → …


Dive into the research topics of 'A New Algorithm for Strategy Synthesis in LTL Games'. Together they form a unique fingerprint.

Cite this