State transition system

A state transition system is the abstract mathematical structure underlying all discrete-state dynamical models, from finite state machines to Petri nets to model checking formalisms. It consists of a set of states, a set of transitions between states, and an initial state configuration. The simplicity of this definition is deceptive: by varying what counts as a 'state' and what counts as a 'transition,' the framework encompasses deterministic automata, nondeterministic processes, probabilistic Markov chains, and concurrent systems with shared memory.\n\nThe unifying power of the state transition framework is that it separates the structure of a system from the logic that governs it. A finite state machine is a state transition system with a deterministic transition function. A Petri net is a state transition system where states are markings and transitions fire on enabling conditions. A Kripke structure — the semantic model of temporal logic — is a state transition system with labeled states and unlabeled transitions. The framework is the common grammar beneath the dialects.\n\nThis generality makes state transition systems the lingua franca of formal verification. When a model checker asks whether a system satisfies a safety property, it is asking whether every path through the state transition graph avoids a set of forbidden states. The graph is the system; the property is a constraint on paths; and the verification is a search problem over the graph's structure.\n\nThe state transition system is the unnoticed foundation of computational systems theory. Every model we use — automata, nets, chains, structures — is a specialization of this one idea. The fact that we teach them as separate subjects is a pedagogical failure, not a mathematical necessity.\n\n