{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T11:40:38Z","timestamp":1683373238013},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2006,1]]},"DOI":"10.1007\/s11390-006-0041-9","type":"journal-article","created":{"date-parts":[[2006,2,5]],"date-time":"2006-02-05T11:01:03Z","timestamp":1139137263000},"page":"41-51","source":"Crossref","is-referenced-by-count":0,"title":["Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking"],"prefix":"10.1007","volume":"21","author":[{"given":"Jian-Hua","family":"Zhao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuan-Dong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tao","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guo-Liang","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"Kim G Larsen, Paul Pettersson, Wang Yi. UPPAAL: Status & Developments. In Proc. the 9th International Conference on Computer-Aided Verification, Orna Grumberg, (ed.), Haifa, Israel, Springer-Verlag, June 1997, LNCS 1254, pp.456\u2013459.","DOI":"10.1007\/3-540-63166-6_47"},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"Daws C, Olivero A, Tripakis S, Yovine S. The tool Kronos. In DIMACS Workshop on Verification and Control of Hybrid Systems, LNCS 1066, Springer-Verlag, October 1995.","DOI":"10.1007\/BFb0020947"},{"key":"41_CR3","doi-asserted-by":"crossref","unstructured":"Henzinger T A, Ho P H. Hytech: The Cornell hybrid technology tool. In Proc. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995, BRICS report series NS-95-2.","DOI":"10.1007\/3-540-60472-3_14"},{"issue":"2","key":"41_CR4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"Alur Rajeev","year":"1994","unstructured":"Rajeev Alur, David L Dill. A theory of timed automata. Journal of Theoretical Computer Science, 1994, 126(2): 183\u2013235.","journal-title":"Journal of Theoretical Computer Science"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen. A Tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13\u201318, 2004, Revised Lectures, Lecture Notes in Computer Science 3185, Springer 2004, ISBN 3-540-23068-8.","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"41_CR6","unstructured":"Tomas Gerhard Rokicki. Representing and modeling digital circuits [Dissertation]. Stanford University, 1993."},{"key":"41_CR7","unstructured":"Johan Bengtsson. Clocks, DBMs and states in timed systems, [Dissertation], Uppsala University, 2002."},{"issue":"5","key":"41_CR8","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/BF02950405","volume":"15","author":"Jianhua Zhao","year":"Sept. 2000","unstructured":"Zhao Jianhua, Dang Van Hung. Checking timed automata for linear duration properties. Journal of Computer Science and Technology, Sept. 2000, 15(5): 423\u2013429.","journal-title":"Journal of Computer Science and Technology"},{"issue":"6","key":"41_CR9","first-page":"689","volume":"17","author":"Yong Li","year":"Nov. 2002","unstructured":"Li Yong, Dang Van Hung. Checking temporal duration properties of timed automata. Journal of Computer Science and Technology, Nov. 2002, 17(6): 689\u2013698.","journal-title":"Journal of Computer Science and Technology"},{"key":"41_CR10","doi-asserted-by":"crossref","unstructured":"Zhao Jianhua, Li Xuandong, Zheng Tao, Zheng Guoliang. Removing irrelevant atomic formulas for checking timed automata efficiently. In Proc. FORMATS'03, Marseille, France, September 6\u20137, 2003, LNCS 2791, pp.34\u201345.","DOI":"10.1007\/978-3-540-40903-8_4"},{"key":"41_CR11","doi-asserted-by":"crossref","unstructured":"Kalus Havelund, Arne Skou, Kim G Larsen, Kristian Lund. 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, December 1997, pp.2\u201313.","DOI":"10.7146\/brics.v4i31.18957"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Daws C, Yovine S. Reducing the number of clock variables of timed automata. In Proc. the 17th IEEE Real Time Systems Symposium, RTSS'96, Washington DC, USA, December 1996, IEEE Computer Society Press, pp.73\u201381.","DOI":"10.1109\/REAL.1996.563702"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0041-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-006-0041-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0041-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T11:18:26Z","timestamp":1683371906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-006-0041-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":12,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["41"],"URL":"https:\/\/doi.org\/10.1007\/s11390-006-0041-9","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}