Research Training Group SCARE

Verification of Stochastic Systems by Stochastic Satisfiability Modulo
Theories with Continuous Domain (CSSMT)

26. April 2017

Organisator:  Yang Gao, M.Sc.

Ort:  OFFIS-Gebäude, Raum F02

M i t t e i l u n g 

Im Rahmen der Disputation seines Promotionsverfahrens hält Herr Yang
Gao, M.Sc., seinen öffentlichen Vortrag zum Thema

„Verification of Stochastic Systems by Stochastic Satisfiability Modulo
Theories with Continuous Domain (CSSMT)”

am Mittwoch, den 26. April 2017, um 9.00 Uhr im OFFIS-Gebäude, Raum F02.


Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative extension of classical Satisfiability Modulo Theories (SMT) inspired by stochastic logics. It extends SMT by the usual as well as randomized quantifiers, facilitating capture of stochastic game properties in the logic, like reachability analysis of hybrid-state Markov decision processes. Solving for SSMT formulae with quantification over finite and thus discrete domain has been addressed by Tino Teige et al. In my PhD work, I consider extending their work to SSMT over continuous quantifier domains (CSSMT) in order to enable capture of, e.g., continuous disturbances and uncertainty in hybrid systems. CSSMT extends the semantics of SSMT and introduces a corresponding solving procedure. My PhD work concentrate on the solving procedure and its soundness for CSSMT along with its algorithmic enhancements, the translation from stochastic hybrid systems to CSSMT formulae and their capability to analyze reachability properties are also considered as the main parts of my PhD work. Meanwhile, the corresponding CSSMT solver is implemented so that the CSSMT formulae can be encoded and solved automatically. Potential applications such as stochastic control problems, scheduling problems etc., are also pursued.

Mit der Teilnahme von Zuhörerinnen und Zuhörern an der anschließenden
Prüfung bis 10.30 Uhr ist Herr Gao einverstanden.

gez. Prof. Dr.-Ing. A. Hahn