In model checking, a field of computer science, a region is a convex polytope in
, and more precisely a zone, satisfying some minimality property.
belong to the same region, then they satisfy the same constraints of
Intuitively, it means that any timed propositional temporal logic-formula, or timed automaton or signal automaton using only the constraints of
to the emptiness problem for a finite or Büchi automaton.
Intuitively, this number represents an upper bound on the values to which the clock
The first definition allow to easily test whether two assignments belong to the same region.
While the previous definition allow to test whether two assignments belong to the same region, it does not allow to easily represents a region as a data structure.
The third definition given below allow to give a canonical encoding of a region.
A region can be explicitly defined as a zone, using a set
of equations and inequations satisfying the following constraints: Since, when
This definition allow to encode a region as a data structure.
It suffices, for each clock, to state to which interval it belongs and to recall the order of the fractional part of the clocks which belong in an open interval of length 1.
Let us now give a third definition of regions.
While this definition is more abstract, it is also the reason why regions are used in model checking.
Intuitively, this definition states that two clock assignments belong to the same region if the differences between them are such that no timed automaton can notice them.
, going through the same locations, reading the same letters, where the only difference is that the time waited between two successive transition may be different, and thus the successive clock variations are different.
belongs to the same region if for each timed automaton
, there is a timed bisimulation between the extended states
More precisely, this bisimulation preserves letters and locations but not the exact clock assignments.
[1]: 7 Some operations are now defined over regions: Resetting some of its clock, and letting time pass.
, the regions which can be attained without resetting a clock are called the time-successors of
, let us define its set of time-successors.
is empty, the least time-successor is defined by the following constraints: There are at most
Intuitively, the region automaton is contructude as a product of
The region graph is a rooted directed graph which models the set of possible clock valuations during a run of a timed-autoamton.
is a finite or Büchi automaton which is essentially a product of
That is, each state of the region automaton is a pair containing a location of
Since two clocks assignment belonging to the same region satisfies the same guard, each region contains enough information to decide which transitions can be taken.
Formally, the region automaton is defined as follows: Given any run