Teige, Tino (2012) Stochastic satisfiability modulo theories : a symbolic technique for the analysis of probabilistic hybrid systems. PhD, Universität Oldenburg.

Preview

Volltext (2964Kb)

Abstract

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.

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	[Keine Schlagwörter von Autor/in vergeben.]
Controlled Keywords:	Hybrides System , Stochastisches Modell
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	17 Jan 2013 14:29
Last Modified:	08 Jul 2013 13:04
URI:	https://oops.uni-oldenburg.de/id/eprint/1389
URN:	urn:nbn:de:gbv:715-oops-14696
DOI:
Nutzungslizenz:

Actions (login required)

View Item