Axiomatizations for probabilistic finite-state behaviors

            Yuxin Deng and Catuscia Palamidessi


 We study a process calculus which combines both
 nondeterministic and probabilistic behavior in the style of Segala
 and Lynch's probabilistic automata. We consider various strong and
 weak behavioral equivalences, and we provide complete axiomatizations
 for finite-state processes, restricted to guarded definitions in case
 of the weak equivalences. We conjecture that in the general case of
 unguarded recursion the ``natural'' weak equivalences are undecidable. 

 This is the first work, to our knowledge, that provides a complete
 axiomatization for  weak equivalences in the presence of recursion and
 both nondeterministic and probabilistic choice.