基于重写的系统分析的语义方法
A Semantic Approach to the Analysis of Rewriting-Based Systems
摘要:
表示为一阶句子的可证性的性质可以通过找到句子的否定的模型来反驳。然而,这一事实仅在有限的情况下才有意义,这取决于句子的形式和所涉系统的类别。在本文中,我们表明,一些有趣的属性重写为基础的系统可以用这种方式进行调查,包括不可行性和非joinability的关键对(条件)重写,非循环的条件重写系统,或安全访问受保护的网页的网站建模为有序排序重写理论。有趣的是,当为处理上述问题而开发的特定技术失败时,这种统一的语义方法就会成功。
英文摘要:
Properties expressed as the provability of a first-order sentence can be disproved by just finding a model of the negation of the sentence. This fact, however, is meaningful in restricted cases only, depending on the shape of the sentence and the class of systems at stake. In this paper we show that a number of interesting properties of rewriting-based systems can be investigated in this way, including infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness of conditional rewrite systems, or the secure access to protected pages of a web site modeled as an order-sorted rewrite theory. Interestingly, this uniform, semantic approach succeeds when specific techniques developed to deal with the aforementioned problems fail.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。