Compositional reasoning for probabilistic finite-state behaviors

Abstract. 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.