Equational Tree Automata : Arithmetic Constraint Definability and the Application Towards Automated Verification

自2001年Ohsaki提出方程树自动机理论以来，方程树自动机及其应用得到了很大的发展。基于等式树自动机的自动验证方法ACTAS（http：//staff.aist.go.jp/hitoshi.ohsaki/actas/）可用于密码协议、XML模式和程序设计语言的分析。正则AC树自动机的叶语言具有非负线性算术约束和半线性集合的表达能力。我们在这个研究计划中研究了一类新的交换文法，它可以是“整数”线性算术约束的对应物，从而可以是向量加法系统。首先，我们引入了（交换）语言上的“逆”的概念，更准确地说，我们通过引入新的算子i和6个新的公理来定义“交换i-Kleene代数”。该代数允许布尔运算和逆运算。这个结果是由霍普金斯和Kozen（1999）的方法可以自然地推广到交换i-Kleene代数而得到的。这意味着（1）交换i-正则文法与交换i-上下文无关文法一样具有表达性，（2）交换i-正则文法是整数线性算术的对应物。除了上述研究活动之外，我们还为日本和海外的年轻研究人员熟悉我们的方程树自动机做出了贡献。

Equational tree automata and the applications have been developed since 2001 when Ohsaki proposed this theory. The automated verification based on equational tree automata, ACTAS (http://staff.aist.go.jp/hitoshi.ohsaki/actas/), can be applied to the analysis of cryptographic protocols, XML schema and programming languages. The leaf-languages of regular AC tree automata are known as expressive as non-negative linear arithmetic constrains and semi-linear sets. We studied in this research program a new class of commutative grammar which can be the counterpart of "integer" linear arithmetic constraints, and thus of vector-addition systems. First we introduce the notion of "inverse" over (commutative) languages, more precisely, we define "commutative i-Kleene algebra" by introducing new operator i and 6 new axioms. The algebra admits Boolean operations together with inverse operation. This result is obtained from the observation that Hopkins and Kozen approach (1999) can be naturally extended to the commutative i-Kleene algebra. This implies that (1) commutative i-regular grammar is as expressive as commutative i-context-free grammar, and thus (2) commutative i-regular grammar is the counterpart of integer linear arithmetic.In addition to the above-mentioned research activity, we contributed for familiarizing our equational tree automata to young researchers in Japan and overseas.