带无穷区间的概率区间时序逻辑与持续时间演算:完备证明系统
计算机科学中的逻辑
2019-03-14 v2
摘要
本文给出了带无穷区间的区间时序逻辑(ITL)与持续时间演算(DC)的概率扩展,并为它们提供了完备的 Hilbert 式证明系统。完备性结果包括:概率 ITL 系统相对于抽象语义的强完备性定理,以及概率 DC 系统相对于实时语义的相对完备性定理。所提出的系统涵盖了文献中已知的概率实时 DC。此外,还建立了所提系统与带有限区间及扩展模态的概率区间时序逻辑系统之间的对应关系。
引用
@article{arxiv.0706.0692,
title = {Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems},
author = {Dimitar P. Guelev},
journal= {arXiv preprint arXiv:0706.0692},
year = {2019}
}
评论
43 pages