More specifically, this appears to allow for more general model-checking, as most programming languages do not explicitly work on transitions (some declarative languages can be exceptions).