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
| |
dbo:wikiPageLength
|
- 14871 (xsd:nonNegativeInteger)
|
dbo:wikiPageRevisionID
| |
dbo:wikiPageWikiLink
| |
dbp:date
| |
dbp:reason
|
- Confusing to those unfamiliar with the topic (en)
|
dbp:wikiPageUsesTemplate
| |
dcterms:subject
| |
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
| |
prov:wasDerivedFrom
| |
foaf:isPrimaryTopicOf
| |
is dbo:wikiPageDisambiguates
of | |
is dbo:wikiPageRedirects
of | |
is dbo:wikiPageWikiLink
of | |
is foaf:primaryTopic
of | |