基于触发路径的主动规则集终止性分析

为满足用户对网络服务的个性化、定制化和主动化需求,主动规则成为解决这些问题的关键技术.研究了在网络环境下基于规则的复杂应用中,大量规则集同时触发所带来的规则终止性问题,提出的分析方法确保主动规则能够有效运行,以提供更加灵活的主动服务.讨论了以静态分析方法为主的主动规则终止性分析相关工作,随后给出问题描述和相关形式化定义.分析了基于关联图的终止性分析方法的保守性,引入触发路径和有限触发环概念,提出了基于触发路径的两种终止情形分析方法,提高了规则集终止性分析的准确性,采用两阶段分析算法保证了分析效率.与相关分析方法的实验比较说明,文中方法能够更准确高效地检测主动规则集的终止性,并适应基于主动规则的其它应用.     

含环触发图对应的主动规则集可终止性分析

主动规则集的可终止性是主动数据库规则集的三大重要特征之一．主动规则集可否保证终止将直接影响到系统的应用．由于主动规则间存在依赖关系，通过对依赖关系的分析，给出了规则的触发传递闭包、依赖传递闭包等概念．以此为基础，提出了用规则触发-依赖图（T—DG）方法来分析主动规则集的终止性．特别讨论了判定含环的触发图（TG）对应的主动规则集是否保证终止的方法，给出了相应的判定算法、算法证明及分析．     

基于活化路径和条件公式的主动规则集可终止性判定方法

支持主动规则机制已经成为现代数据库系统的一个重要特征.主动规则集的可终止性判定是主动数据库中一个核心问题之一,利用触发图和活化图的方法来判定可终止性都存在不同的保守性.为此,提出了为有效活化路径建立条件公式的思想,在此基础上给出了一个新的判定主动规则集可终止性的方法.分析的结果表明,提出的方法较现有方法可以发现更多的可终止性情形,最后给出了相应的算法及其可终止性、正确性证明.     

基于增强条件公式的主动规则集可终止性判定

主动规则集的可终止性判定是一个研究热点问题,现有的基于触发图和活化图的方法没有考虑触发环所有所属规则能否在同一次执行中执行;现有的条件公式判定方法只能包含不可更新或有限次更新变量,当主动规则集只包含可有限次循环执行的触发环时,现有方法不能准确判定它是可终止的。为此,提出了触发环的执行序列的概念和建立包含可更新变量的增强条件公式的方法,新的判定方法将触发环和执行语义有机地结合在一起,较现有方法可以发现更多的可终止性情形,同时给出了新算法的可终止性和正确性证明。     

基于增强条件公式的主动规则集可终止性判定

主动规则集的可终止性判定是一个研究热点问题,现有的基于触发图和活化图的方法没有考虑触发环所有所属规则能否在同一次执行中执行;现有的条件公式判定方法只能包含不可更新或有限次更新变量,当主动规则集只包含可有限次循环执行的触发环时,现有方法不能准确判定它是可终止的。为此,提出了触发环的执行序列的概念和建立包含可更新变量的增强条件公式的方法,新的判定方法将触发环和执行语义有机地结合在一起,较现有方法可以发现更多的可终止性情形,同时给出了新算法的可终止性和正确性证明。     

含有非独立型触发环的主动规则集归约算法研究

可终止性判定问题是主动数据库的一个核心问题。现有的研究工作提出了运用触发图和活化图的方法解决这个问题，其中的一个关键技术就是利用归约算法对主动规则集进行归约。已有的计算方法对一些可归约规则无法识别。本文提出了独立型触发环、非独立型触发环、活化路径、禁止活化环、禁止活化规则等概念。基于这些概念，提出了一个新的归约算法，从而可识别出更多的可归约规则。     

计算主动数据库中不可归约规则集的有效算法

主动数据库中规则集的可终止性判定是一个重要问题，已经成为一个研究热点．有些研究工作提出了在编译阶段运用触发图和活化图的方法解决这个问题，其中的一个关键技术就是计算主动规则集的不可归约规则集．现有的计算方法由于具有一定保守性，使得计算出的不可归约规则集仍可进一步地归约，这无疑将影响到规则集的可终止性判定的准确性和运行阶段规则分析的效率．经过深入分析活化规则可无限执行的特点，提出了活化路径等概念．基于这些概念，提出了一个计算主动规则集的不可归约规则集的有效算法，使现有方法求得的不可归约规则集得到进一步的归约．     

XML中的主动规则及其可终止性分析

主动XML系统一般采用触发器，即“事件-条件-动作”(ECA)规则来提供主动行为。本文提出了一种新的事件监测机制，在XML系统中引入‘主动节点’，即把规则也融入节点，各节点上的ECA规则只需在节点修改时被激活并进行检查，提高了动作的执行效率，增强了系统的实时性。本文结合规则实例给出了分析规则终止性的静态判定算法，引入触发图、活化图、修改后的触发图、触发环等概念，对触发图中的简单触发环进行转换，产生一个对应于触发环的循环语句，对触发环中每一个被修改的节点产生一个递归等式。展开递归等式检验它的可满足性可以用来分析规则集的可终止性。这一算法提高了可终止性判定的精确性，降低了复杂度。     

XML中的主动规则的模型及其可终止性分析

