随机进程代数(SPA)是一种功能与性能相结合的并发系统模型，是通过给经典进程代数模型中的动作发生附加上一个随机变量值，来反映在系统的运行中，动作出现的时间延迟规律而得到的模型。它既能够描述系统的功能，又能够对系统运行的性能进行评价，很多涉及资源共享的系统，例如，大型计算、客户-服务器结构、网络等都可以用这种随机模型作精确的形式化描述。随机进程代数中应用最广泛的是马尔可夫进程代数，在马尔可夫进程代数中，动作出现的随机延迟时间是满足指数分布的随机变量。本论文主要研究了马尔可夫随机进程代数的各种操作语义模型，在这些语义模型下的等价性概念的定义，以及对马尔可夫随机进程的等价性进行判定的计算算法。主要包括以下三方面的内容：1．马尔可夫链代数上的模拟等价判定。马尔可夫链代数是进程间只有时间延迟转移的进程代数，连续时间马尔可夫链(CTMC)代数是并发系统性能评价最早使用的模型。通过状态转移的马尔可夫链分析，可给出系统的性能指标的刻画。在一个CTMC代数模型上的互模拟等价关系是以状态间满足的转移概率值为基础定义的，这和CTMC上的聚集等价关系一致，所以给出了基于状态的“聚集块”的等价块划分算法，并给出了算法的复杂度分析。2．交互式马尔可夫链(IMC)代数上的等价性判定。交互式马尔可夫链代数是通过正交结合经典的进程代数和连续时间马尔可夫链代数得到的随机进程代数模型。本文研究了IMC上的互模拟等价的计算，计算算法的主要思想是对动作和概率转移分别进行划分细化计算，最终得到一个递减关系链的不动点，从而得到互模拟等价。并在CTMC模型的弱模拟等价定义的基础上提出了IMC上强(弱)模拟等价的概念，并且给出了判定模拟前序关系的计算算法，算法的主要思想是通过求解一个线性方程组，判定两个状态的马尔可夫模拟关系，并去掉所有不能进行模拟的状态对。3．一般随机进程代数上的等价性判定。一般随机进程代数是指既有动作转移，又有带随机时间延迟的动作转移的进程代数。这种进程代数的一个关键点是如何定义两个并发进程中同步马尔可夫动作转移的随机延迟分布φ(λ，μ，P，Q)，不同的φ函数定义对应了不同的随机进程代数模型，我们研究了φ(λ，μ)=λμ时的随机进程代数中的互模拟、模拟等价性概念的定义和判定算法，这些算法是IMC上各种判定算法的改进。即，对马尔可夫转移进行判定时，要区分收敛状态和发散状态，同时要对每一个马尔可夫动作转移进行(互)模拟判定。