{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T06:04:41Z","timestamp":1746079481759},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156427"},{"type":"electronic","value":"9783642156434"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-15643-4_23","type":"book-chapter","created":{"date-parts":[[2010,9,20]],"date-time":"2010-09-20T09:39:39Z","timestamp":1284975579000},"page":"306-324","source":"Crossref","is-referenced-by-count":29,"title":["Recursive Timed Automata"],"prefix":"10.1007","author":[{"given":"Ashutosh","family":"Trivedi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Wojtczak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM Transactions on Programming Languages and Systems\u00a027, 786\u2013818 (2005)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci.\u00a0126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. In: ACM SIGSOFT 1998, pp. 175\u2013188 (1998)","DOI":"10.1145\/288195.288305"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: The slam toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-60472-3_4","volume-title":"Hybrid Systems II","author":"A. Bouajjani","year":"1995","unstructured":"Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 64\u201385. Springer, Heidelberg (1995)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/3-540-58179-0_48","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"1994","unstructured":"Bouajjani, A., Echahed, R., Robbana, R.: Verification of context-free timed systems using linear hybrid observers. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 118\u2013131. Springer, Heidelberg (1994)"},{"key":"#cr-split#-23_CR7.1","doi-asserted-by":"crossref","unstructured":"Bouchy, F., Finkel, A., Sangnier, A.: Reachability in timed counter systems. Electronic Notes in Theoretical Computer Science\u00a0239, 167\u2013178 (2009);","DOI":"10.1016\/j.entcs.2009.05.038"},{"key":"#cr-split#-23_CR7.2","unstructured":"Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008)"},{"key":"23_CR8","volume-title":"Hard Real-time Computing Systems: Predictable Scheduling Algorithms and Applications","author":"G.C. Buttazzo","year":"2004","unstructured":"Buttazzo, G.C.: Hard Real-time Computing Systems: Predictable Scheduling Algorithms and Applications. Springer, Santa Clara (2004)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-00602-9_7","volume-title":"Hybrid Systems: Computation and Control","author":"F. Cassez","year":"2009","unstructured":"Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers \u2014 an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol.\u00a05469, pp. 90\u2013104. Springer, Heidelberg (2009)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/3-540-44585-4_48","volume-title":"Computer Aided Verification","author":"Z. Dang","year":"2001","unstructured":"Dang, Z.: Binary reachability analysis of pushdown timed automata with dense clocks. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 506\u2013517. Springer, Heidelberg (2001)"},{"issue":"1-3","key":"23_CR11","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(02)00743-0","volume":"302","author":"Z. Dang","year":"2003","unstructured":"Dang, Z.: Pushdown timed automata: a binary reachability characterization and safety verification. Theor. Comput. Sci.\u00a0302(1-3), 93\u2013121 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"23_CR12","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 Computation\u00a019(6), 1541\u20131575 (2009)","journal-title":"J. Logic Computation"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Emmi, M., Majumdar, R.: Decision problems for the verification of real-time software. In: Hybrid Systems: Computation and Control, pp. 200\u2013211 (2006)","DOI":"10.1007\/11730637_17"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"891","DOI":"10.1007\/11523468_72","volume-title":"Automata, Languages and Programming","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive markov decision processes and recursive stochastic games. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 891\u2013903. Springer, Heidelberg (2005)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-540-24622-0_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Etessami","year":"2004","unstructured":"Etessami, K.: Analysis of recursive game graphs using data flow equations. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 282\u2013296. Springer, Heidelberg (2004)"},{"issue":"9","key":"23_CR16","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1016\/j.peva.2009.12.009","volume":"67","author":"K. Etessami","year":"2010","unstructured":"Etessami, K., Wojtczak, D., Yannakakis, M.: Quasi-Birth-Death processes, Tree-like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems. Performance Evaluation\u00a067(9), 837\u2013857 (2010); Special Issue of QEST 2008 (2008)","journal-title":"Performance Evaluation"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"5","key":"23_CR18","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.ipl.2007.06.006","volume":"104","author":"P. Jancar","year":"2007","unstructured":"Jancar, P., Sawa, Z.: A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett.\u00a0104(5), 164\u2013167 (2007)","journal-title":"Inf. Process. Lett."},{"key":"23_CR19","volume-title":"Computation: finite and infinite machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Englewood Cliffs (1967)"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/11690634_23","volume-title":"Foundations of Software Science and Computation Structures","author":"O. Serre","year":"2006","unstructured":"Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 337\u2013351. Springer, Heidelberg (2006)"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Trivedi, A., Wojtczak, D.: Recursive timed automata. Oxford University Computing Laboratory technical report, RR-10-09 (2010)","DOI":"10.1007\/978-3-642-15643-4_23"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model checking, pp. 62\u201374 (1996)","DOI":"10.1007\/3-540-61474-5_58"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15643-4_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,4]],"date-time":"2019-06-04T19:05:24Z","timestamp":1559675124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15643-4_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156427","9783642156434"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15643-4_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}