Zsfassung in dt. Sprache ; Oldenburg, Univ., Diss., 2012
HochschulschriftHybrides SystemStochastisches ModellStatistisches ModellKontinuierliches SystemDiskretes System
Diese Dissertation untersucht symbolische Ansätze zur Erreichbarkeits- und Erwartungswertanalyse probabilistischer hybrid diskret-kontinuierlicher Systeme, die auf einer probabilistischen Logik namens Stochastic Satisfiability Modulo Theories (SSMT) aufbauen. Aufgrund ihrer Ausdrucksstärke lässt sich die schrittbeschränkte Dynamik probabilistischer hybrider Systeme durch SSMT Formeln beschreiben. Um eine automatische Analyseprozedur zu erzielen, befasst sich ein wesentlicher Teil der Arbeit mit SSMT Lösungsalgorithmen und mit algorithmischen Erweiterungen zur Effizienzsteigerung. Die Anwendbarkeit der resultierenden Prozedur wird anhand einer realistischen Fallstudie aus dem Bereich der vernetzten Automatisierungssysteme demonstriert. Um die Limitierung der Schrittbeschränktheit zu überwinden, wird ein verallgemeinertes Konzept der Craigschen Interpolation eingeführt und seine Verwendung in der probabilistischen Modellprüfung zustandsendlicher Systeme gezeigt. <dt.>
This thesis considers symbolic techniques for reachability as well as expected-value analysis of probabilistic hybrid discrete-continuous systems, being based on a probabilistic logic called stochastic satisfiability modulo theories (SSMT). Due to the expressive power of this logic, the step-bounded dynamics of probabilistic hybrid systems can be encoded by SSMT formulae. Aiming at an automatic analysis procedure, a substantial part of the thesis is devoted to algorithms for solving SSMT problems and to algorithmic enhancements improving performance. Applicability of the resulting bounded model checking procedures is demonstrated on a realistic case study from the domain of networked automation systems. To overcome the limitation of step-boundedness, the thesis introduces a generalized concept of Craig interpolation and shows its use in probabilistic model checking of finite-state systems. <engl.>
Logical methods in computer science Braunschweig : Department of Theoretical Computer Science, Technical University of Braunschweig, 2004 Bd. 8.2012, 2, Paper 16, S. 1 - 32 Online-Ressource
