{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:32:16Z","timestamp":1742916736430,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540731955"},{"type":"electronic","value":"9783540731962"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73196-2_13","type":"book-chapter","created":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T04:50:02Z","timestamp":1183697402000},"page":"196-210","source":"Crossref","is-referenced-by-count":0,"title":["Improvements for the Symbolic Verification of Timed Automata"],"prefix":"10.1007","author":[{"given":"Rongjie","family":"Yan","sequence":"first","affiliation":[]},{"given":"Guangyuan","family":"Li","sequence":"additional","affiliation":[]},{"given":"Wenliang","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Yunquan","family":"Peng","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/BFb0055642","volume-title":"CONCUR \u201998 Concurrency Theory","author":"E. Asarin","year":"1998","unstructured":"Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 470\u2013484. Springer, London (1998)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Computer Aided Verification, pp. 341\u2013353 (1999)","DOI":"10.1007\/3-540-48683-6_30"},{"key":"13_CR4","volume-title":"Dynamic Programming","author":"R. Bellman","year":"1957","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45251-6_18","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"D. Beyer","year":"2001","unstructured":"Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 318\u2013343. Springer, Heidelberg (2001)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 122\u2013125. Springer, Heidelberg (2003)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-39979-7_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Noack, A.: Can decision diagrams overcome state space explosion in real-time verification? In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol.\u00a02767, pp. 193\u2013208. Springer, Heidelberg (2003)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 546\u2013550. Springer, Heidelberg (1998)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data structures for the verification of timed automata. In: Maler, O. (ed.) Hybrid and Real-Time Systems, Grenoble, France. LNCS, pp. 346\u2013360. Springer Verlag, Heidelberg (1997)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Goll\u00fc, A., Puri, A., Varaiya, P.: Discetization of timed automata. In: Proceedings of the 33rd IEEE conferene on decision and control, pp. 957\u2013958 (1994)","DOI":"10.1109\/CDC.1994.410933"},{"key":"13_CR11","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/REAL.1997.641264","volume-title":"Proc. of the 18th IEEE Real-Time Systems Symposium","author":"K. Havelund","year":"1997","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio\/video protocol: An industrial case study using UPPAAL. In: Proc. of the 18th IEEE Real-Time Systems Symposium, pp. 2\u201313. IEEE Computer Society Press, Los Alamitos (1997)"},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst.\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"1-2","key":"13_CR13","doi-asserted-by":"publisher","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. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BFb0054178","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Lindahl","year":"1998","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gear controller. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, pp. 281\u2013297. Springer, Heidelberg (1998)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Computer Science Logic","author":"J. M\u00f8ller","year":"1999","unstructured":"M\u00f8ller, J., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 111\u2013125. Springer, Heidelberg (1999)"},{"key":"13_CR16","first-page":"189","volume-title":"VMCAI 2003","author":"F. Wang","year":"2003","unstructured":"Wang, F.: Efficient verification of timed automata with bdd-like data-structures. In: VMCAI 2003. Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, London, UK, pp. 189\u2013205. Springer-Verlag, Heidelberg (2003)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11560647_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"R. Yan","year":"2005","unstructured":"Yan, R., Li, G., Tang, Z.: Symbolic model checking of finite precision timed automata. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 272\u2013287. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73196-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T06:50:42Z","timestamp":1737183042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73196-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540731955","9783540731962"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73196-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}