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 条
  • [1] [Anonymous], 1976, 062 YAL U DEP COMP S
  • [2] Asperti A., 2002, ACM Transactions on Computational Logic, V3, P137, DOI 10.1145/504077.504081
  • [3] Bojanczyk M., J ACM, V56, P1
  • [4] Analysis of Recursively Parallel Programs
    Bouajjani, Ahmed
    Emmi, Michael
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2013, 35 (03):
  • [5] Courtois J.-B., 2014, ALTERNATING VE UNPUB
  • [6] Vector addition tree automata
    de Groote, P
    Guillaume, B
    Salvati, S
    [J]. 19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 64 - 73
  • [7] The covering and boundedness problems for branching vector addition systems
    Demri, Stephane
    Jurdzinski, Marcin
    Lachish, Oded
    Lazic, Ranko
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2013, 79 (01) : 23 - 38
  • [8] Dimino J., FO2 DATA TREES UNPUB
  • [9] Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma
    Figueira, Diego
    Figueira, Santiago
    Schmitz, Sylvain
    Schnoebelen, Philippe
    [J]. 26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011), 2011, : 269 - 278
  • [10] PETRI NETS, HORN PROGRAMS, LINEAR LOGIC AND VECTOR GAMES
    KANOVICH, MI
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 1995, 75 (1-2) : 107 - 135
123