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
相关论文
共 50 条
12345