Compositional Reasoning for Probabilistic Finite-State Behaviors
 
       Yuxin Deng, Catuscia Palamidessi, and Jun Pang
       
 We study a process algebra which combines both nondeterministic and
 probabilistic behavior in the style of Segala and Lynch's simple
 probabilistic automata. We consider strong bisimulation and observational
 equivalence, and provide complete axiomatizations for a language that
 includes a restricted form of parallel composition and (guarded) recursion.
 The presence of the parallel composition, in particular, introduces
 various technical difficulties, but we believe that a ``good''
 compositional semantics should take it into account since it is an
 essential operator to specify concurrent systems.