Minimization Algorithms for Time Petri Nets

• Autorzy: Półrola A. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

The paper presents three methods for applying partitioning algorithms, used for generating abstract models for timed automata, to the case of time Petri nets. Each of these methods is based on a different approach to the concrete semantics of a net, and can potentially be more efficient than the others in a particular case. Besides the theoretical description, we provide some preliminary experimental results, obtained from the implementation integrated with the model checking tool VeriCS.

Słowa kluczowe

EN

Timed Automata; timed Petri nets; algorithms

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 307--331
• Opis fizyczny: Bibliogr. 39 poz., tab.

Twórcy

autor

Półrola A.

• Faculty of Mathematics, University of Lodz, Banacha 22, 90-238 Lodz, Poland

autor

Penczek W.

• Institute of Computer Science. PAS, Ordona 21. 01-237 Warsaw, Poland

Bibliografia

• [1] R. Alur. C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(l):2-34,1993.
• [2] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS’92), pages 157-166. IEEE Comp. Soc. Press, 1992.
• [3] R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the Int. Colloquium on Automata, Languages and Programming (ICALP'90). volume 443 of LNCS, pages 322-335. Springer-Verlag, 1990.
• [4] В. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using Time Petri Nets. IEEE Trans, on Software Eng., 17(3):259-273, 1991.
• [5] B. Berthomieu and F. Vernadat. State class constructions for branching analysis of Time Petri Nets. In Proc. of the 9th Int. Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 442-457. Springer-Verlag, 2003.
• [6] A. Bouajjani, J-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247-269, 1992.
• [7] A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of the 18th IEEE Real-Time Systems Symposium (RTSS'97), pages 232-243. IEEE Comp. Soc. Press, 1997.
• [8] H. Boucheneb and G. Berthelot. Towards a simplified building of Time Petri Nets reachability graph. In Proc. of the 5th Int. Workshop on Petri Nets and Performance Models, pages 46-55, October 1993.
• [9] M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in prepositional temporal logic. Theoretical Computer Science, 59(1/2): 115-131, 1988.
• [10] F. Cassez and O. H. Roux. Traduction structurelle des Réseaux de Petri Temporeis vers le Automates Temporises. In Proc. of 4ieme Colloque Francophone sur la Modélisation des Systémes Réactifs (MSR'03). Hermes Science, October 2003.
• [11] L. A. Cortés. P. Eles, and Z. Peng. Verification of real-time embedded systems using Petri net models and Timed Automata. In Proc. of the 8th Int. Conf. on Real-Time Computing Systems and Applications (RTCSA'02), pages 191-199. March 2002.
• [12] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), volume 1384 of LNCS, pages 313-329. Springer-Verlag. 1998.
• [13] P. Dembiński. A. Janowska, P. Janowski. W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerlCS: A tool for verifying Timed Automata and Estelle specifications. In Proc. of the 9th Int. Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [14] P. Dembiński, W. Penczek, and A. Półrola. Automated verification of infinite state concurrent systems: an improvement in model generation. In Proc. of the 4th Int. Conf. on Parallel Processing and Applied Mathematics (PPAM'01). volume 2328 of LNCS. pages 247-255. Springer-Verlag, 2002.
• [15] P. Dembiński. W. Penczek, and A. Półrola. Verification of Timed Automata based on similarity. Fundamenta Informaticae, 51(1 -2):59-89. 2002.
• [16] D. Dill. Timing assumptions and verification of finite state concurrent systems. In Automatic Verification Methods for Finite-State Systems. volume 407 of LNCS, pages 197-212. Springer-Verlag. 1989.
• [17] J-C. Fernandez, H. Garavel. A. Kerbrat, R. Mateescu. L. Mounier, and M. Sighireanu. CADP: A protocol validation and verification toolbox. In Proc. of the Stli Int. Conf. on Computer Aided Verification (CAV'96), volume 1102 of LNCS, pages 437-440. Springer-Verlag, 1996.
• [18] G. Gardey. O. H. Roux, and O. F. Roux. Using zone graph method for computing the state space of a Time Petri Net. In Proc. of the 1st Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS'03), LNCS. Springer-Verlag. 2003. to appear.
• [19] Z. Gu and K. Shin. Analysis of event-driven real-time systems with Time Petri Nets. In Proc. of the Int. Conf. on Design and Analysis of Distributed and Embedded Systems (DIPES’02), volume 219 of IFIP Conference Proceedings, pages 31-40. Kluwer, 2002.
• [20] S. Haar, L. Kaiser, F. Simonot-Lion, and J. Toussaint. On equivalence between Timed State Machines and Time Petri Nets. Technical Report RR-4049, INRIA Rhóne-Alpes. 655, avenue de l’Еurоре. 38330 Montbonnot-St-Martin, November 2000.
• [21] M. Huhn. P. Niebert. and F. Wallner. Verification based on local states. In Proc. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of LNCS, pages 36-51. Springer-Verlag, 1998.
• [22] H. Hulgaard and S. M. Burns. Efficient timing analysis of a class of Petri Nets. In Proc. of the 7th Int. Conf. on Computer Aided Verification (CAV'95), volume 939 of LNCS, pages 923-936. Springer-Verlag, 1995.
• [23] R. Janicki. Nets, sequential components and concurrency relations. Theoretical Computer Science. 29:87-121, 1984.
• [24] J. Lilius. Efficient state space search for Time Petri Nets. In Proc. of MFCS Workshop on Concurrency, Brno’98, volume 18 of FN'TCS. Elsevier Science Publishers, 1999.
• [25] D. Lime and O. H. Roux. State class timed automaton of a time Petri net. In Proc. of the 10th Int. Workshop on Petri Nets and Performance Models (PNPM’03). IEEE Comp. Soc. Press, September 2003.
• [26] P. Merlin and D. J. Färber. Recoverability of communication protocols - implication of a theoretical study. IEEE Trans, on Communications, 24(9): 1036-1043, 1976.
• [27] Y. Okawa and T. Yoneda. Symbolic CTL model checking of Time Petri Nets. Electronics and Communications in Japan, Scripta Technica, 80(4): 11-20, 1997.
• [28] W. Penczek. Partial order reductions for checking branching properties of Time Petri Nets. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'00), volume 140 of Informatik-Berichte, pages 189-202. Humboldt University. 2000.
• [29] W. Penczek and A. Półrola. Abstractions and partial order reductions for checking branching properties of Time Petri Nets. In Proc. of the Int. Conf on Applications and Theory of Petri Nets (IC'ATPN'0l). volume 2075 of LNCS, pages 323-342. Springer-Verlag, 2001.
• [30] W. Penczek. B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02). volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [31] A. Pólrola, W. Penczek. and M. Szreter. Towards refining partitioning for checking reachability in Timed Automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'02), volume 161(2) of Informatik-Berichte, pages 278-291. Humboldt University, 2002.
• [32] A. Półrola, W. Penczek, and M. Szreter. Reachability analysis for Timed Automata based on partitioning. Technical Report 961. ICS PAS, Ordona 21, 01-237 Warsaw. June 2003.
• [33] J. Sifakis and S. Yovine. Compositional specification of timed systems. In Proc. of the 13th Annual Symposium on Theoretical Aspects of Computer Science (STACS’96), volume 1046 of LNCS, pages 347-359. Springer-Verlag, 1996.
• [34] S. Tripakis. Minimization of timed systems, http://verimag.imag.fr/~tripakis/dea.ps.gz, 1998.
• [35] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25-68, 2001.
• [36] I. B. Virbitskaite and E. A. Pokozy. A partial order method for the verification of Time Petri Nets. In Fundamental of Computation Theory, volume 1684 of LNCS. pages 547-558. Springer-Verlag, 1999.
• [37] В. Woźna, A. Zbrzezny. and W. Penczek. Checking reachability properties for Timed Automata via SAT. Fundamenta Informaticae, 55(2):223-241, 2003.
• [38] T. Yoneda and H. Ryuba. CTL model checking of Time Petri Nets using geometric regions. IE1CE Trans. Inf and Syst., 3:1-10, 1998.
• [39] S. Yovine. KRONOS: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer. 1 (1/2): 123-133, 1997.