{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:59Z","timestamp":1760202539516},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678977"},{"type":"electronic","value":"9783540446187"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44618-4_15","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T10:38:51Z","timestamp":1188297531000},"page":"183-198","source":"Crossref","is-referenced-by-count":14,"title":["Reachability Analysis for Some Models of Infinite-State Transition Systems"],"prefix":"10.1007","author":[{"given":"Oscar H.","family":"Ibarra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwen","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,12,21]]},"reference":[{"issue":"1","key":"15_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. Courcoibetis, and D. Dill. Model-checking in dense real time. Information & Computation, 104(1):2\u201334, 1993.","journal-title":"Information & Computation"},{"issue":"2","key":"15_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. Automata for modeling real-time systems. Theoretical Computer Science, 126(2):183\u2013236, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"R. Alur and T. A. Henzinger. A really temporal logic. J. ACM, 41(1):181\u2013204, 1994.","journal-title":"J. ACM"},{"issue":"2","key":"15_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 1020 states and beyond. Information & Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information & Computation"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model-Checking. CONCUR 1997, pp. 135\u2013150.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Hybrid Systems 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 In Hybrid Systems II, LNCS 999, 1995."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Godefroid. \u201cSymbolic verification of communication protocols with infinite state spaces using QDDs.\u201d In Proc. Int. Conf. on Computer Aided Verification, 1996.","DOI":"10.1007\/3-540-61474-5_53"},{"issue":"4","key":"15_CR8","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations, and Experimental Results. ACM Trans. on Programming Languages and Systems, 21(4):747\u2013789, July 1999.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proc. 10th Int. Conf. on Computer Aided Verification, 1998.","DOI":"10.1007\/BFb0028755"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Wolper, Symbolic verification with periodic sets, Proc. 6th Int. Conf. on Computer Aided Verification, 1994","DOI":"10.1007\/3-540-58179-0_43"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. Proc. 10th Int. Conf. on Computer Aided Verification, 1998.","DOI":"10.1007\/BFb0028751"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"H. Comon and Y. Jurski. Timed Automata and the Theory of Real Numbers. Proc. CONCUR, 1999.","DOI":"10.1007\/3-540-48320-9_18"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. To appear in Int. Conf. on Computer Aided Verification, 2000.","DOI":"10.1007\/10722167_9"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction. Proc. 7th Int. Conf. on Computer Aided Verification, 1995.","DOI":"10.1007\/3-540-60045-0_40"},{"issue":"2","key":"15_CR15","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. on Programming Languages and Systems, 19(2):253\u2013291, March 1997.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"2","key":"15_CR16","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"J. Esparza. Decidability of Model Checking for Infinite-State Concurrent Systems. Acta Informatica, 34(2):85\u2013107, 1997.","journal-title":"Acta Informatica"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"A. Finkel and G. Sutre. Decidability of reachability problems for classes of two counters automata. STACS\u20192000, 346\u2013357, Springer, 2000.","DOI":"10.1007\/3-540-46541-3_29"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. INFINITY, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"15_CR19","first-page":"220","volume":"22","author":"E. M. Gurari","year":"1981","unstructured":"E. M. Gurari and O. H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. JCSS, 22:220\u2013229, 1981.","journal-title":"JCSS"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"S. A. Greibach. Checking automata and one-way stack languages. SDC Document TM 738\/045\/00, 1968.","DOI":"10.1109\/SWAT.1968.6"},{"issue":"2","key":"15_CR21","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. Symbolic Model Checking for Real-time Systems. Information & Computation, 111(2):193\u2013244, 1994.","journal-title":"Information & Computation"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Raymond, and Y. Proy. Verification of linear hybrid systems by means of convex approximations. In Proc. Int. Symposium on Static Analysis, B. LeCharlier ed., vol. 864, September 1994.","DOI":"10.1007\/3-540-58485-4_43"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O. H. Ibarra","year":"1978","unstructured":"O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, Vol. 25, pp. 116\u2013133, 1978.","journal-title":"J. ACM"},{"issue":"1","key":"15_CR24","first-page":"1","volume":"59","author":"O. H. Ibarra","year":"1999","unstructured":"O. H. Ibarra and J. Su, A Technique for the Containment and Equivalence of Linear Constraint Queries. JCSS, 59(1):1\u201328, 1999.","journal-title":"JCSS"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"O. H. Ibarra, J. Su, and C. Bartzis, Counter Machines and the Safety and Disjointness Problems for Database Queries with Linear Constraints, to appear in Words, Sequences, Languages: Where Computer Science, Biology and Linguistics Meet, Kluwer, 2000.","DOI":"10.1007\/978-94-015-9634-3_11"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"O. H. Ibarra, J. Su, Z. Dang, T. Bultan, and R. Kemmerer, Counter Machines: Decidable Properties and Applications to Verification Problems, To appear in Proc. MFCS\u20192000.","DOI":"10.1007\/3-540-44612-5_38"},{"key":"15_CR27","first-page":"354","volume":"11","author":"Y. Matijasevic","year":"1970","unstructured":"Y. Matijasevic. Enumerable sets are Diophantine. Soviet Math. Dokl, Vol. 11, 1970, pp. 354\u2013357.","journal-title":"Soviet Math. Dokl"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M. Minsky","year":"1961","unstructured":"M. Minsky. Recursive unsolvability of Post\u2019s problem of Tag and other topics in the theory of Turing machines. Ann. of Math., 74:437\u2013455, 1961.","journal-title":"Ann. of Math."},{"key":"15_CR29","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"E. Post","year":"1946","unstructured":"E. Post. A variant of a recursively unsolvable problem. Bull. Am. Math. Soc., 52:264\u2013268, 1946.","journal-title":"Bull. Am. Math. Soc."},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"I. Walukiewicz. Pushdown processes: games and model checking. In Proc. Int. Conf. on Computer Aided Verification, 1996","DOI":"10.1007\/3-540-61474-5_58"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In Proc. Int. Conf. on Computer Aided Verification, 1998.","DOI":"10.1007\/BFb0028736"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2000 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44618-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T13:10:05Z","timestamp":1556802605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44618-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678977","9783540446187"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-44618-4_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}