In dieser Arbeit wird die Komplexität der automatischen Verifikation von parallelen Systemen mittels Temporallogiken untersucht. Es werden dabei zwei verschiedene Typen von Systemen betrachtet: mehrläufige Programme, die rekursive Prozeduren aufrufen, und verteilte Prozesse, die zur Kommunikation untereinander Nachrichten austauschen. Erstere werden typischerweise durch endliche Automaten mit mehreren Kellern modelliert; Letztere üblicherweise durch endliche Automaten, die über FIFO-Kanäle miteinander kommunizieren (CFMs). In beiden Fällen ist das allgemeine Verifikationsproblem selbst für sehr einfache temporale Logiken unentscheidbar. Daher richten wir das Augenmerk auf Heuristiken, die die Läufe des zu untersuchenden Systems unterapproximieren. Im Kontext der message sequence charts (MSCs), welche als Läufe von CFMs aufgefasst werden können, betrachten wir ausschließlich Verhalten, die eine Ausführung mit beschränkt großen Kanälen zulassen. Im Rahmen der Mehrkellerautomaten konzentrieren wir uns auf geschachtelte Wörter, die bezüglich der Anzahl ihrer Phasen, der Größe ihrer Bereiche bzw. ihrer Teilungsweite beschränkt sind. Dabei sind geschachtelte Wörter Zeichenketten, die für jeden Keller eine Relation aufweisen, die zusammengehörige Schreib- und Leseoperationen auf dem jeweiligen Keller explizit miteinander in Verbindung setzt. Die Art der Spezifikationssprache betreffend untersuchen wir temporale Logiken, deren Modalitäten mittels Formeln der monadischen Logik zweiter Stufe definiert werden können. Dieser Typ von Temporallogiken umfasst nahezu alle bisher in der Literatur behandelten temporalen Logiken. Für jedes von uns untersuchte beschränkte Verifikationsproblem geben wir ein Entscheidungsverfahren an, dessen Komplexität n-fach exponentiell in der jeweilig gewählten Verhaltensbeschränkung (beispielsweise in der Größe der Kanäle) ist. Dabei ist n linear in der Anzahl der monadischen Quantorenalternierungen in den Modalitätsdefinitionen. Überraschenderweise ist die Komplexität nur einfach exponentiell in den Größen der temporalen Formel und des Systemmodells. Weiterhin geben wir für jedes Problem beinahe scharfe untere Schranken an. Mit anderen Worten: Es stellt sich beinahe als ein allgemeines Naturgesetz heraus, dass die Komplexität der automatischen Verifikation im Rahmen von parallelen Systemen im Wesentlichen von der Kompliziertheit der temporalen Logik (gemessen in der Anzahl der Quantorenalternierungen in den Modalitätsdefinitionen) und der gewählten Verhaltensbeschränkung beeinflusst wird und viel weniger von den Größen der temporalen Formel und des Systemmodells. Außerdem betrachten wir im Fall der automatischen Verifikation von CFMs zwei weitere Arten von Temporallogiken. Zum einen erforschen wir konkrete Modalitäten, die üblicherweise im Zusammenhang mit parallelen Systemen Verwendung finden. Hier lässt sich zeigen, dass die Platzkomplexität des beschränkten Verifikationsproblems polynomiell in der Beschränkung und exponentiell in der Anzahl der Prozesse ist. Zum anderen zeigen wir für eine Variante der propositional dynamic logic (PDL) die Vollständigkeit des beschränkten Verifikationsproblems für polynomiellen Platz.
This work deals with the complexity of model checking concurrent systems using temporal logics. As sytem types, we consider two different forms of concurrent systems: these are parallel programs with recursive procedure calls and distributed processes communicating using messages. The former are typically modeled by finite automata equipped with multiple stacks whereas the latter are usually represented by communicating finite-state machines which are basically finite automata exchanging messages via first in first out channels. In both cases, the general model checking problem is undecidable even for very simple temporal logics. Therefore, we focus on heuristics under-approximating the set of runs of the system to be examined. In the context of message sequence charts, which can be understood as runs of communicating finite-state machines, we limit ourself to behaviors which allow an execution with bounded channels. Whereas in the setting of multi-stack automata, we concentrate on phase-bounded, scope-bounded and split-width-bounded nested words. The latter are words exhibiting a relation for every stack which explicitly associates push operations with their matching pop actions. On the specification language side, we investigate temporal logics whose modalities can be defined using formulas from the monadic second-order logic. This type of temporal logics subsumes almost all temporal logics considered in the literature so far. For all bounded model checking problems, we obtain a decision procedure whose complexity is n-fold exponential in the chosen behavioral restriction (e.g., in the size of the communication channels) where n is linear in the number of monadic quantifier alterations occurring in the modality definitions. Surprisingly, it is only exponential in the sizes of the temporal formula and the system model. We also state almost tight lower bounds for each setting. In other words, it turns out to be almost a general law of nature that the complexity of model checking concurrent systems is mainly influenced by the elaborateness of the temporal logic (measured by the number of quantifier alternations in the modality definitions) and the chosen behavioral restriction. In comparison, the impact of the sizes of the temporal formula and the system model is less important. Regarding communicating finite-state machines, we also explore the bounded model checking problems for various concrete modalities usually used in the context of concurrent systems and a variant of propositional dynamic logic. Regarding the former, we obtain decision procedures running in space polynomial in the restriction and exponential in the number of processes. For the latter, we prove its PSPACE-completeness.