工作流模型是对业务过程的抽象表示。工作流建模是工作流理论研究和实际应用技术的基础。目前，相对于工作流产品的实现技术而言，工作流建模理论的研究相对滞后，在建模方法上，还没有形成比较系统化的理论体系。已有的各种建模方法也都存在着各自的缺点。P系统是现今较热门的一个研究方向，其思想来源于生物细胞的动态行为，此处我们将之用于研究工作流建模。因为P系统特有的层次性和动态性，所以可以使得工作流建模更加直观和简便，由于在P系统中特有的膜的概念，和现在流行的分布式系统十分接近，使得建模的效果更加理想。而且基于其形式化系统及实现技术，我们可以很方便的进行模型检测。此外，现有的P系统上的模型检测工具都只能进行一些简单的定性分析，但在实际应用中，定量分析往往更为重要。本文中的一个突出贡献是把概率引入到了P系统相关的模型检测中，扩大了模型检测对系统性质评估的作用，对模型的性质不仅仅给出一个简单的检测结果，而且还给出了一个精确的LTL表达式概率计算的结果。在本文中，我们首先就P系统、模型检测和重写逻辑，介绍了一些相关的基础知识并给出了形式化的定义，同时陈述了一些常用的研究方法和未来的发展方向。然后，我们定义了用于建模工作流的带有概率的P系统，给出了一个简要的形式化定义。随后，我们用这种P系统来建模两个具有一定代表性的工作流场景，并使用自己定义的概率重写逻辑的语法进行改写，再使用我们自己编写的软件进行模型检测，计算出模型中各种性质出现的概率，并就此结果进行了评估。最后我们总结本文的工作并指出以后工作的方向。此外，本文中详细列举了实现模型检测软件的相关算法，包括了有限状态的检测算法，状态转换图的生成算法和LTL表达式的概率计算算法等，并证明了这些算法的正确性。在这些算法的基础上，实现了一个用于模型检测和概率计算的程序，利用软件开发的经验进行代码的优化，并通过了所有相关测试。