CISPA
Browse
cispa_all_2642.pdf (417.69 kB)

A Symbolic Algorithm for Lazy Synthesis of Eager Strategies

Download (417.69 kB)
conference contribution
posted on 2023-11-29, 18:08 authored by Swen JacobsSwen Jacobs, Mouhammad Sakr
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.

History

Preferred Citation

Swen Jacobs and Mouhammad Sakr. A Symbolic Algorithm for Lazy Synthesis of Eager Strategies. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2018.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2018-09-19

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_2642, title = "A Symbolic Algorithm for Lazy Synthesis of Eager Strategies", author = "Jacobs, Swen and Sakr, Mouhammad", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2018", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC