模型检测中可变攻击者模型的构造

提出了一个可变攻击者模型构造方案. 该方案通过定义抽象项的概念及其运算规则,大大降低了攻击者进行代数运算的复杂度. 定义了攻击者行为库和攻击规则选择算法,使检测者能根据不同的协议构造不同的攻击者模型. 由于攻击者行为可任意组合,故实现了攻击者模型的可变性. 可变攻击者模型保证了模型检测工具对协议分析的效率和准确性.     

Murg term rewrite systems

The union of a monadic and a right-ground term rewrite system is called a murg term rewrite system. We show that for murg TRSs the ground common ancestor problem is undecidable. We show that for a murg term rewrite system it is undecidable whether the set of descendants of a ground tree is a recognizable tree language. We show that it is undecidable whether a murg term rewrite system over Σ preserves Σ-recognizability.     

On the recursive decomposition ordering with lexicographical status and other related orderings

This paper studies three orderings, useful in theorem proving, especially for proving termination of term rewriting systems: the recursive decomposition ordering with status, the recursive path ordering with status and the closure ordering. It proves the transitivity of the recursive path ordering, the strict inclusion of the recursive path ordering in the recursive decomposition ordering, the totality of the recursive path ordering — therefore of the recursive decomposition ordering — the strict inclusion of the recursive decomposition ordering in the closure ordering and the stability of the closure ordering by instantiation.Part of this work was done while the author was visiting the Institute for New Generation Computer Technology, Tokyo, Japan.     

LEARNING TO IMPROVE PLAN QUALITY

Adaptive automated planning systems that can, over time, improve the quality of plans they produce are a promising prospect. The first part of the article discusses the issues involved in designing quality improving learning for planning systems and reviews recent work on learning to improve plan quality. The second part describes our work on the Performance Improving Planning (PIP) System. The heart of PIP is an analytic technique that compares two planning episodes for solving a planning problem that led to two different quality solutions—a higher-quality solution and a lower quality solution—and identifies the critical differences that were responsible for the resulting differences in the quality of the completed plans. We compare the effectiveness of two different ways of storing and applying the knowledge learned from this analysis—as search-control rules and as rewrite rules. The results show that the search-control rules are more effective in improving plan quality. Further analysis of PIP-search-control—the version of PIP that stores the learned knowledge as search-control rules—shows that it is an effective technique for improving plan quality in a variety of situations.     

On Symbolic Verification of Weakly Extended PAD

We consider the verification problem of a class of infinite-state systems called wPAD. These systems can be used to model programs with (possibly recursive) procedure calls and dynamic creation of parallel processes. They correspond to PAD models extended with an acyclic finite-state control unit, where PAD models can be seen as combinations of prefix rewrite systems (pushdown systems) with context-free multiset rewrite systems (synchronization-free Petri nets). Recently, we have presented symbolic reachability techniques for the class of PAD based on the use of a class of unranked tree automata. In this paper, we generalize our previous work to the class wPAD which is strictly larger than PAD. This generalization brings a positive answer to an open question on decidability of the model checking problem for wPAD against EF logic. Moreover, we show how symbolic reachability analysis of wPAD can be used in (under) approximate analysis of Synchronized PAD, a (Turing) powerful model for multithreaded programs (with unrestricted synchronization between parallel processes). This leads to a pragmatic approach for detecting the presence of erroneous behaviors in these models based on the bounded reachability paradigm where the notion of bound considered here is the number of synchronization actions.     

Structures for Abstract Rewriting

When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding theory, and we propose a Knuth-Bendix–style completion procedure in this abstract framework.     

Cbase数据库查询重写模块的设计与实现

本文详细讨论了重写模块的设计思想与实现技术，并讨论了利用执行引擎特点引入的一组基于等价谓调的简单语句直写规则．测试结果表明，增加重写模块的查询优化器能显著提高系统的查询效率．     

Intersection of finitely generated congruences over term algebra

We show that it is decidable for any given ground term rewrite systems R and S if there is a ground term rewrite system U such that ↔_U^*=↔_R^*∩↔_S^*. If the answer is yes, then we can effectively construct such a ground term rewrite system U. In other words, for any given finitely generated congruences ρ and τ over the term algebra, it is decidable if ρ∩τ is a finitely generated congruence. If the answer is yes, then we can effectively construct a ground term rewrite system U such that ↔_U^*=ρ∩τ.     

一种基于DTD的XPath逻辑优化方法

Xpath成为XML数据查询的基本机制.Xpath中表达节点之间的祖孙关系的‘//'和任意匹配字符的‘*'等非确定操作符,增强了Xpath表达方式的灵活性,但同时引入了Xpath处理的复杂性.如何利用DTD减少Xpath中的不确定操作符,从而提高Xpath的执行效率成为一个基本的研究问题.传统方法主要侧重于特定受限Xpath的确定化重写.利用树自动机在一个框架中表达Xpath和DTD,提出了一种新的Xpath树自动机和DTD树自动机的乘积运算,并证明了乘积的结果就是基于DTD的Xpath优化形式,在多项式时间内基于代价获取了Xpath的优化结果.实验数据表明,基于提出的Xpath的逻辑优化方法,能够有效地提高Xpath执行器的执行效率.     

Toward a formal study of jazz chord sequences generated by Steedman’s grammar

This paper shows how to generate jazz chord sequences incrementally using Steedmans grammar by taking advantage of some formal properties. We point out the specific role played by particular chord sequences called cadential sequences. By precompiling them, one could improve the implementation of Steedmans grammar in a real-time improvisation system, and make it more reactive to the inputs of the user.I thank Mark Steedman for his comments on this text.