{"id":{"repo_id":"oldenburg","oai_identifier":"oai:oops.uni-oldenburg.de:1389"},"canonical_url":"https://search.dev.ndltd.org/etd/oldenburg/oai:oops.uni-oldenburg.de:1389","repository":{"repo_id":"oldenburg","name":"Carl von Ossietzky Universität Oldenburg","base_url":"http://oops.uni-oldenburg.de/cgi/oai2"},"display":{"title":"Stochastic satisfiability modulo theories : a symbolic technique for the analysis of probabilistic hybrid systems","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Teige, Tino"],"institution":"Universität Oldenburg","degree_name":null,"degree_level":"thesis.doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-08-29","date_published":"2012-08-29","updated_at":"2026-07-27T20:28:14Z","subjects":["[Keine Schlagwörter von Autor/in vergeben.]"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://oops.uni-oldenburg.de/1389","outbound_label":"Repository record","outbound_source":"source_url"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Teige, Tino"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:publisher","label":"Institution","values":["BIS der Universität Oldenburg"]},{"key":"dc:type","label":"Dc Type","values":["doctoralThesis"]},{"key":"thesis:degree_level","label":"Degree Level","values":["thesis.doctoral"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Universität Oldenburg"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["[Keine Schlagwörter von Autor/in vergeben.]"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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.","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."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Stochastic satisfiability modulo theories : a symbolic technique for the analysis of probabilistic hybrid systems"]}]}],"canonical_facts":{"dc:creator":["Teige, Tino"],"dc:description.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.","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."],"dc:format.medium":["application/pdf"],"dc:publisher":["BIS der Universität Oldenburg"],"dc:subject":["[Keine Schlagwörter von Autor/in vergeben.]"],"dc:title":["Stochastic satisfiability modulo theories : a symbolic technique for the analysis of probabilistic hybrid systems"],"dc:type":["doctoralThesis"],"thesis:degree_level":["thesis.doctoral"],"thesis:institution_name":["Universität Oldenburg"]},"updated_at":"2026-07-27T20:28:14Z"}