Safety Synthesis Sans Specification
This addresses verification challenges in hardware and software by enabling synthesis without explicit specifications, though it appears incremental as it builds on existing learning frameworks.
The paper tackles the problem of learning a transducer from a target language containing conflicting transducers, ensuring the learned language is a subset of the target, and presents a polynomial-time algorithm with experimental validation.
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.