有界モデルチェック（Bounded Model Checking, BMC）は、ソフトウェアシステムの抽象モデルにおける限定的な実行シナリオ上で、システムが満たすべき性質を効率的に検証するための形式的手法である。この性質はしばしば時相論理（temporal logic）を用いて記述され、システムは状態遷移系としてモデル化される。本論文では、クライアント数が無限に増える可能性のあるクライアント・サーバーシステムの時相的性質を記述するための新たな計数論理 $\mathcal{L}{C}$LC を提案する。さらに、クライアント・サーバーシステムを表現するネットワークにおけるトークン数と実行ステップ数という、二つの区別可能なパラメータを用いる二次元有界モデルチェック（2D-BMC）戦略を提案する。この戦略の特徴は、これらの二つのパラメータが独立に進化することであり、これはペトリネット形式における従来のBMC手法とは異なる。本研究で開発した2D-BMC戦略は、最先端のSMT（Satisfiability Modulo Theories）ソルバZ3を活用するツールDCModelCheckerに実装されている。システムはペトリネットとして与えられ、$\mathcal{L}{C}$LC を用いて指定された性質は、ソルバによって検証可能な論理式に符号化される。本ツールは、モデルチェックコンテスト（Model Checking Contest, MCC）の産業界ベンチマークにも対応しており、その実験結果を報告することで、2D-BMC戦略の実用性と有効性を示している。