Abstracts Category : Other

Verification ofStochastic Systems by Stochastic Satisfiability Modulo Theorieswith Continuous Domain (CSSMT)

by Yang Gao

Stochastic Satisfiability Modulo Theories (SSMT) is a quantitativeextension of Satisfiability Modulo Theories (SMT) inspired bystochastic logics. It extends SMT by randomized quantifiers,facilitating capture of stochastic game properties in the logic,like reachability analysis of hybrid-state Markov decisionprocesses. Solving SSMT formulae with quantification over finiteand thus discrete domain has been addressed by Tino Teige et al. Amajor limitation of the SSMT solving approach is that allquantifiers are confined to range over finite domains. As thisimplies that the support of probability distributions have to befinite, a large number of phenomena cannot be expressed within theSSMT framework. To overcome this limitation, this thesis relaxesthe constraints on the domains of randomized variables, now alsoadmitting dense probability distributions in SSMT solving, whichyields SSMT over continuous quantifier domains(CSSMT). Inspiriert durch stochastische Logiken wurde krzlich einequantitative Erweiterung der existierenden Satisfiability ModuloTheory (SMT) entwickelt. Diese, sogenannte StochasticSatisfiability Modulo Theory, erweitert die SMT, indem neben denAll- und Existenz-Quantoren weitere, randomisierte Quantoreneingefhrt wurden. Das Lsen der entsprechenden SSMT Formeln unterder Einschrnkung von diskreten Quantoren wurde bereits durch TinoTeige et al. adressiert. Einer der grten limitierenden Faktorensolcher Anstze ist, dass die Quantoren auf beschrnkte Bereicheber endlichen Grundmengen limitiert sind. Um kontinuierlicheVerteilungen in existierende SSMT Methoden zu integrieren, soll indieser Arbeit die Erweiterung SSMT over continuous quantifierdomains (CSSMT) entwickelt werden, welche die erwhntenEinschrnkungen relaxiert, sodass nun auch SSMT Ausdrcke behandeltwerden knnen welche Verteilungen mit kontinuierlichem Trgerbeinhalten.Advisors/Committee Members: Frnzle, Martin (advisor), Zuliani, Paolo (advisor).