PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2014 | Vol. 135, nr 4 | 467--482
Tytuł artykułu

SMT-Based Reachability Checking for Bounded Time Petri Nets

Warianty tytułu
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
Wydawca

Rocznik
Strony
467--482
Opis fizyczny
Bibliogr. 20 poz., rys., tab.
Twórcy
  • Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland , polrola@math.uni.lodz.pl
autor
  • Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland , cybula@math.uni.lodz.pl
autor
  • Faculty of Mathematics and Computer Science, University of Łódź, Banacha 22, 90-238 Łódź, Poland , meski@ipipan.waw.pl
  • 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.
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-3338e1fe-8d22-48cd-8694-2b39f9054c4a
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.