论文标题
随机系统的果断性及其在混合模型中的应用（完整版）
Decisiveness of Stochastic Systems and its Application to Hybrid Models (Full Version)
论文作者
论文摘要
在[ABM07]中，Abdulla等。介绍了果断性的概念，这是一种有趣的工具，可以将有限的马尔可夫链的良好特性提升为不可忽视的链。后来，该概念扩展到了更通用的随机过渡系统（STS），从而设计了大量（无限）STS的各种验证算法。我们通过两种方式进一步提高了决定性的理解和效用。首先，我们提供了证明一般STS的果断性的一般标准。该标准非常自然，但其证明是技术性的，（严格地）从文献中概括了所有已知标准。其次，我们专注于随机混合系统（SHSS），这是混合系统的随机扩展。我们建立了一大批SHS的决定性，在数学逻辑中的一些经典假设下，我们展示了如何在此类中解决该类别的可及性问题，即使它们对于一般SHS是不可决定的。这提供了O-Wimimal杂种系统的可确定随机扩展。 [ABM07] Parosh A. Abdulla，Noomene Ben Henda和Richard Mayr。 2007年。决定性马尔可夫连锁店。日志。方法计算。科学。 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).
