×

Checking system boundedness using ordinary differential equations. (English) Zbl 1277.68180

Summary: Boundedness is one of the most important properties of discrete Petri nets. Determining the boundedness of a Petri net is usually done through building coverability graph or coverability tree. However, the computation is infeasible for complex applications because the size of the coverability graph may increase faster than any primitive recursive functions. This paper proposes a new technique to check the boundedness without causing this problem. Let a concurrent system be represented by a (discrete) Petri net. By relaxing the (discrete) Petri net to a continuous Petri net, we can model the concurrent system by a family of ordinary differential equations. It has been shown that the boundedness of the discrete Petri net is equivalent to the boundedness of the solutions of the corresponding ordinary differential equations. Hence, we can check the boundedness of a (discrete) Petri net by analyzing the solutions of a family of ordinary differential equations. A case study demonstrates the benefits of our technique.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ascher, U. M.; Petzold, L. R., Computer Methods for Ordinary Differential Equations and Differential-Algebraic Equations (1998), Society for Industrial and Applied Mathematics: Society for Industrial and Applied Mathematics Philadelphia, PA, USA · Zbl 0908.65055
[2] Ben-Ari, M., Principles of Concurrent and Distributed Programming (2006), Addison Wesley · Zbl 0701.68001
[3] Burch, J. R.; Clarke, E. M.; Long, D. E., Representing circuits more efficiently in symbolic model checking, (Proceedings of the 28th Design Automation Conference (1991), IEEE Computer Society Press: IEEE Computer Society Press Los Alamltos, CA), 403-407
[4] Chang, Y.-C.; Chu, C.-P., Applying learning behavioral Petri nets to the analysis of learning behavior in web-based learning environments, Information Sciences, 180, 995-1009 (2010)
[5] David, R.; Alla, H., Discrete, Continuous, and Hybrid Petri Nets (2005), Springer
[6] Demongodin, I.; Koussoulas, N. T., Differential Petri nets: representing continuous systems in a discrete-event world, IEEE Transactions on Automatic Control, 43, 4, 573-579 (1998) · Zbl 0959.93038
[7] Desel, J.; Esparza, J., Free Choice Petri Nets (1995), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0836.68074
[8] Devillers, R.; Begin, L. V., Boundedness undecidability for synchronized nets, Information Processing Letters, 99, 208-214 (2006) · Zbl 1185.68026
[9] Ding, Z., Static analysis of concurrent programs using ordinary differential equations, Lecture Notes in Computer Sciences, 5684, 1-35 (2009) · Zbl 1250.68090
[10] Du, Y.; Jiang, C.; Zhou, M.; Fu, Y., Modeling and monitoring of E-commerce workflows, Information Sciences, 179, 995-1006 (2009) · Zbl 1189.68081
[11] Esparza, J.; Silva, M., Compositional synthesis of live and bounded free choice Petri nets, (Baeten, J. C.M.; Greote, J. F., Proceedings of the 2nd International Conference on Concurrency Theory. Proceedings of the 2nd International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 527 (1991), Springer: Springer Berlin), 172-187
[12] Hale, J. K., Ordinary Differential Equations (1969), Interscience: Interscience New York · Zbl 0186.40901
[13] Hairer, E.; Nφrsett, S. P.; Wanner, G., Solving Ordinary Differential Equations (I), Nonstiff Problems (1993), Springer-Verlag
[14] J.W. Herrmann, E. Lin, Petri nets-tutorial and applications, in: Proceedings of the 32nd Annual Symposium of the Washington Operations Research, Management Science Council, November 5, 1997, Washington, DC.; J.W. Herrmann, E. Lin, Petri nets-tutorial and applications, in: Proceedings of the 32nd Annual Symposium of the Washington Operations Research, Management Science Council, November 5, 1997, Washington, DC.
[15] Intievergelt, J., Parallel methods for integrating ordinary differential equations, Communications of the ACM, 7, 12, 731-733 (1964) · Zbl 0134.32804
[16] Jiao, L.; Cheung, T.; Lu, W., On liveness and boundedness of asymmetric choice nets, Theoretical Computer Science, 311, 165-197 (2004) · Zbl 1070.68106
[17] Karp, R. M.; Miller, R. E., Parallel program schemata, Journal of Computer and System Sciences, 3, 2, 147-195 (1969) · Zbl 0198.32603
[18] König, B.; Kozioura, V., Incremental construction of coverability graphs, Information Processing Letters, 103, 203-209 (2007) · Zbl 1184.68345
[19] B. Lin, Efficient compilation of process-based concurrent programs without run-time scheduling, in: Proceedings of Design, Automation, and Test in Europe (DATE), Paris, 1998, pp. 211-217.; B. Lin, Efficient compilation of process-based concurrent programs without run-time scheduling, in: Proceedings of Design, Automation, and Test in Europe (DATE), Paris, 1998, pp. 211-217.
[20] Mayr, E. W., An algorithm for the general Petri net reachability problem, SIAM Journal on Computing, 13, 3, 441-460 (1984) · Zbl 0563.68057
[21] Praveen, M.; Lodaya, K., Analyzing reachability for some Petri nets with fast growing markings, Electronic Notes in Theoretical Computer Science, 223, 215-237 (2008) · Zbl 1337.68190
[22] Reisig, W., Petri Nets: An Introduction, EATCS Monographs on Theoretical Computer Science (1985), Springer: Springer Berlin, Germany
[23] Royden, H. L., Real Analysis (1988), Macmillan Publishing Co.: Macmillan Publishing Co. New York · Zbl 0704.26006
[24] Shatz, S. M.; Mai, K.; Black, C.; Tu, S., Design and implementation of a Petri net-based toolkit for Ada tasking analysis, IEEE Transactions on Parallel and Distributed Systems, 1, 4, 424-441 (1990)
[25] Smart, D. R., Fixed Point Theorems (1974), Cambridge University Press: Cambridge University Press Cambridge, UK · Zbl 0297.47042
[26] Valk, R.; Vidal-Naquet, G., Petri nets and regular languages, Journal of Computer and System Sciences, 23, 3, 299-325 (1981) · Zbl 0473.68057
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.