In model checking, a subfield of computer science, a clock is a mathematical object used to model time. More precisely, a clock measures how much time passed since a particular event occurs, in this sense, a clock is more precisely an abstraction of a stopwatch. In a model of some particular program, the value of the clock may either be the time since the program was started, or the time since a particular event occurred in the program. Those clocks are used in the definition of timed automaton, signal automaton, timed propositional temporal logic and . They are also used in programs such as UPPAAL which implement timed automata.