定时概率系统的可判定概率逻辑
计算机科学中的逻辑
2007-05-23 v2
摘要
本文扩展了 [Beauquier 等 2002] 中引入的谓词逻辑，以处理半马尔可夫过程。我们证明，针对定性概率属性，该逻辑应用于半马尔可夫过程时，模型检查是可判定的。此外，我们将逻辑应用于概率定时自动机，考虑经典语义和紧急语义，以及时钟上的谓词。我们证明，半马尔可夫过程的结果同样适用于概率定时自动机，适用于两种语义。此外，我们证明 [Beauquier 等 2002] 中展示的马尔可夫过程的结果可以扩展到考虑紧急语义的概率定时自动机。
引用
@article{arxiv.cs/0411100,
title = {A Decidable Probability Logic for Timed Probabilistic Systems},
author = {Ruggero Lanotte and Daniele Beauquier},
journal= {arXiv preprint arXiv:cs/0411100},
year = {2007}
}