SMT-Based Reachability Checking for Bounded Time Petri Nets

• Autorzy: Półrola A. , Cybula P. , Męski A.

Identyfikatory

DOI

10.3233/FI-2014-1135

• Języki publikacji: EN

Abstrakty

EN

Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).

Słowa kluczowe

EN

Petri nets; bounds; modules; symbolic; mathematical logic; satisfiability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 135, nr 4
• Strony: 467--482
• Opis fizyczny: Bibliogr. 20 poz., rys., tab.

Twórcy

autor

Półrola A.

• Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland

autor

Cybula P.

• Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland

autor

Męski A.

• Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland
• Institute of Computer Science, PAS, Warsaw, Poland

Bibliografia

• [1] Abadi, M., Lamport, L.: An Old-Fashioned Recipe for Real Time, REX workshop on Real-Time: Theory in Practice, 600, Springer-Verlag, 1991.
• [2] Berthomieu, B., Diaz, M.: Modeling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE Trans. on Software Eng., 17(3), 1991, 259–273.
• [3] Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA - Construction of Abstract State Spaces for Petri Nets and Time Petri Nets, International Journal of Production Research, 42(14), 2004.
• [4] Berthomieu, B., Vernadat, F.: State Class Constructions for Branching Analysis of Time Petri Nets, Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), 2619, Springer-Verlag, 2003.
• [5] Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs, Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), 1579, Springer-Verlag, 1999.
• [6] Boucheneb, H., Hadjidj, R.: CTL* Model Checking for Time Petri Nets, Theoretical Computer Science, 353(1), 2006, 208–227.
• [7] Grumberg, O., Long, D. E.: Model Checking and Modular Verification, Proc. of the 2nd Int. Conf. on Concurrency Theory (CONCUR’91), 527, Springer-Verlag, 1991.
• [8] Janowska, A., Penczek, W., Półrola, A., Zbrzezny, A.: Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets, in: Trans. on Petri Nets and Other Models of Concurrency VIII, vol. 8100 of LNCS, Springer-Verlag, 2013, 89–105.
• [9] Lime, D., Roux, O. H.: Model Checking of Time Petri Nets Using the State Class Timed Automaton, Discrete Event Dynamic Systems, 16(2), 2006, 179–205.
• [10] Merlin, P., Farber, D. J.: Recoverability of Communication Protocols – Implication of a Theoretical Study, IEEE Trans. on Communications, 24(9), 1976, 1036–1043.
• [11] Męski, A., Penczek, W., Półrola, A., Woźna-Szcześniak, B., Zbrzezny, A.: Bounded Model Checking Approaches for Verificaton of Distributed Time Petri Nets, Proc. of the Int. Workshop on Petri Nets and Software Engineering (PNSE’11), University of Hamburg, 2011.
• [12] de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver, Proc. of the 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), 4963, Springer-Verlag, 2008.
• [13] Penczek, W., Półrola, A.: Abstractions and Partial Order Reductions for Checking Branching Properties of Time Petri Nets, Proc. of the 22nd Int. Conf. on Applications and Theory of Petri Nets (ICATPN’01), 2075, Springer-Verlag, 2001.
• [14] Penczek, W., Półrola, A., Zbrzezny, A.: SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets, in: Trans. on Petri Nets and Other Models of Concurrency IV, vol. 6550 of LNCS, Springer-Verlag, 2010, 72–97.
• [15] Półrola, A., Cybula, P., Męski, A.: SMT-Based Reachability Checking for Bounded Time Petri Nets (extended abstract), Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’13), 1032, CEUR-WS.org, 2013.
• [16] Popova-Zeugmann, L.: Time Petri Nets State Space Reduction Using Dynamic Programming, Journal of Control and Cybernetics, 35(3), 2006, 721–748.
• [17] Tsinarakis, G., Tsourveloudis, N., Valavanis, K.: Modular Petri Net based modeling, analysis, synthesis and performance evaluation of random topology dedicated production systems, Journal of Intelligent Manufacturing, 16(1), 2005, 67–92.
• [18] Virbitskaite, I. B., Pokozy, E. A.: A Partial Order Method for the Verification of Time Petri Nets, in: Fundamental of Computation Theory, vol. 1684 of LNCS, Springer-Verlag, 1999, 547–558.
• [19] Wan, M., Ciardo, G.: Symbolic reachability analysis of integer timed Petri nets, Proc. 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), 2009.
• [20] Yoneda, T., Ryuba, H.: CTL Model Checking of Time Petri Nets Using Geometric Regions, IEICE Trans. Inf. and Syst., 3, 1998, 1–10.