CISPA
Browse

Explainable Reactive Synthesis

Download (520.28 kB)
conference contribution
posted on 2023-11-29, 18:15 authored by Tom BaumeisterTom Baumeister, Bernd FinkbeinerBernd Finkbeiner, Hazem Torfah
Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. The main advantage of synthesis is that it is automatic. The main disadvantage is that the implementation is usually very difficult to understand. In this paper, we present a new synthesis process that explains the synthesized implementation to the user. The process starts with a simple version of the specification and a corresponding simple implementation. Then, desired properties are added one by one, and the corresponding transformations, repairing the implementation, are explained in terms of counterexample traces. We present SAT-based algorithms for the synthesis of repairs and explanations. The algorithms are evaluated on a range of examples including benchmarks taken from the SYNTCOMP competition.

History

Preferred Citation

Tom Baumeister, Bernd Finkbeiner and Hazem Torfah. Explainable Reactive Synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

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

Legacy Posted Date

2021-03-04

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3380, title = "Explainable Reactive Synthesis", author = "Baumeister, Tom and Finkbeiner, Bernd and Torfah, Hazem", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC