Timing diagrams are widely used in industrial practice to express precedence and timing relationships amongst a collection of signals. This graphical notation is often more convenient than the use of temporal logic or automata. We introduce a class of timing diagrams called Regular Timing Diagrams (RTD’s). RTD’s have a precise syntax, and a formal semantics that is simple and corresponds to common usage. Moreover, RTD’s have an inherent compositional structure, which is exploited to construct an efficient algorithm for model checking a RTD with respect to a system description. The algorithm has time complexity that is linear in the system size and a small polynomial in the representation of the diagram. The algorithm can be easily used with symbolic (BDDbased) model checkers. We illustrate the workings of our algorithm with the verification of a simple master-slave system.