Expressiveness of Petri Nets with Stopwatches. Dense-time Part

• Autorzy: Magnin M , Molinaro P. , Roux O-H.
• Języki publikacji: EN

Abstrakty

EN

With this contribution, we aim to draw a comprehensive classification of Petri nets with stopwatches w.r.t. expressiveness and decidability issues. This topic is too ambitious to be summarized in a single paper. That is why we present our results in two different parts. The scope of this first paper is to address the general results that apply for both dense-time and discrete-time semantics. We study the class of bounded Petri nets with stopwatches and reset arcs (rSwPNs), which is an extension of T-time Petri nets (TPNs) where time is associated with transitions. Stopwatches can be reset, stopped and started. We give the formal dense-time and discrete-time semantics of these models in terms of Transition Systems. We study the expressiveness of rSwPNs and its subclasses w.r.t. (weak) bisimilarity (behavioral semantics). The main results are following: 1) bounded rSw- PNs and 1-safe rSwPNs are equally expressive; 2) For all models, reset arcs add expressiveness. 3) The resulting partial classification of models is given by a set of relations explained in Fig. 7: in the forthcoming paper, we will complete these results by covering expressiveness and decidability issues when discrete-time nets are considered. For the sake of simplicity, our results are explained on a model such that the stopwatches behaviors are expressed using inhibitor arcs. Our conclusions can however be easily extended to the general class of Stopwatch Petri nets.

Słowa kluczowe

EN

real-time system; Time Petri Net; Petri nets with stopwatches; expressiveness

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 97, nr 1/2
• Strony: 111--138
• Opis fizyczny: Bibliogr. 27 poz., wykr.

Twórcy

autor

Magnin M

autor

Molinaro P.

autor

Roux O-H.

• IRCCyN - 1 rue de la No¨e - BP 92101 - 44321 Nantes Cedex 03, France,

Bibliografia

• [1] Araki, T., Kasami, T.: Some Decision Problems Related to the Reachability Problem for Petri Nets, Theoretical Computer Science, 3(1), October 1976, 85-104.
• [2] Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O. H.: Comparison of Different Semantics for Time Petri Nets, Automated Technology for Verification and Analysis (ATVA'05), in LNCS, vol. 3707, Springer, 293-307, Taiwan, 2005.
• [3] Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O. H.: Comparison of the expressiveness of Timed Automata and Time Petri Nets, 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 05), in LNCS, vol. 3829, Springer, 211-225, Uppsala, Sweden, 2005.
• [4] Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O. H.: When are timed automata weakly timed bisimilar to time Petri nets?, Theoretical Computer Science, 403(2-3), 2008, 202-220.
• [5] Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets, IEEE transactions on software engineering, 17(3), 1991, 259-273.
• [6] Berthomieu, B., Lime, D., Roux, O. H., Vernadat, F.: Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches, Journal of Discrete Event Dynamic Systems - Theory and Applications (DEDS), 17(2), 2007, 133-158.
• [7] Berthomieu, B., Menasche, M.: An Enumerative Approach for Analyzing Time Petri Nets., IFIP Congress Series, 9, 1983, 41-46.
• [8] Berthomieu, B., Peres, F., Vernadat, F.: Bridging the Gap Between Timed Automata and Bounded Time Petri Nets., 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06), in LNCS, vol. 4202, Paris, France, 2006.
• [9] Boyer, M., Roux, O. H.: Comparison of the expressiveness of Arc, Place and Transition Time Petri Nets, 28th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN'07), in LNCS, vol. 4546, Springer, 63-82, Siedlce, Poland, 2007.
• [10] Boyer, M., Roux, O. H.: On the compared expressiveness of arc, place and transition time Petri Nets, Fundamenta Informaticae, 88(3), 2008, 225-249.
• [11] Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Time state space analysis of real-time preemptive systems, IEEE transactions on software engineering, 30(2), February 2004, 97-111.
• [12] Cassez, F., Roux, O. H.: Structural Translation from Time Petri Nets to Timed Automata - Model-Checking Time Petri Nets via Timed Automata, The journal of Systems and Software, 79(10), 2006, 1456-1468.
• [13] Dufourd, C.: Réseaux de Petri avec Reset/Transfert: Décidabilité et indécidabilité, Ph.D. Thesis, ENS de Cachan, 1998.
• [14] Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability, ICALP'98 (K. G. Larsen, S. Skyum, G. Winskel, Eds.), 1443, 1998.
• [15] Hack, M.: Decidability Questions for Petri Nets, Technical report, Cambridge,MA, USA, 1976.
• [16] Jones, N. D., Landweber, L. H., Lien, Y. E.: Complexity of Some Problems in Petri Nets., Theoretical Computer Science 4, 1977, 277-299.
• [17] Kosaraju, S. R.: Decidability of reachability in vector addition systems (Preliminary Version), STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory of computing, ACM Press, New York, NY, USA, 1982, ISBN 0-89791-070-2.
• [18] Larsen, K. G., Pettersson, P., Yi,W.: Model-Checking for Real-Time Systems, Fundamentals of Computation Theory, 1995.
• [19] Lime, D., Roux, O. H.: Formal verification of real-time systems with preemptive scheduling, Journal of Real-Time Systems, 41(2), 2009, 118-151.
• [20] Magnin, M., Molinaro, P., Roux, O. H.: Decidability, expressivity and state-space computation of Stopwatch Petri nets with discrete-time semantics., 8th InternationalWorkshop on Discrete Event Systems (WODES'06), Ann Arbor, USA, July 2006.
• [21] Mayr, E. W.: An Algorithm for the General Petri Net Reachability Problem, SIAM Journal on Computing, 13(3), 1984, 441-460.
• [22] Merlin, P.: A study of the recoverability of computing systems, Ph.D. Thesis, Department of Information and Computer Science, University of California, Irvine, CA, 1974.
• [23] Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets, Ph.D. Thesis, Massachusetts Institute of Technology, Cambridge,MA, 1974, Project MAC Report MAC-TR-120.
• [24] Reinhardt, K.: Reachability in Petri nets with inhibitor arcs, 1996.
• [25] Roux, O. H., Déplanche, A.-M.: A T-time Petri net extension for real time-task scheduling modeling, European Journal of Automation (JESA), 36(7), 2002, 973-987.
• [26] Roux, O. H., Lime, D.: Time Petri Nets with Inhibitor Hyperarcs. Formal Semantics and State Space Computation, The 25th International Conference on Application and Theory of Petri Nets, (ICATPN'04), in LNCS, vol. 3099, Springer, 371-390, Bologna, Italy, June 2004.
• [27] Srba, J.: Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets, Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08), 5215, Springer-Verlag, 2008.