Waiting Nets : State Classes and Taxonomy

• Autorzy: Loïc, Hélouët , Pranay, Agrawal
• Języki publikacji: EN

Abstrakty

EN

In time Petri nets (TPNs), time and control are tightly connected: time measurement for a transition starts only when all resources needed to fire it are available. Further, upper bounds on duration of enabledness can force transitions to fire (this is called urgency). For many systems, one wants to decouple control and time, i.e. start measuring time as soon as a part of the preset of a transition is filled, and fire it after some delay and when all needed resources are available. This paper considers an extension of TPN called waiting nets that dissociates time measurement and control. Their semantics allows time measurement to start with incomplete presets, and can ignore urgency when upper bounds of intervals are reached but all resources needed to fire are not yet available. Firing of a transition is then allowed as soon as missing resources are available. It is known that extending bounded TPNs with stopwatches leads to undecidability. Our extension is weaker, and we show how to compute a finite state class graph for bounded waiting nets, yielding decidability of reachability and coverability. We then compare expressiveness of waiting nets with that of other models w.r.t. timed language equivalence, and show that they are strictly more expressive than TPNs.

Słowa kluczowe

EN

Petri nets; state classes; time measurmants; taxonomy

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2024
• Tom: Vol. 190, nr 2-4
• Strony: 63--107
• Opis fizyczny: Bibliogr. 40 poz., rys., tab.

Twórcy

autor

Loïc, Hélouët

• University Rennes, Inria, CNRS, IRISA, France,

autor

Pranay, Agrawal

• ENS-Paris-Saclay, France,

Bibliografia

