Gao, Yang (2017) Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain (CSSMT). PhD, Universität Oldenburg.

Preview

Volltext (2605Kb)

Abstract

Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative extension of Satisfiability Modulo Theories (SMT) inspired by stochastic logics. It extends SMT by randomized quantifiers, facilitating capture of stochastic game properties in the logic, like reachability analysis of hybrid-state Markov decision processes. Solving SSMT formulae with quantification over finite and thus discrete domain has been addressed by Tino Teige et al. A major limitation of the SSMT solving approach is that all quantifiers are confined to range over finite domains. As this implies that the support of probability distributions have to be finite, a large number of phenomena cannot be expressed within the SSMT framework. To overcome this limitation, this thesis relaxes the constraints on the domains of randomized variables, now also admitting dense probability distributions in SSMT solving, which yields SSMT over continuous quantifier domains (CSSMT).

["eprint_fieldname_title_plus" not defined]

Verifikation von stochastischen Systemen durch Satisfiability Modulo Theory mit kontinuierlichem Domain (CSSMT)

["eprint_fieldname_abstract_plus" not defined]

Inspiriert durch stochastische Logiken wurde kürzlich eine quantitative Erweiterung der existierenden Satisfiability Modulo Theory (SMT) entwickelt. Diese, sogenannte Stochastic Satisfiability Modulo Theory, erweitert die SMT, indem neben den All- und Existenz-Quantoren weitere, randomisierte Quantoren eingeführt wurden. Das Lösen der entsprechenden SSMT Formeln unter der Einschränkung von diskreten Quantoren wurde bereits durch Tino Teige et al. adressiert. Einer der größten limitierenden Faktoren solcher Ansätze ist, dass die Quantoren auf beschränkte Bereiche über endlichen Grundmengen limitiert sind. Um kontinuierliche Verteilungen in existierende SSMT Methoden zu integrieren, soll in dieser Arbeit die Erweiterung SSMT over continuous quantifier domains (CSSMT) entwickelt werden, welche die erwähnten Einschränkungen relaxiert, sodass nun auch SSMT Ausdrücke behandelt werden können welche Verteilungen mit kontinuierlichem Träger beinhalten.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Constraint-Programmierung, Stochastisches System, Wahrscheinlichkeitsrechnung, Hybrides System
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	23 Nov 2017 15:18
Last Modified:	23 Nov 2017 15:18
URI:	https://oops.uni-oldenburg.de/id/eprint/3401
URN:	urn:nbn:de:gbv:715-oops-34828
DOI:
Nutzungslizenz:

Actions (login required)

View Item