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

摘要/Abstract

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

关键词: 工作流, 时态逻辑, 模型

Abstract: Using the Petri net to build the behavioral model of workflow, the temporal logic is used to specify the requirements and properties of the workflow model. This method has more descriptive power and is flexible，easy to be used. Based on the tableau and on-the-fly methods of temporal logic, a realization method that mainly uses the Büchi automata to validate the workflow model is presented. It improves the rationality and reliability of the workflow model. Finally, a workflow case of electronic commerce is analyzed and validated.

Key words: workflow, temporal logic, model

中图分类号:

TP311

唐达，徐超，杨晓丽. 工作流建模中时态逻辑的研究与应用[J]. .

TANG Da，XU Chao，YANG Xiao-li. Temporal Logic Applied in Workflow Modeling[J]. .

参考文献

[1]SALIMIFARD K，WRIGHT M. Petri net-based modelling of workflow systems：an overview[J].European Journal of Operational Reseach，2001，134（3）：664-676.

[2]LIN Chuang，TIAN Liqin，WEI Yaya. Performance equivalent analysis of workflow systems[J].Journal of Software， 2002，13（8）：1472-1480（in Chinese）.[林闯，田立勤，魏丫丫.工作流系统模型的性能等价分析[J].软件学报，2002，13（8）：1472-1480.]

[3]LUO Haibin, FAN Yushun, WU Cheng. Analysis of event balance in the verification of workflow soundness[J].Journal of Software，2002，13（8）：1686-1691（in Chinese）.[罗海滨，范玉顺，吴澄.工作流合理性验证中的事件平衡分析[J].软件学报，2002，13(8)：1686-1691.]

[4]LI Jianqiang , FAN Yushun.Research of Petri net based workflow model reduction methods[J]. Information and Control，2002，30（6）：492-497（in Chinese）.[李建强，范玉顺.基于Petri网化简方法的工作流模型验证[J].信息与控制，2002，30（6）：492-497.]

[5]AALST van der W M P，ARTHUR H M，HOFSTEDE T. Verification of workflow task structures：a petri-net-based approach[J].Information Systems，2000，25（1）：43-69 .

[6]FU X，BULTAN T，HULL R，et al. Verification of vortex workflows[A]. Proceeding of the 7th international conference on Tools and Algorithms for the Construction and Analysis of Systems[C]. Berlin：Springer-Verlag，2001.143-157.

[7]UCHIHIRA N. A programming environment for reactive and concurrent systems using petri nets and temporal logic[EB/OL]. www.craft.titech.ac.jp/～uchihira/phd.html,1997-11.

[8]MERZ S. Model checking：a tutorial overview[A].4th Summer School，Modelling and Verification of Parallel Processes (MOVEP00)[C].Berlin：Spinger-Verlag，2001.3-38.

[9]YIH-KUEN T . Compositional verification in linear-time temporal logic[A]. Third International Conference，Foundations of Software Science and Computation Structures 2000[C].Berlin：Spinger-Verlag，2000.344-358 .

[10]ZHANG Guangquan, SUN Min. Comparison and analysis of temporal logic[J].Journal of Yuzhou University（Nat. Scien. Edit），1999，16（2）：15-18（in Chinese）. [张广泉，孙敏.时态逻辑的比较与分析[J].渝州大学学报（自然科学版），1999，16（2）：15-18.]

[1]	王琦,闻立杰,邓雅方,钱忱,王建民. 基于过程模型约束的轨迹乱序事件修复方法[J]. 计算机集成制造系统, 2021, 27(9): 2491-2500.
[2]	郜启凯,李莹,邓水光. 支持跨组织协作的高可靠性服务编排框架[J]. 计算机集成制造系统, 2021, 27(9): 2501-2507.
[3]	唐玄昭,余阳,吴荆璞,潘茂林. 基于区块链的业务流程互操作服务框架[J]. 计算机集成制造系统, 2021, 27(9): 2508-2516.
[4]	高子建,张晗睿,窦万春,徐江民,孟顺梅. 基于谱聚类和隐语义模型的智能协同推荐方法[J]. 计算机集成制造系统, 2021, 27(9): 2517-2524.
[5]	莫启,向吉祥,汪煜祺,代飞,许小龙,齐连永. 基于流程抽象的协同业务过程符合性验证[J]. 计算机集成制造系统, 2021, 27(9): 2542-2555.
[6]	文一凭,王志斌,刘建勋,许小龙,康国胜. 云际协作环境下能耗与成本感知的工作流调度方法[J]. 计算机集成制造系统, 2021, 27(9): 2583-2591.
[7]	张力雯,方贤文,邵叱风,王丽丽. 基于行为校验与偏差组合的过程模型修复[J]. 计算机集成制造系统, 2021, 27(9): 2625-2635.
[8]	方欢,郑雪文,王吴松. 不完备事件日志下的业务系统变化检测及模型修复方法[J]. 计算机集成制造系统, 2021, 27(9): 2647-2660.
[9]	倪维健,吉桂芳,曾庆田,刘彤,段华. 基于表示学习的业务过程模型匹配方法[J]. 计算机集成制造系统, 2021, 27(9): 2661-2669.
[10]	陈明,高铁梁,张志锋,季肖辉,唐启光. 基于用户多兴趣的服务流程推荐方法[J]. 计算机集成制造系统, 2021, 27(9): 2701-2707.
[11]	宫立华,盛妍,李磊,刘鲲鹏,朱银龙,何薇,徐倩丽. 面向电力用户的群簇核心推荐算法[J]. 计算机集成制造系统, 2021, 27(9): 2721-2728.
[12]	张辰源,陶飞. 数字孪生模型评价指标体系[J]. 计算机集成制造系统, 2021, 27(8): 2171-2486.
[13]	占翔南,徐立云,宓宏,李爱平. 双深度多层穿梭车仓储系统并行作业及建模分析[J]. 计算机集成制造系统, 2021, 27(8): 2226-2236.
[14]	王沙沙,张则强,刘俊琦,陈凤. 多路径交互环形过道布置问题建模及改进蚁狮算法优化[J]. 计算机集成制造系统, 2021, 27(8): 2237-2247.
[15]	赵祎乾,吴天宇,顾森,李亚军,朱天陆. 基于人机仿真技术的炮手操作姿势多指标量化评估模型[J]. 计算机集成制造系统, 2021, 27(8): 2350-2361.