The set of variables modeling your system The values of those variables in the initial state(s) Possible actions changing those variables to generate successor states Safety invariants you want to be true in every state You can then use the model checker to validate that your concrete spec refines the abstract spec, and you do this by writing a temporal formula mapping the large behavior set of the concrete spec onto the smaller behavior set of the abstract spec (to be pedantic, both sets probably have countably-infinite cardinality but multiple concrete behaviors will map to each abstract behavior).