English

Safety Synthesis Sans Specification

Formal Languages and Automata Theory 2020-11-30 v2 Machine Learning

Abstract

We define the problem of learning a transducer S{S} from a target language UU containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of S{S} be a subset of UU. 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.

Cite

@article{arxiv.2011.07630,
  title  = {Safety Synthesis Sans Specification},
  author = {Roderick Bloem and Hana Chockler and Masoud Ebrahimi and Dana Fisman and Heinz Riener},
  journal= {arXiv preprint arXiv:2011.07630},
  year   = {2020}
}
R2 v1 2026-06-23T20:15:03.840Z