{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:23:37Z","timestamp":1755221017682,"version":"3.43.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Real-Time Systems"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1023\/a:1025132427497","type":"journal-article","created":{"date-parts":[[2003,9,16]],"date-time":"2003-09-16T18:25:03Z","timestamp":1063736703000},"page":"255-275","source":"Crossref","is-referenced-by-count":17,"title":["Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems"],"prefix":"10.1007","volume":"25","author":[{"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[]},{"given":"Fredrik","family":"Larsson","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5140374_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., and Lamport, L. 1992. An old-fashioned recipe for real time. In Proceedings of REX Workshop Real-Time: Theory in Practice. LNCS No. 600.","DOI":"10.1007\/BFb0031985"},{"key":"5140374_CR2","series-title":"LNCS","first-page":"263","volume-title":"Proceedings of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Aceto","year":"1998","unstructured":"Aceto, L., Bergueno, A., and Larsen, K. G. 1998. Model checking via reachability testing for timed automata. In Bernard Steffen (ed.), Proceedings of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, No. 1384, Berlin: Spring-Verlag, pp. 263\u2013280."},{"issue":"2","key":"5140374_CR3","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"A. V. Aho","year":"1972","unstructured":"Aho, A. V., Garey, M. R., and Ullman, J. D. 1972. The transitive reduction of a directed graph. SIAM Journal on Computing 1(2): 131\u2013137.","journal-title":"SIAM Journal on Computing"},{"key":"5140374_CR4","series-title":"LNCS","first-page":"332","volume-title":"Proc. Of Int. Colloquium on Algorithms, Languages and Programming","author":"R. Alur","year":"1990","unstructured":"Alur, R., and Dill, D. 1990. Automata for modeling real-time systems. In Proc. Of Int. Colloquium on Algorithms, Languages and Programming. LNCS, No. 443, Berlin: Springer-Verlag, pp. 332\u2013335."},{"key":"5140374_CR5","doi-asserted-by":"crossref","unstructured":"Andersen, H. R. 1995. Partial model checking. In Proceedings of Symp. on Logic in Computer Science, pp. 398\u2013407.","DOI":"10.1109\/LICS.1995.523274"},{"key":"5140374_CR6","doi-asserted-by":"crossref","unstructured":"Asarin, E., Maler, O., and Pneuli, A. 1997. Data-structures for the verification of timed automata. In Proceedings of the International Workshop on Hybrid and Real-Time Systems.","DOI":"10.1007\/BFb0014737"},{"key":"5140374_CR7","unstructured":"Bellman, R. 1957. Dynamic Programming. Princeton University Press."},{"key":"5140374_CR8","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Griffioen, W. O. D., Kristoffersen, K. J., Larsen, K. G., Larsson, F., Pettersson, P., and Yi, W. 1996. Verification of an audio protocol with bus collision using UPPAAL. In R. Alur and T. A. Henzinger (eds), Proceedings of the 8th International Conference on Computer Aided Verification. LNCS, No. 697.","DOI":"10.1007\/3-540-61474-5_73"},{"key":"5140374_CR9","unstructured":"Clarke, E. M., Gr\u00fcmberg, O., and Long, D. E. 1992. Model checking and abstraction. In Principles of Programming Languages, pp. 450\u2013462."},{"key":"5140374_CR10","doi-asserted-by":"crossref","unstructured":"Daws C., and Yovine, S. 1995. Two examples of verification of multirate timed automata with KRONOS. In Proceedings of the 16th IEEE Real-Time Systems Symposium, pp. 66\u201375.","DOI":"10.1109\/REAL.1995.495197"},{"key":"5140374_CR11","series-title":"LNCS","first-page":"197","volume-title":"Proceeding of Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1989","unstructured":"Dill, D. 1989. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis (ed.), Proceeding of Automatic Verification Methods for Finite State Systems. LNCS, No. 407, Berlin. Springer-Verlag, 197\u2013212."},{"key":"5140374_CR12","unstructured":"Emerson E. A., and Jutla, C. S. 1993. Symmetry and model checking. In Proceedings of the 5th International Conference on Computer Aided Verification. LNCS, No. 697."},{"key":"5140374_CR13","doi-asserted-by":"crossref","unstructured":"Godefroid P., and Wolper, P. 1991. A partial approach to model checking. In Proceedings of IEEE Symposium on Logic in Computer Science, pp. 406\u2013415.","DOI":"10.1109\/LICS.1991.151664"},{"key":"5140374_CR14","doi-asserted-by":"crossref","unstructured":"Havelund, K., Skou, A., Larsen, K. G., and Lund, K. 1997. Formal modeling and analysis of an audio\/video protocol: An industrial case study using UPPAAL. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pp. 2\u201313.","DOI":"10.1109\/REAL.1997.641264"},{"key":"5140374_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T. A., Ho, P.-H., and W-Toi, H. 1995 A users guide to HYTECH. Technical Report, Department of Computer Science, Cornell University.","DOI":"10.1007\/3-540-60630-0_3"},{"issue":"2","key":"5140374_CR16","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"Henzinger, T. A., Nicollin, X., Sifakis, J., and Yovine, S. 1994. Symbolic Model Checking for Real Time Systems. Information and Computation 111(2): 193\u2013244.","journal-title":"Information and Computation"},{"key":"5140374_CR17","unstructured":"Holzmann, G. 1991. The Design and Validation of Computer Protocols. Prentice Hall."},{"key":"5140374_CR18","doi-asserted-by":"crossref","unstructured":"Kristoffersen, K. J., Larroussinie, F., Larsen, K. G., Pettersson, P., and Yi, W. 1997. A compositional proof of a real-time mutual exclusion protocol. In Proceedings of the 7th International Joint Conference on the Theory and Practice of Software Development, pp. 565\u2013579.","DOI":"10.1007\/BFb0030626"},{"key":"5140374_CR19","doi-asserted-by":"crossref","unstructured":"Larsen, K. G. Petterson, P., and Yi, W. 1995. Compositional and symbolic model-checking of real-time systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pp. 76\u201387.","DOI":"10.1109\/REAL.1995.495198"},{"key":"5140374_CR20","series-title":"LNCS","first-page":"575","volume-title":"Proceedings of Workshop on Verification and Control of Hybrid Systems III","author":"K. G. Larsen","year":"1995","unstructured":"Larsen, K. G. Petterson, P., and Yi, W. 1995. Diagnostic model-checking for real-time systems. In Proceedings of Workshop on Verification and Control of Hybrid Systems III. LNCS, No. 1066, Berlin, Springer-Verlag, 575\u2013586."},{"issue":"1-2","key":"5140374_CR21","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"Larsen, K. G., Pettersson, P., and Yi, W. 1997. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1(1-2): 134\u2013152.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"5140374_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/3-540-61648-9_49","volume-title":"Proceeding of Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P. Pagani","year":"1996","unstructured":"Pagani, P. 1996. Partial orders and verification of real-time systems. In Bengt Jonsson and Joachim Parrow (eds), Proceeding of Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, No. 1135, Berlin: Springer-Verlag, pp. 327\u2013346."},{"key":"5140374_CR23","unstructured":"Papadimitriou, C. H. 1994. Computational Complexity. Addison-Wesley."},{"key":"5140374_CR24","series-title":"LNCS","volume-title":"Hybrid Systems Workshop","author":"A. Puri","year":"1994","unstructured":"Puri, A., and Varaiya, P. 1994. Verification of hybrid systems using abstractions. In Hybrid Systems Workshop. LNCS, No. 818, Berlin, Springer-Verlag."},{"key":"5140374_CR25","unstructured":"Sedgewick, R. 1993. Algorithms. 2nd edn, Addison-Wesley, 1988."},{"key":"5140374_CR26","series-title":"LNCS","volume-title":"Proceedings of the 5th International Conference on Computer Aided Verification","author":"N. Shankar","year":"1993","unstructured":"Shankar, N. 1993. Verification of real-time systems using PVS. In Proceedings of the 5th International Conference on Computer Aided Verification. LNCS, No. 697, Berlin, Springer-Verlag."},{"key":"5140374_CR27","doi-asserted-by":"crossref","unstructured":"Valmari, A. 1990. A stubborn attack on state explosion. Theoretical Computer Science 3.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"5140374_CR28","unstructured":"Vardi, M. Y., and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of Symposium on Logic in Computer Science, pp. 322\u2013331."},{"key":"5140374_CR29","doi-asserted-by":"crossref","unstructured":"Yannakakis, M., and Lee, D. 1993. An efficient algorithm for minimizing real-time transition systems. In Proceedings of the 5th International Conference on Computer Aided Verification, LNCS, No. 697, pp. 210\u2013224.","DOI":"10.1007\/3-540-56922-7_18"},{"key":"5140374_CR30","unstructured":"Yi, W., Pettersson, P., and Daniels, M. 1994. Automatic verification of real-time communicating systems by constraint-solving. In Proceedings of the 7th International Conference on Formal Description Techniques, pp. 223\u2013238."}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025132427497.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1025132427497\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025132427497.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T07:24:08Z","timestamp":1754637848000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1025132427497"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":30,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["5140374"],"URL":"https:\/\/doi.org\/10.1023\/a:1025132427497","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"type":"print","value":"0922-6443"},{"type":"electronic","value":"1573-1383"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}