A Symbolic Algorithm for Lazy Synthesis of Eager Strategies
| Autor: | Swen Jacobs, Mouhammad Sakr |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Set (abstract data type)
0209 industrial biotechnology 020901 industrial engineering & automation Theoretical computer science Computer science Reactive synthesis 0202 electrical engineering electronic engineering information engineering Benchmark (computing) State space 020207 software engineering 02 engineering and technology Symbolic algorithm Representation (mathematics) |
| Zdroj: | Automated Technology for Verification and Analysis ISBN: 9783030010898 ATVA |
| DOI: | 10.1007/978-3-030-01090-4_13 |
| Popis: | We present an algorithm for solving two-player safety games that combines a mixed forward/backward search strategy with a symbolic representation of the state space. By combining forward and backward exploration, our algorithm can synthesize strategies that are eager in the sense that they try to prevent progress towards the error states as soon as possible, whereas standard backwards algorithms often produce permissive solutions that only react when absolutely necessary. We provide experimental results for two new sets of benchmarks, as well as the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017. The results show that our algorithm in many cases produces more eager strategies than a standard backwards algorithm, and solves a number of benchmarks that are intractable for existing tools. Finally, we observe a connection between our algorithm and a recently proposed algorithm for the synthesis of controllers that are robust against disturbances, pointing to possible future applications. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|