线上P2P借贷业务流的Petri网建模与分析

赵雨杉，方 欢

（安徽理工大学数学与大数据学院，安徽淮南232001）

相较于银行贷款的额度门槛高、手续复杂、条件众多等因素，在线金融交易以额度门槛低、操作简单快捷而在实际应用中占有一席之地，尤其是线上P2P借贷平台在实践中得到广泛运用。然而线上P2P借贷平台存在许多问题，例如私人贷款操作极易违约，投资人维权艰难，部分系统与个人征信平台存在信息融合缺失，这些问题导致平台用户的使用风险增大。因此有必要对市场中应用的各类线上借贷业务流程进行建模分析，从根本上保障交易安全。

Petri网是由Carl Adam Petri于20世纪60年代首先提出的。它广泛应用于计算机科学技术、自动化技术等多个领域，以其具备异步、并发、选择等性质而被大量应用于系统的建模与分析。使用Petri网进行建模，可以准确地描述系统的顺序、并发、选择等流程，还可以简化模型的复杂操作，深化系统中的主要细节，用直观的图示进行模拟。最重要的是，可以利用Petri网建模的系统进行多种性质的分析，如活性、可达性、安全性等，以此来检测出系统中是否存在死锁、陷阱等问题。当前，利用Petri网建模的研究工作应用广泛。文献[1-2]采用Petri网建模，分别对学习系统与医疗业务流程进行分析。对于Petri网可达性研究，文献[3]对外卖流程构造其Petri网模型，对模型的可达性进行研究，并优化模型中需要改进模块。而如何验证Petri网的分析结果，大多采用的方法是利用仿真软件进行模拟。文献[4]是对手机公司业务流程进行建模分析，同时采用PIPE软件进行验证；文献[5-6]以物联网技术作为研究对象，分别设计了基于Petri网的物流服务系统和智慧溯源系统，以模型的关联矩阵为分析方法，并采用PIPE仿真软件进行实验。同时，众多学者也对线上P2P借贷平台进行研究，如文献[7]对P2P平台借贷流程构建了风险控制机制，提高了流程安全性，降低了流程的风险。但是，文献中仅对流程中存在的风险项进行了研究，并未对P2P平台借贷流程的整体安全性进行详细的分析与实验。本文针对线上P2P借贷平台中的借贷业务流程，进行Petri网建模分析。首先给出借贷业务流程的建模方法，得到形式化模型，然后采用形式化的分析方法对模型进行可达性、安全性等分析，最后用仿真软件对系统进行仿真模拟。

1 线上P2P借贷业务流的Petri网建模

1.1 Petri网相关定义与记号

定义1[8]（Petri网）满足下列条件的三元组N=(S,T,F)被称作一个网。其中，S为库所，T为变迁，F是网N的流关系：S⋃T≠ ∅，S⋂T≠ ∅，F⊆(S×T)⋃(T×S)，dom(F)⋃ cod(F)=S⋃T,dom(F)={x∈S⋃T|∃y∈S⋃T:(x,y)∈F},cod(F)={x∈S⋃T|∃y∈S⋃T:(y,x)∈F}。

