Multiset rewriting, petri nets, PDDL planning, linear logic, and vector addition systems, are all different representational systems with large overlapping isomorphic fragments. This makes it hard to look up related work, sometimes.

Can anyone help me find work in any of these spaces related to the problem of (checking or generating) *invariants* for specifications written in any of these formal systems? That is, properties that hold in the initial state and are preserved by the transition rules?

The last chapter of my thesis is about this, and I know several people who've worked on it for linear logic in particular, but I could use pointers to related work in those other domains. cc @johncarlosbaez maybe for pointers in the petri net world

My thesis chapter, if anyone's curious or needs more clarification on what I mean: http://www.cs.cmu.edu/~cmartens/thesis/6-reasoning.pdf