{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:59:09Z","timestamp":1725562749515},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642153488"},{"type":"electronic","value":"9783642153495"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15349-5_2","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T03:39:27Z","timestamp":1282361967000},"page":"24-28","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic and Compositional Reachability for Timed Automata"],"prefix":"10.1007","author":[{"given":"Kim Guldstrand","family":"Larsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2001","unstructured":"Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 49\u201362. Springer, Heidelberg (2001)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/3-540-44585-4_46","volume-title":"Computer Aided Verification","author":"Y. Abdedda\u00efm","year":"2001","unstructured":"Abdedda\u00efm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 478\u2013492. Springer, Heidelberg (2001)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-36577-X_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 254\u2013277. Springer, Heidelberg (2003)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-540-24730-2_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 312\u2013326. Springer, Heidelberg (2004)"},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G. Behrmann","year":"2006","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. STTT\u00a08(3), 204\u2013215 (2006)","journal-title":"STTT"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Software \u2013 Practice and Experience (to appear, 2010)","DOI":"10.1002\/spe.1006"},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/S0019-9958(58)80003-0","volume":"1","author":"R. Bellman","year":"1958","unstructured":"Bellman, R.: Dynamic programming and stochastic control processes. Information and Control\u00a01(3), 228\u2013239 (1958)","journal-title":"Information and Control"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 147\u2013161. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"2_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2008.05.002","volume":"77","author":"A.W. Brekling","year":"2008","unstructured":"Brekling, A.W., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Log. Algebr. Program.\u00a077(1-2), 1\u201319 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-49059-0_12","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Andersen, H.R., Hulgaard, H., Lind-Nielsen, J.: Verification of hierarchical state\/event systems using reusability and compositionality. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 163\u2013177. Springer, Heidelberg (1999)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"CONCUR 2000 - Concurrency Theory","author":"F. Cassez","year":"2000","unstructured":"Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 138\u2013152. Springer, Heidelberg (2000)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"2_CR15","series-title":"Computational Analysis, Synthesis, and Design of Dynamic Systems","volume-title":"Model-Based Design for Embedded Systems","author":"A. David","year":"2009","unstructured":"David, A., Larsen, K.G., Illum, J., Skou, A.: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1. In: Model-Based Design for Embedded Systems. Computational Analysis, Synthesis, and Design of Dynamic Systems. CRC Press, Boca Raton (2009)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-540-75221-9_13","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"M.R. Hansen","year":"2007","unstructured":"Hansen, M.R., Madsen, J., Brekling, A.W.: Semantics and verification of a language for modelling hardware architectures. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol.\u00a04700, pp. 300\u2013319. Springer, Heidelberg (2007)"},{"issue":"6","key":"2_CR17","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1007\/s10009-006-0025-7","volume":"8","author":"M. Hendriks","year":"2006","unstructured":"Hendriks, M., van den Nieuwelaar, B., Vaandrager, F.W.: Model checker aided design of a controller for a wafer scanner. STTT\u00a08(6), 633\u2013647 (2006)","journal-title":"STTT"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-85778-5_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G. Igna","year":"2008","unstructured":"Igna, G., Kannan, V., Yang, Y., Basten, T., Geilen, M., Vaandrager, F.W., Voorhoeve, M., de Smet, S., Somers, L.J.: Formal modeling and scheduling of datapaths of digital document printers. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 170\u2013187. Springer, Heidelberg (2008)"},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1007\/978-0-387-35394-4_27","volume-title":"Proc. IFIP Joint Int. Conf. on Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV\u201998)","author":"F. Laroussinie","year":"1998","unstructured":"Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model-checking of real-time systems. In: Proc. IFIP Joint Int. Conf. on Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV\u201998), pp. 439\u2013456. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"2_CR20","first-page":"439","volume-title":"FORTE, IFIP Conference Proceedings","author":"F. Laroussinie","year":"1998","unstructured":"Laroussinie, F., Larsen, K.G.: Cmc: A tool for compositional model-checking of real-time systems. In: Budkowski, S., Cavalli, A.R., Najm, E. (eds.) FORTE, IFIP Conference Proceedings, vol.\u00a0135, pp. 439\u2013456. Kluwer, Dordrecht (1998)"},{"key":"2_CR21","first-page":"14","volume-title":"IEEE Real-Time Systems Symposium","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: IEEE Real-Time Systems Symposium, pp. 14\u201324. IEEE Computer Society, Los Alamitos (1997)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/3-540-60246-1_158","volume-title":"Mathematical Foundations of Computer Science 1995","author":"F. Laroussinie","year":"1995","unstructured":"Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic \u2013 and back. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 529\u2013539. Springer, Heidelberg (1995)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0054173","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Lind-Nielsen","year":"1998","unstructured":"Lind-Nielsen, J., Andersen, H.R., Behrmann, G., Hulgaard, H., Kristoffersen, K. J., Larsen, K.G.: Verification of large state\/event systems using compositionality and dependency analysis. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 201\u2013216. Springer, Heidelberg (1998)"},{"issue":"1-2","key":"2_CR24","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., Yi, W.: Uppaal in a nutshell. STTT\u00a01(1-2), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"2_CR25","unstructured":"Nyman, U.: Compositional bachwards reachability of timed automata. Master\u2019s thesis, Department of Computer Science, Aalborg University (2002)"},{"key":"2_CR26","unstructured":"Poulsen, D.B., van Vliet, J.W.B.P.T.: Concrete traces for uppaal. Master\u2019s thesis, Department of Computer Science. Aalborg University (2010)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-61474-5_72","volume-title":"Computer Aided Verification","author":"S. Tripakis","year":"1996","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems based on time-abstracting bisimulation. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 232\u2013243. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15349-5_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:04:55Z","timestamp":1606187095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15349-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642153488","9783642153495"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15349-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}