Our interest is in large systems of concurrently executing components. A crucial aspect of the correctness of such systems is their temporal behavior. Behavioral properties can be classified as follows [12]: (1) Safety properties: ``nothing bad happens'' -- for example, when an elevator is moving up, it does not attempt to move down without stopping first, and (2) Liveness properties: ``progress occurs in the system'' -- for example, if a button inside an elevator is pressed, then the elevator eventually arrives at the corresponding floor. The required behavioral properties are given by a specification, which precisely documents what the system must achieve. Formal methods are those that provide a rigorous mathematical guarantee that a large software system conforms to a specification. Formal methods can be roughly classified as (1) Proof-theoretic: a suitable deductive system is used, and correctness proofs are built manually, or using a theorem prover, and (2) Model-theoretic: a model of the run-time behavior of the software is built, and this model is checked (usually mechanically) for the required properties. In our work, we emphasize model-theoretic methods, due to their greater potential for automation.