Theoretical foundations of handling large substitution sets in temporal integrity monitoring (Q914364)

Temporal constraints can be expressed by temporal logic formulae which are satisfied in a database evolution if they are valid for all substitutions for their free variables. The technique to represent historical information relies on the fact that temporal formulae can be transformed into so-called transition graphs which are some kind of finite state machine and whose transition conditions are non-temporal formulae. This reduces the needed historical data to the information about which substitution is associated with which node of the transition graph. This technique is extended in order to get a more compact representation of the possibly infinite substitution sets. For this purpose substitutions are generalized to the notion of so-called descriptions which represent whole sets of substitutions. The notions of formula validity and of stepwise monitoring potential validity of temporal constraints are redefined for descriptions. Based on these notions an algorithm for monitoring temporal integrity by handling descriptions is presented. Finally, a syntactical characterization of the constraints which can be monitored with acceptable storage requirements is defined.