定义2[8]（变迁发生规则）设∑=(S,T;F,M0)为一个标识网系统，则在标识M∈R(M0)下的变迁发生规则是：对t∈T，若∀s∈S:s∈·t→M(s)≥ 1，称t在标识M下有发生权，记作M[t＞。若标识M授权t发生，则变迁t在M下可以发生，得到新的标识M′，M′与M的关系记为M[t＞M′。对∀s∈S，有

定义3[8]（可达性）设∑=(S,T;F,M)为一个Petri 网。如果存在t∈T，使M[t＞M′，则称M′为从M直 接 可 达 的 。 如 果 存 在 变 迁 序 列t1,t2,…,tk和 标 识 序 列M1,M2,…,Mk使 得M[t1＞M1[t2＞M2[t3…Mk-1[tk＞Mk，则称Mk为从M可达的。从M可达的一切标识的集合记为R(M)。约定M∈R(M)。

定义4[8]（有界性）设 ∑=(S,T;F,M)为一个Petri 网，s∈S。若存在正整数B，∀M∈R(M0):M(s)≤B，则称库所s是有界的，并称满足此条件的最小正整数B为库所s的界，记为B(s)，即B(s)=min{B|∀M∈R(M0):M(s)≤B}。当B(s)=1时，称库所s为安全的。

定义5[8]（安全性）设∑=(S,T;F,M)为一个Petri网，如果每个s∈S都是有界的，则称Σ为有界Petri网。称B(Σ)=max{B(s)|s∈S}为Σ的界。当B(Σ)=1是，称Σ为安全的。

定义6[8]（可达标识图）设Σ=(S,T;F,M0)为一个有界Petri 网。Σ的可达标识图为一个三元组RG(Σ)=(R(M0),E,P)，其中E={(Mi,Mj)|Mi,Mj∈R(M0)}，R(M0)为RG(Σ)的顶点集，E为RG(Σ)的弧集。

1.2 线上P2P借贷业务流的Petri网建模

线上P2P借贷业务是通过线上P2P平台作为中介机构来进行的快速融资手段。线上P2P平台认定使用者（借款人、投资人）的参与资格。对于符合资格的使用者，借款人可以委托平台公开预期融资项目招标文件，而投资人对志愿的项目进行投标。一旦双方确认项目达成，项目主管将审核借款人的担保证明与其他必备文件材料。在借款文件审核通过之后，平台开通使用者的资金账户，后续的资金的收付将在该账户中进行。线上P2P借贷业务具体流程如图1所示。

线上P2P借贷业务的目的是满足使用者安全可靠地达到融资投资的期望。使用者的满意程度是建立在安全完成的借贷业务上的，而使用Petri网对业务建模，就能够分析模型中的安全性等性质。建模的主要步骤：（1）基于线上P2P借贷业务中实际状态与发生条件，确定该模型中的条件集S与事件集T，并确认模型中条件与事件的关系；（2）将模型中对应条件的库所与对应事件的变迁进行关联，建立Petri网模型Σ1；（3）确定所建立Petri网模型Σ1的初始状态，确定初始标识M0，确认初始状态的token数量；（4）对建立的Petri网模型Σ1进行检验。图2是线上P2P借贷业务流Petri网模型Σ1图。

图1 线上P2P借贷业务流程图

图2 线上P2P借贷业务流Petri网模型Σ1图

该模型的条件集S、事件集T的定义与描述如表1所示。

表1 条件集S与事件集T表

2 Petri网建模模型分析与验证

一般从两个方面检验Petri 网模型是否合理可靠，一方面是验证Petri 网模型的动态性质，例如网模型的可达性、有界性、安全性、活性等；另一方面，验证Petri网模型的结构性质，例如死锁与陷阱、结构有界性、S-不变量等。本文采用可达标识图的方法，针对模型Σ1的可达性、安全性进行分析与验证。

2.1 利用可达标识图进行分析

在上一节中，模型Σ1通过其关联矩阵A以及S-不变量验证得出模型的可达性。模型Σ1可达标识图RG(Σ1)如图3所示。

图3 Petri模型可达标识图RG(Σ1)

由可达标识图RG(Σ1)可见，M0= ( 1 ,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0 )为模型初始状态，代表使用者的登录状态。在初始状态下，t（1登录）具有发生权。由t1引发后续变迁发生直至t（3项目匹配）。此时，新标识为M3=(0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0)，在t（4项目投标/竞标）发生状态下，存在一个选择结构，即借款人选择t（5确认）竞标结果、t（6上传资产证明）、t（7上传担保证明），或是投资人选择t（8确认材料）。此状态完成后，将会得到两种标识，标识M10=(0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0)代表交易失败，投资人拒绝投资；而标识M11=(0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0)代表交易继续进行，投资人同意投资。此状态下，该交易会提交给部门主管去进行业务审核，即t10发生，又得到两种标识，标识M12=(0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0)代表审核未通过，部门主管拒绝该业务的成立；标识M13=(0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0)代表审核通过，主管同意进行该业务，满足t1（1账户开通）的发生条件。随着后续变迁t12（投资人充值）、t13（借款人提现）的发生，可以达到最终状态，标识M16=(0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1),代表该交易成功。

综上，由模型的可达标识图RG(Σ1)可以得出：在模型Σ1中对于任意M ∈R(M0)，都有R(M)⊆R(M0)，因此模型是可达的；对任意M∈R(M0)，都存在M′∈R(M)，使得M′[t＞，则该模型Σ1具有活性；在初始标识下，模型Σ1的变迁t1具有发生权，对任意s∈S，每个库所的界为B(si)=1，i=1,2,…,17，显然模型是有界的，并且B(Σ1)=1，即模型是安全的。

2.2 线上P2P借贷业务流模型仿真验证

实际应用中，通常使用Petri 网仿真建模工具PIPE 4.3 来进行线上P2P 平台模型的仿真验证与性质分析。在PIPE 4.3中，先搭建线上P2P借贷平台Petri网模型的框架，接着运行模型Σ1。在模型构建并运行成功后，利用PIPE 4.3中各个模块对模型Σ1进行仿真验证。

首先，通过运行classification功能模块对模型Σ1的网系统进行验证，结果如表2所示，可以直观地看出模型Σ1属于一个扩展的自由选择网。

表2 classification功能结果汇总表

其次，利用PIPE4.3中的Incidence and Marking模块，可以计算模型Σ1中的输出矩阵A+、输入矩阵A-、关联矩阵A。同时，该模块还可以对模型Σ1的初始标识M0、变迁t，以及随着变迁变化的状态标识M进行仿真验证。接着，利用PIPE 4.3中的Invariant Analysis模块，可以分析模型Σ1中的T-不变量与S-不变量。将模型Σ1中的关联矩阵A与S-不变量相结合进行分析，且其中不存在T-不变量。也就是说，模型Σ1中存在确定的6个S-不变量，没有确定的T-不变量覆盖，可以确定该模型是有界的，结果与2.1节结论一致。另外，软件还得出了模型对应的6个S-不变量方程：

最后，综上实验结果得出，模型Σ1是一个可达的、有界安全的、扩展的自由选择网。也就是说，线上P2P借贷平台的借贷款业务流程是合理可靠的，在实际应用中的可行性高。

3 总 结

随着线上P2P借贷业务的广泛应用，对流程进行Petri网建模，来分析验证其是否稳定可靠是必不可少的。Petri网作为具有分布式系统的建模分析工具，模型分析方面具有优势，可以满足多种系统的建模需求。本文通过对线上P2P借贷业务流的Petri网建模，采用可达标识图方法对模型进行分析，最后使用Petri网仿真软件PIPE进行实验。实验结果表明，线上P2P借贷业务流的Petri网建模具有合理性、可靠性及安全性等性质。针对线上P2P借贷平台等系统，本文的分析结果提供了进行优化更新的优秀范例。同时，基于模型的分析方法，也为了其他多种系统的建模分析提供了数据与模型参考。