{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:41:19Z","timestamp":1777347679857,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540857778","type":"print"},{"value":"9783540857785","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85778-5_17","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T17:32:04Z","timestamp":1220031124000},"page":"233-249","source":"Crossref","is-referenced-by-count":17,"title":["Compositional Abstraction in Real-Time Model Checking"],"prefix":"10.1007","author":[{"given":"Jasper","family":"Berendsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"17_CR2","first-page":"481","volume-title":"Proceedings 2 nd Joint Conference on Artificial Intelligence","author":"R. Milner","year":"1971","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings 2 nd Joint Conference on Artificial Intelligence, pp. 481\u2013489. British Computer Society Press, London (1971)"},{"key":"#cr-split#-17_CR3.1","doi-asserted-by":"crossref","unstructured":"Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the 6 th Annual ACM Symposium on Principles of Distributed Computing, August 1987, pp. 137\u2013151 (1987);","DOI":"10.1145\/41840.41852"},{"key":"#cr-split#-17_CR3.2","unstructured":"A full version is available as MIT Technical Report MIT\/LCS\/TR-387"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-54430-5_99","volume-title":"CONCUR \u201991","author":"B. Jonsson","year":"1991","unstructured":"Jonsson, B.: Simulations between specifications of distributed systems. In: Baeten, J., Groote, J. (eds.) CONCUR 1991. LNCS, vol.\u00a0527, pp. 346\u2013360. Springer, Heidelberg (1991)"},{"issue":"2","key":"17_CR5","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science\u00a082(2), 253\u2013284 (1991)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations, I: Untimed systems. Information and Computation\u00a0121(2), 214\u2013233 (1995)","journal-title":"Information and Computation"},{"key":"17_CR7","unstructured":"Jensen, H.: Abstraction-Based Verification of Distributed Systems. PhD thesis, Department of Computer Science, Aalborg University, Denmark (June 1999)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45352-0_4","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"H. Jensen","year":"2000","unstructured":"Jensen, H., Larsen, K., Skou, A.: Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol.\u00a01926, Springer, Heidelberg (2000)"},{"issue":"4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1145\/1024922.1024923","volume":"5","author":"W. Griffioen","year":"2004","unstructured":"Griffioen, W., Vaandrager, F.: A theory of normed simulations. ACM Transactions on Computational Logic\u00a05(4), 577\u2013610 (2004)","journal-title":"ACM Transactions on Computational Logic"},{"key":"17_CR10","unstructured":"Frehse, G.: Compositional Verification of Hybrid Systems using Simulation Relations. PhD thesis, Radboud University Nijmegen (October 2005)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Kaynar, D., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I\/O Automata. Synthesis Lecture on Computer Science, p. 101. Morgan & Claypool Publishers (2006) ISBN 159829010X","DOI":"10.1007\/978-3-031-01794-0"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1145\/1176887.1176923","volume-title":"Proceedings 6th Annual ACM & IEEE Conference on Embedded Software (EMSOFT 2006)","author":"B. Gebremichael","year":"2006","unstructured":"Gebremichael, B., Vaandrager, F., Zhang, M.: Analysis of the Zeroconf protocol using Uppaal. In: Proceedings 6th Annual ACM & IEEE Conference on Embedded Software (EMSOFT 2006), Seoul, South Korea, October 22-25, 2006, pp. 242\u2013251. ACM Press, New York (2006)"},{"issue":"3","key":"17_CR13","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"17_CR14","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive Modules. Formal Methods in System Design\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"key":"17_CR15","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/BFb0020971","volume-title":"Hybrid Systems III","author":"N. Lynch","year":"1996","unstructured":"Lynch, N., Segala, R., Vaandrager, F., Weinberg, H.: Hybrid I\/O automata. In: Alur, R., Henzinger, T., Sontag, E. (eds.) Hybrid Systems III. LNCS, vol.\u00a01066, pp. 496\u2013510. Springer, Heidelberg (1996)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF01221097","volume":"6","author":"J. Groote","year":"1994","unstructured":"Groote, J., Ponse, A.: Process algebra with guards. Combining Hoare logic with process algebra. Formal Aspects of Computing\u00a06, 115\u2013164 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"17_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11559306_5","volume-title":"Frontiers of Combining Systems","author":"L. Alfaro de","year":"2005","unstructured":"de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 81\u2013105. Springer, Heidelberg (2005)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-540-71493-4_45","volume-title":"Hybrid Systems: Computation and Control","author":"D.A. Beek van","year":"2007","unstructured":"van Beek, D.A., Reniers, M.A., Schiffelers, R.R.H., Rooda, J.E.: Foundations of a compositional interchange format for hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 587\u2013600. Springer, Heidelberg (2007)"},{"key":"17_CR20","unstructured":"Berendsen, J., Vaandrager, F.: Parallel composition in a paper of Jensen, Larsen and Skou is not associative. Technical note (September 2007), http:\/\/www.ita.cs.ru.nl\/publications\/papers\/fvaan\/BV07.html"},{"key":"17_CR21","unstructured":"Berendsen, J., Vaandrager, F.: Parallel composition in a paper by De Alfaro e.a. is not associative. Technical note available electronically (May 2008), http:\/\/www.ita.cs.ru.nl\/publications\/papers\/fvaan\/BV07.html"},{"key":"17_CR22","series-title":"IFIP Conference Proceedings","first-page":"321","volume-title":"FORTE","author":"G. Bhat","year":"1997","unstructured":"Bhat, G., Cleaveland, R., L\u00fcttgen, G.: Dynamic priorities for modeling real-time. In: Togashi, A., Mizuno, T., Shiratori, N., Higashino, T. (eds.) FORTE. IFIP Conference Proceedings, vol.\u00a0107, pp. 321\u2013336. Chapman & Hall, Boca Raton (1997)"},{"issue":"2","key":"17_CR23","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/S0304-3975(97)00221-1","volume":"195","author":"R. Cleaveland","year":"1998","unstructured":"Cleaveland, R., L\u00fcttgen, G., Natarajan, V.: A process algebra with distributed priorities. Theor. Comput. Sci.\u00a0195(2), 227\u2013258 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/3-540-44685-0_21","volume-title":"CONCUR 2001 - Concurrency Theory","author":"I. Phillips","year":"2001","unstructured":"Phillips, I.: CCS with priority guards. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 305\u2013320. Springer, Heidelberg (2001)"},{"issue":"1","key":"17_CR25","first-page":"1","volume":"111","author":"L. Aceto","year":"1994","unstructured":"Aceto, L., Bloom, B., Vaandrager, F.: Turning SOS rules into equations. LICS 1992 Special Issue of Information and Computation\u00a0111(1), 1\u201352 (1994)","journal-title":"LICS 1992 Special Issue of Information and Computation"},{"key":"17_CR26","unstructured":"Berendsen, J., Gebremichael, B., Vaandrager, F., Zhang, M.: Formal specification and analysis of zeroconf using Uppaal. Report ICIS-R07032, Institute for Computing and Information Sciences, Radboud University Nijmegen (December 2007)"},{"key":"17_CR27","unstructured":"Berendsen, J., Vaandrager, F.: Compositional abstraction in real-time model checking. Technical Report ICIS\u2013R07027, Institute for Computing and Information Sciences, Radboud University Nijmegen (2007), http:\/\/www.ita.cs.ru.nl\/publications\/papers\/fvaan\/BV07.html"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-48683-6_2","volume-title":"Computer Aided Verification","author":"J. Sifakis","year":"1999","unstructured":"Sifakis, J.: The compositional specification of timed systems - a tutorial. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 2\u20137. Springer, Heidelberg (1999)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-48778-6_20","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"H. Bowman","year":"1999","unstructured":"Bowman, H.: Modelling timeouts without timelocks. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, p. 20. Springer, Heidelberg (1999)"},{"issue":"3","key":"17_CR30","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.: Model checking and modular verification. ACM Trans. Program. Lang. Syst.\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Wachter","year":"2007","unstructured":"Wachter, B., Westphal, B.: The Spotlight Principle: On Process-Summarizing State Abstractions. In: Podelski, A., Cook, B. (eds.) VMCAI 2007. LNCS, vol.\u00a04349. Springer, Heidelberg (2007)"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 66\u201380. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85778-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T19:54:10Z","timestamp":1684526050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85778-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540857778","9783540857785"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85778-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}