{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T08:41:07Z","timestamp":1659429667567},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,6,1]],"date-time":"2017-06-01T00:00:00Z","timestamp":1496275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s11432-016-9027-y","type":"journal-article","created":{"date-parts":[[2017,9,6]],"date-time":"2017-09-06T13:23:52Z","timestamp":1504704232000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Updatable timed automata with one updatable clock"],"prefix":"10.1007","volume":"61","author":[{"given":"Guoqiang","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yunqing","family":"Wen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoji","family":"Yuen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,1]]},"reference":[{"key":"9027_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. Theor Comput Sci, 1994, 126: 183\u2013235","journal-title":"Theor Comput Sci"},{"key":"9027_CR2","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/10722167_35","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification","author":"P Bouyer","year":"2000","unstructured":"Bouyer P, Dufourd C, Fleury E, et al. Are timed automata updatable? In: Proceedings of the 12th International Conference on Computer Aided Verification, Chicago, 2000. 464\u2013479"},{"key":"9027_CR3","first-page":"232","volume-title":"Proceedings of International Symposium on Mathematical Foundations of Computer, Bratislava","author":"P Bouyer","year":"2000","unstructured":"Bouyer P, Dufourd C, Fleury E, et al. Expressiveness of updatable timed automata. In: Proceedings of International Symposium on Mathematical Foundations of Computer, Bratislava, 2000. 232\u2013242"},{"key":"9027_CR4","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.tcs.2004.04.003","volume":"321","author":"P Bouyer","year":"2004","unstructured":"Bouyer P, Dufourd C, Fleury E, et al. Updatable timed automata. Theor Comput Sci, 2004, 321: 291\u2013345","journal-title":"Theor Comput Sci"},{"key":"9027_CR5","volume-title":"Upper Saddle River: Prentice-Hall","author":"M L Minsky","year":"1967","unstructured":"Minsky M L. Computation: Finite and Infinite Machines. Upper Saddle River: Prentice-Hall, 1967"},{"key":"9027_CR6","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer P. Forward analysis of updatable timed automata. Form Method Syst Des, 2004, 24: 281\u2013320","journal-title":"Form Method Syst Des"},{"key":"9027_CR7","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1109\/QRS-C.2015.47","volume-title":"Proceedings of IEEE International Conference on the Software Quality, Reliability and Security - Companion, Vancouver","author":"B B Fang","year":"2015","unstructured":"Fang B B, Li G Q, Fang L, et al. A refined algorithm for reachability analysis of updatable timed automata. In: Proceedings of IEEE International Conference on the Software Quality, Reliability and Security - Companion, Vancouver, 2015. 230\u2013236"},{"key":"9027_CR8","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T A Henzinger","year":"1998","unstructured":"Henzinger T A, Kopke P W, Puri A, et al. What\u2019s decidable about hybrid automata? J Comput Syst Sci, 1998, 57: 94\u2013124","journal-title":"J Comput Syst Sci"},{"key":"9027_CR9","first-page":"147","volume-title":"Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method, Pairs","author":"Y Q Wen","year":"2015","unstructured":"Wen Y Q, Li G Q, Yuen S. On reachability analysis of updatable timed automata with one updatable clock. In: Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method, Pairs, 2015, 147\u2013161"},{"key":"9027_CR10","first-page":"35","volume-title":"Proceedings of 27th Annual IEEE Symposium on Logic in Computer Science, Dubrovnik","author":"P A Abdulla","year":"2012","unstructured":"Abdulla P A, Atig M F, Stenman J. Dense-timed pushdown automata. In: Proceedings of 27th Annual IEEE Symposium on Logic in Computer Science, Dubrovnik, 2012. 35\u201344"},{"key":"9027_CR11","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-22975-1_13","volume-title":"Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems","author":"G Q Li","year":"2015","unstructured":"Li G Q, Ogawa M, Yuen S. Nested timed automata with frozen clocks. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Madrid, 2015, 189\u2013205"},{"key":"9027_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0890-5401(03)00171-8","volume":"188","author":"P Jancar","year":"2004","unstructured":"Jancar P, Kucera A, Moller F, et al. DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inform Comput, 2004, 188: 1\u201319","journal-title":"Inform Comput"},{"key":"9027_CR13","first-page":"369","volume-title":"Proceedings of the International Conference on Concurrency Theory, Bologna","author":"C Haase","year":"2009","unstructured":"Haase C, Kreutzer S, Ouaknine J, et al. Reachability in succinct and parametric one-counter automata. In: Proceedings of the International Conference on Concurrency Theory, Bologna, 2009. 369\u2013383"},{"key":"9027_CR14","volume-title":"Dissertation for Ph.D. Degree. Munich: Technical University of Munich","author":"S Schwoon","year":"2000","unstructured":"Schwoon S. Model-checking pushdown system. Dissertation for Ph.D. Degree. Munich: Technical University of Munich, 2000"},{"key":"9027_CR15","doi-asserted-by":"publisher","first-page":"1541","DOI":"10.1093\/logcom\/exp037","volume":"19","author":"S Demri","year":"2009","unstructured":"Demri S, Gascon R. The effects of bounding syntactic resources on presburger LTL. J Logic Comput, 2009, 19: 1541\u20131575","journal-title":"J Logic Comput"},{"key":"9027_CR16","doi-asserted-by":"publisher","first-page":"1149","DOI":"10.1016\/j.ic.2007.01.009","volume":"205","author":"E Fersman","year":"2007","unstructured":"Fersman E, Krcal P, Pettersson P, et al. Task automata: schedulability, decidability and undecidability. Inform Comput, 2007, 205: 1149\u20131172","journal-title":"Inform Comput"},{"key":"9027_CR17","first-page":"54","volume-title":"Proceedings of the 19th IEEE Symposium on Logic in Computer Science, Turku","author":"J Ouaknine","year":"2004","unstructured":"Ouaknine J, Worrell J. On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science, Turku, 2004. 54\u201363"},{"key":"9027_CR18","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0054179","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon","author":"P A Abdulla","year":"1998","unstructured":"Abdulla P A, Jonsson B. Verifying networks of timed processes. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, 1998. 298\u2013312"},{"key":"9027_CR19","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"P A Abdulla","year":"2003","unstructured":"Abdulla P A, Jonsson B. Model checking of systems with many identical time processes. Theor Comput Sci, 2003, 290: 241\u2013264","journal-title":"Theor Comput Sci"},{"key":"9027_CR20","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-40229-6_12","volume-title":"Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Buenos Aires","author":"G Q Li","year":"2013","unstructured":"Li G Q, Cai X J, Ogawa M, et al. Nested timed automata. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Buenos Aires, 2013. 168\u2013182"},{"key":"9027_CR21","first-page":"371","volume":"5","author":"C Choffrut","year":"2000","unstructured":"Choffrut C, Goldwurm M. Timed automata with periodic clock constraints. J Autom Lang Comb, 2000, 5: 371\u2013404","journal-title":"J Autom Lang Comb"},{"key":"9027_CR22","first-page":"455","volume-title":"Proceedings of the 9th International Conference on Concurrency Theory, Nice","author":"F Demichelis","year":"1998","unstructured":"Demichelis F, Zielonka W. Controlled timed automata. In: Proceedings of the 9th International Conference on Concurrency Theory, Nice, 1998. 455\u2013469"},{"key":"9027_CR23","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/j.entcs.2009.05.038","volume":"239","author":"F Bouchy","year":"2009","unstructured":"Bouchy F, Finkel A, Sangnier A. Reachability in timed counter systems. Electr Notes Theor Comput Sci, 2009, 239: 167\u2013178","journal-title":"Electr Notes Theor Comput Sci"},{"key":"9027_CR24","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Proceedings of International Workshop on Hybrid Systems: Computation and Control, Rome","author":"R Alur","year":"2001","unstructured":"Alur R, La Torre S, Pappas G J. Optimal paths in weighted timed automata. In: Proceedings of International Workshop on Hybrid Systems: Computation and Control, Rome, 2001, 49\u201362"},{"key":"9027_CR25","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Proceedings of the International Workshop on Hybrid Systems: Computation and Control, Rome","author":"G Behrmann","year":"2001","unstructured":"Behrmann G, Fehnker A, Hune T, et al. Minimum-cost reachability for priced timed automata. In: Proceedings of the International Workshop on Hybrid Systems: Computation and Control, Rome, 2001, 147\u2013161"},{"key":"9027_CR26","first-page":"393","volume":"10","author":"P Bouyer","year":"2005","unstructured":"Bouyer P, Chevalier F. On conciseness of extensions of timed automata. J Autom Lang Combin 2005, 10: 393\u2013405","journal-title":"J Autom Lang Combin"},{"key":"9027_CR27","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-85778-5_7","volume-title":"Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Saint Malo","author":"P V Suman","year":"2008","unstructured":"Suman P V, Pandya P K, Krishna S N, et al. Timed automata with integer resets: language inclusion and expressiveness. In: Proceedings of International Conference on Formal Modeling and Analysis of Timed Systems, Saint Malo, 2008. 78\u201392"},{"key":"9027_CR28","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/978-3-642-00982-2_62","volume-title":"Proceedings of International Conference on Language and Automata Theory and Applications, Tarragona","author":"P V Suman","year":"2009","unstructured":"Suman P V, Pandya P K. Determinization and expressiveness of integer reset timed automata with silent transitions. In: Proceedings of International Conference on Language and Automata Theory and Applications, Tarragona, 2009, 728\u2013739"},{"key":"9027_CR29","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-15643-4_23","volume-title":"Proceedings of International Symposium on Automated Technology for Verification and Analysis, Singapore","author":"A Trivedi","year":"2010","unstructured":"Trivedi A, Wojtczak D. Recursive timed automata. In: Proceedings of International Symposium on Automated Technology for Verification and Analysis, Singapore, 2010. 306\u2013324"},{"key":"9027_CR30","first-page":"62","volume-title":"Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method, Luxembourg","author":"Y Q Wen","year":"2014","unstructured":"Wen Y Q, Li G Q, Yuen S J. An over-approximation forward analysis for nested timed automata. In: Proceedings of International Workshop on Structured Object-Oriented Formal Language and Method, Luxembourg, 2014. 62\u201380"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-016-9027-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9027-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9027-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T08:10:36Z","timestamp":1659427836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-016-9027-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["9027"],"URL":"https:\/\/doi.org\/10.1007\/s11432-016-9027-y","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,6]]},"assertion":[{"value":"7 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2016","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 February 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 September 2017","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"012102"}}