×

zbMATH — the first resource for mathematics

Verification of timed-arc Petri nets. (English) Zbl 1298.68175
Černá, Ivana (ed.) et al., SOFSEM 2011: Theory and practice of computer science. 37th conference on current trends in theory and practice of computer science, Nový Smokovec, Slovakia, January 22–28, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18380-5/pbk). Lecture Notes in Computer Science 6543, 46-72 (2011).
Summary: Timed-Arc Petri Nets (TAPN) are an extension of the classical P/T nets with continuous time. Tokens in TAPN carry an age and arcs between places and transitions are labelled with time intervals restricting the age of tokens available for transition firing. The TAPN model posses a number of interesting theoretical properties distinguishing them from other time extensions of Petri nets. We shall give an overview of the recent theory developed in the verification of TAPN extended with features like read/transport arcs, timed inhibitor arcs and age invariants. We will examine in detail the boundaries of automatic verification and the connections between TAPN and the model of timed automata. Finally, we will mention the tool TAPAAL that supports modelling, simulation and verification of TAPN and discuss a small case study of alternating bit protocol.
For the entire collection see [Zbl 1205.68007].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] TAPAAL, http://www.tapaal.net
[2] UPPAAL, http://www.uppaal.com · Zbl 1105.68350
[3] Abdulla, P.A., Nylén, A.: Better is better than well: On efficient verification of infinite-state systems. In: Proceedings of 15th Annual IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 132–140 (2000)
[4] Abdulla, P.A., Nylén, A.: Timed Petri nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001) · Zbl 0986.68092
[5] Abdulla, P.A., Deneux, J., Mahata, P., Nylén, A.: Forward reachability analysis of timed Petri nets. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 343–362. Springer, Heidelberg (2004) · Zbl 1109.68509
[6] Abdulla, P.A., Mahata, P., Mayr, R.: Dense-timed Petri nets: Checking zenoness, token liveness and boundedness. Logical Methods in Computer Science 3(1), 1–61 (2007) · Zbl 1128.68057
[7] Alur, R., Dill, D.: Automata for modelling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990) · Zbl 0765.68150
[8] Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994) · Zbl 0803.68071
[9] Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM 12(5), 260–261 (1969)
[10] Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004) · Zbl 1105.68350
[11] Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Software Eng. 17(3), 259–273 (1991) · Zbl 05113493
[12] Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research 42(14), 2741–2756 (2004) · Zbl 1060.68695
[13] Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time Petri nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 82–97. Springer, Heidelberg (2006) · Zbl 1141.68426
[14] Bolognesi, T., Cremonese, P.: The weakness of some timed models for concurrent systems. Technical Report CNUCE C89-29, CNUCE–C.N.R (1989)
[15] Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: Proceedings of the IFIP WG 6.1 Tenth International Symposium on Protocol Specification, Testing and Verification (Ottawa 1990), pp. 1–14. North-Holland, Amsterdam (1990)
[16] Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets. Journal of Logic and Computation 19(6), 1509–1540 (2009) · Zbl 1188.68182
[17] Bouyer, P., Haddad, S., Reynier, P.-A.: Timed Petri nets and timed automata: On the discriminating power of zeno sequences. Information and Computation 206(1), 73–107 (2008) · Zbl 1133.68053
[18] Bouyer, P., Haddad, S., Reynier, P.A.: Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. Information and Computation 206(1), 73–107 (2008) · Zbl 1133.68053
[19] Bowden, F.D.J.: Modelling time in Petri nets. In: Proceedings of the Second Australia-Japan Workshop on Stochastic Models (1996)
[20] Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
[21] Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 237–267. Springer, Heidelberg (2004) · Zbl 1105.68352
[22] Byg, J., Jørgensen, K.Y., Srba, J.: An efficient translation of timed-arc Petri nets to networks of timed automata. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 698–716. Springer, Heidelberg (2009) · Zbl 05635836
[23] Byg, J., Jørgensen, K.Y., Srba, J.: TAPAAL: Editor, simulator and verifier of timed-arc Petri nets. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 84–89. Springer, Heidelberg (2009) · Zbl 05640929
[24] Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. ENTCS 128(6), 145 (2005); Proc. of AVoCS 2004 (2004) · Zbl 1272.68294
[25] Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed Automata Patterns. IEEE Transactions on Software Engingeering 34(6), 844–859 (2008)
[26] Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001) · Zbl 0973.68170
[27] Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: A tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005) · Zbl 1081.68618
[28] Hack, M.: Petri Net Language. Technical Report MIT-LCS-TR-159, Massachusetts Institute of Technology, Cambridge, MA, USA (1976)
[29] Hanisch, H.M.: Analysis of place/transition nets with timed-arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282–299. Springer, Heidelberg (1993)
[30] Heitmann, F., Moldt, D., Mortensen, K.H., Rölke, H.: Petri nets tools database quick overview, http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/quick.html (accessed: 28.10.2010)
[31] Jacobsen, L., Jacobsen, M., Møller, M.H.: Undecidability of coverability and boundedness for timed-arc Petri nets with invariants. In: Proc. of MEMICS 2009. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2009) ISBN 978-3-939897-15-6 · Zbl 1247.68186
[32] Jacobsen, L., Jacobsen, M., Møller, M.H.: Modelling and verification of timed-arc Petri nets. Master’s thesis, Department of Computer Science, Aalborg University, Denmark (2010a), http://tapaal.net · Zbl 1247.68186
[33] Jacobsen, L., Jacobsen, M., Møller, M.H., Srba, J.: A framework for relating timed transition systems and preserving TCTL model checking. In: Aldini, A., Bernardo, M., Bononi, L., Cortellessa, V. (eds.) EPEW 2010. LNCS, vol. 6342, pp. 83–98. Springer, Heidelberg (2010) · Zbl 05805009
[34] Jacobsen, L., Jacobsen, M., Møller, M.H., Srba, J.: A framework for relating timed transition systems and preserving TCTL model checking. Technical Report FIMU-RS-2010-09, Faculty of Informatics, Masaryk Univ. (2010c)
[35] Janowska, A., Janowski, P., Wróblewski, D.: Translation of Intermediate Language to Timed Automata with Discrete Data. Fundamenta Informaticae 85(1-4), 235–248 (2008) · Zbl 1158.68020
[36] Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5(1), 1–11 (1987)
[37] Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model-checking of real-time systems. In: Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), pp. 439–456. Kluwer, B.V (1998)
[38] Mayr, E.W.: An algorithm for the general Petri net reachability problem (preliminary version). In: Proceedings of the 13th Ann. ACM Symposium on Theory of Computing, pp. 238–246. ACM, New York (1981)
[39] Merlin, P.M.: A Study of the Recoverability of Computing Systems. PhD thesis, University of California, Irvine, CA, USA (1974)
[40] Merlin, P.M., Faber, D.J.: Recoverability of communication protocols: Implications of a theoretical study. IEEE Transactions on Communications 24(9), 1036–1043 (1976) · Zbl 0362.68096
[41] Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967) · Zbl 0195.02402
[42] Nielsen, M., Sassone, V., Srba, J.: Properties of distributed timed-arc Petri nets. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 280–291. Springer, Heidelberg (2001) · Zbl 1052.68639
[43] Pelayo, F.L., Cuartero, F., Valero, V., Macia, H., Pelayo, M.L.: Applying timed-arc Petri nets to improve the performance of the MPEG-2 encoding algorithm. In: Proceedings of the 10th International Multimedia Modelling Conference (MMM 2004), pp. 49–56. IEEE Computer Society, Los Alamitos (2004)
[44] Pelayo, F.L., Cuartero, F., Valero, V., Pelayo, M.L., Merayo, M.G.: How does the memory work? by timed-arc Petri nets. In: Proceedings of the 4th IEEE International Conference on Cognitive Informatics (ICCI 2005), pp. 128–135 (2005)
[45] Penczek, W., Pólrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Springer, Heidelberg (2006) · Zbl 1110.68087
[46] Petri, C.A.: Kommunikation mit Automaten. PhD thesis, Darmstadt (1962)
[47] Ramchandani, C.: Performance Evaluation of Asynchronous Concurrent Systems by Timed Petri Nets. PhD thesis, Massachusetts Institute of Technology, Cambridge (1973)
[48] Ruiz, V.V., Cuartero Gomez, F., de Frutos Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: Proceedings of the 8th International Workshop on Petri Net and Performance Models (PNPM 1999), pp. 188–196 (1999)
[49] Ruiz, V.V., de Frutos Escrig, D., Marroquin Alonso, O.: Decidability of properties of timed-arc petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 187–206. Springer, Heidelberg (2000) · Zbl 0986.68077
[50] Ruiz, V.V., Pardo, J.J., Cuartero, F.: Translating TPAL specifications into timed-arc Petri nets. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 414–433. Springer, Heidelberg (2002) · Zbl 1047.68090
[51] Ruiz, V.V., Pelayo, F.L., Cuartero, F., Cazorla, D.: Specification and analysis of the MPEG-2 video encoder with timed-arc Petri nets. Electronic Notes Theoretial Computer Science 66(2) (2002)
[52] Sifakis, J.: Use of Petri nets for performance evaluation. In: Proceedings of the Third International Symposium IFIP W.G. 7.3., Measuring, Modelling and Evaluating Computer Systems (Bonn-Bad Godesberg), pp. 75–93. Elsevier Science Publishers, Amsterdam (1977)
[53] Sifakis, J., Yovine, S.: Compositional specification of timed systems. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 347–359. Springer, Heidelberg (1996) · Zbl 1379.68240
[54] Srba, J.: Timed-arc Petri nets vs. networks of timed automata. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 385–402. Springer, Heidelberg (2005) · Zbl 1128.68069
[55] Srba, J.: Comparing the expressiveness of timed automata and timed extensions of Petri nets. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 15–32. Springer, Heidelberg (2008) · Zbl 1171.68579
[56] Wang, J.: Timed Petri Nets, Theory and Application. Kluwer Academic Publishers, Dordrecht (1998) ISBN ISBN 0-7923-8270-6 · Zbl 0924.68147
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.