“大多数”导致不可判定性：向LTL添加频率失败
"Most of" leads to undecidability: Failure of adding frequencies to LTL
摘要：
有限迹上的线性时态逻辑是形式化验证中常用的一种健壮的规范框架。然而，尽管近年来对逻辑的兴趣很高，但其定量扩展的主题尚未得到充分探讨。这项工作的主要目标是研究添加弱形式的百分比约束（例如，大多数的位置在过去满足给定的条件，或sigma是最频繁的字母发生在过去）的LTL片段的效果。这种扩展可能用于验证影响网络或统计推理。不幸的是，正如我们在论文中证明的那样，事实证明，即使是很小的LTL片段的百分比扩展也具有不可判定的可满足性和模型检查问题。我们的不可判定性证明，不仅锐化了大多数的不可判定性结果的逻辑与算术解释的话从文献中已知的，但也是相当简单的。我们还证明了通过限制否定的允许使用可以避免不可判定性，并简要讨论了不可判定性结果如何转移到一阶词逻辑。
英文摘要：
Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and briefly discuss how the undecidability results transfer to first-order logic on words.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
