STeP's modular transition systems allow concise, modular, possibly recursive and parameterized system descriptions. A transition module consists of an interface that describes the interaction with the environment, and a body that describes its actions. Communication between a module and its environment can be asynchronous, through shared variables, and synchronous, through synchronization of transitions. More complex modules can be constructed from simpler ones by (recursive) module expressions, allowing the description of hierarchical systems of unbounded depth. Module expressions can refer to (instances of parameterized) modules defined earlier by name, thus enabling the reuse of code and the reuse of properties proven about these modules. Apart from the usual hiding and renaming operations, the language provides a construct to augment the interface with new variables that provide a summary value of multiple variables within the module. Symmetrically, the restrict operation allows the module environment to combine or rearrange the variables it presents to the module. A LTL property holds over a module if it holds over any system that includes that module (taking into account variable renamings). STeP's property inheritance mechanism automatically generates modular lemmas from lemmas of modules used in the description.