On metrics for probabilistic systems: definitions and algorithms


Chen, Taolue and Han, Tingting and Lu, Jian (2009) On metrics for probabilistic systems: definitions and algorithms. Computers & Mathematics with Applications, 57 (6). pp. 991-999. ISSN 0898-1221

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract: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 . 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.
Item Type:Article
Copyright:© 2009 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/80128
Official URL:https://doi.org/10.1016/j.camwa.2008.10.041
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page