Type systems question: is there a name for a type system which natively encodes state transitions? So not just that sum types which enumerate valid states, but also encode the transitions between those states as part of the type?

It's almost-but-not-quite the same as session types. So like, I feel like there must be prior art for this, but I don't know what to look for.