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 classes of crafted benchmarks, the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017, as well as a set of randomly generated benchmarks. 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.
History
Preferred Citation
Swen Jacobs and Mouhammad Sakr. A symbolic algorithm for lazy synthesis of eager strategies. In: Acta Informatica. 2019.
Primary Research Area
Reliable Security Guarantees
Legacy Posted Date
2019-11-17
Journal
Acta Informatica
Open Access Type
Green
Sub Type
Article
BibTeX
@article{cispa_all_2973,
title = "A symbolic algorithm for lazy synthesis of eager strategies",
author = "Jacobs, Swen and Sakr, Mouhammad",
journal="{Acta Informatica}",
year="2019",
}