Abstract
Parity games play an important role for LTL synthesis as evidenced by recent breakthroughs on LTL synthesis, which rely in part on parity game solving. Yet state space explosion remains a major issue if we want to scale to larger systems or specifications. In order to combat this problem, we need to investigate symbolic methods such as BDDs, which have been successful in the past to tackle exponentially large systems. It is therefore essential to have symbolic parity game solving algorithms, operating using BDDs, that are fast and that can produce the winning strategies used to synthesize the controller in LTL synthesis.
Current symbolic parity game solving algorithms do not yield winning strategies. We now propose two symbolic algorithms that yield winning strategies, based on two recently proposed fixpoint algorithms. We implement the algorithms and empirically evaluate them using benchmarks obtained from SYNTCOMP 2020. Our conclusion is that the algorithms are competitive with or faster than an
earlier symbolic implementation of Zielonka’s recursive algorithm, while also providing the winning strategies.
Current symbolic parity game solving algorithms do not yield winning strategies. We now propose two symbolic algorithms that yield winning strategies, based on two recently proposed fixpoint algorithms. We implement the algorithms and empirically evaluate them using benchmarks obtained from SYNTCOMP 2020. Our conclusion is that the algorithms are competitive with or faster than an
earlier symbolic implementation of Zielonka’s recursive algorithm, while also providing the winning strategies.
Original language | English |
---|---|
Title of host publication | Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification |
Subtitle of host publication | Brussels, Belgium, September 21-22, 2020 |
Editors | Jean-Francois Raskin, Davide Bresolin |
Place of Publication | Waterloo, NSW |
Publisher | Open Publishing Association |
Pages | 18-32 |
DOIs | |
Publication status | Published - 22 Sept 2020 |
Event | 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020 - Online Duration: 21 Sept 2020 → 23 Sept 2020 Conference number: 11 http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=100226©ownerid=55210 |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science |
---|---|
Publisher | Open Publishing Association |
Volume | 326 |
ISSN (Electronic) | 2075-2180 |
Conference
Conference | 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020 |
---|---|
Abbreviated title | GandALF |
Period | 21/09/20 → 23/09/20 |
Internet address |