I introduce subsequence invariants, a new class of invariants for the specification and verification of concurrent systems. Unlike state invariants, which refer to the state variables of the system, subsequence invariants characterize the behavior of a concurrent system in terms of the occurrences of sequences of synchronization events.

Subsequence invariants satisfy an interesting combination of properties: They are compositional in the sense that a system inherits all the invariants of its constituent processes; they can be computed in polynomial time; and they can still express interesting system properties. The mathematics behind subsequence invariants are interesting in their own right and suggest some promising extensions to the existing theory.