{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T01:09:44Z","timestamp":1725412184903},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative exten-<\/jats:p><jats:p>sion of classical Satisfiability Modulo Theories (SMT) inspired by stochastic<\/jats:p><jats:p>logics. It extends SMT by the usual as well as randomized quantifiers, fa-<\/jats:p><jats:p>cilitating capture of stochastic game properties in the logic, like reachability<\/jats:p><jats:p>analysis of hybrid-state Markov decision processes. Solving for SSMT for-<\/jats:p><jats:p>mulae with quantification over finite and thus discrete domain has been ad-<\/jats:p><jats:p>dressed by Tino Teige et al. In our work, we extend their work to SSMT<\/jats:p><jats:p>over continuous quantifier domains (CSSMT) in order to enable capture of,<\/jats:p><jats:p>e.g., continuous disturbances and uncertainty in hybrid systems. We extend<\/jats:p><jats:p>the semantics of SSMT and introduce a corresponding solving procedure. A<\/jats:p><jats:p>discussion regarding to reachability analysis is given to demonstrate applica-<\/jats:p><jats:p>bility of our framework to reachability problems in hybrid systems.<\/jats:p>","DOI":"10.29007\/wm3j","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:03:02Z","timestamp":1516748582000},"page":"2--8","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain"],"prefix":"10.29007","volume":"37","author":[{"given":"Yang","family":"Gao","sequence":"first","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Symbolic and Numerical Methods for Reachability Analysis, 1st International Workshop, SNR 2015"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:04:05Z","timestamp":1516748645000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/TWf"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/wm3j","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}