This HTML5 document contains 54 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
n9http://dbpedia.org/resource/File:
foafhttp://xmlns.com/foaf/0.1/
n16https://global.dbpedia.org/id/
n10http://hal.archives-ouvertes.fr/docs/00/26/24/22/PDF/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
n5http://commons.wikimedia.org/wiki/Special:FilePath/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n8https://moves.rwth-aachen.de/wp-content/uploads/WS1617/amc/
wikipedia-enhttp://en.wikipedia.org/wiki/
dbchttp://dbpedia.org/resource/Category:
provhttp://www.w3.org/ns/prov#
dbphttp://dbpedia.org/property/
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbr:Difference_bound_matrix
rdfs:label
Difference bound matrix
rdfs:comment
In model checking, a field of computer science, a difference bound matrix (DBM) is a data structure used to represent some convex polytopes called zones. This structure can be used to efficiently implement some geometrical operations over zones, such as testing emptyness, inclusion, equality, and computing the intersection and the sum of two zones. It is, for example, used in the Uppaal model checker; where it is also distributed as an independent library.
foaf:depiction
n5:Showing_x_1_less_than_3_and_4.png n5:X(3_y)-3.png n5:X_incompatible.png n5:X_less_than_3,_x_less_than_y+3.png
dcterms:subject
dbc:Polytopes dbc:Geometric_data_structures dbc:Convex_geometry
dbo:wikiPageID
60274693
dbo:wikiPageRevisionID
1076482890
dbo:wikiPageWikiLink
dbr:Convex_polytope dbr:Commutative dbr:Monoid dbr:Greatest-lower-bound_property dbc:Polytopes dbr:Minkowski_addition n9:Showing_x_1_less_than_3_and_4.png dbr:Distributive_property dbr:Model_checking dbr:Integer dbr:Floyd–Warshall_algorithm dbr:Real_number dbr:Module_(mathematics) dbr:Lexicographical_order dbr:Total_order dbr:Region_(model_checking) dbc:Geometric_data_structures dbr:Rational dbr:Idempotent_semiring dbr:Least-upper-bound_property dbr:Data_structure dbc:Convex_geometry n9:X(3_y)-3.png dbr:Clock_(model_checking) n9:X_incompatible.png n9:X_less_than_3,_x_less_than_y+3.png dbr:Computer_science dbr:Polytope dbr:Directed_graph dbr:Uppaal_model_checker dbr:Tropical_semiring dbr:Associative
dbo:wikiPageExternalLink
n8:amc16_lec20_reduced.pdf n10:PeronHalbwachsVMCAI07.pdf%7Cdoi-access=free
owl:sameAs
n16:9nW3L wikidata:Q65084273
dbp:wikiPageUsesTemplate
dbt:Cite_journal dbt:Data_structures
dbo:thumbnail
n5:X_incompatible.png?width=300
dbo:abstract
In model checking, a field of computer science, a difference bound matrix (DBM) is a data structure used to represent some convex polytopes called zones. This structure can be used to efficiently implement some geometrical operations over zones, such as testing emptyness, inclusion, equality, and computing the intersection and the sum of two zones. It is, for example, used in the Uppaal model checker; where it is also distributed as an independent library. More precisely, there is a notion of canonical DBM; there is a one-to-one relation between canonical DBMs and zones and from each DBM a canonical equivalent DBM can be efficiently computed. Thus, equality of zone can be tested by checking for equality of canonical DBMs.
prov:wasDerivedFrom
wikipedia-en:Difference_bound_matrix?oldid=1076482890&ns=0
dbo:wikiPageLength
25232
foaf:isPrimaryTopicOf
wikipedia-en:Difference_bound_matrix