本論文では、パラメータ化されたマルチエージェントシステム（MAS）の安全性検証について考察しています。特に、特定の状態式で表される望ましくない状態がMASに到達可能かどうか、すなわちMASが安全でないかを検証するタスクに焦点を当てています。MASはパラメータ化されており、モデルは可能なエージェントテンプレートの有限集合を表しますが、各テンプレートの具体的なエージェントインスタンスの数は無限で予測できないため、状態空間は無限になります。このため、エージェントインスタンスの数に関係なく正しい検証結果を得る必要があります。この問題に対処するために、満たすべき条件（SMT）に基づく無限状態モデルチェックを適用し、配列ベースのシステム理論を利用します。さらに、2つの実行セマンティクス（同時と交互実行）に基づいて、これらのMASを特定の配列ベースのシステムとして示し、実装アプローチである「SAFE: Swarm Safety Detector」を紹介します。最終的には、今後の研究として、文献における最先端の解法を超えた豊かなパラメータ化及びデータ対応のMAS設定について考察します。