CISPA
Browse
cispa_all_3080.pdf (527.47 kB)

Synthesizing Approximate Implementations for Unrealizable Specifications

Download (527.47 kB)
conference contribution
posted on 2023-11-29, 18:12 authored by Rayna DimitrovaRayna Dimitrova, Bernd FinkbeinerBernd Finkbeiner, Hazem Torfah
The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automata-theoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative implementations from unrealizable specifications. Such implementations may violate the specification in general, but are guaranteed to satisfy the specification on at least a specified portion of the bounded-size lassos. We evaluate the algorithms on different arbiter specifications.

History

Preferred Citation

Rayna Dimitrova, Bernd Finkbeiner and Hazem Torfah. Synthesizing Approximate Implementations for Unrealizable Specifications. In: Computer Aided Verification (CAV). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date

2020-05-25

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3080, title = "Synthesizing Approximate Implementations for Unrealizable Specifications", author = "Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem", booktitle="{Computer Aided Verification (CAV)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC