{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:37:24Z","timestamp":1725550644804},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291077"},{"type":"electronic","value":"9783540320722"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560647_18","type":"book-chapter","created":{"date-parts":[[2005,10,20]],"date-time":"2005-10-20T14:04:06Z","timestamp":1129817046000},"page":"272-287","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Model Checking of Finite Precision Timed Automata"],"prefix":"10.1007","author":[{"given":"Rongjie","family":"Yan","sequence":"first","affiliation":[]},{"given":"Guangyuan","family":"Li","sequence":"additional","affiliation":[]},{"given":"Zhisong","family":"Tang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"18_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":"18_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: A Really Temproal Logic. In: IEEE FOCS, pp. 164\u2013169 (1989)","DOI":"10.1109\/SFCS.1989.63473"},{"key":"18_CR3","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.) HART 1997. LNCS, vol.\u00a01201, pp. 346\u2013360. Springer, Heidelberg (1997)"},{"key":"18_CR4","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., Weise, C., Wang, Y., Pearson, J.: 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":"18_CR5","volume-title":"Dynamic Programming","author":"R. Bellman","year":"1957","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"CONCUR \u201998 Concurrency Theory","author":"J. Bengtsson","year":"1998","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Wang, Y.: Partial Order Reductions for Timed System. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 485\u2013500. Springer, Heidelberg (1998)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J. Bengtsson","year":"2004","unstructured":"Bengtsson, J., Wang, Y.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"18_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"B. Berard","year":"2001","unstructured":"Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)"},{"key":"18_CR9","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":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/3-540-45251-6_30","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"D. Bosnacki","year":"2001","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: A Heuristic for Symmetry Reductions with Scalarsets. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 518\u2013533. Springer, Heidelberg (2001)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","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: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 298\u2013302. Springer, Heidelberg (1998)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-63166-6_19","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1997","unstructured":"Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some Progress in the Symbolic Verification of Timed Automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 179\u2013190. Springer, Heidelberg (1997)"},{"issue":"8","key":"18_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/10722167_9","volume-title":"Computer Aided Verification","author":"Z. Dang","year":"2000","unstructured":"Dang, Z., Ibarra, O.H., Bultan, T., Kemmerer, R.A., Su, J.: Binary Reachability Analysis of Discrete Pushdown Timed Automata. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 69\u201384. Springer, Heidelberg (2000)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C. Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 208\u2013219. Springer, Heidelberg (1996)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Daws, C., Yovine, S.: Reducing the Number of Clock Variables of Timed Automata. In: IEEE RTSS, pp.\u00a073\u201381 (1996)","DOI":"10.1109\/REAL.1996.563702"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-45739-9_1","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"B. Gerd","year":"2002","unstructured":"Gerd, B., Johan, B., Alexandre, D., Larsen, K.G., Paul, P., Wang, Y.: UPPAAL Implementation Secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 3\u201322. Springer, Heidelberg (2002)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-40903-8_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Hendriks","year":"2004","unstructured":"Hendriks, M., Behrmann, G., Larsen, K.G., Vaandrager, F.: Adding Symmetry Reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 46\u201359. Springer, Heidelberg (2004)"},{"issue":"1","key":"18_CR19","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 Transactions on Computer Systems\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Transactions on Computer Systems"},{"issue":"1\/2","key":"18_CR20","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., Wang, Y.: 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":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0035387","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.F. Raskin","year":"1997","unstructured":"Raskin, J.F., Schoebbens, P.: Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 165\u2013182. Springer, Heidelberg (1997)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-46419-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Wang","year":"2000","unstructured":"Wang, F.: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 157\u2013171. Springer, Heidelberg (2000)"},{"key":"18_CR23","unstructured":"Wang, F.: Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems. In: COMPSAC, pp. 509\u2013515 (2000)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-36384-X_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Wang","year":"2002","unstructured":"Wang, F.: Efficient Verification of Timed Automata with BDD-like Data-Structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 189\u2013205. Springer, Heidelberg (2002)"},{"issue":"8","key":"18_CR25","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.1109\/JPROC.2004.831197","volume":"92","author":"F. Wang","year":"2004","unstructured":"Wang, F.: Formal Verification of Timed Systems: A Survery and Perspective. Proceedings of the IEEE\u00a092(8), 1283\u20131307 (2004)","journal-title":"Proceedings of the IEEE"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2005"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560647_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T11:07:57Z","timestamp":1586516877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560647_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291077","9783540320722"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11560647_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}