关于含时长与无时长动作的马尔可夫进程演算的表达能力
计算机科学中的逻辑
2010-06-09 v1
摘要
文献中提出了多种马尔可夫进程演算，它们在多个方面互不相同。在动作表示方面，我们区分了集成时间马尔可夫进程演算（其中每个动作关联一个指数分布的时长）和正交时间马尔可夫进程演算（其中动作执行与时间流逝分离）。类似于确定性时间进程演算，我们通过展示从集成时间马尔可夫进程演算到正交时间马尔可夫进程演算的三个映射来证明这两种选择并非不可调和，这些映射在动作执行的不同解释（急切、懒惰和最大进展）下保持了进程项的行为等价性。这些映射限于集成时间马尔可夫进程演算中对并行组合有约束的进程项类，且不涉及正交时间马尔可夫进程演算表达非确定性选择的全部能力，从而阐明了两种演算之间仅有的两个重要区别：它们的同步纪律和解决选择的方式。
引用
@article{arxiv.1006.1412,
title = {On the Expressiveness of Markovian Process Calculi with Durational and Durationless Actions},
author = {Marco Bernardo},
journal= {arXiv preprint arXiv:1006.1412},
year = {2010}
}