{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:32:15Z","timestamp":1759638735892,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_18","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:48:36Z","timestamp":1180666116000},"page":"262-277","source":"Crossref","is-referenced-by-count":22,"title":["Pushdown Specifications"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"crossref","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"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In 10th LICS, pp. 123\u2013133, 1995. IEEE.","DOI":"10.1109\/LICS.1995.523250"},{"key":"18_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"8th Concur","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In 8th Concur, LNCS 1243, pp. 135\u2013150, 1997."},{"key":"18_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-540-48654-1_8","volume-title":"5th Concur","author":"A. Bouajjani","year":"1994","unstructured":"A. Bouajjani, R. Echahed, and R. Robbana. Verification of nonregular temporal properties for context-free processes. In 5th Concur, LNCS 836, pp. 81\u201397, 1994."},{"key":"18_CR5","series-title":"Lect Notes Comput Sci","first-page":"454","volume-title":"13th CAV","author":"P. Biesse","year":"2001","unstructured":"P. Biesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessors using satisfiability solvers. In 13th CAV, LNCS 2102, pp. 454\u2013464. 2001."},{"key":"18_CR6","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pages 1\u201312, Stanford, 1962."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"O. Burkart. Model checking rationally restricted right closures of recognizable graphs. In 2nd INFINITY, 1997.","DOI":"10.1016\/S1571-0661(05)80424-4"},{"issue":"2","key":"18_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"13th CAV","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi. Benefits of bounded model checking at an industrial setting. In 13th CAV, LNCS 2102, pp. 436\u2013453. Springer-Verlag, 2001."},{"key":"18_CR10","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. Tree automata, \u03bc-calculus and determinacy. In 32nd FOCS, pp. 368\u2013377, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"5th CAV","author":"E.A. Emerson","year":"1993","unstructured":"E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of \u03bc-calculus. In 5th CAV, LNCS 697, pp. 385\u2013396, 1993. Springer-Verlag."},{"issue":"2","key":"18_CR13","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0020-0190(87)90097-4","volume":"24","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson. Uniform inevitability is tree automaton ineffable. Information Processing Letters, 24(2):77\u201379, January 1987.","journal-title":"Information Processing Letters"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation (2nd Edition). Addison-Wesley, 2000.","DOI":"10.1145\/568438.568455"},{"issue":"2","key":"18_CR15","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1006\/inco.1994.1073","volume":"113","author":"D. Harel","year":"1994","unstructured":"D. Harel and D. Raz. Deciding emptiness for stack automata on infinite trees. Information and Computation, 113(2):278\u2013299, September 1994.","journal-title":"Information and Computation"},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/3-540-60246-1_160","volume-title":"Proc. 20th MFCS","author":"D. Janin","year":"1995","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal \u03bc-calculus and related results. In Proc. 20th MFCS, LNCS 969, pp. 552\u2013562. Springer-Verlag, 1995."},{"key":"18_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/3-540-45657-0_31","volume-title":"Proc. 14th CAV","author":"O. Kupferman","year":"2002","unstructured":"O. Kupferman, N. Piterman, and M.Y. Vardi. Model checking linear properties of prefix-recognizable systems. In Proc. 14th CAV, LNCS 2404, pp. 371\u2013385. 2002."},{"key":"18_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/10722167_7","volume-title":"12th CAV","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman and M.Y. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In 12th CAV, LNCS 1855, pp. 36\u201352. Springer-Verlag, 2000."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. On clopen specifications. In Proc. 8th LPAR, LNAI 2250, pp. 24\u201338. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45653-8_2"},{"issue":"2","key":"18_CR20","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, March 2000.","journal-title":"Journal of the ACM"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d-on the temporal logic of programs. In 7th POPL, pp. 174\u2013185, 1980.","DOI":"10.1145\/567446.567463"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In 12th POPL, pp. 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"18_CR23","unstructured":"M.L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1967."},{"key":"18_CR24","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"D.E. Muller and P.E. Schupp. The theory of ends, pushdown automata, and second order logic. Theoretical Computer Science, 37:51\u201375, 1985.","journal-title":"Theoretical Computer Science"},{"key":"18_CR25","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267\u2013276, 1987.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"18_CR26","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1142\/S0129054195000123","volume":"6","author":"W. Peng","year":"1995","unstructured":"W. Peng and S. P. Iyer. A new typee of pushdown automata on infinite tree. IJFCS, 6(2):169\u2013186, 1995.","journal-title":"IJFCS"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In 18th FOCS, pp. 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In 12th ICALP, pp. 15\u201332. Springer-Verlag, 1985.","DOI":"10.1007\/BFb0015727"},{"key":"18_CR29","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th Int. Symp. on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int. Symp. on Programming, LNCS 137, pp. 337\u2013351, 1981."},{"key":"18_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1\u201335, 1969.","journal-title":"Transaction of the AMS"},{"issue":"1\/2","key":"18_CR31","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/S0019-9958(84)80043-1","volume":"63","author":"A. Sistla","year":"1984","unstructured":"A. Sistla, E.M. Clarke, N. Francez, and Y Gurevich. Can message buffers be axiomatized in linear temporal logic. Information and Control, 63(1\/2):88\u2013112, 1984.","journal-title":"Information and Control"},{"key":"18_CR32","series-title":"Lect Notes Comput Sci","first-page":"130","volume-title":"5th. DLT","author":"W. Thomas","year":"2001","unstructured":"W. Thomas. A short introduction to infinite automata. In 5th. DLT, LNCS 2295, pp. 130\u2013144. Springer-Verlag, July 2001."},{"key":"18_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"25th ICALP","author":"M.Y. Vardi","year":"1998","unstructured":"M.Y. Vardi. Reasoning about the past with two-way automata. In 25th ICALP, LNCS 1443, pp. 628\u2013641. Springer-Verlag, 1998."},{"key":"18_CR34","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In 1st LICS, pp. 332\u2013344, 1986."},{"issue":"2","key":"18_CR35","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I. Walukiewicz","year":"2001","unstructured":"I. Walukiewicz. Pushdown processes: Games and model-checking. Information and Computation, 164(2):234\u2013263, 2001.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:00:11Z","timestamp":1737061211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}