{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:55:13Z","timestamp":1772121313493,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540422525","type":"print"},{"value":"9783540457404","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45740-2_5","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T15:30:51Z","timestamp":1195140651000},"page":"53-70","source":"Crossref","is-referenced-by-count":76,"title":["Timed Petri Nets and BQOs"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Aletta","family":"Nyl\u00e9n","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,28]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BFb0055627","volume-title":"Proc. CONCUR\u2019 98, 9th Int. Conf. on Concurrency Theory","author":"P. A. Abdulla","year":"1998","unstructured":"Parosh Aziz Abdulla and Karlis \u010cer\u0101ns. Simulation is decidable for one-counter nets. In Proc. CONCUR\u2019 98, 9th Int. Conf. on Concurrency Theory, volume 1466 of Lecture Notes in Computer Science, pages 253\u2013268, 1998."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th IEEE Int. Symp. on Logic in Computer Science, pages 414\u2013425, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis \u010cer3x0101;ns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. 11th IEEE Int. Symp. on Logic in Computer Science, pages 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis \u010cer\u0101ns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. 11th IEEE Int. Symp. on Logic in Computer Science, pages 313\u2013321, 1996. To appear in the journal of Information and Computation.","DOI":"10.1109\/LICS.1996.561359"},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Proc. ICALP\u2019 90","author":"R. Alur","year":"1990","unstructured":"R. Alur and D. Dill. Automata for modeeling real-time systems. In Proc. ICALP\u2019 90, volume 443 of Lecture Notes in Computer Science, pages 322\u2013335, 1990."},{"issue":"2","key":"5_CR6","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P. A. Abdulla","year":"1996","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91\u2013101, 1996.","journal-title":"Information and Computation"},{"key":"5_CR7","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Ensuring completeness of symbolic verification methods for infinite-state systems, 1998. To appear in the journal of Theoretical Computer Science."},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0054179","volume-title":"Proc. TACAS\u2019 98, 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. A. Abdulla","year":"1998","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying networks of timed processes. In Bernhard Steffen, editor, Proc. TACAS\u2019 98, 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 298\u2013312, 1998."},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Aletta Nyl\u00e9n. Better is better than well: On efficient verification of infinite-state systems. In Proc. 15th IEEE Int. Symp. on Logic in Computer Science, pages 132\u2013140, 2000.","DOI":"10.1109\/LICS.2000.855762"},{"issue":"3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Software Engineering, 17(3):259\u2013273, 1991.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR11","unstructured":"F. D. J. Bowden. Modelling time in Petri nets. In Proc. Second Australian-Japan Workshop on Stochastic Models, 1996."},{"issue":"2","key":"5_CR12","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"O. Burkart and B. Steffen. Composition, decomposition, and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89\u2013125, 1995.","journal-title":"Nordic Journal of Computing"},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-58201-0_56","volume-title":"Proc. ICALP\u2019 94","author":"K. \u010cer\u0101ns","year":"1994","unstructured":"K. \u010cer\u0101ns. Deciding properties of integral relational automata. In Abiteboul and Shamir, editors, Proc. ICALP\u2019 94, volume 820of Lecture Notes in Computer Science, pages 35\u201346. Springer Verlag, 1994."},{"issue":"2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"D. de Frutos Escrig, V. Valero Ruiz, and O. Marroqu\u00b4in Alonso. Decidability of properties of timed-arc Petri nets. In ICATPN 2000, number 1825, pages 187\u2013206, 2000.","DOI":"10.1007\/3-540-44988-4_12"},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Automatic Verification Methods for Finite-State Systems","author":"D.L. Dill","year":"1989","unstructured":"D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Automatic Verification Methods for Finite-State Systems, volume 407 of Lecture Notes in Computer Science. Springer Verlag, 1989."},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","first-page":"21","volume-title":"Proc. Fundementals of Computation Theory","author":"J. Esparza","year":"1995","unstructured":"J. Esparza. Petri nets, commutative context-free grammers, and basic parallel processes. In Proc. Fundementals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 221\u2013232, 1995."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3), 1994.","DOI":"10.1007\/BF02277857"},{"issue":"2","key":"5_CR19","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1109\/32.67597","volume":"17","author":"C. Ghezzi","year":"1991","unstructured":"C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezz\u00e8. A unified high-level Petri net formalism for time-critical systems. IEEE Trans. on Software Engineering, 17(2):160\u2013172, 1991.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"3","key":"5_CR20","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675\u2013735, 1992.","journal-title":"Journal of the ACM"},{"issue":"2","key":"5_CR21","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149\u2013164, 1993.","journal-title":"Formal Methods in System Design"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger. Hybrid automata with finite bisimulations. In Proc. ICALP\u2019 95, 1995.","DOI":"10.1007\/3-540-60084-1_85"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"P. Jan\u010dar. Bisimulation equivalence is decidable for one-counter processes. In Proc. ICALP\u2019 97, pages 549\u2013559, 1997.","DOI":"10.1007\/3-540-63165-8_210"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0304-3975(77)90014-7","volume":"4","author":"N. D. Jones","year":"1977","unstructured":"N. D. Jones, L. H. Landweber, and Y. E. Lyen. Complexity of some problems in Petri nets. Theoretical Computer Science, (4):277\u2013299, 1977.","journal-title":"Theoretical Computer Science"},{"key":"5_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/3-540-60218-6_26","volume-title":"Proc. CONCUR\u2019 95, 6th Int. Conf. on Concurrency Theory","author":"P. Jan\u010dar","year":"1995","unstructured":"P. Jan\u010dar and F. Moller. Checking regular properties of Petri nets. In Proc. CONCUR\u2019 95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 348\u2013362. Springer Verlag, 1995."},{"issue":"2","key":"5_CR26","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1006\/inco.1993.1069","volume":"107","author":"B. Jonsson","year":"1993","unstructured":"B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of non \u2010 finite \u2010 state programs. Information and Computation, 107(2):272\u2013302, Dec. 1993.","journal-title":"Information and Computation"},{"key":"5_CR27","first-page":"424","volume-title":"Proc. 9th Int. Conf. on Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254, pages 424\u2013435, Haifa, Israel, 1997. Springer Verlag."},{"key":"5_CR28","unstructured":"K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient timed reachability analysis using clock difference diagrams. In Proc. 11th Int. Conf. on Computer Aided Verification, 1999."},{"key":"5_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-60249-6_41","volume-title":"Model-checking for realtime systems","author":"K. G. Larsen","year":"1995","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Model-checking for realtime systems. In Horst Reichel, editor, Proceedings of 10th International Fundamentals of Computation Theory, number 965 in LNCS, pages 62\u201388, Dresden, Germany, August 1995."},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1-2), 1997.","DOI":"10.1007\/s100090050010"},{"key":"5_CR31","first-page":"1036","volume":"COM-24","author":"P. Merlin","year":"1976","unstructured":"P. Merlin and D.J. Farber. Recoverability of communication protocols-implications of a theoretical study. IEEE Trans. on Computers, COM-24:1036\u20131043, Sept. 1976.","journal-title":"IEEE Trans. on Computers"},{"key":"5_CR32","unstructured":"Jesper M\u00f8ller and Jakob Lichtenberg. Difference decision diagrams. Master\u2019s thesis, Department of Information Technology, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark, August 1998."},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Jesper M\u00f8ller, Jakob Lichtenberg, Henrik R. Andersen, and Henrik Hulgaard. Difference decision diagrams. Technical Report IT-TR-1999-023, Department of Information Technology, Technical University of Denmark, February 1999.","DOI":"10.1007\/3-540-48168-0_9"},{"key":"5_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"5th International Symposium on Programming, Turin","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In 5th International Symposium on Programming, Turin, volume 137 of Lecture Notes in Computer Science, pages 337\u2013352. Springer Verlag, 1982."},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"V. Valero Ruiz, F. Cuartero Gomez, and D. de Frutos Escrig. On nondecidability of reachability for timed-arc Petri nets. In Proceedings of the 8th Int. Workshop on Petri Net and Performance Models (PNPM\u201999), pages 188\u2013196, 1999.","DOI":"10.1109\/PNPM.1999.796565"},{"key":"5_CR36","unstructured":"R. Razouk and C. Phelps. Performance analysis using timed Petri nets. In Protocol Testing, Specification, and Verification, pages 561\u2013576, 1985."},{"key":"5_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032010","volume-title":"Real-Time: Theory in Practice","author":"F. B. Schneider","year":"1992","unstructured":"F. B. Schneider, Bloom B, and Marzullo K. Putting time into proof outlines. In de Bakker, Huizing, de Roever, and Rozenberg, editors, Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, 1992."},{"key":"5_CR38","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st IEEE Int. Symp. on Logic in Computer Science, pages 332\u2013344, June 1986."},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184\u2013193, Jan. 1986.","DOI":"10.1145\/512644.512661"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer, 1(1-2), 1997.","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Applications and Theory of Petri Nets 2001"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45740-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T11:31:11Z","timestamp":1737545471000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45740-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422525","9783540457404"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-45740-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}