{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T09:36:17Z","timestamp":1769765777803,"version":"3.49.0"},"reference-count":56,"publisher":"Informa UK Limited","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[2010,1]]},"DOI":"10.3166\/jancl.20.313-344","type":"journal-article","created":{"date-parts":[[2011,3,10]],"date-time":"2011-03-10T03:49:26Z","timestamp":1299728966000},"page":"313-344","source":"Crossref","is-referenced-by-count":12,"title":["Model-checking CTL* over flat Presburger counter systems"],"prefix":"10.1080","volume":"20","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[{"name":"LSV, ENS Cachan, CNRS, INRIA","place":["France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[{"name":"LSV, ENS Cachan, CNRS, INRIA","place":["France"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valentin","family":"Goranko","sequence":"additional","affiliation":[{"name":"Technical University of Denmark","place":["Denmark"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Govert","family":"van Drimmelen","sequence":"additional","affiliation":[{"name":"University of Johannesburg","place":["South Africa"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"301","published-online":{"date-parts":[[2012,4,13]]},"reference":[{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_3_1","first-page":"368","volume-title":"CAV'01, volume 2102 of Lecture Notes in Computer Science","author":"Annichini A.","year":"2001","unstructured":"Annichini , A. , Bouajjani , A. and Sighireanu , M. 2001 . \u201c TReX: a tool for reachablity analysis of complex systems \u201d . In CAV'01, volume 2102 of Lecture Notes in Computer Science , 368 \u2013 372 . Springer ."},{"key":"e_1_2_1_4_1","first-page":"576","volume-title":"TACAS'04, volume 2988 of Lecture Notes in Computer Science","author":"Bardin S.","year":"2004","unstructured":"Bardin , S. , Finkel , A. and Leroux , J. 2004 . \u201c FASTer acceleration of counter automata in practice \u201d . In TACAS'04, volume 2988 of Lecture Notes in Computer Science , 576 \u2013 590 . Springer ."},{"key":"e_1_2_1_5_1","first-page":"118","volume-title":"CAV'03, volume 2725 of Lecture Notes in Computer Science","author":"Bardin S.","year":"2003","unstructured":"Bardin , S. , Finkel , A. , Leroux , J. and Petrucci , L. 2003 . \u201c FAST: Fast Acceleration of Symbolic Transition systems \u201d . In CAV'03, volume 2725 of Lecture Notes in Computer Science , 118 \u2013 121 . Springer ."},{"key":"e_1_2_1_6_1","first-page":"474","volume-title":"ATVA'05, volume 3707 of Lecture Notes in Computer Science","author":"Bardin S.","year":"2005","unstructured":"Bardin , S. , Finkel , A. , Leroux , J. and Schnoebelen , P. 2005 . \u201c Flat acceleration in symbolic model checking \u201d . In ATVA'05, volume 3707 of Lecture Notes in Computer Science , 474 \u2013 488 . Springer ."},{"key":"e_1_2_1_7_1","volume-title":"AVIS'06","author":"Bardin S.","year":"2006","unstructured":"Bardin , S. , Finkel , A. , Lozes , E. and Sangnier , A. 2006a . \u201c From pointer systems to counter systems using shape analysis \u201d . In AVIS'06"},{"key":"e_1_2_1_8_1","first-page":"63","volume-title":"CAV'06, volume 4144 of Lecture Notes in Computer Science","author":"Bardin S.","year":"2006","unstructured":"Bardin , S. , Leroux , J. and Point , G. 2006b . \u201c FAST Extended Release \u201d . In CAV'06, volume 4144 of Lecture Notes in Computer Science , 63 \u2013 66 . Springer ."},{"key":"e_1_2_1_9_1","first-page":"596","volume-title":"Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS)","author":"Blumensath A.","unstructured":"Blumensath , A. Axiomatising tree-interpretable structures . Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS) . pp. 596 \u2013 607 . Springer-Verlag ."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1133-y"},{"key":"e_1_2_1_11_1","volume-title":"Symbolic methods for exploring infinite state spaces","author":"Boigelot B.","year":"1998","unstructured":"Boigelot , B. 1998 . Symbolic methods for exploring infinite state spaces , Universit\u00e9 de Li\u00e8ge . PhD thesis"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00314-1"},{"key":"e_1_2_1_13_1","first-page":"55","volume-title":"CAV'94, volume 818 of Lecture Notes in Computer Science","author":"Boigelot B.","year":"1994","unstructured":"Boigelot , B. and Wolper , P. 1994 . \u201c Symbolic verification with periodic sets \u201d . In CAV'94, volume 818 of Lecture Notes in Computer Science , 55 \u2013 67 . Springer ."},{"key":"e_1_2_1_14_1","first-page":"299","volume-title":"Proceedings of the American Mathematical Society","volume":"55","author":"Borosh I.","unstructured":"Borosh , I. and Treybig , L. Bounds on positive integral solutions of linear Diophantine equations . Proceedings of the American Mathematical Society . Vol. 55 , pp. 299 \u2013 304 ."},{"key":"e_1_2_1_15_1","first-page":"517","volume-title":"CAV'06, volume 4144 of Lecture Notes in Computer Science","author":"Bouajjani A.","year":"2006","unstructured":"Bouajjani , A. , Bozga , M. , Habermehl , P. , Iosif , R. , Moro , P. and Vojnar , T. 2006 . \u201c Programs with lists are counter automata \u201d . In CAV'06, volume 4144 of Lecture Notes in Computer Science , 517 \u2013 531 . Springer ."},{"key":"e_1_2_1_16_1","first-page":"123","volume-title":"LICS'95","author":"Bouajjani A.","year":"1995","unstructured":"Bouajjani , A. , Echahed , R. and Habermehl , P. 1995 . \u201c On the verification problem of nonregular properties for nonregular processes \u201d . In LICS'95 123 \u2013 133 ."},{"key":"e_1_2_1_17_1","first-page":"135","volume-title":"CONCUR'97, volume 1243 of LNCS","author":"Bouajjani A.","year":"1997","unstructured":"Bouajjani , A. , Esparza , J. and Maler , O. 1997 . \u201c Reachability analysis of pushdown automata: Application to model checking \u201d . In CONCUR'97, volume 1243 of LNCS , 135 \u2013 150 . Springer ."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00033-X"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2009-0044"},{"key":"e_1_2_1_20_1","first-page":"687","volume-title":"STACS'03, volume 2607 of Lecture Notes in Computer Science","author":"Bruy\u00e8re V.","year":"2003","unstructured":"Bruy\u00e8re , V. , Dall'Olio , E. and Raskin , J. 2003 . \u201c Durations, parametric model-checking in timed automata with Presburger arithmetic \u201d . In STACS'03, volume 2607 of Lecture Notes in Computer Science , 687 \u2013 698 . Springer ."},{"key":"e_1_2_1_21_1","first-page":"400","volume-title":"CAV'97, volume 1254 of Lecture Notes in Computer Science","author":"Bultan T.","year":"1997","unstructured":"Bultan , T. , Gerber , R. and Pugh , W. 1997 . \u201c Symbolic model checking of infinite state systems using Presburger arithmetic \u201d . In CAV'97, volume 1254 of Lecture Notes in Computer Science , 400 \u2013 411 . Springer ."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1016\/B978-044482830-9\/50027-8","volume-title":"Handbook of Process Algebra","author":"Burkart O.","year":"2001","unstructured":"Burkart , O. , Caucal , D. , Moller , F. and Steffen , B. 2001 . \u201c Verification of infinite structures \u201d . In Handbook of Process Algebra , 545 \u2013 623 . Elsevier ."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00089-5"},{"key":"e_1_2_1_24_1","first-page":"35","volume-title":"ICALP, volume 820 of Lecture Notes in Computer Science","author":"\u010cer\u0101ns K.","year":"1994","unstructured":"\u010cer\u0101ns , K. 1994 . \u201c Deciding properties of integral relational automata \u201d . In ICALP, volume 820 of Lecture Notes in Computer Science , 35 \u2013 46 . Springer ."},{"key":"e_1_2_1_25_1","first-page":"262","volume-title":"CSL'00, volume 1862 of Lecture Notes in Computer Science","author":"Comon H.","year":"2000","unstructured":"Comon , H. and Cortier , V. 2000 . \u201c Flatness is not a weakness \u201d . In CSL'00, volume 1862 of Lecture Notes in Computer Science , 262 \u2013 276 . Springer ."},{"key":"e_1_2_1_26_1","first-page":"268","volume-title":"CAV'98, volume 1427 of Lecture Notes in Computer Science","author":"Comon H.","year":"1998","unstructured":"Comon , H. and Jurski , Y. 1998 . \u201c Multiple counters automata, safety analysis and Presburger analysis \u201d . In CAV'98, volume 1427 of Lecture Notes in Computer Science , 268 \u2013 279 . Springer ."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2003001"},{"key":"e_1_2_1_28_1","first-page":"193","volume-title":"Handbook of Theoretical Computer Science, Volume B, Formalmodels and semantics","author":"Courcelle B.","year":"1990","unstructured":"Courcelle , B. 1990 . \u201c Graph rewriting: An algebraic and logic approach \u201d . In Handbook of Theoretical Computer Science, Volume B, Formalmodels and semantics , Edited by: Leeuwen , J. V. 193 \u2013 242 . Elsevier ."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00485-1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.02.019"},{"key":"e_1_2_1_31_1","first-page":"493","volume-title":"Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of Lecture Notes in Computer Science","author":"Demri S.","unstructured":"Demri , S. , Finkel , A. , Goranko , V. and van Drimmelen , G. Towards a model-checker for counter systems . Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of Lecture Notes in Computer Science . pp. 493 \u2013 507 . Springer ."},{"key":"e_1_2_1_32_1","series-title":"IIsc Research Monographs","volume-title":"Modern Applications of Automata Theory","author":"Demri S.","year":"2009","unstructured":"Demri , S. and Gastin , P. 2009 . Modern Applications of Automata Theory , IIsc Research Monographs World Scientific . chapter Specification and Verification using Temporal Logics, To appear"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_34_1","first-page":"70","volume-title":"LICS'98","author":"Emerson A.","year":"1998","unstructured":"Emerson , A. and Namjoshi , K. 1998 . \u201c On model checking for non-deterministic infinite-state systems \u201d . In LICS'98 , 70 \u2013 80 . IEEE ."},{"key":"e_1_2_1_35_1","first-page":"352","volume-title":"LICS'99","author":"Esparza J.","year":"1999","unstructured":"Esparza , J. , Finkel , A. and Mayr , R. 1999 . \u201c On the verification of broadcast protocols \u201d . In LICS'99 352 \u2013 359 ."},{"key":"e_1_2_1_36_1","first-page":"145","volume-title":"FST&TCS'02, volume 2256 of Lecture Notes in Computer Science","author":"Finkel A.","year":"2002","unstructured":"Finkel , A. and Leroux , J. 2002 . \u201c How to compose Presburger accelerations: Applications to broadcast protocols \u201d . In FST&TCS'02, volume 2256 of Lecture Notes in Computer Science , 145 \u2013 156 . Springer ."},{"key":"e_1_2_1_37_1","volume-title":"Infinity in Logic and Computation, volume 5489 of Lecture Notes in Artificial Intelligence","author":"Finkel A.","year":"2009","unstructured":"Finkel , A. , Lozes , E. and Sangnier , A. 2009 . \u201c Towards model-checking programs with lists \u201d . In Infinity in Logic and Computation, volume 5489 of Lecture Notes in Artificial Intelligence , Springer . To appear"},{"key":"e_1_2_1_38_1","first-page":"346","volume-title":"STACS'00, volume 2256 of Lecture Notes in Computer Science","author":"Finkel A.","year":"2000","unstructured":"Finkel , A. and Sutre , G. 2000 . \u201c Decidability of reachability problems for classes of two counters automata \u201d . In STACS'00, volume 2256 of Lecture Notes in Computer Science , 346 \u2013 357 . Springer ."},{"key":"e_1_2_1_39_1","volume-title":"INFINITY'97, volume 9 of ENTCS","author":"Finkel A.","year":"1997","unstructured":"Finkel , A. , Willems , B. and Wolper , P. 1997 . \u201c A direct symbolic approach to model checking pushdown systems (extended abstract) \u201d . In INFINITY'97, volume 9 of ENTCS , Elsevier Science ."},{"key":"e_1_2_1_40_1","first-page":"213","volume-title":"CONCUR'97, volume 1243 of Lecture Notes in Computer Science","author":"Fribourg L.","year":"1997","unstructured":"Fribourg , L. and Ols\u00e9n , H. 1997 . \u201c Proving safety properties of infinite state systems by compilation into presburger arithmetic \u201d . In CONCUR'97, volume 1243 of Lecture Notes in Computer Science , 213 \u2013 227 . Springer ."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1966.16.285"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/322047.322058"},{"key":"e_1_2_1_44_1","first-page":"426","volume-title":"MFCS'00, volume 1893 of Lecture Notes in Computer Science","author":"Ibarra O.","year":"2000","unstructured":"Ibarra , O. , Su , J. , Dang , Z. , Bultan , T. and Kemmerer , A. 2000 . \u201c Counter machines: Decidable properties and applications to verification problems \u201d . In MFCS'00, volume 1893 of Lecture Notes in Computer Science , 426 \u2013 435 . Springer ."},{"key":"e_1_2_1_45_1","first-page":"367","volume-title":"Logic and Computation Complexity, volume 1995 of Lecture Notes in Computer Science","author":"Khoussainov B.","year":"1995","unstructured":"Khoussainov , B. and Nerode , A. 1995 . \u201c Automatic presentations of structures \u201d . In Logic and Computation Complexity, volume 1995 of Lecture Notes in Computer Science , 367 \u2013 392 . Berlin : Springer ."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1985.11971528"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2817"},{"key":"e_1_2_1_48_1","volume-title":"Algorithmique de la v\u00e9rification des syst\u00e8mes \u00e0 compteurs. Approximation et acc\u00e9l\u00e9ration. Impl\u00e9mentation de l'outil FAST","author":"Leroux J.","year":"2003","unstructured":"Leroux , J. 2003 . Algorithmique de la v\u00e9rification des syst\u00e8mes \u00e0 compteurs. Approximation et acc\u00e9l\u00e9ration. Impl\u00e9mentation de l'outil FAST , France : ENS de Cachan . PhD thesis"},{"key":"e_1_2_1_49_1","volume-title":"Regular acceleration for number decision diagrams","author":"Leroux J.","year":"2006","unstructured":"Leroux , J. 2006 . Regular acceleration for number decision diagrams , LABRI . Technical Report 1385-06"},{"key":"e_1_2_1_50_1","first-page":"489","volume-title":"ATVA'05, volume 3707 of Lecture Notes in Computer Science","author":"Leroux J.","year":"2005","unstructured":"Leroux , J. and Sutre , G. 2005 . \u201c Flat counter systems are everywhere! \u201d . In ATVA'05, volume 3707 of Lecture Notes in Computer Science , 489 \u2013 503 . Springer ."},{"key":"e_1_2_1_51_1","volume-title":"Computation, Finite and Infinite Machines","author":"Minsky M.","year":"1967","unstructured":"Minsky , M. 1967 . Computation, Finite and Infinite Machines , Prentice Hall ."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90087-8"},{"key":"e_1_2_1_53_1","first-page":"345","volume-title":"DLT'04, volume 3340 of Lecture Notes in Computer Science","author":"Papadimitriou C.","year":"1981","unstructured":"Papadimitriou , C. 1981 . \u201c On the complexity of integer programming. JACM, 28(4), 765\u2013768. Potapov, I. (2004). From Post systems to the reachability problems for matrix semigroups and multicounter automata \u201d . In DLT'04, volume 3340 of Lecture Notes in Computer Science , 345 \u2013 356 . Springer ."},{"key":"e_1_2_1_54_1","first-page":"92","volume-title":"Comptes Rendus du premier congr\u00e8s de math\u00e9maticiens des Pays Slaves, Warszawa","author":"Presburger M.","year":"1929","unstructured":"Presburger , M. 1929 . \u201c \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt \u201d . In Comptes Rendus du premier congr\u00e8s de math\u00e9maticiens des Pays Slaves, Warszawa 92 \u2013 101 ."},{"key":"e_1_2_1_55_1","first-page":"67","volume-title":"SEFM'04","author":"Schuele T.","year":"2004","unstructured":"Schuele , T. and Schneider , K. 2004 . \u201c Global vs. local model checking: A comparison of verification techniques for infinite state systems \u201d . In SEFM'04 , 67 \u2013 76 . IEEE ."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"},{"key":"e_1_2_1_57_1","first-page":"72","article-title":"Temporal logic can be more expressive","volume":"56","author":"Wolper P.","year":"1983","unstructured":"Wolper , P. 1983 . Temporal logic can be more expressive . Information and Computation , 56 : 72 \u2013 99 .","journal-title":"Information and Computation"}],"container-title":["Journal of Applied Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.tandfonline.com\/doi\/pdf\/10.3166\/jancl.20.313-344","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T18:18:15Z","timestamp":1769710695000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.tandfonline.com\/doi\/full\/10.3166\/jancl.20.313-344"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":56,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["10.3166\/jancl.20.313-344"],"URL":"https:\/\/doi.org\/10.3166\/jancl.20.313-344","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1]]}}}