1[1]WfMC. Workflow Management Coalition Interface1: Process Definition Interchange Process Model. WFMC2TC210162P [S]. Version 1.1, Oct.1999
2[2]Zaidi A K. On temporal logic programming using Petri nets [J]. IEEE Transactions on Systems, Man and Cybernetics, 1999, 29(3): 245-254.
3[3]Yao Y. A Petri net model for temporal knowledge representation and reasoning [J]. IEEE Trans. Systems, Man and Cybernetics, 1994, 24(9): 1374 - 1382.
4[4]Lin C, Chanson S T. Logical inference of clauses based on Petri net models [J]. International Journal of Intelligent Systems, John Wiley & Sons, 1998, 13: 821-840.
5[5]Lin C, Chaudhury A, Whinston A B, Marinescu D C. Logical inference of Horn clauses in Petri net models [J]. IEEE Trans. on Knowledge and Data Engineering, 1993, 5(4): 416-425.
6[6]E.A.Emerson, J.Y.Halpern. "Sometimes" and "not Never " Revisited: on Branching versus Linear Time [J]. Jounal of the ACM, 1986, 33(1): 151-178.
7[7]C. Girault, R. Valk. Petri Nets for System Engineering: A Guide to Modeling Verification and Application [M]. Springer-Verlag, 2003.
8[8]林闯. Petri网和系统性能评价[M]. 北京: 清华大学出版社, 2000.
9[10]O. Grumberg, D. Long. Model checking and modular verification [J]. ACM Transactions on Programming Languages and Systems, 1994, 16(3): 843-871.
10[11]F.L. Tiplea, D.C. Marinescu, C. Lin. Model Checking and Abstraction for Workflow Net Verification [C]. First International Workshop on Petri Nets and Coordination PNC 04, Bologna, Italy, 2004, 131-145.
