Approximating Markov Processes by Averaging

被引:17
作者
Chaput, Philippe [1 ]
Danos, Vincent [2 ]
Panangaden, Prakash [1 ]
Plotkin, Gordon [2 ]
机构
[1] McGill Univ, Montreal, PQ H3A 0G4, Canada
[2] Univ Edinburgh, Edinburgh EH8 9YL, Midlothian, Scotland
基金
加拿大自然科学与工程研究理事会;
关键词
Theory; Verification; Markov processes; Markov operators; approximation; bisimulation; duality; modal logic; TRANSITION-SYSTEMS; BISIMULATION; METRICS;
D O I
10.1145/2537948
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Normally, one thinks of probabilistic transition systems as taking an initial probability distribution over the state space into a new probability distribution representing the system after a transition. We, however, take a dual view of Markov processes as transformers of bounded measurable functions. This is very much in the same spirit as a "predicate-transformer" view, which is dual to the state-transformer view of transition systems. We redevelop the theory of labelled Markov processes from this viewpoint; in particular, we explore approximation theory. We obtain three main results. (i) It is possible to define bisimulation on general measure spaces and show that it is an equivalence relation. The logical characterization of bisimulation can be done straightforwardly and generally. (ii) A new and flexible approach to approximation based on averaging can be given. This vastly generalizes and streamlines the idea of using conditional expectations to compute approximations. (iii) We show that there is a minimal process bisimulation-equivalent to a given process, and this minimal process is obtained as the limit of the finite approximants.
引用
收藏
页数:45
相关论文
共 53 条
[1]  
[Anonymous], 2005, PROF UAI 2005
[2]  
[Anonymous], 1989, REAL ANAL PROBABILIT
[3]  
[Anonymous], 1966, Introduction to Measure and Probability
[4]  
[Anonymous], 1974, GRADUATE TEXTS MATH
[5]  
Arendt W., 1986, Lecture Notes in Math., V1184
[6]  
Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[7]   A hierarchy of probabilistic system types [J].
Bartels, F ;
Sokolova, A ;
de Vink, E .
THEORETICAL COMPUTER SCIENCE, 2004, 327 (1-2) :3-22
[8]  
Billingsley Patrick, 1995, Probability and Measure
[9]  
BLUTE R, 1997, P 12 IEEE S LOG COMP
[10]   An approximation algorithm for labelled Markov processes:: towards realistic approximation [J].
Bouchard-Côté, A ;
Ferns, N ;
Panangaden, P ;
Precup, D .
SECOND INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, PROCEEDINGS, 2005, :54-61