State Transition Graph
	• One way to represent a finite state machine is as a state transition graph – S is a finite set of states – R is a binary relation that defines the possible transitions between states in S – P is a function that assigns atomic propositions to each state in S • e.g., that a specific process holds a lock • Other representations include regular expressions, etc.