A computation tree
	• From a given start state, you can represent all possible paths with an infinite computation tree • Model checking allows us to answer questions about this tree structure • Because the underlying machine is finite-state, the structure of the computation tree is constrained