在对XML数据模型主动机制研究的基础上，结合规则实例提出了一种新的分析规则终止性的静态判定算法。此算法基于触发环的概念，首先对触发环中每一个被修改的节点产生一个递归等式，然后通过展开递归等式并检验其可满足性，就可以分析规则集的可终止性，这样不仅可以得到更高的精确度及更小的复杂度，而且可以得到有效的判定主动规则可终止性的条件。     

主动数据库中基于图的规则的指称语义研究

1 引言主动数据库的主动特性一般使用E-C-A(Event-Condi-tion-Action)规则模型描述。我们用CA规则表示ECA规则模型中的Condition和Action部分,ECA规则语言的语义可描述为:事件E的发生可触发CA规则的执行,该CA规则的执行又可导致其它事件的发生,进而触发其它CA规则的执行,形成触发规则集。主动规则源于人工智能的知识表示的产生式系统(OPS5),许多主动数据库规则系统的执行语义均源于OPS5产生式规则语言的recognize-act cycle算法(如图     

Active Rule Termination Analysis: An Implementation and Evaluation of the Refined Triggering Graph Method

This paper describes the implementation of the Refined Triggering Graph (RTG) method for active rule termination analysis and provides an evaluation of the approach based on the application of the method to a sample active application. The RTG method has been defined in the context of an active-deductive, object-oriented database language known as CDOL (Comprehensive, Declarative, Object Language). The RTG method studies the contents of rule pairs and rule cycles in a triggering graph and tests for: (1) the successful unification of one rule's action with another rule's triggering event, and (2) the satisfiability of active rule conditions, asking whether it is possible for the condition of a triggered rule to evaluate to true in the context of the triggering rule's condition. If the analysis can provably demonstrate that one rule cannot trigger another rule, the directed vector connecting the two rules in a basic triggering graph can be removed, thus refining the triggering graph. An important aspect in the implementation of the method is the development of a satisfiability algorithm for CDOL conditions. This paper presents the tool that was developed based on the RTG method, describing how techniques from constraint logic programming are integrated with other techniques for testing the satisfiability of rule triggering conditions. The effectiveness of the approach within the context of a sample application is also addressed.     

Compile-time and runtime analysis of active behaviors

Active rules may interact in complex and sometimes unpredictable ways, thus possibly yielding infinite rule executions by triggering each other indefinitely. This paper presents analysis techniques focused on detecting termination of rule execution. We describe an approach which combines static analysis of a rule set at compile-time and detection of endless loops during rule processing at runtime. The compile-time analysis technique is based on the distinction between mutual triggering and mutual activation of rules. This distinction motivates the introduction of two graphs defining rule interaction, called Triggering and Activation Graphs, respectively. This analysis technique allows us to identify reactive behaviors which are guaranteed to terminate and reactive behaviors which may lead to infinite rule processing. When termination cannot be guaranteed at compile-time, it is crucial to detect infinite rule executions at runtime. We propose a technique for identifying loops which is based on recognizing that a given situation has already occurred in the past and, therefore, will occur an infinite number of times in the future. This technique is potentially very expensive, therefore, we explain how it can be implemented in practice with limited computational effort. A particular use of this technique allows us to develop cycle monitors, which check that critical rule sequences, detected at compile time, do not repeat forever We bridge compile-time analysis to runtime monitoring by showing techniques, based on the result of rule analysis, for the identification of rule sets that can be independently monitored and for the optimal selection of cycle monitors     

Graphillion: software library for very large sets of labeled graphs

Several graph libraries have been developed in the past few decades, and they were basically designed to work with a few graphs. However, there are many problems in which we have to consider all subgraphs satisfying certain constraints on a given graph. Since the number of subgraphs can increase exponentially with the graph size, explicitly representing these sets is infeasible. Hence, libraries concerned with efficiently representing a single graph instance are not suitable for such problems. In this paper, we develop Graphillion, a software library for very large sets of (vertex-)labeled graphs, based on zero-suppressed binary decision diagrams. Graphillion is not based on a traditional representation of graphs. Instead, a graph set is simply regarded as a “set of edge sets” ignoring vertices, which allows us to employ powerful tools of a “family of sets” (a set of sets) and permits large graph sets to be handled efficiently. We also utilize advanced graph enumeration algorithms, which enable the simple family tools to understand the graph structure. Graphillion is implemented as a Python library to encourage easy development of its applications, without introducing significant performance overheads. In experiments, we consider two case studies, a puzzle solver and a power network optimizer, in which several operations and heavy optimization have to be performed over very large sets of constrained graphs (i.e., cycles or forests with complicated conditions). The results show that Graphillion allows us to manage a huge number of graphs with very low development effort.     

Constant Thresholds Can Make Target Set Selection Tractable

Target Set Selection, which is a prominent NP-hard problem occurring in social network analysis and distributed computing, is notoriously hard both in terms of achieving useful polynomial-time approximation as well as fixed-parameter algorithms. Given an undirected graph, the task is to select a minimum number of vertices into a “target set” such that all other vertices will become active in the course of a dynamic process (which may go through several activation rounds). A vertex, equipped with a threshold value t, becomes active once at least t of its neighbors are active; initially, only the target set vertices are active. We contribute further insights into the existence of islands of tractability for Target Set Selection by spotting new parameterizations characterizing some sparse graphs as well as some “cliquish” graphs and developing corresponding fixed-parameter tractability and (parameterized) hardness results. In particular, we demonstrate that upper-bounding the thresholds by a constant may significantly alleviate the search for efficiently solvable, but still meaningful special cases of Target Set Selection.