# A New Algorithm for Strategy Synthesis in LTL Games

Research output: Contribution to journal › Article › peer-review

## Standard

**A New Algorithm for Strategy Synthesis in LTL Games.** / Harding, Aidan; Ryan, Mark; Schobbens, P-Y.

Research output: Contribution to journal › Article › peer-review

## Harvard

*Lecture Notes in Computer Science*, vol. 3440, pp. 477-492. https://doi.org/10.1007/978-3-540-31980-1_31

## APA

*Lecture Notes in Computer Science*,

*3440*, 477-492. https://doi.org/10.1007/978-3-540-31980-1_31

## Vancouver

## Author

## Bibtex

}

## RIS

TY - JOUR

T1 - A New Algorithm for Strategy Synthesis in LTL Games

AU - Harding, Aidan

AU - Ryan, Mark

AU - Schobbens, P-Y

PY - 2005/1/1

Y1 - 2005/1/1

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-31980-1_31

DO - 10.1007/978-3-540-31980-1_31

M3 - Article

VL - 3440

SP - 477

EP - 492

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

T2 - Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05)

Y2 - 1 January 2005

ER -