概率项重写系统的期望内部运行复杂度与强几乎必然终止的依赖对
计算机科学中的逻辑
2025-10-16 v2
摘要
依赖对（DP）框架是自动化终止和复杂度分析项重写系统（TRS）最强大的技术之一。虽然DP已被扩展用于证明概率项重写系统（PTRS）的几乎必然终止，但针对PTRS的自动复杂度分析仍鲜有探索。我们引入第一个针对分析期望复杂度以及证明最内侧重写（innermost rewriting）的正或强几乎必然终止（SAST）的DP框架，即有限期望运行时间。我们将该框架实现于工具AProVE中，并与现有证明SAST技术相比较，展示了其强大的能力。
引用
@article{arxiv.2507.12918,
title = {Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting},
author = {Jan-Christoph Kassing and Leon Spitzer and Jürgen Giesl},
journal= {arXiv preprint arXiv:2507.12918},
year = {2025}
}