A New Algorithm for Strategy Synthesis in LTL Games

Research output: Contribution to journalArticlepeer-review

Standard

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

In: Lecture Notes in Computer Science, Vol. 3440, 01.01.2005, p. 477-492.

Research output: Contribution to journalArticlepeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{778b9e5dd8544f508b8bc02968c746a2,
title = "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 2EXPTIME-complete complexity of the problem, and the intricate nature of Pnueli and Rosner{\textquoteright}s solution. A key difficulty in their procedure is the determinisation of B{\"u}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.",
author = "Aidan Harding and Mark Ryan and P-Y Schobbens",
year = "2005",
month = jan,
day = "1",
doi = "10.1007/978-3-540-31980-1_31",
language = "English",
volume = "3440",
pages = "477--492",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer",
note = "Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05) ; Conference date: 01-01-2005",

}

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 -