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