{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:13:04Z","timestamp":1759637584306},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_31","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"371-385","source":"Crossref","is-referenced-by-count":13,"title":["Model Checking Linear Properties of Prefix-Recognizable Systems"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. Unpublished manuscript, 2000.","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"O. Burkart and J. Esparza. More infinite results. Electronic Notes in TCS, 6, 1996.","DOI":"10.1016\/S1571-0661(05)80680-2"},{"key":"31_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, 135\u2013150, 1997."},{"key":"31_CR4","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, 454\u2013464, 2001."},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"O. Burkart and Y.-M. Quemener. Model checking of infinite graphs defined by graph grammers. In 1st Infinity, ENTCS 6, 1996.","DOI":"10.1016\/S1571-0661(05)01231-4"},{"key":"31_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"3rd Concur","author":"O. Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. In 3rd Concur, LNCS 630, 123\u2013137, 1992."},{"key":"31_CR7","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"O. Burkart and B. Steffen. Composition, decomposition and model checking of pushdown processes. Nordic J. Comut., 2:89\u2013125, 1995.","journal-title":"Nordic J. Comut."},{"key":"31_CR8","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O. Burkart","year":"1999","unstructured":"O. Burkart and B. Steffen. Model checking the full modal \u03bc-calculus for infinite sequential processes. Theoretical Computer Science, 221:251\u2013270, 1999.","journal-title":"Theoretical Computer Science"},{"key":"31_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-69678-4","volume-title":"Automatic verification of sequential infinite-state processes","author":"O. Burkart","year":"1997","unstructured":"O. Burkart. Automatic verification of sequential infinite-state processes. LNCS 1354."},{"key":"31_CR10","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"},{"key":"31_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/3-540-61440-0_128","volume-title":"23rd ICALP","author":"D. Caucal","year":"1996","unstructured":"D. Caucal. On infinite transition graphs having a decidable monadic theory. In 23rd ICALP, LNCS 1099, 194\u2013205, 1996."},{"key":"31_CR12","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":"C.F.F.+.0.1._.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, 436\u2013453, 2001."},{"key":"31_CR13","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. J. of ACM, 28(1):114\u2013133, January 1981.","DOI":"10.1145\/322234.322243"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"M. Dam. CTL* and ECTL* as fragments of the modal \u03bc-calculus. TCS, 126:77\u201396.","DOI":"10.1016\/0304-3975(94)90269-0"},{"key":"31_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"12th CAV","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In 12th CAV, LNCS 1855, 232\u2013247, 2000."},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. Jutla. Tree automata, \u03bc-calculus and determinacy. In Proc. 32nd FOCS, 368\u2013377, October 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"31_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-45500-0_16","volume-title":"4th STACS","author":"J. Esparza","year":"2001","unstructured":"J. Esparza, A. Kucera, and S. Schwoon. Model-checking LTL with regular valuations for pushdown systems. In 4th STACS, LNCS 2215, 316\u2013339, 2001."},{"key":"31_CR19","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional \u03bc-calculus. In 1st LICS, 267\u2013278, 1986."},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown automata. In 2nd Infinity, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"31_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60630-0_3","volume-title":"TACAS","author":"T. A. Henzinger","year":"1995","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to hytech. In TACAS, LNCS 1019, 41\u201371, 1995."},{"key":"31_CR22","unstructured":"O. Kupferman and A. Pnueli. Once and for all. In 10th LICS, 25\u201335, 1995."},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"31_CR24","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, 36\u201352, 2000."},{"key":"31_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-45653-8_2","volume-title":"8th LPAR","author":"O. Kupferman","year":"2001","unstructured":"O. Kupferman and M. Y. Vardi. On clopen specifications. In 8th LPAR, LNCS 2250, 24\u201338, 2001."},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Y. Vardi. Weak alternating automata are not that weak. ACM Trans. on Computational Logic, 2001(2):408\u2013429, July 2001.","DOI":"10.1145\/377978.377993"},{"issue":"2","key":"31_CR27","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":"31_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"9th CAV","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Petterson, and W. Yi. UPPAAL: Status & developments. In 9th CAV, LNCS 1254, 456\u2013459, 1997."},{"key":"31_CR29","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/322033.322037","volume":"24","author":"N. Lynch","year":"1977","unstructured":"N. Lynch. Log space recognition and translation of parenthesis languages. Journal ACM, 24:583\u2013590, 1977.","journal-title":"Journal ACM"},{"key":"31_CR30","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. TCS, 37:51\u201375, 1985.","journal-title":"TCS"},{"key":"31_CR31","unstructured":"N. Piterman. Extending temporal logic with \u03c9-automata. M.Sc. Thesis, The Weizmann Institute of Science, Israel, 2000. http:\/\/www.wisdom.weizmann.ac.il\/home\/nirp\/public_html\/ publications\/mscthesis.ps."},{"key":"31_CR32","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In 18th FOCS, 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"31_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"598","DOI":"10.1007\/3-540-44683-4_52","volume-title":"26th MFCS","author":"N. Piterman","year":"2001","unstructured":"N. Piterman and M. Vardi. From bidirectionality to alternation. In 26th MFCS, LNCS 2136, 598\u2013609, 2001."},{"key":"31_CR34","doi-asserted-by":"crossref","unstructured":"N. Piterman and M. Vardi. From bidirectionality to alternation. TCS, 2001. to appear.","DOI":"10.1007\/3-540-44683-4_52"},{"key":"31_CR35","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, 628\u2013641, 1998."},{"issue":"1","key":"31_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"key":"31_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"8th CAV","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Pushdown processes: games and modal logic. In 8th CAV, LNCS 1102, 62\u201374, 1996."},{"key":"31_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"20th FSTTCS","author":"I. Walukiewicz","year":"2000","unstructured":"I. Walukiewicz. Model checking ctl properties of pushdown systems. In 20th FSTTCS, LNCS 1974, 127\u2013138, 2000."},{"key":"31_CR39","doi-asserted-by":"crossref","unstructured":"P. Wolper, M. Y. Vardi, and A. P. Sistla. Reasoning about infinite computation paths. In 24th FOCS, 185\u2013194, 1983.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:21:19Z","timestamp":1556428879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_31","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}