{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:21:06Z","timestamp":1737091266906,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540004004"},{"type":"electronic","value":"9783540363903"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"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":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36390-4_7","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T23:45:05Z","timestamp":1180223105000},"page":"74-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Past Pushdown Timed Automata"],"prefix":"10.1007","author":[{"given":"Zhe","family":"Dang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oscar H.","family":"Ibarra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard A.","family":"Kemmerer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,12,18]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill, \u201cModel-checking in dense real time,\u201d Information and Computation, 104 (1993) 2\u201334","journal-title":"Information and Computation"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill, \u201cA theory of timed automata,\u201d TCS, 126 (1994) 183\u2013236","journal-title":"TCS"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"R. Alur, T. Feder, and T.A. Henzinger, \u201cThe benefits of relaxing punctuality,\u201d J. ACM, 43 (1996) 116\u2013146","journal-title":"J. ACM"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, T.A. Henzinger, \u201cReal-time logics: complexity and expressiveness,\u201d Information and Computation, 104 (1993) 35\u201377","journal-title":"Information and Computation"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur, T.A. Henzinger, \u201cA really temporal logic,\u201d J. ACM, 41 (1994) 181\u2013204","journal-title":"J. ACM"},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler, \u201cReachability analysis of pushdown automata: application to model-checking,\u201d, CONCUR\u201997, LNCS 1243, pp. 135\u2013150"},{"key":"7_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/3-540-60472-3_4","volume-title":"Hybrid System II","author":"A. Bouajjani","year":"1995","unstructured":"A. Bouajjani, R. Echahed, and R. Robbana, \u201cOn the automatic verification of systems with continuous variables and unbounded discrete data structures,\u201d Hybrid System II, LNCS 999, 1995, pp. 64\u201385"},{"key":"7_CR8","first-page":"572","volume":"23","author":"A. Coen-Porisini","year":"1997","unstructured":"A. Coen-Porisini, C. Ghezzi and R. Kemmerer, \u201cSpecification of real-time systems using ASTRAL,\u201d TSE, 23 (1997) 572\u2013598","journal-title":"TSE"},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/3-540-48320-9_18","volume-title":"CONCUR\u201999","author":"H. Comon","year":"1999","unstructured":"H. Comon and Y. Jurski, \u201cTimed automata and the theory of real numbers,\u201d CONCUR\u201999, LNCS 1664, pp. 242\u2013257"},{"key":"7_CR10","first-page":"548","volume":"20","author":"A. Coen-Porisini","year":"1994","unstructured":"A. Coen-Porisini, R. Kemmerer and D. Mandrioli, \u201cA formal framework for ASTRAL intralevel proof obligations,\u201d TSE, 20 (1994) 548\u2013561","journal-title":"TSE"},{"key":"7_CR11","unstructured":"Z. Dang, \u201cVerification and debugging of infinite state real-time systems,\u201d PhD Dissertation, UCSB, August 2000. Available at http:\/\/www.cs.ucsb.edu\/~dang"},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1007\/3-540-44585-4_48","volume-title":"CAV\u201901","author":"Z. Dang","year":"2001","unstructured":"Z. Dang, \u201cBinary reachability analysis of timed pushdown automata with dense clocks,\u201d CAV\u201901, LNCS 2102, pp. 506\u2013517"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Z. Dang and R.A. Kemmerer, \u201cUsing the ASTRAL model checker to analyze Mobile IP,\u201d ICSE\u201999, pp. 132\u2013141","DOI":"10.1145\/302405.302459"},{"key":"7_CR14","unstructured":"Z. Dang and R. A. Kemmerer, \u201cUsing the ASTRAL symbolic model checker as a specification debugger: three approximation techniques,\u201d ICSE\u201900, pp. 345\u2013354"},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/10722167_9","volume-title":"CAV\u201900","author":"Z. Dang","year":"2000","unstructured":"Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer and J. Su, \u201cBinary reachability analysis of discrete pushdown timed automata,\u201d CAV\u201900, LNCS 1855, pp. 69\u201384"},{"key":"7_CR16","unstructured":"A. Finkel, B. Willems and P. Wolper, \u201cA direct symbolic approach to model checking pushdown systems,\u201d INFINITY\u201997"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer and N. Lynch. \u201cThe generalized railroad crossing: a case study in formal verification of real-time systems,\u201d RTSS\u201994, pp. 120\u2013131","DOI":"10.1109\/REAL.1994.342724"},{"key":"7_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"ICALP\u201992","author":"T.A. Henzinger","year":"1992","unstructured":"T. A. Henzinger, Z. Manna, and A. Pnueli, \u201cWhat good are digital clocks?,\u201d ICALP\u201992, LNCS 623, pp. 545\u2013558"},{"key":"7_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"T. A. Henzinger","year":"1995","unstructured":"T. A. Henzinger and Pei-Hsin Ho, \u201cHyTech: the Cornell hybrid technology tool,\u201d Hybrid Systems II, LNCS 999, 1995, pp. 265\u2013294"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, \u201cSymbolic model checking for real-time systems,\u201d Information and Computation, 111 (1994) 193\u2013244","journal-title":"Information and Computation"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. H. Ibarra","year":"1978","unstructured":"O. H. Ibarra, \u201cReversal-bounded multicounter machines and their decision problems,\u201c J. ACM, 25 (1978) 116\u2013133","journal-title":"J. ACM"},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1018934104631","volume":"7","author":"P.Z. Kolano","year":"1999","unstructured":"P. Z. Kolano, Z. Dang and R. A. Kemmerer. \u201cThe design and analysis of realtime systems using the ASTRAL software development environment,\u201d Annals of Software Engineering, 7 (1999) 177\u2013210","journal-title":"Annals of Software Engineering"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pattersson, and W. Yi, \u201cUPPAAL in a nutshell,\u201d International Journal on Software Tools for Technology Transfer, 1 (1997) 134\u2013152","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"7_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/3-540-60246-1_158","volume-title":"MFCS\u201995","author":"F. Laroussinie","year":"1995","unstructured":"F. Laroussinie, K. G. Larsen, and C. Weise, \u201cFrom timed automata to logic-and back,\u201d MFCS\u201995, LNCS 969, pp. 529\u2013539"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Amir Pnueli, \u201cThe temporal logic of programs,\u201d FOCS\u201977, pp. 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0014711","volume-title":"HART\u201997","author":"J. Raskin","year":"1997","unstructured":"J. Raskin and P. Schobben, \u201cState clock logic: a decidable real-time logic,\u201d HART\u201997, LNCS 1201, pp. 33\u201347"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"H. Straubing, Finite automata, formal logic, and circuit complexity. Birkhauser, 1994","DOI":"10.1007\/978-1-4612-0289-9"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"W. Thomas, \u201cAutomata on infinite objects,\u201d in Handbook of Theoretical Computer Science, Volume B (J. van Leeuwen eds.), Elsevier, 1990","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"7_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-58468-4_191","volume-title":"Specifying timed state sequences in powerful decidable logics and timed automata","author":"T. Wilke","year":"1994","unstructured":"T. Wilke, \u201cSpecifying timed state sequences in powerful decidable logics and timed automata,\u201d LNCS 863, pp. 694\u2013715, 1994"},{"key":"7_CR30","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"S. Yovine, \u201cA verification tool for real-time systems,\u201d International Journal on Software Tools for Technology Transfer, 1 (1997): 123\u2013133","journal-title":"International Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36390-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:23:44Z","timestamp":1737051824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36390-4_7"}},"subtitle":["Extended Abstract"],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540004004","9783540363903"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-36390-4_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"18 December 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}