LMNtalは階層グラフ書換えに基づく統合計算モデルとして設計され発展してきたが，我々は新たにLMNtalの検証および探索分野への応用を目指して，LMNtalをモデリング言語とするモデル検査器を構築し，モデリングと検証の経験を蓄積している．本論文では，状態空間探索や検証の可視化機能を備えた統合開発環境LMNtalEditorとそれを利用したモデル記述例，動作例，可視化例を紹介する．新たに構築したLMNtalEditorは，全状態空間や反例の可視化とブラウジング機能や，特定の条件を満たす状態の検索機能などを備えている．並行計算やAI探索問題を含む多様な例題をLMNtalEditor上で実行することで，本統合環境がモデルや反例の理解に重要な役割を果たし，検証作業の効率を大幅に高めることが確認できた．またPromela, MSR, Coloured Petri Netなどのモデリング言語による記述のLMNtalへの変換実験を通じて，LMNtalの表現力がカバーする範囲を検証分野に拡大することができた．