随机环境下的高质量综合
High-Quality Synthesis Against Stochastic Environments
摘要：
在经典的综合问题中，我们给出了一个LTL公式psi的输入和输出信号的集合，我们合成了一个传感器，实现psi。自动综合在实际应用中的一个缺点是没有考虑综合系统的质量。实际上，经典的设置是布尔型的：一个计算满足或不满足一个规范。因此，虽然合成的系统是正确的，但它的质量没有保证。近年来，研究人员考虑将经典布尔设置扩展到定量设置。逻辑LTL [F]是一个多值逻辑，它用质量算子扩充了LTL。LTL [F]公式的满意值是[0，1]中的实值，其中该值越高，计算满足规范的质量越高。LTL的决策问题变成了LFL的搜索或优化问题[F]。特别是，在合成问题中，目标是生成满足最高质量规格的换能器。以前的工作考虑了最坏情况的设置，目标是以最小的质量最大化计算的质量。我们引入并解决了随机设置，其中的目标是生成一个换能器，最大限度地提高预期的计算质量，受到给定的输入信号分布。因此，环境不是敌对的，而是被假设为概率性的，这对应于许多现实的设置。我们发现，这个问题是2EXPTIME完全的，像经典的LTL合成，仍然是这样，在两个扩展，我们认为：一个最大限度地提高预期的质量，同时保证最低的质量是，概率$1$，在给定的阈值以上，和一个允许对环境的假设。
英文摘要：
In the classical synthesis problem, we are given an LTL formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi. One weakness of automated synthesis in practice is that it pays no attention to the quality of the synthesized system. Indeed, the classical setting is Boolean: a computation satisfies a specification or does not satisfy it. Accordingly, while the synthesized system is correct, there is no guarantee about its quality. In recent years, researchers have considered extensions of the classical Boolean setting to a quantitative one. The logic LTL[F] is a multi-valued logic that augments LTL with quality operators. The satisfaction value of an LTL[F] formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. Decision problems for LTL become search or optimization problems for LFL[F]. In particular, in the synthesis problem, the goal is to generate a transducer that satisfies the specification in the highest possible quality. Previous work considered the worst-case setting, where the goal is to maximize the quality of the computation with the minimal quality. We introduce and solve the stochastic setting, where the goal is to generate a transducer that maximizes the expected quality of a computation, subject to a given distribution of the input signals. Thus, rather than being hostile, the environment is assumed to be probabilistic, which corresponds to many realistic settings. We show that the problem is 2EXPTIME-complete, like classical LTL synthesis, and remains so in two extensions we consider: one that maximizes the expected quality while guaranteeing that the minimal quality is, with probability $1$, above a given threshold, and one that allows assumptions on the environment.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
