中文摘要：

稳固是为工作流的正确性的一个很重要的标准。与计算树逻辑(CTL ) 指定稳固允许我们与符号的模型检查器验证稳固。因此，在验证稳固的州的爆炸问题能高效地被克服。当性质没被系统满足时，模型检查能给一个反例，它能指导我们改正工作流。另外，放松了稳固是为工作流的另一个重要标准。我们也证明那棵计算树是逻辑 *(CTL *) 能习惯于特性工作流的放松的稳固。

英文摘要：

The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.