权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

戦略を導入した項書換え系における到達可能性の研究

引入策略的术语重写系统可达性研究

基本信息

批准号：
10J08166
负责人：
小島芳治
金额：
$ 1.34万
依托单位：
Nagoya University
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2010
资助国家：
日本
起止时间：
2010 至 2012
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10J08166/
关键词：
項書換え系戦略到達可能性木オートマトン書換え戦略

项目摘要

本研究では戦略を導入した項書換え系における到達可能性の検証方法を確立することで、ソフトウェアの安全性、信頼性、セキュリティ等への応用を目指す。本年度は最外書換えという戦略を導入した場合の到達可能性の検証方法について研究を行ったが、具体的な検証方法を発見することは出来なかった。検証のためのアイデアとして、2方向木オートマトンを用いることを以前から考えていたが、2方向木オートマトンの性質は最外書換えを導入した場合の検証に役立つものではないことがわかった。項書換え系の書換え規則の両辺が非常に浅い場合については過去の結果の応用による検証が可能ではないかと考えたが、今年度中の検証方法の確立には至らなかった。また、以前からフランスのFlorent Jacquemard氏と共同で研究を進めているControlled Term Rewriting(以下CntTRS)についても研究を進めた。CntTRSは木オートマトンを用いて書換え可能な位置を指定する戦略を用いた項書換え系であるが、昨年度までの研究で具体的な検証方法の確立が困難であることがわかっている。そこで、本年度は特定の制限を加えたCntTRSについての到達可能性の検証方法を示した。具体的には、木オートマトンによる書換え可能位置の指定を項の頂点から書換え可能な位置までのパターンに限定した。このような制限下で基底項のCntTRSの到達可能性について決定可能な検証法が存在することを示した。また、同様の制限下において、線形かつ右シャローというクラスについて、書換えを項の深い位置から順に行うように制限した場合についても到達可能性の決定可能な検証法が存在することを示した。深さによる書換えの順番の指定が無い場合は決定可能な検証法は存在しないため、本結果は有意義であると言える。

This study introduces a new approach to the identification of arrival probability in the system, and provides guidance on the safety, reliability and application of the system. This year, the most important part of the book is to introduce the possibility of arrival detection methods, research, and specific detection methods. The test results show that the test results are correct, and the test results show that the test results are correct. The rules of the book exchange are very shallow, the results of the past are used, the test is possible, the test method of the current year is established, and the test method is established. Florent Jacquemard's joint research into Controlled Term Rewriting(hereinafter CntTRS) CntTRS is the most difficult method to establish in the research of the past year. This year, we will increase the number of specific restrictions and test the probability of arrival. The specified vertex of the possible position of the switch is limited. The probability of arrival of CntTRS under the control limit determines the probability of existence of CntTRS. In the case of the same restriction, the possibility of arrival is determined by the existence of the linear restriction. The result of the test is meaningful.