转移系统和马尔可夫报酬链的强、弱和分支互模拟：统一矩阵方法
Strong, Weak and Branching Bisimulation for Transition Systems and Markov Reward Chains: A Unifying Matrix Approach
摘要：
我们首先研究具有显式成功终止的标记转移系统。我们建立的概念，强，弱，分支互模拟的布尔矩阵理论，从而引入一种新颖的和强大的代数仪器。接下来，我们考虑马尔可夫报酬链，这是标准的实矩阵理论。通过解释在此设置中的互模拟得到的矩阵条件，我们自动获得马尔可夫报酬链的强，弱和分支互模拟的定义。得到的强和弱互模拟与一些现有的概念相吻合，而得到的分支互模拟是新的，但其有用性是值得怀疑的。
英文摘要：
We first study labeled transition systems with explicit successful termination. We establish the notions of strong, weak, and branching bisimulation in terms of boolean matrix theory, introducing thus a novel and powerful algebraic apparatus. Next we consider Markov reward chains which are standardly presented in real matrix theory. By interpreting the obtained matrix conditions for bisimulations in this setting, we automatically obtain the definitions of strong, weak, and branching bisimulation for Markov reward chains. The obtained strong and weak bisimulations are shown to coincide with some existing notions, while the obtained branching bisimulation is new, but its usefulness is questionable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
