随机系统的决定性及其在混合模型中的应用
Decisiveness of Stochastic Systems and its Application to Hybrid Models
摘要：
在[ABM 07]中，Abdulla等人引入了决定性的概念，这是一个有趣的工具，可以将有限马尔可夫链的良好性质提升到可数性质。后来，这个概念被扩展到更一般的随机转移系统（STS），允许设计各种验证算法的大类（无限）STS。我们通过两种方式进一步提高对决策的理解和利用。首先，我们提供了一个一般的标准证明一般STS的决定性。这个标准，这是非常自然的，但其证明是相当技术，（严格）概括了所有已知的标准，从文献。其次，我们专注于随机混合系统（SHS），混合系统的随机扩展。我们建立了一个大类的SHS的决定性，并根据一些经典的假设，从数理逻辑，我们展示了如何决定可达性问题，在这个类中，即使他们是不可判定的一般SHS。这提供了一个可判定的O-最小混合系统的随机扩展。[ABM07] Parosh A. Abdulla，Noomene Ben Henda，and Richard Mayr. 2007.决定性的马尔可夫链。Log.方法计算Sci. 3、4（2007年）。
英文摘要：
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
