Provably correct and complete transaction rules for GIS

Abstract

This paper provides a set of transaction rules which preserve the consistency of geometry and topology in a Geographic Information System (GIS). We show that the given rules are safe in the sense that once a given database of a GIS is consistent, this consistency is preserved by iterative applications of the given rules. The focus is on maps specifying an irregular tessellation of the plane. Consistency is specified by a set of map axioms which are simplified with regard to specific transactions. Updates of the database are invoked by rules completing the required change to a consistent transaction. We show that any map may be generated and dismantled by iterative applications of the given rules, and discuss other application scenarios.