Computers and Mathematics with Applications on Metrics for Probabilistic Systems: Definitions and Algorithms
Computers and Mathematics with Applications on Metrics for Probabilistic Systems: Definitions and Algorithms
复制标题
DOI：
--
复制
发表时间：
--
期刊：
影响因子：
--
通讯作者：
Taolue Chen;Tingting Han;Jian Lu
中科院分区：
文献类型：
--
作者：
Taolue Chen;Tingting Han;Jian Lu
在本文中，我们考虑概率系统的行为伪度量，从距离零捕获概率双相似性的意义上说，它是概率双相似性的定量模拟。我们感兴趣的模型是概率自动机，它基于状态转移系统，并明确区分概率和非确定性选择。伪度量定义为完备状态度量格上单调泛函的最大不动点。这种伪度量的一个显著特点在于它不贴现未来，这解决了计算模型中两个状态之间距离的一些算法挑战。我们通过提供一个近似算法来解决这个问题：直到任何所需的精度ε，距离可以近似为ε内的时间指数模型的大小和对数1 ε。我们的算法的关键成分之一是表示一个伪度量是一个后定点作为基本的句子在真实的封闭的领域，这使我们能够利用塔斯基的决策过程，连同二分搜索近似的行为距离。
In this paper, we consider the behavioral pseudometrics for probabilistic systems, which are a quantitative analogue of probabilistic bisimilarity in the sense that the distance zero captures the probabilistic bisimilarity. The model we are interested in is probabilistic automata, which are based on state transition systems and make a clear distinction between probabilistic and nondeterministic choices. The pseudometrics are defined as the greatest fixpoint of a monotonic functional on the complete lattice of state metrics. A distinguished characteristic of this pseudometric lies in that it does not discount the future, which addresses some algorithmic challenges to compute the distance of two states in the model. We solve this problem by providing an approximation algorithm: up to any desired degree of accuracy ε, the distance can be approximated to within ε in time exponential in the size of the model and logarithmic in 1 ε. One of the key ingredients of our algorithm is to express a pseudometric being a post-fixpoint as the elementary sentence over real closed fields, which allows us to exploit Tarski's decision procedure, together with the binary search to approximate the behavioral distance.