论文标题
“大多数”导致不可证明：将频率添加到LTL的失败
"Most of" leads to undecidability: Failure of adding frequencies to LTL
论文作者
论文摘要
在有限痕迹上解释的线性时间逻辑（LTL）是一个在形式验证中流行的强大规范框架。然而，尽管近年来对逻辑引起了极大的兴趣，但尚未充分探索其定量扩展的主题。这项工作的主要目的是研究添加较弱的百分比约束形式的效果（例如，过去的大多数位置满足给定的条件，或者Sigma是过去发生的最频繁的字母）。这种扩展可能有可能用于验证影响网络或统计推理。不幸的是，正如我们在论文中证明的那样，事实证明，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.
