2010 Fiscal Year Final Research Report
Equational Tree Automata : Arithmetic Constraint Definability and the Application Towards Automated Verification
| Project/Area Number |
21700022
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
OHSAKI Hitoshi National Institute of Advanced Industrial Science and Technology, 産学官連携推進部門, 連携研究体副体長 (00356627)
|
|---|
| Project Period (FY) |
2009 – 2010
|
| Keywords | ツリーオートマトン / 書換系(rewriting systems) / 可換文法 / 算術制約 |
|---|
| Research Abstract |
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.
|
Research Products
(11 results)