• [1] Merlin PM. A Study of the Recoverability of Computing Systems. Ph.D. thesis, University of California, Irvine, CA, USA, 1974.
• [2] Esparza J. Decidability and Complexity of Petri Net Problems - An Introduction. In: Proc. of Petri Nets, volume 1491 of LNCS. 1998 pp. 374-428. doi:10.1007/3-540-65306-6 20.
• [3] Rackoff C. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 1978. 6(2):223-231. doi:10.1016/0304-3975(78)90036-1.
• [4] Mayr E. An Algorithm for the General Petri Net Reachability Problem. In: Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA. ACM, 1981 pp. 238-246. doi:10.1145/800076.802477.
• [5] Popova-Zeugmann L. On Time Petri Nets. J. Inf. Process. Cybern., 1991. 27(4):227-244.
• [6] Berthomieu B, Diaz M. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Trans. Software Eng., 1991. 17(3):259-273. doi:10.1109/32.75415.
• [7] Lime D, Roux O. Model Checking of Time Petri Nets Using the State Class Timed Automaton. Discret. Event Dyn. Syst., 2006. 16(2):179-205. doi:10.1007/s10626-006-8133-9.
• [8] Ramchandani C. Analysis of asynchronous concurrent systems by timed Petri nets. Ph.D. thesis, Massachusetts Institute of Technology, 1974.
• [9] Abdulla P, Nylén A. Timed Petri Nets and BQOs. In: ICATPN. LNCS 2075, p.53-70, 2001.
• [10] Reynier P, Sangnier A. Weak Time Petri Nets Strike Back! In: Proc. of CONCUR 2009, volume 5710 of LNCS. 2009 pp. 557-571. doi:10.1007/978-3-642-04081-8 37.
• [11] Ruiz VV, Gomez FC, Frutos-Escrig Dd. On Non-Decidability of Reachability for Timed-Arc Petri Nets. In: PNPM. IEEE Computer Society, 1999 pp. 188. doi:10.1109/PNPM.1999.796565.
• [12] Akshay S, Genest B, Héloüet L. Decidable Classes of Unbounded Petri Nets with Time and Urgency. In: Kordon F, Moldt D (eds.), Application and Theory of Petri Nets and Concurrency - 37th International Conference, Petri Nets 2016, Toru´n, Poland, June 19-24, 2016. Proceedings, volume 9698 of Lecture Notes in Computer Science. Springer, 2016 pp. 301-322. doi:10.1007/978-3-319-39086-4 18.
• [13] Jacobsen L, Jacobsen M, Møller MH, Srba J. Verification of Timed-Arc Petri Nets. In: SOFSEM’11.LNCS 6543, p.46-72, 2011 . doi:10.1007/978-3-642-18381-2_4.
• [14] Bowden F. Modelling time in Petri nets. In: Proc. Second Australia-Japan Workshop on Stochastic
• Models. 1996.
• [15] Berthomieu B, Lime D, Roux O, Vernadat F. Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches. Discret. Event Dyn. Syst., 2007. 17(2):133-158. doi:10.1007/s10626-006-0011-y.
• [16] Cassez F, Larsen K. The Impressive Power of Stopwatches. In: Palamidessi C (ed.), CONCUR 2000 -
• Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science. Springer, 2000 pp. 138-152. doi:10.1007/3-540-44618-4 12.
• [17] Bucci G, Fedeli A, Sassoli L, Vicario E. Timed State Space Analysis of Real-Time Preemptive Systems. IEEE Trans. Software Eng., 2004. 30(2):97-111. doi:10.1109/TSE.2004.1265815.
• [18] Parrot R, Briday M, Roux O. Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design. In: Buchs D, Carmona J (eds.), Application and Theory of Petri Nets and Concurrency - 42nd International Conference, Petri Nets 2021, Virtual Event, June 23-25, 2021, Proceedings, volume 12734 of Lecture Notes in Computer Science. Springer, 2021 pp. 55-75. doi:10.1007/978-3-030-76983-3 4.
• [19] Jones N, Landweber LH, Lien YE. Complexity of Some Problems in Petri Nets. Theor. Comput. Sci., 1977. 4(3):277-299. doi:10.1016/0304-3975(77)90014-7.
• [20] Frutos-Escrig Dd, Ruiz V, Marroquin Alonso O. Decidability of Properties of Timed-Arc Petri Nets. In: Nielsen M, Simpson D (eds.), Application and Theory of Petri Nets 2000, 21st International Conference, ICATPN 2000, Aarhus, Denmark, June 26-30, 2000, Proceeding, volume 1825 of Lecture Notes in Computer Science. Springer, 2000 pp. 187-206. doi:10.1007/3-540-44988-4 12.
• [21] Hélouët L, Agrawal P. Waiting Nets. In: Bernardinello L, Petrucci L (eds.), Proc. of PETRI NETS 2022, volume 13288 of LNCS. 2022 pp. 67-89. doi:10.1007/978-3-031-06653-5 4.
• [22] Dill D. Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis J (ed.), Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, volume 407 of Lecture Notes in Computer Science. Springer, 1989 pp. 197-212. doi:10.1007/3-540-52148-8 17.
• [23] Alur R, Dill D. A Theory of Timed Automata. Theor. Comput. Sci., 1994. 126(2):183-235.
• [24] Cassez F, Roux O. Structural translation from Time Petri Nets to Timed Automata. Journal of Systems and Software, 2006. 79(10):1456-1468. doi:10.1016/j.jss.2005.12.021.
• [25] Bérard B, Cassez F, Haddad S, Lime D, Roux OH. The expressive power of Time Petri nets. TCS, 2013. 474:1-20. doi:10.1016/j.tcs.2012.12.005.
• [26] Menasche M, Berthomieu B. Time Petri Nets for Analyzing and Verifying Time Dependent Communication Protocols. In: Rudin H, West CH (eds.), Protocol Specification, Testing, and Verification, III, Proceedings of the IFIP WG 6.1 Third International Workshop on Protocol Specification, Testing and Verification, organized by IBM Research, Rüschlikon, Switzerland, 31 May - 2 June, 1983. North-Holland, 1983 pp. 161-172.
• [27] Menasche M. Analyse des r´eseaux de Petri temporisés et Application aux syst`emes distribu´es. Ph.D. thesis, Univ. Paul Sabatier, Toulouse, 1982.
• [28] Bengtsson J, Yi W. Timed Automata: Semantics, Algorithms and Tools. In: Desel J, Reisig W, Rozenberg G (eds.), Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science. Springer, 2003 pp. 87-124. doi:10.1007/978-3-540-27755-2 3.
• [29] Cheng A, Esparza J, Palsberg J. Complexity Results for 1-Safe Nets. Theor. Comput. Sci., 1995. 147(1-2):117-136. doi:10.1016/0304-3975(94)00231-7.
• [30] Diekert V, Gastin P, Petit A. Removing epsilon-Transitions in Timed Automata. In: Reischuk R, Morvan M (eds.), STACS 97, 14th Annual Symposium on Theoretical Aspects of Computer Science, Lübeck, Germany, February 27 - March 1, 1997, Proceedings, volume 1200 of Lecture Notes in Computer Science. Springer, 1997 pp. 583-594. doi:10.1007/BFb0023491.
• [31] Akshay S, Hélouët L, Phawade R. Combining free choice and time in Petri nets. J. Log. Algebraic Methods Program., 2020. 110. doi:10.1016/j.jlamp.2018.11.006.
• [32] Walter B. Timed Petri-Nets for Modelling and Analysing Protocols with Real-Time Characteristics. In: Proc. of PSTV. 1983 pp. 149-159. https://dblp.org/rec/conf/ifip/Walter83.bib.
• L. Hélouët and P. Agrawal / Waiting Nets: State Classes and Taxonomy 97 [33] Hack M. Decidability Questions for Petri Nets. Ph.D. thesis, M.I.T., MIT, CA, USA, 1976.
• [34] David A, Jacobsen L, Jacobsen M, Srba J. A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets. In: SSV’12, volume 102 of EPTCS. 2012 pp. 125-140. doi:10.4204/EPTCS.102.12.
• [35] Dantzig G, Eaves BC. Fourier-Motzkin Elimination and Its Dual. J. Comb. Theory, Ser. A, 1973. 14(3):288-297. doi:10.1016/0097-3165(73)90004-6.
• [36] Bérard B, Cassez F, Haddad S, Lime D, Roux O. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: FORMATS, volume 3829 of Lecture Notes in Computer Science. 2005 pp. 211-225. doi:10.1007/11603009 17.
• [37] Bouyer P, Haddad S, Reynier PA. Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. Inf. Comput., 2008. 206(1):73-107. doi:10.1016/j.ic.2007.10.004.
• [38] Bérard B, Cassez F, Haddad S, Lime D, Roux OH. When are timed automata weakly timed bisimilar to time Petri nets ? Theoretical Computer Science, 2008. 403(2-3):202-220. doi:10.1016/j.tcs.2008.03.030.
• [39] Berthomieu B, Peres F, Vernadat F. Bridging the gap between timed automata and bounded Time Petri Nets. In: FORMATS’06, volume 4202 of LNCS. 2006 pp. 82-97. doi:10.1007/11867340 7.
• [40] Walter B. Timed Petri Nets for Modelling and Analyzing Protocols with Real-time Characteristics. In: Protocol Specification, Testing, and Verification, III. 1983 pp. 149-159. https://dblp.org/rec/conf/ifip/Walter83.bib

Identyfikatory

DOI

10.3233/FI-242167