{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:40Z","timestamp":1751660500225},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_35","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T17:27:52Z","timestamp":1252949272000},"page":"485-499","source":"Crossref","is-referenced-by-count":6,"title":["Model Checking FO(R) over One-Counter Processes and beyond"],"prefix":"10.1007","author":[{"given":"Anthony Widjaja","family":"To","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","unstructured":"Bekker, W., Goranko, V.: Symbolic model checking of tense logics on rational Kripke models. To appear in proceedings of ILC 2007 (2007)"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"Blumensath, A., Gr\u00e4del, E.: Automatic structures. In: LICS 2000, pp. 51\u201362 (2000)","DOI":"10.1109\/LICS.2000.855755"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"issue":"1","key":"35_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(90)90080-L","volume":"48","author":"K.J. Compton","year":"1990","unstructured":"Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. Ann. Pure Appl. Logic\u00a048(1), 1\u201379 (1990)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"35_CR5","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J. Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput.\u00a0186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"issue":"2","key":"35_CR6","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/inco.2001.2953","volume":"179","author":"K. Etessami","year":"2002","unstructured":"Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput.\u00a0179(2), 279\u2013295 (2002)","journal-title":"Inf. Comput."},{"key":"35_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"J. Ferrante","year":"1979","unstructured":"Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories, vol.\u00a0718. Springer, Heidelberg (1979)"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"G\u00f6ller, S., Mayr, R., To, A.W.: On the computational complexity of verifying one-counter processes. To appear in LICS 2009 (2009)","DOI":"10.1109\/LICS.2009.37"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Grohe, M., Schweikardt, N.: The succinctness of first-order logic on linear orders. Logical Methods in Computer Science 1(1) (2005)","DOI":"10.2168\/LMCS-1(1:6)2005"},{"issue":"5","key":"35_CR10","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.ipl.2007.06.006","volume":"104","author":"P. Jancar","year":"2007","unstructured":"Jancar, P., Sawa, Z.: A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett.\u00a0104(5), 164\u2013167 (2007)","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"35_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0890-5401(03)00171-8","volume":"188","author":"P. Jan\u010dar","year":"2004","unstructured":"Jan\u010dar, P., Ku\u010dera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inf. Comput.\u00a0188(1), 1\u201319 (2004)","journal-title":"Inf. Comput."},{"key":"35_CR12","volume-title":"Theory of Computation","author":"D.C. Kozen","year":"2006","unstructured":"Kozen, D.C.: Theory of Computation. Springer, Heidelberg (2006)"},{"issue":"3","key":"35_CR13","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1016\/0022-0000(88)90039-6","volume":"36","author":"M.W. Krentel","year":"1988","unstructured":"Krentel, M.W.: The complexity of optimization problems. J. Comput. Syst. Sci.\u00a036(3), 490\u2013509 (1988)","journal-title":"J. Comput. Syst. Sci."},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-45022-X_28","volume-title":"Automata, Languages and Programming","author":"A. Ku\u010dera","year":"2000","unstructured":"Ku\u010dera, A.: Efficient verification algorithms for one-counter processes. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 317\u2013328. Springer, Heidelberg (2000)"},{"key":"35_CR15","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements Of Finite Model Theory","author":"L. Libkin","year":"2004","unstructured":"Libkin, L.: Elements Of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"issue":"2","key":"35_CR16","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/s00224-004-1170-6","volume":"39","author":"C. L\u00f6ding","year":"2006","unstructured":"L\u00f6ding, C.: Reachability problems on regular ground tree rewriting graphs. Theory Comput. Syst.\u00a039(2), 347\u2013383 (2006)","journal-title":"Theory Comput. Syst."},{"issue":"1-3","key":"35_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.apal.2003.11.002","volume":"126","author":"J.A. Makowsky","year":"2004","unstructured":"Makowsky, J.A.: Algorithmic uses of the Feferman-Vaught Theorem. Ann. Pure Appl. Logic\u00a0126(1-3), 159\u2013213 (2004)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1-2","key":"35_CR18","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0304-3975(00)00101-8","volume":"256","author":"R. Mayr","year":"2001","unstructured":"Mayr, R.: Decidability of model checking with the temporal logic EF. Theor. Comput. Sci.\u00a0256(1-2), 31\u201362 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"35_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-46432-8_17","volume-title":"Foundation of Software Science and Computation Structures","author":"C. Morvan","year":"2000","unstructured":"Morvan, C.: On rational graphs. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol.\u00a01784, pp. 252\u2013266. Springer, Heidelberg (2000)"},{"key":"35_CR20","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci.\u00a037, 51\u201375 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"35_CR21","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(92)90328-D","volume":"93","author":"P. P\u00e9ladeau","year":"1992","unstructured":"P\u00e9ladeau, P.: Logically defined subsets of N k . Theor. Comput. Sci.\u00a093(2), 169\u2013183 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"35_CR22","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1182613.1182617","volume":"8","author":"A. Rabinovich","year":"2007","unstructured":"Rabinovich, A.: On compositionality and its limitations. ACM Trans. Comput. Logic\u00a08(1), 4 (2007)","journal-title":"ACM Trans. Comput. Logic"},{"key":"35_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/11690634_23","volume-title":"Foundations of Software Science and Computation Structures","author":"O. Serre","year":"2006","unstructured":"Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 337\u2013351. Springer, Heidelberg (2006)"},{"key":"35_CR24","unstructured":"Stockmeyer, L.J.: The complexity of decision problems in automata theory and logic. PhD thesis, Department of Electrical Engineering, MIT (1974)"},{"key":"35_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-45138-9_6","volume-title":"Mathematical Foundations of Computer Science 2003","author":"W. Thomas","year":"2003","unstructured":"Thomas, W.: Constructing infinite graphs with a decidable MSO-theory. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 113\u2013124. Springer, Heidelberg (2003)"},{"key":"35_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-540-89439-1_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A.W. To","year":"2008","unstructured":"To, A.W., Libkin, L.: Recurrent reachability analysis in regular model checking. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 198\u2013213. Springer, Heidelberg (2008)"},{"key":"35_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"I. Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 127\u2013138. Springer, Heidelberg (2000)"},{"issue":"2","key":"35_CR28","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I. Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput.\u00a0164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"W\u00f6hrle, S., Thomas, W.: Model checking synchronized products of infinite transition systems. Logical Methods in Computer Science\u00a03(4) (2007)","DOI":"10.2168\/LMCS-3(4:5)2007"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T15:19:27Z","timestamp":1558538367000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}