{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T16:19:25Z","timestamp":1790439565055,"version":"4.1.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T00:00:00Z","timestamp":1433203200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["ReacHard 11-BS02-001-01"],"award-info":[{"award-number":["ReacHard 11-BS02-001-01"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,7,8]]},"abstract":"<jats:p>\n            We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is T\n            <jats:sc>ower<\/jats:sc>\n            -hard already in the affine case\u2014and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its T\n            <jats:sc>ower<\/jats:sc>\n            -completeness. We also show that provability in propositional contractive linear logic is A\n            <jats:sc>ckermann<\/jats:sc>\n            -complete.\n          <\/jats:p>","DOI":"10.1145\/2733375","type":"journal-article","created":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T18:19:47Z","timestamp":1433269187000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Nonelementary Complexities for Branching VASS, MELL, and Extensions"],"prefix":"10.1145","volume":"16","author":[{"given":"Ranko","family":"Lazi\u0107","sequence":"first","affiliation":[{"name":"DIMAP, Department of Computer Science, University of Warwick, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sylvain","family":"Schmitz","sequence":"additional","affiliation":[{"name":"ENS Cachan &amp; INRIA, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,6,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_9"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504081"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2518188"},{"key":"e_1_2_1_5_1","first-page":"478","article-title":"Reachability games on extended vector addition systems with states. In Proc. ICALP 2010. Lect. Notes","volume":"6199","author":"Br\u00e1zdil Tom\u00e1\u0161","year":"2010","unstructured":"Tom\u00e1\u0161 Br\u00e1zdil , Petr Jan\u010dar , and Anton\u00edn Ku\u010dera . 2010 . Reachability games on extended vector addition systems with states. In Proc. ICALP 2010. Lect. Notes in Comput. Sci. , Vol. 6199. Spring er, 478 -- 489 . DOI:10.1007\/978-3-642-14162-1&lowbar;40 10.1007\/978-3-642-14162-1&lowbar;40 Tom\u00e1\u0161 Br\u00e1zdil, Petr Jan\u010dar, and Anton\u00edn Ku\u010dera. 2010. Reachability games on extended vector addition systems with states. In Proc. ICALP 2010. Lect. Notes in Comput. Sci., Vol. 6199. Springer, 478--489. DOI:10.1007\/978-3-642-14162-1&lowbar;40","journal-title":"Comput. Sci."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_7_1","volume-title":"Proc. FSTTCS 2010. Leibniz Int. Proc. Inf.","volume":"8","author":"Chatterjee Krishnendu","year":"2010","unstructured":"Krishnendu Chatterjee , Laurent Doyen , Thomas A. Henzinger , and Jean-Fran\u00e7ois Raskin . 2010 . Generalized mean-payoff and energy games . In Proc. FSTTCS 2010. Leibniz Int. Proc. Inf. , Vol. 8 . LZI, 505--516. DOI:10.4230\/LIPIcs.FSTTCS.2010.505 10.4230\/LIPIcs.FSTTCS.2010.505 Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-Fran\u00e7ois Raskin. 2010. Generalized mean-payoff and energy games. In Proc. FSTTCS 2010. Leibniz Int. Proc. Inf., Vol. 8. LZI, 505--516. DOI:10.4230\/LIPIcs.FSTTCS.2010.505"},{"key":"e_1_2_1_8_1","first-page":"220","article-title":"Alternating vector addition systems with states. In Proc. MFCS 2014. Lect. Notes","volume":"8634","author":"Courtois Jean-Baptiste","year":"2014","unstructured":"Jean-Baptiste Courtois and Sylvain Schmitz . 2014 . Alternating vector addition systems with states. In Proc. MFCS 2014. Lect. Notes in Comput. Sci. , Vol. 8634. Spring er, 220 -- 231 . DOI:10.1007\/978-3-662-44522-8&lowbar;19 10.1007\/978-3-662-44522-8&lowbar;19 Jean-Baptiste Courtois and Sylvain Schmitz. 2014. Alternating vector addition systems with states. In Proc. MFCS 2014. Lect. Notes in Comput. Sci., Vol. 8634. Springer, 220--231. DOI:10.1007\/978-3-662-44522-8&lowbar;19","journal-title":"Comput. Sci."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.51"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2012.04.002"},{"key":"e_1_2_1_11_1","unstructured":"J\u00e9r\u00e9mie Dimino Florent Jacquemard and Luc Segoufin. 2013. FO2(&lt; &plus; 1 &sim;) on data trees data tree automata and an extension of BVASS. (2013). http:\/\/hal.inria.fr\/hal-00769249 Manuscript.  J\u00e9r\u00e9mie Dimino Florent Jacquemard and Luc Segoufin. 2013. FO 2 (&lt; &plus; 1 &sim;) on data trees data tree automata and an extension of BVASS. (2013). http:\/\/hal.inria.fr\/hal-00769249 Manuscript."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.39"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00060-G"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2834"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275637"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422091"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2010.06.008"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90075-B"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01967649"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322271"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586501"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.3115\/981732.981768"},{"key":"e_1_2_1_25_1","volume-title":"Proc. ACL","author":"Schmitz Sylvain","year":"2010","unstructured":"Sylvain Schmitz . 2010 . On the computational complexity of dominance links in grammatical formalisms . In Proc. ACL 2010. ACL Press, 514--524. Sylvain Schmitz. 2010. On the computational complexity of dominance links in grammatical formalisms. In Proc. ACL 2010. ACL Press, 514--524."},{"key":"e_1_2_1_26_1","unstructured":"Sylvain Schmitz. 2013. Complexity Hierarchies Beyond Elementary. Preprint. Retrieved from http:\/\/arxiv.org\/abs\/1312.5686.  Sylvain Schmitz. 2013. Complexity Hierarchies Beyond Elementary. Preprint. Retrieved from http:\/\/arxiv.org\/abs\/1312.5686."},{"key":"e_1_2_1_27_1","first-page":"395","article-title":"Implicational relevance logic is 2-ExpTime-complete. In Proc. RTA-TLCA 2014. Lect. Notes","volume":"8560","author":"Schmitz Sylvain","year":"2014","unstructured":"Sylvain Schmitz . 2014 . Implicational relevance logic is 2-ExpTime-complete. In Proc. RTA-TLCA 2014. Lect. Notes in Comput. Sci. , Vol. 8560. Spring er, 395 -- 409 . DOI:10.1007\/978-3-319-08918-8&lowbar;27 10.1007\/978-3-319-08918-8&lowbar;27 Sylvain Schmitz. 2014. Implicational relevance logic is 2-ExpTime-complete. In Proc. RTA-TLCA 2014. Lect. Notes in Comput. Sci., Vol. 8560. Springer, 395--409. DOI:10.1007\/978-3-319-08918-8&lowbar;27","journal-title":"Comput. Sci."},{"key":"e_1_2_1_28_1","first-page":"616","article-title":"Revisiting Ackermann-hardness for lossy counter machines and reset Petri Nets. In Proc. MFCS 2010. Lect. Notes","volume":"6281","author":"Schnoebelen Philippe","year":"2010","unstructured":"Philippe Schnoebelen . 2010 . Revisiting Ackermann-hardness for lossy counter machines and reset Petri Nets. In Proc. MFCS 2010. Lect. Notes in Comput. Sci. , Vol. 6281. Spring er, 616 -- 628 . DOI:10.1007\/978-3-642-15155-2&lowbar;54 10.1007\/978-3-642-15155-2&lowbar;54 Philippe Schnoebelen. 2010. Revisiting Ackermann-hardness for lossy counter machines and reset Petri Nets. In Proc. MFCS 2010. Lect. Notes in Comput. Sci., Vol. 6281. Springer, 616--628. DOI:10.1007\/978-3-642-15155-2&lowbar;54","journal-title":"Comput. Sci."},{"key":"e_1_2_1_29_1","volume-title":"CSLI Lecture Notes","volume":"29","author":"Troelstra Anne Sjerp","year":"1992","unstructured":"Anne Sjerp Troelstra . 1992 . Lectures on Linear Logic . CSLI Lecture Notes , Vol. 29 . Center for the Study of Language and Information. Anne Sjerp Troelstra. 1992. Lectures on Linear Logic. CSLI Lecture Notes, Vol. 29. Center for the Study of Language and Information."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586811"},{"key":"e_1_2_1_31_1","volume-title":"Proc. Logic Colloquium\u201998","volume":"13","author":"Urquhart Alasdair","year":"2000","unstructured":"Alasdair Urquhart . 2000 . The complexity of linear logic with weakening . In Proc. Logic Colloquium\u201998 . Lect. Notes in Logic , Vol. 13 . ASL, 500--515. Alasdair Urquhart. 2000. The complexity of linear logic with weakening. In Proc. Logic Colloquium\u201998. Lect. Notes in Logic, Vol. 13. ASL, 500--515."},{"key":"e_1_2_1_32_1","first-page":"217","article-title":"Karp-Miller trees for a branching extension of VASS","volume":"7","author":"Verma Kumar Neeraj","year":"2005","unstructured":"Kumar Neeraj Verma and Jean Goubault-Larrecq . 2005 . Karp-Miller trees for a branching extension of VASS . Disc. Math. Theor. Comput. Sci. 7 , 1 (2005), 217 -- 230 . Kumar Neeraj Verma and Jean Goubault-Larrecq. 2005. Karp-Miller trees for a branching extension of VASS. Disc. Math. Theor. Comput. Sci. 7, 1 (2005), 217--230.","journal-title":"Disc. Math. Theor. Comput. Sci."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2733375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2733375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:17:02Z","timestamp":1750227422000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2733375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,2]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,7,8]]}},"alternative-id":["10.1145\/2733375"],"URL":"https:\/\/doi.org\/10.1145\/2733375","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,2]]},"assertion":[{"value":"2014-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}