Complexity questions on linear logic

I'm also curious about the status of the propositional linear logic
decision problem.

Research on connections between Petri nets (vector addition systems)
and fragments of propositional linear logic has shown that the
decision problem for linear logic with the connectives:

  -o (linear implication)  ox  (tensor product)  ! (of course)

must be at least has hard as the decision problem for forward
markings.  Since the latter was a significant topic of research for
some time, it seems that propositional linear logic (with the
modalities) must encode some quite difficult decision problems.

---carl gunter