Active rules termination analysis through conditional formula containing updatable variable

Abstract

While active rules have been applied in many areas including active databases, XML documentation and Semantic Web, current methods remain largely uncertain of how to terminate active behaviors. Some existing methods have been provided in the form of a logical formula for a rule set, but they suffer two problems, (i) Only those variables, which are non-updatable or finitely updatable, can be contained by a formula, (ii) They cannot conclude termination if a rule set only contains some cycles that can be executed in a finite number of times. Many active rule systems, which only contain updatable variables, can still be terminated. This paper presents an algorithm to construct a formula, which can contain updatable variable. Also, a method is proposed to detect if a cycle can only be executed in a finite number of times. Theoretical analysis shows more termination cases, which is indetctive for existing methods, can be detected by our method. © Springer-Verlag Berlin Heidelberg 2007.