Paths-based criteria and application to linear logic subsystems characterizing polynomial time

These criteria can be used to prove the complexity soundness of several existing variants of linear logic. We define a decidable syntactic subsystem of linear logic: SDNLL. We prove that the proof-nets of SDNLL satisfy the three criteria, which implies that SDNLL is sound for Ptime. Several previous subsystems of linear logic characterizing polynomial time (LLL, mL4, maximal system of MS) are embedded in SDNLL, proving its Ptime completeness.