{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T22:40:16Z","timestamp":1740868816279,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231677"},{"type":"electronic","value":"9783540302063"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30206-3_18","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:19:15Z","timestamp":1295345955000},"page":"246-262","source":"Crossref","is-referenced-by-count":1,"title":["Bounded Model Checking for Region Automata"],"prefix":"10.1007","author":[{"given":"Fang","family":"Yu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yao-Wen","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for Real-time Systems. In: IEEE 5th Annual Symposium on Logi In Computer Science (LICS), Philadelphia (June 1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"18_CR2","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, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-36577-X_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2003","unstructured":"Amla, N., Kurshan, R., McMillan, K., Medel, R.K.: Experimental Analysis of Different Techniques for Bounded Model Checking. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 34\u201348. Springer, Heidelberg (2003)"},{"key":"18_CR4","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_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-36135-9_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Cimatti, A., Korniowicz, A., Sebastiani, R.: Bounded Model Checking for Timed Systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 243\u2013259. Springer, Heidelberg (2002)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1994","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the Fly Model Checking of RCTL Formulas. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, Springer, Heidelberg (1994)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic Model Checking Using SAT Procedures Instead of BDDs. In: Proc. DAC 1999, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (1998)"},{"key":"18_CR9","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. In: Formal Methods in System Design (July 2001)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral Consistency of C and Verilog Programs using Bounded Model Checking. In: Proc. DAC 2003, Session 23.3, Anaheim, CA (2003)","DOI":"10.21236\/ADA461052"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"G\u00f6ll\u00fc, A., Puri, A., Varaiya, P.: Discretization of timed automata. In: Proc. of the 33rd IEEE conferene on decision and control, pp. 957\u2013958 (1994)","DOI":"10.1109\/CDC.1994.410933"},{"key":"18_CR12","doi-asserted-by":"publisher","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., Yovine, S.: Symbolic Model Checking for Real-Time Systems. Information and Computation\u00a0111, 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"18_CR13","unstructured":"Huang, Y.-W., Yu, F., Hang, C., Tsai, C.-H., Lee, D.-T., Kuo, S.-Y.: Verifying Web Applications Using Bounded Model Checking. In: Proc. DSN 2004, Italy (June 2004)"},{"key":"18_CR14","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 - and back. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 529\u2013539. Springer, Heidelberg (1995)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Wang, Y.: Compositional and Symbolic Model Checking of Real-time System. In: Proc. RTSS 1995, Pisa, Italy (1995)","DOI":"10.1109\/REAL.1995.495198"},{"issue":"1-2","key":"18_CR16","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1998","unstructured":"Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1998)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"18_CR17","unstructured":"Lu, F., Wnag, L.-C., Cheng, K.-T., Huan, R.C.-Y.: A Circuit SAT Solver With Signal Correlation Guided Learning. In: Proc. DATE 2003 (March 2003)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Moller, M.O., Rue, H., Sorea, M.: Predicate Abstraction for Dense Real-time Systems. In: Theory and Practice of Timed Systems, TPTS 2002 (2002)","DOI":"10.7146\/brics.v8i44.21704"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. DAC (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"18_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shanker, N., Sorea, M.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 496\u2013500. Springer, Heidelberg (2004)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45739-9_15","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P. Niebert","year":"2002","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Jain, N., Maler, O.: Verification of Timed Automata via Satisfiability Checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, p. 225. Springer, Heidelberg (2002)"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45739-9_17","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wozna, B., Zbrzezny, A.: Towards Bounded Model Checking for the Universal Fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 265\u2013288. Springer, Heidelberg (2002)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-45069-6_16","volume-title":"Computer Aided Verification","author":"S.A. Seshia","year":"2003","unstructured":"Seshia, S.A., Bryant, R.E.: Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 154\u2013166. Springer, Heidelberg (2003)"},{"key":"18_CR25","unstructured":"Sorea, M.: Bounded Model Checking for Timed Automata. CSL Technical Report SRICSL- 02-03 (2002)"},{"key":"18_CR26","series-title":"LNCS","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":"2","key":"18_CR27","first-page":"223","volume":"55","author":"B. Wozna","year":"2003","unstructured":"Wozna, B., Penczek, W., Zbrzezny, A.: Checking Reachability Properties for Timed Automata via SAT. Fundamenta Informaticae\u00a055(2), 223\u2013241 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"Lectures on Embedded Systems","author":"S. Yovine","year":"1998","unstructured":"Yovine, S.: Model-checking Timed Automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol.\u00a01494, Springer, Heidelberg (1998)"},{"key":"18_CR29","unstructured":"Yu, F., Wang, B.-Y.: Toward Unbounded Model Checking for Region Automata (paper submitted)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30206-3_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T22:09:19Z","timestamp":1740866959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30206-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231677","9783540302063"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30206-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}