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

点击翻译按钮获取中文摘要

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