Models for Discrete Nondeterministic Stochastic Systems

Roberto Segala (roberto.segala@univr.it)
Universitˆ di Verona
Strada Le Grazie 15, caÕ Vignal 2
37134 Verona ITALY

Abstract

We describe the model of Probabilistic Automata for the description of systems that exhibit nondeterministic behavior and discrete stochastic behavior, and we compare it with other existing models of concurrent stochastic systems like Markov Decision Processes, Reactive Systems, and Labeled Concurrent Markov Chains. We extend to Probabilistic Automata concepts that are typical of nondeterministic systems like simulation and bisimulation based semantics and trace semantics. In doing so we analyze the differences between the models that are proposed in the literature. In particular we concentrate on the comparison between Labeled Concurrent Markov Chains, also called the alternating model, and Probabilistic Automata, also called the non-alternating model.