论无否定 MTL 中时态算子的语法简化
计算机科学中的逻辑
2025-09-15 v1
摘要
在动态、数据密集的环境中，时态推理越来越需要兼具表达力与可处理性的逻辑框架。传统方法通常依赖否定来表达缺失或矛盾。在此类语境中，通常使用“否定即失败”来从缺乏正面证据的情况推断负面信息。然而，在诸如物联网网络或语义网等开放和分布式系统中，由于数据不完整和异步，“否定即失败”语义变得不可靠。这促使人们对基于时态规则系统的无否定片段产生越来越浓厚的兴趣，因为这些片段保持了单调性并能够实现可扩展的推理。本文研究了无否定 MTL 的表达能力，这是一种为随时间变化的基于规则的推理而设计的时态逻辑框架。我们表明，MTL 中的“always”算子通常被视为其他时态构造组合的语法糖，但可以使用“once”、“since”和“until”算子将其消去。值得注意的是，甚至“once”算子也可以被移除，从而得到一个仅基于“until”和“since”的片段。这些结果挑战了否定对于表达普遍时态约束是必要的这一假设，并揭示了一个能够捕获存在性和不变时态模式的稳健片段。此外，这些结果导致了 MTL 语法的简化，进而可以为理论研究和实现工作提供益处。
引用
@article{arxiv.2509.10146,
title = {On Syntactical Simplification of Temporal Operators in Negation-free MTL},
author = {Mathijs van Noort and Femke Ongenae and Pieter Bonte},
journal= {arXiv preprint arXiv:2509.10146},
year = {2025}
}