オートマトンは定理自動証明や計算モデル解析において活用されている。利用の形態は様々であるが、オートマトンを別のオートマトンに変換する操作が基本的な役割を果たすことが多い。本研究では、オートマトン変換の設計、分析を支援する枠組の基礎を築くことを目的とし、変換前のオートマトンと変換後のオートマトンの状態の対応関係を容易に取り扱うための変換系のモデルを与える。さらに、状態対応関係の合成演算を導入して多段変換に対応できるようにするとともに、2つのオートマトンの対応関係を状態の等価関係をもとに自動的に生成する手法を提案する。これらのモデルとアルゴリズムをプログラミング言語MLを用いて変換系として実装する。