Stochastic satisfiability modulo theories : a symbolic technique for the analysis of probabilistic hybrid systems

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2012

Author dc:creator

• Teige, Tino

• [Keine Schlagwörter von Autor/in vergeben.]

Repository record source_url

http://oops.uni-oldenburg.de/1389

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:1389