Name
Abstract | ||
|---|---|---|
Two-player games are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This requires keeping track of all discovered winning states and can lead to space explosion even when using efficient symbolic representations. We propose a new method for solving reachability games. Our method works by exploring a subset of the possible concrete runs of the game and proving that these runs can be generalised into a winning strategy on behalf of one of the players. We use counterexample-guided backtracking search to identify a subset of runs that are sufficient to consider to solve the game. We evaluate our algorithm on several families of benchmarks derived from real-world device driver synthesis problems. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-08867-9_35 | CAV |
Field | DocType | Volume |
Combinatorial game theory,Computer science,Algorithm,Reachability,Theoretical computer science,Artificial intelligence,Formalism (philosophy),Reactive system,Backtracking | Conference | 8559 |
ISSN | Citations | PageRank |
0302-9743 | 7 | 0.50 |
References | Authors | |
18 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nina Narodytska | 1 | 449 | 39.28 |
| Alexander Legg | 2 | 24 | 3.17 |
| Fahiem Bacchus | 3 | 7 | 0.50 |
| Leonid Ryzhyk | 4 | 212 | 16.05 |
| Adam Walker | 5 | 28 | 2.90 |