Strategy Representation by Decision Trees in Reactive Synthesis

D 2018

Strategy Representation by Decision Trees in Reactive Synthesis

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Jan KŘETÍNSKÝ and Viktor TOMAN

Basic information

Original name

Strategy Representation by Decision Trees in Reactive Synthesis

Authors

BRÁZDIL, Tomáš (203 Czech Republic, guarantor, belonging to the institution), Krishnendu CHATTERJEE (356 India), Jan KŘETÍNSKÝ (203 Czech Republic) and Viktor TOMAN (703 Slovakia)

Edition

Cham, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), p. 385-407, 23 pp. 2018

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/18:00118582

Organization unit

Faculty of Informatics

ISBN

978-3-319-89959-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-89960-2_21

UT WoS

000546326300021

Keywords in English

INFINITE GAMES; AUTOMATA

Abstract

V originále

Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with w-regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.

Citovat

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Jan KŘETÍNSKÝ and Viktor TOMAN. Strategy Representation by Decision Trees in Reactive Synthesis. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018). Cham: Springer, 2018, p. 385-407. ISBN 978-3-319-89959-6. Available from: https://dx.doi.org/10.1007/978-3-319-89960-2_21.

@inproceedings{1768257,
   author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Křetínský, Jan and Toman, Viktor},
   address = {Cham},
   booktitle = {24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)},
   doi = {http://dx.doi.org/10.1007/978-3-319-89960-2_21},
   keywords = {INFINITE GAMES; AUTOMATA},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-319-89959-6},
   pages = {385-407},
   publisher = {Springer},
   title = {Strategy Representation by Decision Trees in Reactive Synthesis},
   year = {2018}
}

TY  - JOUR
ID  - 1768257
AU  - Brázdil, Tomáš - Chatterjee, Krishnendu - Křetínský, Jan - Toman, Viktor
PY  - 2018
TI  - Strategy Representation by Decision Trees in Reactive Synthesis
PB  - Springer
CY  - Cham
SN  - 9783319899596
KW  - INFINITE GAMES
KW  - AUTOMATA
N2  - Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with w-regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.
ER  -

BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Jan KŘETÍNSKÝ and Viktor TOMAN. Strategy Representation by Decision Trees in Reactive Synthesis. In \textit{24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)}. Cham: Springer, 2018, p.~385-407. ISBN~978-3-319-89959-6. Available from: https://dx.doi.org/10.1007/978-3-319-89960-2\_{}21.

Detailed Information on Publication Record