Synchronous product of automata and parallel composition of transition systems. Reason about multi-module hardware by composing per-component models.
Part of Mathematical Foundations of Model Checking on formal.org.