{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T19:28:24Z","timestamp":1790969304879,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540643562","type":"print"},{"value":"9783540697534","type":"electronic"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054179","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:43:43Z","timestamp":1153979023000},"page":"298-312","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":38,"title":["Verifying networks of timed processes"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"20_CR1","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":"20_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho. Hybrid automata: An algorithmic approach to the specification and verificationof hybrid systems. In Grossman, Nerode, Ravn, and Rischel, editors, Hybrid Systems, number 736 in Lecture Notes in Computer Science, pages 209\u2013229, 1992.","DOI":"10.1007\/3-540-57318-6_30"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis \u010der\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.","DOI":"10.1109\/LICS.1996.561359"},{"issue":"2","key":"20_CR4","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":"20_CR5","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Mats Kindahl. Decidability of simulation and bisimulation between lossy channel systems and finite state systems. In Lee and Smolka, editors, Proc. CONCUR '95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 333\u2013347. Springer Verlag, 1995.","DOI":"10.1007\/3-540-60218-6_25"},{"issue":"3","key":"20_CR6","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"},{"issue":"2","key":"20_CR7","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":"20_CR8","doi-asserted-by":"crossref","unstructured":"K. \u010der\u0101ns. Deciding properties of integral relational automata. In Abiteboul and Shamir, editors, Proc. ICALP '94, volume 820 of Lecture Notes in Computer Science, pages 35\u201346. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58201-0_56"},{"issue":"2","key":"20_CR9","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":"20_CR10","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In Lee and Smolka, editors, Proc. CONCUR '95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 395\u2013407. Springer Verlag, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144\u2013179, 1990.","journal-title":"Information and Computation"},{"issue":"2","key":"20_CR12","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"},{"key":"20_CR13","unstructured":"J.C. Godskesen. Timed Modal Specifications. PhD thesis, Aalborg University, 1994."},{"issue":"3","key":"20_CR14","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"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger. Hybrid automata with finite bisimulations. In Proc. ICALP '95, 1995.","DOI":"10.1007\/3-540-60084-1_85"},{"key":"20_CR16","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc, 2:326\u2013336, 1952.","journal-title":"Proc. London Math. Soc"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"P. Jancar and F. Moller. Checking regular properties of Petri nets. In Proc. CONCUR '95, 6th Int. Conf. on Concurrency Theory, pages 348\u2013362, 1995.","DOI":"10.1007\/3-540-60218-6_26"},{"issue":"2","key":"20_CR18","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-finite-state programs. Information and Computation, 107(2):272\u2013302, Dec. 1993.","journal-title":"Information and Computation"},{"key":"20_CR19","volume-title":"Lecture Notes in Computer Science","author":"K.J. Kristoffersen","year":"1997","unstructured":"K.J. Kristoffersen, F. Larroussinie, K. G. Larsen, P. Pettersson, and W. Yi. A compositional proof of a real-time mutual exclusion protocol. In TAP-SOFT '97 7th International Joint Conference on the Theory and Practice of Software Development, Lecture Notes in Computer Science, Lille, France, April 1997. Springer Verlag."},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In Proc. 8th ACM Symp. on Principles of Distributed Computing, Canada, pages 239\u2013247, Edmonton, Alberta, 1989.","DOI":"10.1145\/72981.72998"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, B. Steffen, and C. Weise. Fischer's protocol revisited: a simples proof using modal constraints. In 4th DIM ACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, Oct. 1995.","DOI":"10.1007\/BFb0020979"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"F. B. Schneider, Bloom B, and Marzullo K. Putting time into proof outlines. In de Bakker, Huizing, de Roever, and Rozenberg, editors, RealTime: Theory in Practice, volume 600 of Lecture Notes in Computer Science, 1992.","DOI":"10.1007\/BFb0032010"},{"key":"20_CR23","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":"20_CR24","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in prepositional 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":"20_CR25","unstructured":"Wang Yi. CCS + Time = an interleaving model for real time systems. In Leach Albert, Monien, and Rodriguez Artalejo, editors, Proc. ICALP '91, volume 510 of Lecture Notes in Computer Science. Springer Verlag, 1991."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054179","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T03:07:37Z","timestamp":1736478457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054179"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643562","9783540697534"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0054179","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}