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 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 clock temporal logic. They are also used in programs such as UPPAAL which implement timed automata.^[1]

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.

Let us assume that we want to modelize an elevator in a building with ten floors. Our model may have n {\displaystyle n} clocks c 0 , … , c 9 {\displaystyle c_{0},\dots ,c_{9}} , such that the value of the clock c i {\displaystyle c_{i}} is the time someone had wait for the elevator at floor i {\displaystyle i} . This clock is started when someone calls the elevator on floor i {\displaystyle i} (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 i {\displaystyle i} . In this example, we actually need ten distinct clocks because we need to track ten independent events. Another clock s {\displaystyle s} 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 s {\displaystyle s} is always smaller than fifteen seconds, each clock c i {\displaystyle c_{i}} is turned off before it reaches three minutes.

Formally, a set X {\displaystyle X} of clocks is simply a finite set^[1]: 191. Each element of a set of clocks 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 take a number of different values.

A clock valuation or clock interpretation^[1]: 193 ν {\displaystyle \nu } over X = { x 1 , … , x n } {\displaystyle X=\{x_{1},\dots ,x_{n}\}} is usually defined as a function from X {\displaystyle X} to the set of non-negative reals. Equivalently, a valuation can be considered as a point in R ≥ 0 n {\displaystyle \mathbb {R} _{\geq 0}^{n}} .

The initial assignment ν 0 {\displaystyle \nu _{0}} is the constant function sending each clock to 0. Intuitively, it represents the initial time of the program, where all clocks are initialized simultaneously.

Given a clock assignment ν {\displaystyle \nu } , and a real t ≥ 0 {\displaystyle t\geq 0} , ν + t {\displaystyle \nu +t} denotes the clock assignment sending each clock x ∈ C {\displaystyle x\in C} to ν ( x ) + t {\displaystyle \nu (x)+t} . Intuitively, it represents the valuation ν {\displaystyle \nu } after which t {\displaystyle t} time units passed.

Given a subset r ⊆ C {\displaystyle r\subseteq C} of clocks, ν [ r → 0 ] {\displaystyle \nu [r\rightarrow 0]} denotes the assignment similar to ν {\displaystyle \nu } in which the clocks of r {\displaystyle r} are reset. Formally, ν [ r → 0 ] {\displaystyle \nu [r\rightarrow 0]} sends each clock x ∈ r {\displaystyle x\in r} to 0 and each clock x ∉ r {\displaystyle x\not \in r} to ν ( x ) {\displaystyle \nu (x)} .

The program UPPAAL introduces the notion of inactive clocks.^[2] 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 c i {\displaystyle c_{i}} is considered to be inactive when the elevator arrive at floor i {\displaystyle i} , and remains inactive until someone call the elevator at floor i {\displaystyle i} .

When allowing for inactive clocks, a valuation may associate a clock x {\displaystyle x} to some special value ⊥ {\displaystyle \bot } to indicate that it is inactive. If ν ( x ) = ⊥ {\displaystyle \nu (x)=\bot } then ( ν + t ) ( x ) {\displaystyle (\nu +t)(x)} also equals ⊥ {\displaystyle \bot } .

An atomic clock constraint is simply a term of the form x ∼ c {\displaystyle x\sim c} , where x {\displaystyle x} is a clock, ∼ {\displaystyle \sim } is a comparison operator, such as <, ≤, = ≥, or >, and c ∈ N {\displaystyle c\in \mathbb {N} } is an integral constant. In our previous example, we may use the atomic clock constraints c i ≤ 180 {\displaystyle c_{i}\leq 180} to state that the person at floor i {\displaystyle i} waited for less than three minutes, and s > 15 {\displaystyle s>15} to state that the elevator stayed at some floor for more than fifteen seconds. A valuation ν {\displaystyle \nu } satisfies an atomic clock valuation x ∼ c {\displaystyle x\sim c} if and only if ν ( x ) ∼ c {\displaystyle \nu (x)\sim c} .

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 ν {\displaystyle \nu } satisfies a clock constraint ⋀ i = 1 n x i ∼ i c i {\displaystyle \bigwedge _{i=1}^{n}x_{i}\sim _{i}c_{i}} if it satisfies each atomic clock constraint x i ∼ i c i {\displaystyle x_{i}\sim _{i}c_{i}} .

Depending on the context, an atomic clock constraint may also be of the form x i ∼ x j + c {\displaystyle x_{i}\sim x_{j}+c} . Such a constraint is called a diagonal constraint, because x 1 = x 2 + c {\displaystyle x_{1}=x_{2}+c} defines a diagonal line in R ≥ 0 2 {\displaystyle \mathbb {R} _{\geq 0}^{2}} .

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 a constraint with Boolean variables and non-diagonal constraints.

A diagonal constraint x i ∼ x j + c {\displaystyle x_{i}\sim x_{j}+c} may be simulated using non-diagonal constraints as follows. When x j {\displaystyle x_{j}} is reset, check whether x i ∼ c {\displaystyle x_{i}\sim c} holds or not. Recall this information in a Boolean variable b i , j , c {\displaystyle b_{i,j,c}} and replace x i ∼ x j + c {\displaystyle x_{i}\sim x_{j}+c} by this variable. When x i {\displaystyle x_{i}} is reset, set b i , j , c {\displaystyle b_{i,j,c}} to true if ∼ {\displaystyle \sim } is < or ≤ or if ∼ {\displaystyle \sim } is = and c = 0 {\displaystyle c=0} .

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 x i , j , c {\displaystyle x_{i,j,c}} , whose value is 0 if and only if b i , j , c {\displaystyle b_{i,j,c}} is false. That is, x i , j , c {\displaystyle x_{i,j,c}} is reset as long as x i , j , c {\displaystyle x_{i,j,c}} is supposed to be false. In timed propositional temporal logic, the formula x i . ϕ {\displaystyle x_{i}.\phi } , which restart x i {\displaystyle x_{i}} and then evaluates ϕ {\displaystyle \phi } , can be replaced by the formula x i . ( ( x i ∼ x j + c ⟹ ϕ ⊤ ) ∧ ( ¬ x i ∼ x j + c ⟹ ϕ ⊥ ) ) {\displaystyle x_{i}.((x_{i}\sim x_{j}+c\implies \phi _{\top })\land (\neg x_{i}\sim x_{j}+c\implies \phi \bot ))} , where ϕ ⊤ {\displaystyle \phi _{\top }} and ϕ ⊥ {\displaystyle \phi _{\bot }} are copies of the formulas ϕ {\displaystyle \phi } , where x i ∼ x j + c {\displaystyle x_{i}\sim x_{j}+c} are replaced by the true and false constant respectively.

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 M {\displaystyle M} , it uses a finite number of constants in its clock constraints. Let K {\displaystyle K} be the greatest constant used. A region is a non-empty zone in which no constraint greater than K {\displaystyle K} are used, and furthermore, such that it is minimal for the inclusion.

• Timed automaton
• Signal automaton
• Clock temporal logic
• Timed propositional temporal logic