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 futures. 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.
Definition Let C = { x 1 , … , x d } {\displaystyle C=\{x_{1},\dots ,x_{d}\}} a set of clocks. For each x ∈ N {\displaystyle x\in \mathbb {N} } let c x ∈ N {\displaystyle c_{x}\in \mathbb {N} } . Intuitively, this number represents an upper bound on the values to which the clock x {\displaystyle x} can be compared. The definition of a region over the clocks of C {\displaystyle C} uses those numbers c x {\displaystyle c_{x}} 's. Three equivalent definitions are now given. Given a clock assignment ν {\displaystyle \nu } , [ ν ] {\displaystyle [\nu ]} denotes the region in which ν {\displaystyle \nu } belongs. The set of regions is denoted by R {\displaystyle {\mathcal {R}}} .
Equivalence of clocks assignment The first definition allow to easily test whether two assignments belong to the same region. A region may be defined as an equivalence class for some equivalence relation. Two clocks assignments ν 1 {\displaystyle \nu _{1}} and ν 2 {\displaystyle \nu _{2}} are equivalent if they satisfy the following constraints:
… excerpt ends here. Continue reading the full article.
