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.
Those clocks are used in the definition of timed automaton, signal automaton, timed propositional temporal logic and clock temporal logic.
They are also used in programs such as UPPAAL which implement timed automata.
Those multiple clocks are required in order to track a bounded number of events.
That means that the difference in value between two fixed clocks is constant until one of them is restarted.
In the language of electronics, it means that clock's jitter is null.
Let us assume that we want to modelize an elevator in a building with ten floors.
This clock is started when someone calls the elevator on floor
This clock can be turned off when the elevator arrives at floor
may be used to check how much time an elevator spent at a particular floor.
Intuitively, a clock is similar to a variable in first-order logic, it is an element which may be used in a logical formula and which may takes a number of differente values.
The program UPPAAL introduce the notion of inactive clocks.
is considered to be inactive when the elevator arrive at floor
, and remains inactive until someone call the elevator at floor
An atomic clock constraint is simply a term of the form
to state that the elevator stayed at some floor for more than fifteen seconds.
A clock constraint is either a finite conjunction of atomic clock constraint or is the constant "true" (which can be considered as the empty conjunction).
Depending on the context, an atomic clock constraint may also be of the form
Allowing diagonal constraints may allow to decrease the size of a formula or of an automaton used to describe a system.
However, algorithm's complexity may increase when diagonal constraints are allowed.
In most system using clocks, allowing diagonal constraint does not increase the expressivity of the logic.
The way to encode a Boolean variable depends on the system which uses the clock.
For example, UPPAAL supports Boolean variables directly.
In timed propositional temporal logic, the formula
A clock constraint defines a set of valuations.
A zone is a non-empty set of valuations satisfying a clock constraint.
Zones and clock constraints are implemented using difference bound matrix.
, it uses a finite number of constants in its clock constraints.
A region is a non-empty zone in which no constraint greater than