谷歌Chrome浏览器插件
订阅小程序
在清言上使用

Reachability, Confluence, And Termination Analysis With State-Compatible Automata

Inf. Comput.(2017)

引用 30|浏览29
暂无评分
摘要
Regular tree languages are a popular device for reachability analysis over term rewrite systems, with many applications like analysis of cryptographic protocols, or confluence and termination analysis. At the heart of this approach lies tree automata completion, first introduced by Genet for left-linear rewrite systems. Korp and Middeldorp introduced so-called quasi-deterministic automata to extend the technique to non-left-linear systems. In this paper, we introduce the simpler notion of state-compatible automata, which are slightly more general than quasi-deterministic, compatible automata. This notion also allows us to decide whether a regular tree language is closed under rewriting, a problem which was not known to be decidable before.The improved precision has a positive impact in applications which are based on reachability analysis, namely termination and confluence analysis.Our results have been formalized in the theorem prover Isabelle/HOL. This allows to certify automatically generated proofs that are using tree automata techniques. (C) 2016 The Authors. Published by Elsevier Inc.
更多
查看译文
关键词
automata,termination analysis,confluence,state-compatible
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要