工作流建模中时态逻辑的研究与应用

摘要

在使用Petri网构建工作流行为结构模型的同时,使用时态逻辑描述工作流模型的需求与特性,则具有描述能力强、灵活方便的优点.在此基础上,综合考虑时态逻辑列表法和即时验证方法的特点,给出一种主要利用Büchi自动机进行工作流模型需求及特性验证的方法,提高了工作流模型的合理性和可靠性.最后,验证分析了电子商务的工作流实例.