Counting state-space size and applying the pigeonhole principle. Understand why explicit enumeration fails at scale and where BDDs and SAT must take over.
Part of Mathematical Foundations of Model Checking on formal.org.