{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T10:40:25Z","timestamp":1743590425458,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_16","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T20:35:34Z","timestamp":1340310934000},"page":"179-193","source":"Crossref","is-referenced-by-count":7,"title":["Taming Past LTL and 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":"16_CR1","unstructured":"Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1090\/S0002-9939-1976-0396605-3","volume":"55","author":"I. Borosh","year":"1976","unstructured":"Borosh, I., Treybig, L.: Bounds on positive integral solutions of linear Diophantine equations. American Mathematical Society\u00a055, 299\u2013304 (1976)","journal-title":"American Mathematical Society"},{"key":"16_CR3","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":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-44622-2_17","volume-title":"Computer Science Logic","author":"H. Comon","year":"2000","unstructured":"Comon, H., Cortier, V.: Flatness Is Not a Weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 262\u2013276. Springer, Heidelberg (2000)"},{"key":"16_CR5","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":"16_CR6","doi-asserted-by":"crossref","unstructured":"Demri, S., Dhar, A., Sangnier, A.: Taming past LTL and flat counter systems. Technical report (2012), ArXiv","DOI":"10.1007\/978-3-642-31365-3_16"},{"issue":"4","key":"16_CR7","first-page":"313","volume":"20","author":"S. Demri","year":"2010","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Model-checking $\\textsf{CTL}^{*}$ over flat Presburger counter systems. JANCL\u00a020(4), 313\u2013344 (2010)","journal-title":"JANCL"},{"key":"16_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-540-74621-8_11","volume-title":"Frontiers of Combining Systems","author":"C. Dixon","year":"2007","unstructured":"Dixon, C., Fisher, M., Konev, B.: Temporal Logic with Capacity Constraints. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 163\u2013177. Springer, Heidelberg (2007)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359 (1999)","DOI":"10.1109\/LICS.1999.782630"},{"issue":"1\u20132","key":"16_CR10","first-page":"88","volume":"160","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Wilke, T.: An until hierarchy and other applications of an Ehrenfeucht-Fra\u00efss\u00e9 game for temporal logic. I&C\u00a0160(1\u20132), 88\u2013108 (2000)","journal-title":"I&C"},{"key":"16_CR11","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)"},{"key":"16_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-03092-5_6","volume-title":"Infinity in Logic and Computation","author":"A. Finkel","year":"2009","unstructured":"Finkel, A., Lozes, \u00c9., Sangnier, A.: Towards Model-Checking Programs with Lists. In: Archibald, M., Brattka, V., Goranko, V., L\u00f6we, B. (eds.) ILC 2007. LNCS (LNAI), vol.\u00a05489, pp. 56\u201386. Springer, Heidelberg (2009)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Temporal Logic in Specification","author":"D. Gabbay","year":"1989","unstructured":"Gabbay, D.: The Declarative Past and Imperative Future. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol.\u00a0398, pp. 409\u2013448. Springer, Heidelberg (1989)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-04081-8_25","volume-title":"CONCUR 2009 - Concurrency Theory","author":"C. Haase","year":"2009","unstructured":"Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in Succinct and Parametric One-Counter Automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 369\u2013383. Springer, Heidelberg (2009)"},{"key":"16_CR15","unstructured":"Kuhtz, L.: Model Checking Finite Paths and Trees. PhD thesis, Universit\u00e4t des Saarlandes (2010)"},{"key":"16_CR16","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":"7\u20138","key":"16_CR17","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\u20138), 415\u2013434 (2005)","journal-title":"Acta Informatica"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: LICS 2002, pp. 383\u2013392. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029846"},{"key":"16_CR19","first-page":"236","volume":"156","author":"F. Laroussinie","year":"2000","unstructured":"Laroussinie, F., Schnoebelen, P.: Specification in CTL + past for verification in CTL. I&C\u00a0156, 236\u2013263 (2000)","journal-title":"I&C"},{"key":"16_CR20","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 Automata Almost Everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"key":"16_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/3-540-45744-5_5","volume-title":"Automated Reasoning","author":"C. Lutz","year":"2001","unstructured":"Lutz, C.: NE ${\\textsc{xp}}$ T ${\\textsc{ime}}$ -Complete Description Logics with Concrete Domains. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 45\u201360. Springer, Heidelberg (2001)"},{"key":"16_CR22","unstructured":"Minsky, M.: Computation, Finite and Infinite Machines. Prentice Hall (1967)"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. IPL\u00a063, 243\u2013246 (1997)","journal-title":"IPL"},{"issue":"2","key":"16_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS\u00a06(2), 223\u2013231 (1978)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T10:17:03Z","timestamp":1743589023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}