Region (model checking) (original) (raw)
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.
| Property | Value |
|---|---|
| dbo:abstract | 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üchi automaton which accepts untimed . In particular, it allows to reduce the emptiness problem for to the emptiness problem for a finite or Büchi automaton. This technique is used for example by the software UPPAAL. (en) |
| dbo:wikiPageID | 60442605 (xsd:integer) |
| dbo:wikiPageLength | 14871 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1120220838 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Uppaal_Model_Checker dbr:Timed_propositional_temporal_logic dbr:Timed_word dbr:Model_checking dbr:Convex_polytope dbr:Clock_(model_checking) dbr:Computer_science dbr:Büchi_automaton dbr:Directed_graph dbr:Fractional_part dbc:Convex_geometry dbc:Model_checking dbc:Polytopes dbr:Bisimulation dbr:Zone_(convex_polytope) dbc:Data_structures dbr:Signal_automaton dbr:Timed_automaton dbr:Finite_automaton dbr:Zone_(model_checking) |
| dbp:date | April 2019 (en) |
| dbp:reason | Confusing to those unfamiliar with the topic (en) |
| dbp:wikiPageUsesTemplate | dbt:Confusing dbt:R dbt:Rp |
| dct:subject | dbc:Convex_geometry dbc:Model_checking dbc:Polytopes dbc:Data_structures |
| rdfs:comment | 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) |
| rdfs:label | Region (model checking) (en) |
| owl:sameAs | wikidata:Region (model checking) https://global.dbpedia.org/id/9rQnk |
| prov:wasDerivedFrom | wikipedia-en:Region_(model_checking)?oldid=1120220838&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Region_(model_checking) |
| is dbo:wikiPageDisambiguates of | dbr:Region_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Region_(Model_checking) |
| is dbo:wikiPageWikiLink of | dbr:Region_(Model_checking) dbr:Clock_(model_checking) dbr:Difference_bound_matrix dbr:Region_(disambiguation) dbr:Timed_automaton |
| is foaf:primaryTopic of | wikipedia-en:Region_(model_checking) |