The metric analogue of weak bisimulation for probabilistic processes
Proceedings - Symposium on Logic in Computer Science - Trang 413-422
Tóm tắt
We observe that equivalence is not a robust concept in the presence of numerical information - such as probabilities-in the model. We develop a metric analogue of weak bisimulation in the spirit of our earlier work on metric analogues for strong bisimulation. We give a fixed point characterization of the metric. This makes available conductive reasoning principles and allows us to prove metric analogues of the usual algebraic laws for process combinators. We also show that quantitative properties of interest are continuous with respect to the metric, which says that if two processes are close in the metric then observable quantitative properties of interest are indeed close. As an important example of this we show that nearby processes have nearby channel capacities - a quantitative measure of their propensity to leak information.
Từ khóa
#Computer science #Probability distribution #Robustness #Channel capacity #Concurrent computing #Distributed computing #Stochastic systems #State-space methods #Logic #Boolean functionsTài liệu tham khảo
10.1016/0890-5401(91)90030-6
10.1016/0022-0000(81)90036-2
10.1016/0022-0000(85)90012-1
10.1109/LICS.1995.523277
10.1007/BFb0039071
10.1016/S0019-9958(86)80001-8
10.1512/iumj.1981.30.30055
10.1109/REAL.1990.128759
hansson, 1994, Time and probability in formal design of distributed systems, Real-Time Safety Critical Systems, 1
philippou, 2000, Weal bisimulation for probabilistic processes, Lecture Notes in Computer Science, 1877, 334, 10.1007/3-540-44618-4_25
lincoln, 1998, A probabilistic poly-time framework for protocol analysis, ACM Computer and Communication Security (CCS-5)
segala, 1995, Modeling and Verification of Randomized Distributed Real-Time Systems
10.1109/LICS.1992.185529
ulidowski, 1994, Local Testing and Implementable Concurrent Processes
van breugel, 2001, An algorithm for quantitative verification of probabilistic systems, Lecture Notes in Computer Science, 2154, 336, 10.1007/3-540-44685-0_23
van breugel, 2001, Towards quantitative verification of probabilistic systems, Proceedings of the Twenty-eighth International Colloquium on Automata Languages and Programming
10.1016/S0304-3975(97)00056-X
bandini, 2001, Axiomatizations for probabilistic bisimulation, Lecture Notes in Computer Science, 2076, 370, 10.1007/3-540-48224-5_31
10.1006/inco.1995.1135
gupta, 1997, Robust timed automata, Lecture Notes in Coputer Science, 1201, 331, 10.1007/BFb0014736
anderson, 1987, Linear programming in infinite-dimensional spaces, Discrete Mathematics in Computer Science
desharnais, 1999, Metrics for labeled Markov processes, Proc Lecture Notes in Computer Science, 10.1007/3-540-48320-9_19
10.1109/LICS.1998.705681
10.1002/0471200611
cleaveland, 1992, Testing preorders for probabilistic processes, Lecture Notes in Computer Science, 623, 708, 10.1007/3-540-55719-9_116
10.1007/978-1-4757-2958-0
10.1109/LICS.2000.855759