Non-Elementary Complexities for Branching VASS, MELL, and Extensions

被引：0

作者：

Lazic, Ranko ^{[1
]}

Schmitz, Sylvain ^{[2
,3
,4
]}

机构：

[1] Univ Warwick, Dept Comp Sci, Coventry, W Midlands, England

[2] ENS Cachan, LSV, Gif Sur Yvette, France

[3] CNRS, Paris, France

[4] INRIA, Rocquencourt, France

来源：

PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2014年

关键词：

Fast-growing complexity; linear logic; substructural logic; vector addition systems; FINITE-MODEL PROPERTY; LINEAR LOGIC; FRAGMENTS;

D O I：

10.1145/2603088.2603129

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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 TOWER-hard already in the affine case-and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its TOWER-completeness. We also show that provability in propositional contractive linear logic is ACKERMANN-complete.

引用

页数：10

共 25 条

[11] Decidability of linear affine logic
Kopylov, AP
[J]. INFORMATION AND COMPUTATION, 2001, 164 (01) : 173 - 198
[12] The finite model property for various fragments of linear logic
Lafont, Y
[J]. JOURNAL OF SYMBOLIC LOGIC, 1997, 62 (04) : 1202 - 1208
[13] Nondeterministic Phase Semantics and the Undecidability of Boolean BI
Larchey-Wendling, Dominique
Galmiche, Didier
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2013, 14 (01)
[14] The reachability problem for branching vector addition systems requires doubly-exponential space
Lazic, Ranko
[J]. INFORMATION PROCESSING LETTERS, 2010, 110 (17) : 740 - 745
[15] DECISION-PROBLEMS FOR PROPOSITIONAL LINEAR LOGIC
LINCOLN, P
MITCHELL, J
SCEDROV, A
SHANKAR, N
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1992, 56 (1-3) : 239 - 311
[16] THE COMPLEXITY OF THE FINITE CONTAINMENT-PROBLEM FOR PETRI NETS
MAYR, EW
MEYER, AR
[J]. JOURNAL OF THE ACM, 1981, 28 (03) : 561 - 576
[17] The finite model property for various fragments of intuitionistic linear logic
Okada, M
Terui, K
[J]. JOURNAL OF SYMBOLIC LOGIC, 1999, 64 (02) : 790 - 802
[18] Rackoff C., 1978, Theoretical Computer Science, V6, P223, DOI 10.1016/0304-3975(78)90036-1
[19] RAMBOW O, 1994, 32ND ANNUAL MEETING OF THE ASSOCIATION FOR COMPUTATIONAL LINGUISTICS, P263
[20] Schmitz S., 2014, LNCS

← 1 2 3 →