论文标题
安全合成不指定
Safety Synthesis Sans Specification
论文作者
论文摘要
我们使用会员查询和猜想查询来定义从目标语言$ u $中学习传感器$ {s} $的问题。要求是$ {s} $的语言是$ u $的子集。我们认为,在硬件和软件验证的许多情况下,这是一个自然的问题。我们为此问题设计了一种学习算法,并表明其时间和查询复杂性相对于目标语言的等级,其不兼容度量以及给定反例的最大长度是多项式的。我们报告使用原型实现进行的实验。
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.