A New Algorithm for Strategy Synthesis in LTL Games

Research output: Contribution to journalArticlepeer-review

Authors

Colleges, School and Institutes

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

Details

Original languageEnglish
Pages (from-to)477-492
Number of pages16
JournalLecture Notes in Computer Science
Volume3440
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 → …