马尔可夫检验等价性与指数时间内作用
Markovian Testing Equivalence and Exponentially Timed Internal Actions
摘要：
在马尔可夫过程的测试理论发展至今，指数时间的内部行动是不承认的过程。当存在时，这些操作不能被抽象掉，因为它们的执行花费非零的时间，因此可以被观察到。另一方面，必须认真考虑这些因素，以免将从时间观点来看可以区分的进程等同起来。在本文中，我们重新定义的马尔可夫测试等价的马尔可夫过程演算的框架内，包括指数时间的内部行动。然后，我们表明，由此产生的行为等价是一个同余，有一个健全的和完整的公理化，具有模态逻辑特征，并可以决定在多项式时间。
英文摘要：
In the theory of testing for Markovian processes developed so far, exponentially timed internal actions are not admitted within processes. When present, these actions cannot be abstracted away, because their execution takes a nonzero amount of time and hence can be observed. On the other hand, they must be carefully taken into account, in order not to equate processes that are distinguishable from a timing viewpoint. In this paper, we recast the definition of Markovian testing equivalence in the framework of a Markovian process calculus including exponentially timed internal actions. Then, we show that the resulting behavioral equivalence is a congruence, has a sound and complete axiomatization, has a modal logic characterization, and can be decided in polynomial time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
