@article {223, title = {Abstract Probabilistic Automata}, journal = {Information and Computation}, volume = {232}, year = {2013}, pages = {66 - 116}, abstract = {Abstract Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In \{APAs\} uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behavior is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.}, keywords = {Probabilistic Automata}, issn = {0890-5401}, doi = {http://dx.doi.org/10.1016/j.ic.2013.10.002}, url = {http://www.sciencedirect.com/science/article/pii/S0890540113001132}, author = {Benoit Delahaye and Joost-Pieter Katoen and Kim G. Larsen and Axel Legay and Mikkel L. Pedersen and Falak Sher and Andrzej Wasowski} }