Monitoring dynamic integrity constraints based on temporal logic

摘要

Dynamic integrity constraints are used to specify admissible sequences of database states. We present algorithmic fundamentals of monitoring constraints expressed in temporal logic. The essential means are finite transition graphs which can be constructed from temporal formulae by utilizing an appropriate normalform. To ensure admissibility of a state sequence, the integrity monitor has to follow a corresponding path through the graph and to check certain nontemporal conditions in each state; these conditions are provided as edge labels. Thus, monitoring dynamic integrity is reduced to a controlled checking of static integrity. All errors in present database behaviour are detected as well as many inevitable future errors.