Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100190, Peoples R China. Univ Chinese Acad Sci, Beijing 100049, Peoples R China. Ecole Polytech, F-91120 Palaiseau, France.
Abstract:
The notion of amortisation has been integrated in quantitative bisimulations to make long-term behavioral comparisons between nondeterministic systems. In this paper, we present sound and complete proof systems for amortised strong probabilistic bisimulation and its observational congruence on a process algebra with probability and nondeterminism, and prove their soundness and completeness. Our results make it possible to reason about long-term (observable) probabilistic behaviors by syntactic manipulations.
English Abstract:
The notion of amortisation has been integrated in quantitative bisimulations to make long-term behavioral comparisons between nondeterministic systems. In this paper, we present sound and complete proof systems for amortised strong probabilistic bisimulation and its observational congruence on a process algebra with probability and nondeterminism, and prove their soundness and completeness. Our results make it possible to reason about long-term (observable) probabilistic behaviors by syntactic manipulations.
Xu, LL,Lin, HM. Complete Proof Systems for Amortised Probabilistic Bisimulations[J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY,2016-01-01,31(2):300-316.
