Eine Plattform für die Wissenschaft: Bauingenieurwesen, Architektur und Urbanistik
Eine Plattform für die Wissenschaft: Bauingenieurwesen, Architektur und Urbanistik
Model Checking Concurrent Systems Using Temporal Logics ; Automatische Verifikation paralleler Systeme mittels temporaler Logiken
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 ...
Model Checking Concurrent Systems Using Temporal Logics ; Automatische Verifikation paralleler Systeme mittels temporaler Logiken
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 ...
Model Checking Concurrent Systems Using Temporal Logics ; Automatische Verifikation paralleler Systeme mittels temporaler Logiken
Mennicke, Roy (Autor:in) / Kuske, Dietrich / Gastin, Paul / Leucker, Martin
25.11.2015
Hochschulschrift
Elektronische Ressource
Englisch
Systeme paralleler Scherbänder unter Extension im ebenen Verformungszustand
| UB Braunschweig | 2011
Automatische Verifikation von Straßen in digitalen Luftbildern auf Basis von Profilen
| Online Contents | 1996