Isn't this how Operational Semantics works for describing formally a given programming language? You define what the state of execution of the program is made of, and how state transitions occur during one execution step.

The wikipedia link describing it is overly arcane but here it is anyway: https://en.wikipedia.org/wiki/Operational_semantics