A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain
A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain
复制标题
连续域随机可满足性模理论的求解过程
DOI：
10.1007/978-3-319-22264-6_19
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
M. Fränzle
中科院分区：
文献类型：
--
作者：
M. Fränzle
随机可满足性模理论（Stochastic Satisfiability Modulo Theories，SSMT）[1]是受随机逻辑启发的经典可满足性模理论（Satisfiability Modulo Theories，SMT）的定量扩展。它扩展了SMT通常以及随机量词，便于捕获的随机博弈性质的逻辑，如可达性分析的混合状态马尔可夫决策过程。Tino Teige等人[2]已经解决了在有限域和离散域上量化SSMT公式的求解问题。在本文中，我们将他们的工作扩展到连续量词域（CSSMT）的SSMT，以便能够捕获混合系统中的连续干扰和不确定性。我们扩展了SSMT的语义，并介绍了相应的解决方案。一个简单的案例研究进行证明我们的框架的可达性问题的混合动力系统的适用性。
Stochastic Satisfiability Modulo Theories (SSMT) [1] 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. [2]. In this paper, we extend their work to SSMT over continuous quantifier domains (CSSMT) in order to enable capture of continuous disturbances and uncertainty in hybrid systems. We extend the semantics of SSMT and introduce a corresponding solving procedure. A simple case study is pursued to demonstrate applicability of our framework to reachability problems in hybrid systems.
登录
查看更多内容
影响因子：
3.9
作者：
M. Fränzle;H. Hermanns;Tino Teige
通讯作者：
M. Fränzle;H. Hermanns;Tino Teige
影响因子：
2.9
作者：
Tino Teige;M. Fränzle
通讯作者：
M. Fränzle
一种计算区间约束关系的内部近似的算法
DOI：
--
发表时间：
1999
期刊：
Ershov Memorial Conference
影响因子：
--
作者：
F. Benhamou;F. Goualard;Éric Languénou;M. Christie
通讯作者：
M. Christie
DOI：
--
发表时间：
2002
期刊：
Symposium on Abstraction, Reformulation and Approximation
影响因子：
--
作者：
Xuan;Djamila Sam;M. Silaghi
通讯作者：
M. Silaghi