马尔可夫测试等价与指数定时内部动作
计算机科学中的逻辑
2009-12-12 v1 性能
摘要
在迄今为止发展起来的马尔可夫过程测试理论中，进程内不允许存在指数定时的内部动作。当这些动作存在时，它们无法被抽象掉，因为其执行需要非零的时间量，从而可以被观察。另一方面，必须仔细考虑它们，以免将那些从定时视角可区分的进程等同起来。本文在包含指数定时内部动作的马尔可夫进程演算框架下，重新阐述了马尔可夫测试等价的定义。然后，我们证明了所得的行为等价是一个同余关系，具有可靠且完备的公理化，具有模态逻辑刻画，并且可以在多项式时间内判定。
引用
@article{arxiv.0912.1899,
title = {Markovian Testing Equivalence and Exponentially Timed Internal Actions},
author = {Marco Bernardo},
journal= {arXiv preprint arXiv:0912.1899},
year = {2009}
}