{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:05:14Z","timestamp":1725573914927},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540216711"},{"type":"electronic","value":"9783540409038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-40903-8_4","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:37:38Z","timestamp":1294414658000},"page":"34-45","source":"Crossref","is-referenced-by-count":5,"title":["Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently"],"prefix":"10.1007","author":[{"given":"Jianhua","family":"Zhao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tao","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoliang","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 456\u2013459. Springer, Heidelberg (1997)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (1996)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.-H.: Hytech: The Cornell hybrid technology tool. In: Proc. of Workshop on Tools and Algorithms for the Construction and Analysis of Systems, BRICS report series NS-95-2 (1995)","DOI":"10.1007\/3-540-60472-3_14"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Wang-Toi, H.: Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Stanford University (1994)","DOI":"10.1142\/9789812831583_0007"},{"key":"4_CR5","volume-title":"Proc. of the 18th 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 Structures and State-Space Reduction. In: Proc. of the 18th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial Order Reductions for Timed Systems. In: Proc. of the 9th International Conference on Concurrency Theory (September 1998)","DOI":"10.1007\/BFb0055643"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/3-540-45739-9_24","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J. Zhao","year":"2002","unstructured":"Zhao, J., Xu, H., Li, X., Zheng, T., Zheng, G.: Partial Order Path Technique for Checking Parallel Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, p. 417. Springer, Heidelberg (2002)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Daws","year":"1998","unstructured":"Daws, C., Yovine, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 313. Springer, Heidelberg (1998)"},{"key":"4_CR9","volume-title":"Proc. of 18th IEEE Real-Time Systems Symposium","author":"K. Havelund","year":"1997","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal Modelling and Analysis of an Audio\/Video Protocol: An Industrial Case Study Using Uppaal. In: Proc. of 18th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, Los Alamitos (1997)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40903-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T02:37:39Z","timestamp":1637116659000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40903-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540216711","9783540409038"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40903-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}