GR（1）公式的弱性度量
A Weakness Measure for GR(1) Formulae
摘要：
尽管近年来系统综合的理论和算法的发展，很少有人致力于量化的质量的规格用于综合。在处理不可实现的规格时，找到最弱的环境假设，以确保可实现性通常是一个可取的属性;在这种情况下，假设的弱点是一个主要的质量参数。一个假设是否比另一个假设弱的问题通常使用隐含或等效的语言包含来解释。然而，这种解释并没有提供任何进一步的洞察假设的弱点时，含义不成立。据我们所知，在这种情况下，能够比较两个公式的唯一度量是熵，但即使它也不能在GR（1）公式的情况下提供足够精确的弱点概念，GR（1）公式是线性时序逻辑公式的子集，在控制器合成中特别感兴趣。在本文中，我们提出了一个更精细的措施的基础上的Hausdorff维数，一个概念，捕捉的概念，满足线性时序逻辑公式的欧米茄语言的大小的弱点。我们确定的条件下，该措施是保证区分较弱和较强的GR（1）公式。我们在计算GR（1）假设改进的背景下评估我们提出的弱点度量。
英文摘要：
In spite of the theoretical and algorithmic developments for system synthesis in recent years, little effort has been dedicated to quantifying the quality of the specifications used for synthesis. When dealing with unrealizable specifications, finding the weakest environment assumptions that would ensure realizability is typically a desirable property; in such context the weakness of the assumptions is a major quality parameter. The question of whether one assumption is weaker than another is commonly interpreted using implication or, equivalently, language inclusion. However, this interpretation does not provide any further insight into the weakness of assumptions when implication does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it fails to provide a sufficiently refined notion of weakness in case of GR(1) formulae, a subset of linear temporal logic formulae which is of particular interest in controller synthesis. In this paper we propose a more refined measure of weakness based on the Hausdorff dimension, a concept that captures the notion of size of the omega-language satisfying a linear temporal logic formula. We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae. We evaluate our proposed weakness measure in the context of computing GR(1) assumptions refinements.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
