Expressiveness of Petri Nets with Stopwatches. Discrete-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. In the first part of our work, we established new results regarding to both dense-time and discrete-time semantics. We now focus on the discrete-time specificities. We address 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 recall 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) Discrete-time bounded TPNs, discrete-time bounded rSwPNs and untimed Petri nets are equally expressive; 2) The resulting (final) classification of models is given by a set of relations explained in Fig. 7. While investigating expressiveness, we exhibit proofs that can be easily extended to the resolution of decidability issues. Among other results, we prove that, for bounded rSwPNs, the state and marking reachability problems - undecidable with dense-time semantics - are decidable when discrete-time is considered. Table 1 gives a synthesis of the main decidability results for these models. 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; discrete-time semantics; Petri nets with stopwatches; expressiveness; decidability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 97, nr 1/2
• Strony: 139--176
• Opis fizyczny: Bibliogr. 25 poz., tab., 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] Arnold, A.: Finite transition systems: semantics of communicating systems, Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK, 1994, ISBN 0-13-092990-5, Translator-Plaice,, John.
• [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] Cortadella, J., Kishinevsky, M., Lavagno, L., Yakovlev, A.: Deriving Petri Nets from Finite Transition Systems, IEEE Transactions on Computers, 47(8), 1998, 859-882.
• [14] Jones, N. D., Landweber, L. H., Lien, Y. E.: Complexity of Some Problems in Petri Nets., Theoretical Computer Science 4, 1977, 277-299.
• [15] Larsen, K. G., Pettersson, P., Yi,W.: Model-Checking for Real-Time Systems, Fundamentals of Computation Theory, 1995.
• [16] Lime, D., Roux, O. H.: Formal verification of real-time systems with preemptive scheduling, Journal of Real-Time Systems, 41(2), 2009, 118-151.
• [17] Magnin, M., Lime, D., Roux, O. H.: Symbolic State Space of Stopwatch Petri Nets with Discrete-Time Semantics (Theory Paper), PETRI NETS '08: Proceedings of the 29th international conference on Applications and Theory of Petri Nets (ATPN'08), in LNCS, vol. 5062, Springer-Verlag, Berlin, Heidelberg, 2008.
• [18] 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.
• [19] Magnin, M., Molinaro, P., Roux, O. (H.).: Expressiveness of Petri Nets with Stopwatches. Dense-time part., Fundamenta Informaticae 97(1-2), 2009, 111-138.
• [20] 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.
• [21] Popova, L.: On Time Petri Nets., Journal Inform. Process. Cybern., EIK (formerly: Elektron. Inform. verarb. Kybern.), 27(4), 1991, 227-244.
• [22] 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.
• [23] 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.
• [24] 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.
• [25] 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.