{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:49:05Z","timestamp":1742950145617,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291893"},{"type":"electronic","value":"9783540320845"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"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":[[2005]]},"DOI":"10.1007\/11562436_8","type":"book-chapter","created":{"date-parts":[[2005,10,19]],"date-time":"2005-10-19T09:40:51Z","timestamp":1129714851000},"page":"83-97","source":"Crossref","is-referenced-by-count":11,"title":["Fast Generic Model-Checking for Data-Based Systems"],"prefix":"10.1007","author":[{"given":"Dezhuang","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: RTSS 1992 (1992)","DOI":"10.1109\/REAL.1992.242667"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Model checking and boolean graphs. Theoretical Computer Science\u00a0126(1) (1994)","DOI":"10.1016\/0304-3975(94)90266-6"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Balarin, F.: Approximate reachability analysis of timed automata. In: IEEE RTSS 1996 (1996)","DOI":"10.1109\/REAL.1996.563700"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Uppaal implementation secrets. In: FTRTFT 2002 (2002)","DOI":"10.1007\/3-540-45739-9_1"},{"key":"8_CR5","unstructured":"Berezin, S.: Model Checking and Theorem Proving: a Unified Framework. PhD thesis, Carnegie Mellon University (2002)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_39"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the 5th IEEE Symposium on Logic in Computer Science, Philadelphia, PA, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"8_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/978-3-540-48654-1_31","volume-title":"CONCUR 1994: Concurrency Theory","author":"R. Cleaveland","year":"1994","unstructured":"Cleaveland, R., Riely, J.: Testing-based abstractions for concurrent systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 417\u2013432. Springer, Heidelberg (1994)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/3-540-55179-4_6","volume-title":"Computer Aided Verification","author":"R. Cleaveland","year":"1992","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternationfree modal mu-calculus. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 48\u201358. Springer, Heidelberg (1992)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"8_CR13","doi-asserted-by":"crossref","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. Springer, Heidelberg (1996)","DOI":"10.1007\/BFb0020947"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1989","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, Springer, Heidelberg (1989)"},{"key":"8_CR15","unstructured":"Du, X., Ramakrishnan, C.R., Smolka, S.A.: Tabled resolution + constraints: A recipe for model checking real-time systems. In: RTSS 2000 (2000)"},{"key":"8_CR16","unstructured":"Groote, J.F., Willemse, T.A.C.: A checker for modal formulas for processes with data. Technical report, Technische Universiteit Eindhoven, The Neitherlands (2002)"},{"issue":"4","key":"8_CR17","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BF01178384","volume":"32","author":"M. Hennessy","year":"1995","unstructured":"Hennessy, M., Liu, X.: A modal logic for message passing processes. Acta Informatica\u00a032(4), 375\u2013393 (1995)","journal-title":"Acta Informatica"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for realtime systems. Information and Computation\u00a0111(2) (1994)","DOI":"10.1006\/inco.1994.1045"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(92)90183-G","volume":"96","author":"J. Bradfield","year":"1992","unstructured":"Bradfield, J., Stirling, C.: Local model checking for infinite state spaces. Theoretical Computer Science\u00a096, 157\u2013174 (1992)","journal-title":"Theoretical Computer Science"},{"key":"8_CR20","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 nutshel. Software Tools for Technology Transfer\u00a01, 134\u2013152 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-61604-7_47","volume-title":"CONCUR 1996: Concurrency Theory","author":"H. Lin","year":"1996","unstructured":"Lin, H.: Symbolic graphs with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 50\u201365. Springer, Heidelberg (1996)"},{"key":"8_CR22","unstructured":"Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, M\u00fcchen, Techn-Univ. (1997)"},{"key":"8_CR23","unstructured":"Mateescu, R.: Local model-checking of an alternation-free value-based modal mu-calculus. In: VMCAI 1998 (September 1998)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137. Springer, Heidelberg (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45241-9_1","volume-title":"Practical Aspects of Declarative Languages","author":"C.R. Ramakrishnan","year":"2001","unstructured":"Ramakrishnan, C.R.: A model checker for value-passing mu-calculus using logic programming. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol.\u00a01990, p. 1. Springer, Heidelberg (2001)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Rathke, J., Hennessy, M.: Local model checking for value-passing processes. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281. Springer, Heidelberg (1997)","DOI":"10.1007\/BFb0014555"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Sokolsky, O., Smolka, S.: Local model checking for real-time systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60045-0_52"},{"key":"8_CR28","unstructured":"Szalas, A.: Logic for computer science. lecture notes, http:\/\/www.ida.liu.se\/~andsz"},{"key":"8_CR29","doi-asserted-by":"crossref","first-page":"81","DOI":"10.3233\/FI-1996-2616","volume":"26","author":"A. Sza\u0142as","year":"1996","unstructured":"Sza\u0142as, A.: On natural deduction in first-order fixpoint logics. Fundamenta Informaticae\u00a026, 81\u201394 (1996)","journal-title":"Fundamenta Informaticae"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-45657-0_37","volume-title":"Computer Aided Verification","author":"L. Tan","year":"2002","unstructured":"Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 455. Springer, Heidelberg (2002)"},{"key":"8_CR31","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)"},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: A verification tool for real-time systems. Software Tools for Technology Transfer\u00a01, 123\u2013133 (1997)","journal-title":"Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems - FORTE 2005"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11562436_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T01:44:39Z","timestamp":1736041479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11562436_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291893","9783540320845"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11562436_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}