Safety Synthesis Sans Specification

TL;DR

This paper introduces a method for synthesizing transducers from a target language with potential conflicts, using membership and conjecture queries, relevant for hardware and software verification, with a polynomial complexity algorithm.

Contribution

It presents a novel learning algorithm for transducer synthesis from conflicting sources, with proven polynomial time and query complexity.

Findings

Algorithm is efficient with polynomial complexity.

Prototype implementation demonstrates practical viability.

Applicable to hardware and software verification scenarios.

Abstract

We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation.