Synthesizing Approximate Implementations for Unrealizable Specifications

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

[img]
Preview
 Text
DFT19.pdf
Download (540kB) | Preview

Abstract

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.

Item Type: Conference or Workshop Item (A Paper) (Paper)
Conference: CAV Computer Aided Verification
Depositing User: Bernd Finkbeiner
Date Deposited: 25 May 2020 11:42
Last Modified: 11 May 2021 13:47
Primary Research Area: NRA2: Reliable Security Guarantees
URI: https://publications.cispa.saarland/id/eprint/3080

Actions

Actions (login required)

View Item View Item
CISPA is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.