{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:24:21Z","timestamp":1725791061768},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548611"},{"type":"electronic","value":"9783642548628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_21","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:33:34Z","timestamp":1395394414000},"page":"310-325","source":"Crossref","is-referenced-by-count":12,"title":["Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata"],"prefix":"10.1007","author":[{"given":"Ting","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shanping","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-75698-9_7","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Ouaknine, J., Quaas, K., Worrell, J.B.: Zone-Based Universality Analysis for Single-Clock Timed Automata. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol.\u00a04767, pp. 98\u2013112. Springer, Heidelberg (2007)"},{"issue":"2","key":"21_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. Theory of Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theory of Computer Science"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","volume":"211","author":"R. Alur","year":"1999","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock Automata: A Determinizable Class of Timed Automata. Theoretical Computer Science\u00a0211, 253\u2013273 (1999)","journal-title":"Theoretical Computer Science"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-02930-1_4","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"2009","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When Are Timed Automata Determinizable? In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol.\u00a05556, pp. 43\u201354. Springer, Heidelberg (2009)"},{"issue":"3","key":"21_CR5","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and Upper Bounds in Zone-based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer\u00a08(3), 204\u2013215 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-19805-2_17","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Bertrand","year":"2011","unstructured":"Bertrand, N., Stainer, A., J\u00e9ron, T., Krichen, M.: A Game Approach to Determinize Timed Automata. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 245\u2013259. Springer, Heidelberg (2011)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-55179-4_25","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1992","unstructured":"Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for Language Inclusion Using Simulation Preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 255\u2013265. Springer, Heidelberg (1992)"},{"issue":"2","key":"21_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.entcs.2005.10.035","volume":"153","author":"V. Gruhn","year":"2006","unstructured":"Gruhn, V., Laue, R.: Patterns for Timed Property Specifications. Electronic Notes in Theoretical Computer Science\u00a0153(2), 117\u2013133 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/3-540-60084-1_93","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The Expressive Power of Clocks. In: F\u00fcl\u00f6p, Z. (ed.) ICALP 1995. LNCS, vol.\u00a0944, pp. 417\u2013428. Springer, Heidelberg (1995)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What Good are Digital Clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 545\u2013558. Springer, Heidelberg (1992)"},{"issue":"2","key":"21_CR11","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. Journal of Information and Computation\u00a0111(2), 193\u2013244 (1994)","journal-title":"Journal of Information and Computation"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.C.: Real-time Specification Patterns. In: ICSE, pp. 372\u2013381 (2005)","DOI":"10.1145\/1062455.1062526"},{"issue":"3","key":"21_CR13","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/s10703-009-0065-1","volume":"34","author":"M. Krichen","year":"2009","unstructured":"Krichen, M., Tripakis, S.: Conformance Testing for Real-Time Systems. Formal Methods in System Design\u00a034(3), 238\u2013304 (2009)","journal-title":"Formal Methods in System Design"},{"issue":"1-2","key":"21_CR14","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Petterson, P., Wang, Y.: UPPAAL in a Nutshell. Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"21_CR15","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1090\/S0002-9947-1994-1219735-8","volume":"345","author":"A. Marcone","year":"1994","unstructured":"Marcone, A.: Foundations of BQO Theory. Transactions of the American Mathematical Society\u00a0345(2), 641\u2013660 (1994)","journal-title":"Transactions of the American Mathematical Society"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On The Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In: LICS, pp. 54\u201363 (2004)","DOI":"10.21236\/ADA461167"},{"issue":"3","key":"21_CR17","first-page":"247","volume":"4","author":"J. Raskin","year":"1999","unstructured":"Raskin, J., Schobbens, P.: The Logic of Event Clocks - Decidability, Complexity and Expressiveness. Journal of Automata, Languages, and Combinatories\u00a04(3), 247\u2013286 (1999)","journal-title":"Journal of Automata, Languages, and Combinatories"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-85778-5_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P.V. Suman","year":"2008","unstructured":"Suman, P.V., Pandya, P.K., Krishna, S.N., Manasa, L.: Timed Automata with Integer Resets: Language Inclusion and Expressiveness. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 78\u201392. Springer, Heidelberg (2008)"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"21_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Tabakov","year":"2005","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental Evaluation of Classical Automata Constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 396\u2013411. Springer, Heidelberg (2005)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol.\u00a01601, pp. 299\u2013314. Springer, Heidelberg (1999)"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M. Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A New Algorithm for Checking Universality of Finite Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 17\u201330. Springer, Heidelberg (2006)"},{"issue":"1-2","key":"21_CR23","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: a Verification Tool for Real-time Systems. Journal on Software Tools for Technology Transfer\u00a01(1-2), 123\u2013133 (1997)","journal-title":"Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T07:58:18Z","timestamp":1558857498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}