GR(1) 公式的弱度度量
计算机科学中的逻辑
2018-05-09 v1
摘要
尽管近年来在系统综合的理论与算法方面取得了进展，但鲜有工作致力于量化用于综合的规约的质量。在处理不可实现规约时，寻找能确保可实现性的最弱环境假设通常是一种期望的性质；在此背景下，假设的弱度是一个主要的质量参数。一个假设是否弱于另一个假设的问题通常用蕴含或等价的语言包含来解释。然而，当蕴含不成立时，这种解释不能提供关于假设弱度的进一步洞察。据我们所知，唯一能在此情况下比较两个公式的度量是熵，但即便如此，对于 GR(1) 公式——线性时序逻辑公式的一个子集，在控制器综合中尤为受关注——它也无法提供足够精细的弱度概念。本文提出一种基于 Hausdorff 维数的更精细弱度度量，该概念刻画了满足线性时序逻辑公式的 omega-语言的大小。我们确定了该度量保证区分较弱与较强 GR(1) 公式的条件。我们在计算 GR(1) 假设精化的背景下评估了我们提出的弱度度量。
引用
@article{arxiv.1805.03151,
title = {A Weakness Measure for GR(1) Formulae},
author = {Davide G. Cavezza and Dalal Alrajeh and András György},
journal= {arXiv preprint arXiv:1805.03151},
year = {2018}
}
备注
To appear in FM2018 proceedings