About: Region (model checking)

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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
dbp:date
  • April 2019 (en)
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
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License