时态概率系统的可决定性概率逻辑
摘要：基于半马尔可夫过程，对引入于Beauquier等人的谓词逻辑进行扩展，该论文证明了在定性概率性质方面，对该逻辑应用于半马尔可夫过程的模型检验是可判定的。此外，我们将这种逻辑应用于考虑了经典和紧急语义以及时钟谓词的概率时态自动机。证明了半马尔可夫过程的结果同样适用于这两种考虑的概率时态自动机。另外，证明了在考虑了紧急语义的概率时态自动机中，Markov过程的结果可推广。
作者：Ruggero Lanotte (Dipartimento di Scienze della Cultura, Politiche e dell'Informazione), Daniele Beauquier (LACL, Dept. of Informatics)
论文ID：cs/0411100
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23