Bounded Model Checking (BMC) ist eine effiziente formale Verifikationstechnik, die es ermöglicht, gewünschte Eigenschaften eines Software-Systems anhand beschränkter Laufzeiten eines abstrakten Modells des Systems zu überprüfen. Die Eigenschaften werden häufig in einer temporalen Logik beschrieben, während das System als Zustandsübergangssystem modelliert wird. In diesem Artikel stellen wir eine neuartige Zähllogik $mathcal{L}{C}$mathcalLC vor, die dazu dient, zeitliche Eigenschaften von Client-Server-Systemen mit einer unbeschränkten Anzahl an Clients zu beschreiben. Außerdem präsentieren wir eine zweidimensionale Bounded Model Checking-(2D-BMC)-Strategie, die zwei unterscheidbare Parameter verwendet: einen für die Anzahl der Ausführungsschritte und einen für die Anzahl an Tokens im Netz, das ein Client-Server-System darstellt. Diese beiden Parameter entwickeln sich unabhängig voneinander, was sich von den herkömmlichen BMC-Techniken im Petri-Netz-Formalismus unterscheidet. Diese 2D-BMC-Strategie wurde in einem Werkzeug namens DCModelChecker implementiert, das die 2D-BMC-Technik mit einem modernen Satisfiability Modulo Theories (SMT)-Solver, Z3, kombiniert. Das System wird als Petri-Netz gegeben, und die mit $mathcal{L}{C}$mathcalLC spezifizierten Eigenschaften werden in Formeln kodiert, die vom Solver überprüft werden. Unser Werkzeug ist zudem in der Lage, industrielle Benchmarks aus dem Model Checking Contest (MCC) zu verarbeiten. Wir berichten über diese Experimente, um die Anwendbarkeit der 2D-BMC-Strategie zu veranschaulichen.