一句话：提出 Skolem 提取算法，从规约合成具随机行为的见证，保证正确性并提升响应多样性。
现有合成方法通常通过寻找见证 Skolem 函数来构造符合规约的实现，而这些函数传统上是确定性的，难以产生行为多样性。本文提出一种新的 Skolem 提取算法，使合成出的见证具有随机行为，并将其用于无限状态反应式系统。所合成实现按设计保证满足给定规约，同时对外部刺激的响应呈现高度多样性。案例研究表明，该框架可将合成用于基于模型的模糊测试，生成与通用模糊器性能相当的模糊器，也可用于机器人运动规划中合成控制器。
Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification, while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed framework unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.
@inproceedings{paperbot5907,
title = {Synthesis of infinite-state systems with random behavior},
author = {Andreas Katis and Grigory Fedyukovich and Jeffrey Chen and David Greve and Sanjai Rayadurgam and Michael W. Whalen},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416586}
}