paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Riesz Modal Logic with Threshold Operators

带阈值算子的 Riesz 模态逻辑
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 该论文是纯逻辑与形式化验证方向，研究 Riesz 模态逻辑扩展及其在概率 CTL 上的公理化，不涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，与用户画像核心方向几乎无交集。引用 7 inbox
Matteo Mio
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：为带阈值算子的 Riesz 模态逻辑给出可靠完备公理化，使其能刻画离散与连续 Markov 链上的概率 CTL 有界片段。

本文研究 Riesz 模态逻辑在引入阈值算子后的公理化问题。作者在原有逻辑上扩展一个归纳定义的算子，用以表达阈值条件，并给出该扩展逻辑的可靠且完备的公理化系统。该逻辑能够解释离散与连续 Markov 链上的概率 CTL（probabilistic CTL）有界片段，从而为概率时序性质的逻辑刻画提供统一框架。关键结果是所提出的公理化既可靠又完备，说明扩展后的阈值算子可在该逻辑框架内被完全公理化。

问题
Riesz 模态逻辑缺少阈值算子，难以直接表达概率 CTL 有界片段中的阈值性质；本文要为其扩展形式提供公理化。
方法
通过引入一个归纳定义的算子来定义阈值算子，并构造可靠且完备的公理化系统。
评估
以离散和连续 Markov 链为语义模型，展示该逻辑可解释概率 CTL 的有界片段，并证明公理化的可靠性与完备性。
原文摘要（Abstract）

We present a sound and complete axiomatisation of the Riesz modal logic extended with one inductively defined operator which allows the definition of threshold operators. This logic is capable of interpreting the bounded fragment of the logic probabilistic CTL over discrete and continuous Markov chains.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot4391,
  title = {Riesz Modal Logic with Threshold Operators},
  author = {Matteo Mio},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209118}
}