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 am...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.展开更多
基金This work was supported by the National Natural Science Foundation of China under Grant No. 60833001.
文摘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.
