Robustness of Time Petri Nets under Guard Enlargement

• Autorzy: Akshay S. , Jard C. , Hélouët L. , Reynier P.-A.

Identyfikatory

DOI

10.3233/FI-2016-1312

• Języki publikacji: EN

Abstrakty

EN

Robustness of timed systems aims at studying whether infinitesimal perturbations in clock values can result in new discrete behaviors. A model is robust if the set of discrete behaviors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for time Petri nets (TPNs, for short) by considering the model of parametric guard enlargement which allows time-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter. We show that TPNs are not robust in general and checking if they are robust with respect to standard properties (such as boundedness, safety) is undecidable. We then extend the marking class timed automaton construction for TPNs to a parametric setting, and prove that it is compatible with guard enlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded (i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): we provide two decidable robustly bounded subclasses, and show that one can effectively build a timed automaton which is timed bisimilar even in presence of perturbations. This allows us to apply existing results for timed automata to these TPNs and show further robustness properties.

Słowa kluczowe

EN

time Petri nets; robustness; timed automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 3/4
• Strony: 207--234
• Opis fizyczny: Bibliogr. 26 poz., rys., tab.

Twórcy

autor

Akshay S.

• Indian Institute of Technology, Bombay, India

autor

Jard C.

• Université de Nantes, Nantes, France

autor

Hélouët L.

• INRIA/IRISA, Rennes, France

autor

Reynier P.-A.

• Aix Marseille Université, CNRS, LIF UMR 7279 F-13288, Marseille, France

Bibliografia

• [1] Alur R, Dill D. A Theory of Timed Automata. In TCS. 1994;126(2):183–235. doi:10.1016/0304-3975(94)90010-8.
• [2] Merlin P.M. A Study of the Recoverability of Computing Systems. University of California. Irvine, C.A, USA; 1974.
• [3] Puri A. Dynamical Properties of Timed Automata. In DEDS Discrete Event Dynamic Systems. 2000;10(1-2):87–113. doi:10.1023/A:1008387132377.
• [4] Bouyer P, Markey N, Reynier P.A. Robust Model-Checking of Linear-Time Properties in Timed Automata. In: Proc. of LATIN. vol. 3887 of LNCS. Springer; 2006. p. 238–249. doi:10.1007/11682462 25.
• [5] Bouyer P, Markey N, Reynier P.A. Robust Analysis of Timed Automata via Channel Machines. In: Proc. of FoSSaCS. vol. 4962 of LNCS. Springer; 2008. p. 157–171.
• [6] De Wulf M, Doyen L, Markey N, Raskin J.F. Robust Safety of Timed Automata. Formal Methods in System Design. 2008;33(1-3):45–84. doi:10.1007/s10703-008-0056-7.
• [7] Bouyer P, Markey N, Sankur O. Robust Model-Checking of Timed Automata via Pumping in Channel Machines. In: Proc. of FORMATS. vol. 6919 of LNCS. Springer; 2011. p. 97–112. doi:10.1007/978-3-642-24310-3 8.
• [8] Sankur O. Untimed Language Preservation in Timed Systems. In: Proc. of MFCS. vol. 6907 of LNCS. Springer; 2011. p. 556–567. doi:10.1007/978-3-642-22993-0 50.
• [9] De Wulf M, Doyen L, Raskin J.F. Systematic Implementation of Real-Time Models. In: Proc. of Formal Methods. vol. 3582 of LNCS. Springer; 2005. p. 139–156. doi:10.1007/11526841 11.
• [10] Gardey G, Roux O.H, Roux O.F. A Zone-Based Method for Computing the State Space of a Time Petri Net. In: Proc. of FORMATS. vol. 2791 of LNCS; 2003. p. 246–259. doi:10.1007/978-3-540-40903-8 20.
• [11] Cassez F, Roux O.H. 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.
• [12] Lime D, Roux O.H. Model Checking of Time Petri Nets Using the State Class Timed Automaton. Discrete Event Dynamic Systems. 2006;16(2):179–205. doi:10.1007/s10626-006-8133-9.
• [13] D’Aprile D, Donatelli S, Sangnier A, Sproston J. From Time Petri Nets to Timed Automata: An Untimed Approach. In: Proc. of TACAS. vol. 4424 of LNCS. Springer; 2007. p. 216–230. doi:10.1007/978-3-540-71209-1 18.
• [14] Akshay S, Hélouët L, Jard C, Reynier P.A. Robustness of Time Petri Nets under Guard Enlargement. In: Proc. of RP. vol. 7550 of LNCS. Springer; 2012. p. 92–106. Available from: https://hal.inria.fr/hal-01237124.
• [15] Bërard B, Cassez F, Haddad S, Lime D, Roux O.H. Comparison of Different Semantics for Time Petri Nets. In: Proc. of ATVA. vol. 3707 of LNCS. Springer; 2005. p. 293–307. doi:10.1007/11562948 23.
• [16] Berthomieu B, Diaz M. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Trans in Software Engineering. 1991;17(3):259–273. doi:10.1109/32.75415.
• [17] Swaminathan M, Fränzle M, Katoen J.P. The Surprising Robustness of (Closed) Timed Automata against Clock-Drift. In: Proc. of TCS. Springer; 2008. p. 537–553. doi:10.1007/978-0-387-09680-3 36.
• [18] Bérard B, Cassez F, Haddad S, Lime D, Roux O.H. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: Proc. of FORMATS. vol. 3829. Springer; 2005. p. 211–225. doi:10.1007/11603009 17.
• [19] Karp R.M, Miller R.E. Parallel program chemata. In JCSS. 1969;3:147–195. doi:10.1016/S0022-0000(69)80011-5.
• [20] Hack M. Decidability Questions for Petri Nets. M.I.T.. MIT, CA, USA; 1976.
• [21] Giua A, Seatzu C. Modeling and Supervisory Control of Railway Networks Using Petri Nets. IEEE T Automation Science and Engineering. 2008;5(3):431–445. doi:10.1109/TASE.2008.916925.
• [22] Janczura C.W. Modelling and Analysis of Railway Network Control Logic using Coloured Petri Nets. School of Mathematics University of South Australia. Adelaide, South Australia; 1998.
• [23] Burkolter D.M. Capacity of Railways in Station Areas using Petri Nets. Swiss Federal Institute of Technology. Zurich, Switzerland; 2005.
• [24] Bjork J, Hagalisletto A.M. Challenges in simulating railway systems using Petri Nets. Precise Modeling and Analysis, Department of Informatics, Univesity of Oslo; 2005.
• [25] Zimmermann A, Hommel G. A Train Control System Case Study in Model-Based Real Time System Desig. In: IPDPS; 2003. p. 118. doi:10.1109/IPDPS.2003.1213234.
• [26] Chatain T, Jard C. Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets. In: Proc. Of ICATPN; 2006. p. 125–145. doi:10.1007/11767589 8.