非決定性Streaming String TransducerとParikh才ー卜マトンを用いた文字列制約の充足可能性判定

摘要

正規表現や文字列操作関数などを含む論理式は文字列制約と呼ばれ，文字列を扱うプログラムの分析に現れる.本研究は構文的に制限された文字列制約の充足可能性を，トランスデューサを用いて判定する.Streaming String Transducer (SST)は文字列を別の文字列に変換するトランスデューザの一種であり，文字列を保持できる定数個の変数を使用して出力を計算する.またParikhオートマトン（PA)は入力文字列から自然数のベクトルを計算し，それが予め決められた論理式を満たすかで受理を判定する.本研究は非決定性SSTによるPAの逆像が計算できることを示す.さらにこれを応用し，正規表現とキヤプチャグループを使う文字列置換や，文字列と整数を入力とする関数substringを含む文字列制約の充足可能性が決定可能であることを示す.本研究はこの手法を文字列理論のSMTソルバとして実装し，いくつかの制約を解く実験によって既存のソルバと比較した.