"April 2019"@en . . . . . . "60442605"^^ . . . . "Region (model checking)"@en . . . "1120220838"^^ . . . . . . . . . . . "Confusing to those unfamiliar with the topic"@en . . "In model checking, a field of computer science, a region is a convex polytope in for some dimension , and more precisely a zone, satisfying some minimality property. The regions partition . The set of zones depends on a set of constraints of the form , , and , with and some variables, and a constant. The regions are defined such that if two vectors and belong to the same region, then they satisfy the same constraints of . 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 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 ensure that is a possible future of . Taking a product of this region automaton and of a timed automaton which accepts a language creates a finite automaton or a B\u00FCchi automaton which accepts untimed . In particular, it allows to reduce the emptiness problem for to the emptiness problem for a finite or B\u00FCchi automaton. This technique is used for example by the software UPPAAL."@en . "In model checking, a field of computer science, a region is a convex polytope in for some dimension , and more precisely a zone, satisfying some minimality property. The regions partition . The set of zones depends on a set of constraints of the form , , and , with and some variables, and a constant. The regions are defined such that if two vectors and belong to the same region, then they satisfy the same constraints of . 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 can not distinguish both vectors."@en . . . . . . . "14871"^^ . . . . .