{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:49:15Z","timestamp":1725738555894},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642392115"},{"type":"electronic","value":"9783642392122"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39212-2_17","type":"book-chapter","created":{"date-parts":[[2013,7,2]],"date-time":"2013-07-02T13:09:19Z","timestamp":1372770559000},"page":"162-173","source":"Crossref","is-referenced-by-count":6,"title":["On the Complexity of Verifying Regular Properties on Flat Counter Systems,"],"prefix":"10.1007","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amit Kumar","family":"Dhar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 227\u2013242. Springer, Heidelberg (2010)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counter automata, safety analysis and PA. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"17_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-31365-3_16","volume-title":"Automated Reasoning","author":"S. Demri","year":"2012","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: Taming Past LTL and Flat Counter Systems. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 179\u2013193. Springer, Heidelberg (2012)"},{"key":"17_CR5","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: On the complexity of verifying regular properties on flat counter systems (2013), \n                    \n                      http:\/\/arxiv.org\/abs\/1304.6301"},{"issue":"4","key":"17_CR6","first-page":"313","volume":"20","author":"S. Demri","year":"2010","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking \n                    \n                      \n                    \n                    $\\textsf{CTL}^{*}$\n                   over flat Presburger counter systems. JANCL\u00a020(4), 313\u2013344 (2010)","journal-title":"JANCL"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"issue":"5","key":"17_CR8","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.ipl.2007.06.006","volume":"104","author":"P. Jan\u010dar","year":"2007","unstructured":"Jan\u010dar, P., Sawa, Z.: A note on emptiness for alternating finite automata with a one-letter alphabet. IPL\u00a0104(5), 164\u2013167 (2007)","journal-title":"IPL"},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M. Jurdzi\u0144ski","year":"1998","unstructured":"Jurdzi\u0144ski, M.: Deciding the winner in parity games is in UP \u2229 co-UP. IPL\u00a068(3), 119\u2013124 (1998)","journal-title":"IPL"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-23217-6_28","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"L. Kuhtz","year":"2011","unstructured":"Kuhtz, L., Finkbeiner, B.: Weak kripke structures and LTL. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 419\u2013433. Springer, Heidelberg (2011)"},{"issue":"3","key":"17_CR11","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"7-8","key":"17_CR12","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/s00236-005-0164-4","volume":"41","author":"A. Ku\u010dera","year":"2005","unstructured":"Ku\u010dera, A., Strej\u010dek, J.: The stuttering principle revisited. Acta Informatica\u00a041(7-8), 415\u2013434 (2005)","journal-title":"Acta Informatica"},{"key":"17_CR13","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: LICS 2002, pp. 383\u2013392. IEEE (2002)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J. Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter systems are everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-45187-7_17","volume-title":"CONCUR 2003 - Concurrency Theory","author":"N. Markey","year":"2003","unstructured":"Markey, N., Schnoebelen, P.: Model checking a path. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 251\u2013265. Springer, Heidelberg (2003)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Markey, N., Schnoebelen, P.: Mu-calculus path checking. IPL\u00a097(6) (2006)","DOI":"10.1016\/j.ipl.2005.11.010"},{"key":"17_CR17","unstructured":"Minsky, M.: Computation, Finite and Infinite Machines. Prentice Hall (1967)"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theor. Comput. Sci.\u00a032, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR19","unstructured":"Piterman, N.: Extending temporal logic with \u03c9-automata. Master\u2019s thesis, The Weizmann Institute of Science (2000)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-53904-2_94","volume-title":"Rewriting Techniques and Applications","author":"L. Pottier","year":"1991","unstructured":"Pottier, L.: Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol.\u00a0488, pp. 162\u2013173. Springer, Heidelberg (1991)"},{"issue":"3","key":"17_CR21","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. JACM\u00a032(3), 733\u2013749 (1985)","journal-title":"JACM"},{"key":"17_CR22","unstructured":"Stockmeyer, L.J.: The complexity of decision problems in automata and logic. PhD thesis, MIT (1974)"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Vardi, M.: A temporal fixpoint calculus. In: POPL 1988, pp. 250\u2013259. ACM (1988)","DOI":"10.1145\/73560.73582"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115 (1994)","DOI":"10.1006\/inco.1994.1092"},{"key":"17_CR25","first-page":"72","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. I&C\u00a056, 72\u201399 (1983)","journal-title":"I&C"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39212-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:43:03Z","timestamp":1558316583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39212-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642392115","9783642392122"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39212-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}