K. Bimbó, The decidability of the intensional fragment of classical linear logic, Theor. Comput. Sci, vol.597, pp.1-17, 2015.

K. Bimbó and J. Michael-dunn, On the decidability of implicational ticket entailment, J. Symb. Log, vol.78, issue.1, pp.214-236, 2013.

A. Carbone, Turning cycles into spirals, Ann. Pure Appl. Logic, vol.96, issue.1-3, pp.57-73, 1999.
DOI : 10.1016/s0168-0072(98)00031-1
URL : https://doi.org/10.1016/s0168-0072(98)00031-1

K. Chaudhuri, Undecidability of multiplicative subexponential logic, 3rd International Workshop on Linearity (LINEARITY), vol.176, pp.1-8, 2014.
DOI : 10.4204/eptcs.176.1
URL : https://hal.archives-ouvertes.fr/hal-00998753

J. E. Dawson and R. Goré, Issues in machine-checking the decidability of implicational ticket entailment, Automated Reasoning with Analytic Tableaux and Related Methods-26th International Conference, vol.10501, pp.347-363, 2017.

P. De-groote, B. Guillaume, and S. Salvati, Vector addition tree automata, 19th IEEE Symposium on Logic in Computer Science (LICS 2004, pp.64-73, 2004.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, pp.1-102, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075966

A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, pp.1-64, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00441254

A. Guglielmi and T. Gundersen, Normalisation control in deep inference via atomic flows, Logical Methods in Computer Science, vol.4, issue.9, pp.1-36, 2008.
DOI : 10.2168/lmcs-4(1:9)2008
URL : https://lmcs.episciences.org/1081/pdf

A. Guglielmi, T. Gundersen, and L. Straßburger, Breaking paths in atomic flows for classical logic, LICS 2010, 2010.
DOI : 10.1109/lics.2010.12
URL : https://hal.archives-ouvertes.fr/hal-00541076

A. Guglielmi and L. Straßburger, Non-commutativity and MELL in the calculus of structures, Computer Science Logic, vol.2142, pp.54-68, 2001.

. Springer-verlag, , 2001.

, which are finite structures that are crucial for the decidability proof for VASS, play in that proof a similar role as the RMELL derivations in Bimbó's proof attempt for MELL. Given that it is still a big leap from Karp-Miller trees to the full decidability of the reachability problem for VASS, a proof of Conjecture 4.6 will very likely be much harder than it seems on first sight

A. Guglielmi and L. Straßburger, A non-commutative extension of MELL, Logic for Programming, vol.2514, pp.231-246, 2002.

A. Guglielmi and L. Straßburger, A system of interaction and structure V: the exponentials and splitting, Mathematical Structures in Computer Science, vol.21, issue.3, pp.563-584, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00441254

D. Nuel, J. R. Belnap, and . Wallace, A decision procedure for the system e¯ i of entailmengt with negation, Zeitschrift für Mathematische Logic und Grundlagen der Mathematik, vol.11, pp.277-289, 1965.

, Ozan Kahramano? gullar?. System BV is NP-complete. Annals of Pure and Applied Logic, 2007.

M. I. Kanovich, Horn programming in linear logic is NP-complete, Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS 92, 1992.

M. Richard, R. E. Karp, and . Miller, Parallel program schemata, J. Comput. Syst. Sci, vol.3, issue.2, pp.147-195, 1969.

S. R. Kosaraju, Decidability of reachability in vector addition systems (preliminary version), Proceedings of the 14th Annual ACM Symposium on Theory of Computing, pp.267-281, 1982.

A. Saul and . Kripke, The problem of entailment (abstract), The Journal of Symbolic Logic, vol.24, issue.4, p.1959

Y. Lafont and A. Scedrov, The undecidability of second order multiplicative linear logic, Information and Computation, vol.125, pp.46-51, 1996.

J. Lambek, How to program an infinite abacus, Canad. Math. Bull, vol.4, issue.3, pp.295-302, 1961.

R. Lazic and S. Schmitz, Nonelementary complexities for branching VASS, MELL, and extensions, ACM Trans. Comput. Log, vol.16, issue.3, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01076694

J. Leroux, Vector addition systems reachability problem (A simpler solution), EPiC Series in Computing, vol.10, pp.214-228, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00674970

J. Leroux and S. Schmitz, Demystifying reachability in vector addition systems, 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, pp.56-67, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01168388

P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar, Decision problems for propositional linear logic, Annals of Pure and Applied Logic, vol.56, issue.1-3, pp.239-311, 1992.

R. J. Lipton, The reachability problem requires exponential space, 1976.

E. W. Mayr, An algorithm for the general petri net reachability problem, Proceedings of the 13th Annual ACM Symposium on Theory of Computing, pp.238-246, 1981.

E. W. Mayr, An algorithm for the general petri net reachability problem, SIAM J. Comput, vol.13, issue.3, pp.441-460, 1984.

M. L. Minsky, Recursive unsolvability of Post's problem of "tag" and other topics in theory of Turing machines, The Annals of Mathematics, vol.74, issue.3, pp.437-455, 1961.

V. Mogbil, Sémantique des phases, réseaux de preuve et diversprobì emes de décision en logique linéaire. (Phase semantics, proof nets and some decision problems in linear logic), 2001.

V. Nigam, Exploiting non-canonicity in the sequent calculus, 2009.
URL : https://hal.archives-ouvertes.fr/pastel-00005487

V. Nigam and D. Miller, Algorithmic specifications in linear logic with subexponentials, ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp.129-140, 2009.
DOI : 10.1145/1599410.1599427
URL : http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ppdp09.pdf

M. Okada and K. Terui, The finite model property for various fragments of intuitionistic linear logic, J. Symb. Log, vol.64, issue.2, pp.790-802, 1999.

V. Padovani, Ticket entailment is decidable. CoRR, abs/1106.1875, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00599342

C. A. Petri, Kommunikation mit Automaten. Dissertation, 1962.

C. Retoré, Pomset logic: A non-commutative extension of classical linear logic, Typed Lambda Calculus and Applications, TLCA'97, vol.1210, pp.300-318, 1997.

C. Reutenauer, Aspects mathématiques des réseaux de Petri, 1989.

J. Riche, K. Robert, . Meyer, . Belnap, R. Urquhart et al., Computer Science Logic, 12th International Workshop, CSL '98, Annual Conference of the EACSL, vol.1584, pp.224-240, 1998.

S. Schmitz, Implicational relevance logic is 2-exptime-complete, J. Symb. Log, vol.81, issue.2, pp.641-661, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01340113

L. Straßburger, MELL in the Calculus of Structures, Theoretical Computer Science, vol.309, issue.1-3, pp.213-285, 2003.

L. Straßburger, System NEL is undecidable, 10th Workshop on Logic, Language, Information and Computation (WoLLIC), vol.84, 2003.

L. Straßburger and A. Guglielmi, A system of interaction and structure IV: The exponentials and decomposition, ACM Trans. Comput. Log, vol.12, issue.4, p.23, 2011.

A. Urquhart, The complexity of decision procedures in relevance logic, Truth or Consequences: Essays in Honor of Nuel Belnap, pp.61-76, 1990.

A. Urquhart, The complexity of decision procedures in relevance logic II, J. Symb. Log, vol.64, issue.4, pp.1774-1802, 1999.

A. Weiermann and M. Bunder, Ackermannian lower bounds for a combinatorial problem related to the decidability of certain relevant logics. Unpublished note, 2006.