分布式算法在实际应用中具有重要的价值意义，本文采用一种基于概率模型检测技术验证和分析了两类分布式算法的性质，并这些性质给出了相应的证明。由于概率模型检测可以穷举状态空间，相比于传统方法，使得它更接近真实应用环境,更利于我们研究算法的安全性和有效性；同时概率模型检测器中的马尔科夫技术可以分析出模型中那些不确定因素。随机分布式算法中有一种自动恢复状态的算法—自稳定算法，MitchellFlatebo提出的自稳定算法是通过一个简单随机的解决方案解决n个进程令牌环中的故障，使故障自动恢复正常。他证明出最坏的情况有n-1个令牌，所需要的时间的上界是0.5N2-0.5N-2。从实验中，发现这个上限出现的可能很小。而在实际应用中，我们更注重系统预期恢复稳定状态的时间—预期最差时间。实验中，主要采用PRISM工具验证了Flatebo算法的性质，并且把它与同类型Herman自稳定算法做了比较，当系统中的结点数目增加时，它的性能会逐渐提高，优于Herman算法；另外，还用线性回归从实验结果中拟合出预期最差时间在O(N1.45)和O(N1.47)之间；最后还给出一个验证和分析自稳定算法的简单方法。本文研究的另一个分布式算法是随机互斥算法，提出了一个基于概率模型检测工具PRISM方法,用于验证和分析Kerry Raymond提出的分布式K互斥算法，首先验证了互斥算法无死锁和无饥饿两种基本性质；然后通过PRISM验证某一进程进入临界区平均及时时间；接着分析我们的实验结果，当各个进程的相对访问临界区资源的时间相差不大时，增加临界资源k的数量，不能很明显提高进程的平均及时时间，但如果其中某一进程访问临界资源的时间较长，那么增加k的值，就会大大提高运行效率。随后我们通过添加额外的存储结构，获得了新的改进k互斥算法，可以大大降低进程之间的发送和接受延时。最后给出改进的k分布式算法。