×

zbMATH — the first resource for mathematics

Model checking Petri nets with MSVL. (English) Zbl 1427.68210
Summary: This paper presents three translations from Petri nets to Modeling, Simulation and Verification Language (MSVL) programs. Each translation is directed by one of the three semantics of Petri nets, namely interleaving, concurrency and max-concurrency. Further, for each translation, an equivalence relation between Petri nets and generated MSVL programs is proved. As a result, the supporting tool MSV for MSVL can be used to verify the properties of Petri nets. Case studies are given to show how to do so with MSV under each semantics.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Workcraft; TINA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Al-Ahmari, A., Optimal robotic cell scheduling with controllers using mathematically based timed Petri nets, Inf. Sci., 329, 638-648 (2016)
[2] Amparore, E. G.; Beccuti, M.; Donatelli, S., (Stochastic) model checking in GreatSPN, (Ciardo, G.; Kindler, E., Proceedings of Thirty Fifth International Conference on Application and Theory of Petri Nets and Concurrency. Proceedings of Thirty Fifth International Conference on Application and Theory of Petri Nets and Concurrency, LNCS, vol. 8489 (2014), Springer: Springer Berlin, Germany), 354-363
[3] Bell, A.; Haverkort, B. R., Sequential and distributed model checking of Petri nets, Int. J. Softw. Tools Technol. Transf., 7, 1, 43-60 (2005)
[4] Berthomieu, B.; Ribet, P. O.; Vernadat, F., The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets, Int. J. Prod. Res., 42, 14, 2741-2756 (2004)
[5] Birch, S. V.; Jacobsen, T. S.; Jensen, J. J.; Moesgaard, C.; Samuelsen, N. N.; Srba, J., Interval abstraction refinement for model checking of timed-arc Petri nets, (Legay, A.; Bozga, M., Proceedings of Twelfth International Conference on Formal Modeling and Analysis of Timed Systems. Proceedings of Twelfth International Conference on Formal Modeling and Analysis of Timed Systems, LNCS, vol. 8711 (2014), Springer: Springer Berlin, Germany), 237-251
[6] Bonet, B.; Haslum, P.; Khomenko, V.; Thiébaux, S.; Vogler, W., Recent advances in unfolding technique, Theor. Comput. Sci., 551, 84-101 (2014)
[7] Chen, Y.; Li, Z.; Barkaoui, K., Maximally permissive liveness-enforcing supervisor with lowest implementation cost for flexible manufacturing systems, Inf. Sci., 256, 74-90 (2014)
[8] Clarke, E. M.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 8, 2, 244-263 (1986)
[9] Desel, J.; Kilinç, G., Observable liveness of Petri nets, Acta Inform., 52, 2-3, 153-174 (2015)
[10] Duan, Z., Temporal Logic and Temporal Logic Programming (2005), Science Press: Science Press Beijin, China
[11] Duan, Z.; Tian, C., A unified model checking approach with projection temporal logic, (Liu, S.; Maibaum, T.; Araki, K., Proceedings of Tenth International Conference on Formal Engineering Methods. Proceedings of Tenth International Conference on Formal Engineering Methods, LNCS, vol. 5256 (2008), Springer: Springer Berlin, Germany), 167-186
[12] Duan, Z.; Tian, C., A practical decision procedure for propositional projection temporal logic with infinite models, Theor. Comput. Sci., 554, 169-190 (2014)
[13] Esmaili, M. E.; Entezari-Maleki, R.; Movaghar, A., Improved region-based TCTL model checking of time Petri nets, J. Comput. Sci. Eng., 9, 1, 9-19 (2015)
[14] Esparza, J.; Heljanko, K., Implementing LTL model checking with net unfoldings, (Dwyer, M., Proceedings of Eighth International SPIN Workshop on Model Checking Software. Proceedings of Eighth International SPIN Workshop on Model Checking Software, LNCS, vol. 2057 (2001), Springer: Springer Berlin, Germany), 37-56
[15] Feldmann, K.; Colombo, A.; Schnur, C.; Stockel, T., Specification, design and implementation of logic controllers based on colored Petri net models and the standard IEC 1131. I. specification and design, IEEE Trans. Control Syst. Technol., 7, 6, 657-665 (1999)
[16] Geebelen, D.; Geebelen, K.; Truyen, E.; Michiels, S.; Suykens, J. A.; Vandewalle, J.; Joosen, W., Qos prediction for web service compositions using kernel-based quantile estimation with online adaptation of the constant offset, Inf. Sci., 268, 397-424 (2014)
[17] Girault, C.; Valk, R., Petri Nets for Systems Engineering: A Guide to Modeling, Verification and Applications (2001), Springer
[18] Hajdu, Á.; Vörös, A.; Bartha, T., New search strategies for the Petri net CEGAR approach, (Devillers, R.; Valmari, A., Proceedings of Thirty Sixth International Conference on Application and Theory of Petri Nets and Concurrency. Proceedings of Thirty Sixth International Conference on Application and Theory of Petri Nets and Concurrency, LNCS, vol. 9115 (2015), Springer: Springer Berlin, Germany), 309-328
[19] Hou, Y.; Li, Z.; Zhao, M.; Liu, D., Extended elementary siphon-based deadlock prevention policy for a class of generalised Petri nets, Int. J. Comput. Integr. Manuf., 27, 1, 85-102 (2014)
[20] Klein, S.; Frey, G.; Minas, M., PLC programming with signal interpreted Petri nets, (van der Aalst, W.; Best, E., Proceedings of Twenty Fourth International Conference on Applications and Theory of Petri Nets. Proceedings of Twenty Fourth International Conference on Applications and Theory of Petri Nets, LNCS, vol. 2679 (2003), Springer: Springer Berlin, Germany), 440-449
[21] Liu, G.; Barkaoui, K., A survey of siphons in Petri nets, Inf. Sci., 1-23 (2015)
[22] Liu, H.; Xing, K.; Wu, W.; Zhou, M.; Zhou, H., Deadlock prevention for flexible manufacturing systems via controllable siphon basis of Petri nets, IEEE Trans. Syst. Man Cybern. Syst., 45, 3, 519-529 (2015)
[23] Piedrafita, R.; Villarroel, J., Performance evaluation of Petri nets centralized implementation: The execution time controller, Discret. Event Dyn. Syst., 21, 2, 139-169 (2011)
[24] Poliakov, I.; Khomenko, V.; Yakovlev, A., Workcraft - a framework for interpreted graph models, (Franceschinis, G.; Wolf, K., Proceedings of Thirtieth International Conference on Applications and Theory of Petri Nets. Proceedings of Thirtieth International Conference on Applications and Theory of Petri Nets, LNCS, vol. 5606 (2009), Springer: Springer Berlin, Germany), 333-342
[26] Sistla, A. P.; Clarke, E. M., The complexity of propositional linear temporal logics, J. ACM, 32, 3, 733-749 (1985)
[27] Szpyrka, M.; Biernacka, A.; Biernacki, J., Methods of translation of Petri nets to NuSMV language, (Popova-Zeugmann, L., Proceedings of the Twenty Third International Workshop on Concurrency, Specification and Programming. Proceedings of the Twenty Third International Workshop on Concurrency, Specification and Programming, CEUR Workshop Proceedings, vol. 1269 (2014), CEUR-WS: CEUR-WS Chemnitz, Germany), 245-256
[28] Tian, C.; Duan, Z., Expressiveness of propositional projection temporal logic with star, Theor. Comput. Sci., 412, 18, 1729-1744 (2011)
[29] Uzam, M.; Gelen, G.; Saleh, T. L., Think-globally-act-locally approach with weighted arcs to the synthesis of a liveness-enforcing supervisor for generalized Petri nets modeling FMSs, Inf. Sci., 1-26 (2015)
[30] Wang, S.; Gan, M.; Zhou, M., Macro liveness graph and liveness of ω-independent unbounded nets, Sci. China Inf. Sci., 58, 3, 1-10 (2015)
[31] Wang, S.; Gan, M.; Zhou, M.; You, D., A reduced reachability tree for a class of unbounded Petri nets, IEEE/CAA J. Autom. Sin., 2, 4, 353-360 (2015)
[32] Winskel, G., The Formal Semantics of Programming Languages: An Introduction (1993), MIT Press: MIT Press Cambridge, MA
[33] Yang, X.; Duan, Z., Operational semantics of framed tempura, J. Logic Algebraic Program., 78, 1, 22-51 (2008)
[34] Yoneda, T.; Hatori, H.; Takahara, A.; Minato, S., BDDs vs. zero-suppressed BDDs: For CTL symbolic model checking of Petri nets, (Srivas, M.; Camilleri, A., Proceedings of First International Conference on Formal Methods in Computer-Aided Design. Proceedings of First International Conference on Formal Methods in Computer-Aided Design, LNCS, vol. 1166 (1996), Springer: Springer Berlin, Germany), 435-449
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.