1 Answers
In model checking, a field of computer science, a region is a convex polytope in R d {\displaystyle \mathbb {R} ^{d}} for some dimension d {\displaystyle d} , and more precisely a zone, satisfying some minimality property. The regions partition R d {\displaystyle \mathbb {R} ^{d}}.
The set of zones depends on a set K {\displaystyle K} of constraints of the form x ≤ c {\displaystyle x\leq c} , x ≥ c {\displaystyle x\geq c} , x 1 ≤ x 2 + c {\displaystyle x_{1}\leq x_{2}+c} and x 1 ≥ x 2 + c {\displaystyle x_{1}\geq x_{2}+c} , with x 1 {\displaystyle x_{1}} and x 2 {\displaystyle x_{2}} some variables, and c {\displaystyle c} a constant. The regions are defined such that if two vectors x → {\displaystyle {\vec {x}}} and x → ′ {\displaystyle {\vec {x}}'} belong to the same region, then they satisfy the same constraints of K {\displaystyle K}. Furthermore, when those vectors are considered as a tuple of clocks, both vectors have the same set of possible futurs. Intuitively, it means that any timed propositional temporal logic-formula, or timed automaton or signal automaton using only the constraints of K {\displaystyle K} can not distinguish both vectors.
The set of region allows to create the region automaton, which is a directed graph in which each node is a region, and each edge r → r ′ {\displaystyle r\to r'} ensure that r ′ {\displaystyle r'} is a possible future of r {\displaystyle r}. Taking a product of this region automaton and of a timed automaton A {\displaystyle {\mathcal {A}}} which accepts a language L {\displaystyle L} creates a finite automaton or a Büchi automaton which accepts untimed L {\displaystyle L}. In particular, it allows to reduce the emptiness problem for A {\displaystyle {\mathcal {A}}} to the emptiness problem for a finite or Büchi automaton. This technique is used for example by the software UPPAAL.