計算モデルである論理制約付き項書換え系（LCTRS）を用いたプログラム検証を状態遷移機械の到達可能性などの検証に応用する研究がされており，Uppaalなどのモデル検査ツールなどとの比較が望ましい．しかし，Uppaal記述をLCTRSで記述するのは煩雑な作業であり，Uppaal記述に比べてプロセスの追加などは容易ではない．本論文では，アージェントロケーションを含むUppaal記述を対象とし，LCTRSへの変換を試みる．それにより，LCTRSを直接記述する必要がなくなり，モデル検査との比較が容易になることを期待できる．