In: Formal Methods and Software Engineering (ICFEM 2002), Proceedings of the 4th International Conference on Formal Engineering Methods, Shanghai, China, October 21-25, 2002, pages 221-225. Volume 2495 of Lecture Notes in Computer Science / C. George, H. Miao (Eds.) --- Springer Verlag, October 2002.
Abstract: This paper focuses on mitigating efficiently the problem of state explosion in Petri net models. A new modeling and analyzing method, logical Petri net workflows (LPNW), of the real-time systems with batch data process procedures is presented based on Petri net and workflow techniques. The use of LPNWs is illustrated by a useful example of a batch stock trading system. The properties and functional correctness of the modeled system are analyzed and verified formally on the basis of temporal logic. It has been sufficiently shown that this approach can avoid the problem of state explosion to a certain extent. Finally, further research work is proposed.