{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:47:29Z","timestamp":1725493649907},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405344"},{"type":"electronic","value":"9783540450719"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45071-8_18","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T04:04:43Z","timestamp":1193457883000},"page":"159-171","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Verification of Multi-queue Discrete Timed Automata"],"prefix":"10.1007","author":[{"given":"Pierluigi","family":"San Pietro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhe","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"P. Abdulla","year":"2002","unstructured":"P. Abdulla and B. Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1):241\u2013264, 2002.","journal-title":"Theoretical Computer Science"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"P. Abdulla and A. Nyl\u00e9n. Timed petri nets and bqos. In ICATPN\u20192001, 22nd Int. Conf. on application and theory of Petri nets, 2001.","DOI":"10.1007\/3-540-45740-2_5"},{"issue":"1","key":"18_CR3","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. Model-checking in dense real-time. Information and Computation, 104(1):2\u201334, May 1993.","journal-title":"Information and Computation"},{"issue":"2","key":"18_CR4","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. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013235, April 1994.","journal-title":"Theoretical Computer Science"},{"key":"18_CR5","series-title":"Lect Notes Comput Sci","first-page":"652","volume-title":"ICALP 2001","author":"M. B. P. Godefroid","year":"2001","unstructured":"M. Benedikt P. Godefroid and T. Reps. Model checking of unrestricted hierarchical state machines. In ICALP 2001, of LNCS 2076, pp. 652\u2013666. Springer, 2001."},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1142\/S0129054196000191","volume":"7","author":"L. Breveglieri","year":"1996","unstructured":"L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi Reghizzi. Multiple pushdown languages and grammars. Int. Journal of Found. of Computer Science, 7:253\u2013291, 1996.","journal-title":"Int. Journal of Found. of Computer Science"},{"key":"18_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-55092-5_8","volume-title":"FTRTFT\u201992","author":"L. Breveglieri","year":"1992","unstructured":"L. Breveglieri, A. Cherubini, and S. Crespi Reghizzi. Real-time scheduling by queue automata. In FTRTFT\u201992, vol\/ 571 of LNCS, pages 131\u2013148. Springer, 1992."},{"key":"18_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-48321-7_12","volume-title":"Fundamentals of Computation Theory","author":"L. Breveglieri","year":"1999","unstructured":"L. Breveglieri, A. Cherubini, and S. Crespi Reghizzi. Modelling operating systems schedulers with multi-stack-queue grammars. In Fundamentals of Computation Theory, volume 1684 of LNCS, pages 161\u2013172. Springer, 1999."},{"key":"18_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/3-540-63166-6_31","volume-title":"CAV\u201997","author":"G. Cece","year":"1997","unstructured":"G. Cece and A. Finkel. Programs with quasi-stable channels are effectively recognizable. In CAV\u201997, volume 1254 of LNCS, pages 304\u2013315. Springer, 1997."},{"key":"18_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"CAV\u201998","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In CAV\u201998, volume 1427 of LNCS, pages 268\u2013279. Springer, 1998."},{"key":"18_CR11","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. Timed automata and the theory of real numbers. In CONCUR\u201999, volume 1664 of LNCS, pages 242\u2013257. Springer, 1999."},{"key":"18_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":"Zhe Dang. Binary reachability analysis of pushdown timed automata with dense clocks. In CAV\u201901, volume 2102 of LNCS, pages 506\u2013517. Springer, 2001."},{"key":"18_CR13","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":"Zhe Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability analysis of discrete pushdown timed automata. In CAV\u201900, LNCS 1855, pages 69\u201384. Springer, 2000."},{"key":"18_CR14","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"S. Ginsburg and E. Spanier. Semigroups, presburger formulas, and languages. Pacific J. of Mathematics, 16:285\u2013296, 1966.","journal-title":"Pacific J. of Mathematics"},{"key":"18_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-45657-0_11","volume-title":"CAV\u201902","author":"P. Godefroid","year":"2002","unstructured":"P. Godefroid and R. Jagadeesan. Automatic abstraction using generalized model checking. In CAV\u201902, volume 2404 of LNCS, pages 137\u2013150. Springer, 2002."},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1007\/3-540-49253-4_37","volume-title":"AMAST\u201998","author":"B. Grahlmann","year":"1998","unstructured":"B. Grahlmann. The state of pep. In AMAST\u201998, LNCS 1548, pages 522\u2013526. Springer, 1998."},{"issue":"2","key":"18_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, June 1994.","journal-title":"Information and Computation"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R. Parikh","year":"1966","unstructured":"R. Parikh. On context-free languages. Journal of the ACM, 13:570\u2013581, 1966.","journal-title":"Journal of the ACM"},{"key":"18_CR19","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Livenss and acceleraiton in parameterized verification. In CAV\u201900, volume 1855 of LNCS. Springer, 2000."},{"issue":"8","key":"18_CR20","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 35(8):102\u2013114, 1992.","journal-title":"Communications of the ACM"},{"key":"18_CR21","series-title":"Lect Notes Comput Sci","first-page":"419","volume-title":"ICALP\u201997","author":"B. Steffen","year":"1997","unstructured":"B. Steffen and O. Burkart. Model checking the full modal mu-calculus for infinite sequential processes. In ICALP\u201997, volume 1256 of LNCS, pages 419\u2013429."}],"container-title":["Lecture Notes in Computer Science","Computing and Combinatorics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45071-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:09:05Z","timestamp":1556921345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45071-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405344","9783540450719"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45071-8_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}