Clock (model checking)

In model checking, a subfield of computer science, a clock is a mathematical object used to model time. More precisely, a clock measure 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 clock temporal logic. They are also used in programs such as UPPAAL which implement timed automata.
Generally, the model of a system uses many clocks. Those multiple clocks are required in order to track a bounded number of events. All of those clocks are synchronized. 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.
Example.
Let us assume that we want to modelize an elevator in a building with ten floors. Our model may have formula_1 clocks formula_2, such that the value of the clock formula_3 is the time someone had wait for the elevator at floor formula_4. This clock is started when someone calls the elevator on floor formula_4 (and the elevator was not already called on this floor since last time it visited that floor). This clock can be turned off when the elevator arrives at floor formula_4. In this example, we actually need ten distinct clocks because we need to track ten independent events. Another clock formula_7 may be used to check how much time an elevator spent at a particular floor.
A model of this elevator can then use those clocks to assert whether the elevator's program satisfies properties such as "assuming the elevator is not kept on a floor for more than fifteen seconds, then no one has to wait for the elevator for more than three minutes". In order to check whether this statement holds, it suffices to check that, in every run of the model in which the clock formula_7 is always smaller than fifteen seconds, each clock formula_3 is turned off before it reaches three minutes.
Definition.
Formally, a set formula_10 of clocks is simply a finite set. Each element of a set of clock is called a clock. 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.
Clock valuations.
A clock valuation or clock interpretation formula_11 over formula_12 is usually defined as a function from formula_10 to the set of non-negative real. Equivalently, a valuation can be considered as a point in formula_14.
The initial assignment formula_15 is the constant function sending each clock to 0. Intuitively, it represents the initial time of the program, where each clocks are initialized simultaneously.
Given a clock assignment formula_11, and a real formula_17, formula_18 denotes the clock assignment sending each clock formula_19 to formula_20. Intuitively, it represents the valuation formula_11 after which formula_22 time units passed.
Given a subset formula_23 of clocks, formula_24 denotes the assignment similar to formula_11 in which the clocks of formula_26 are reset. Formally, formula_24 sends each clock formula_28 to 0 and each clock formula_29 to formula_30.
Inactive clocks.
The program UPPAAL introduce the notion of inactive clocks. A clock is inactive at some time if there is no possible future in which the clock's value is checked without being reset first. In our example above, the clock formula_3 is considered to be inactive when the elevator arrive at floor formula_4, and remains inactive until someone call the elevator at floor formula_4.
When allowing for inactive clock, a valuation may associate a clock formula_34 to some special value formula_35 to indicate that it is inactive. If formula_36 then formula_37 also equals formula_35.
Clock constraint.
An atomic clock constraint is simply a term of the form formula_39, where formula_34 is a clock, formula_41 is a comparison operator, such as <, ≤, = ≥, or >, and formula_42 is an integral constant. In our previous example, we may use the atomic clock constraints formula_43 to state that the person at floor formula_4 waited for less than three minutes, and formula_45 to state that the elevator stayed at some floor for more than fifteen seconds. A valuation formula_11 satisfies an atomic clock valuation formula_39 if and only if formula_48.
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). A valuation formula_11 satisfies a clock constraint formula_50 if it satisfies each atomic clock constraint formula_51.
Diagonal constraint.
Depending on the context, an atomic clock constraint may also be of the form formula_52. Such a constraint is called a diagonal constraint, because formula_53 defines a diagonal line in formula_54.
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. We now explain how to encode such constraint with Boolean variable and non-diagonal constraint.
A diagonal constraint formula_52 may be simulated using non-diagonal constraint as follows. When formula_56 is reset, check whether formula_57 holds or not. Recall this information in a Boolean variable formula_58 and replace formula_52 by this variable. When formula_60 is reset, set formula_58 to true if formula_41 is < or ≤ or if formula_41 is = and formula_64.
The way to encode a Boolean variable depends on the system which uses the clock. For example, UPPAAL supports Boolean variables directly. Timed automata and signal automata can encode a Boolean value in their locations. In clock temporal logic over timed words, the Boolean variable may be encoded using a new clock formula_65, whose value is 0 if and only if formula_58 is false. That is, formula_65 is reset as long as formula_65 is supposed to be false. In timed propositional temporal logic, the formula formula_69, which restart formula_60 and then evaluates formula_71, can be replaced by the formula formula_72, where formula_73 and formula_74 are copies of the formulas formula_71, where formula_52 are replaced by the true and false constant respectively.
Sets defined by clock constraints.
A clock constraint defines a set of valuations. Two kinds of such sets are considered in the literature.
A zone is a non-empty set of valuations satisfying a clock constraint. Zones and clock constraints are implemented using difference bound matrix.
Given a model formula_77, it uses a finite number of constants in its clock constraints. Let formula_78 be the greatest constant used. A region is a non-empty zone in which no constraint greater than formula_78 are used, and furthermore, such that it is minimal for the inclusion.