{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:56:08Z","timestamp":1725490568282},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540424918"},{"type":"electronic","value":"9783540446743"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44674-5_12","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T13:49:49Z","timestamp":1188308989000},"page":"145-156","source":"Crossref","is-referenced-by-count":1,"title":["Reachability and Safety in Queue Systems"],"prefix":"10.1007","author":[{"given":"Oscar H.","family":"Ibarra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,20]]},"reference":[{"issue":"1","key":"12_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 and Computation, 104(1):2\u201334, 1993.","journal-title":"Information and Computation"},{"issue":"2","key":"12_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":"12_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"},{"key":"12_CR4","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":"12_CR5","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, pages 1\u201312, 1996.","DOI":"10.1007\/3-540-61474-5_53"},{"key":"12_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":"12_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u201996","author":"A. Bouajjani","year":"1996","unstructured":"A. Bouajjani and P. Habermehl. \u201cConstrained Properties, Semilinear Systems, and Petri Nets.\u201d In CONCUR\u201996, LNCS 1119, 1996."},{"issue":"1-2","key":"12_CR8","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","volume":"221","author":"A. Bouajjani","year":"1999","unstructured":"A. Bouajjani and P. Habermehl. \u201cSymbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations.\u201d Theoretical Computer Science, 221(1-2): 211\u2013250, 1999.","journal-title":"Theoretical Computer Science"},{"key":"12_CR9","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":"12_CR10","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, pp. 268\u2013279, 1998.","DOI":"10.1007\/BFb0028751"},{"key":"12_CR11","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"},{"issue":"2","key":"12_CR12","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":"12_CR13","unstructured":"A. Finkel and G. Sutre. Decidability of Reachability Problems for Classes of Two Counter Automata. STACS\u201900."},{"key":"12_CR14","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":"12_CR15","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":"12_CR16","first-page":"368","volume":"4","author":"J. Hartmanis","year":"1970","unstructured":"J. Hartmanis and J. Hopcroft. What makes some language theory problems undecidable. JCSS, 4: 368\u2013376, 1970.","journal-title":"JCSS"},{"issue":"2","key":"12_CR17","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 and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"12_CR18","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"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"O.H. Ibarra, T. Bultan, and J. Su. Reachability Analysis for Some Models of Infinite-state Transition Systems. To appear in CONCUR\u20192000.","DOI":"10.1007\/3-540-44618-4_15"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jcss.1999.1624","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. Journal of Computer and System Sciences, 59(1):1\u201328, 1999.","journal-title":"Journal of Computer and System Sciences"},{"key":"12_CR21","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":"12_CR22","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 MFCS\u20192000.","DOI":"10.1007\/3-540-44612-5_38"},{"key":"12_CR23","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":"12_CR24","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"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44674-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:06:13Z","timestamp":1556816773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44674-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424918","9783540446743"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44674-5_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}