Abstract Probabilistic Automata

TitleAbstract Probabilistic Automata
Publication TypeJournal Article
Year of Publication2013
AuthorsDelahaye, B, Katoen, J-P, Larsen, KG, Legay, A, Pedersen, ML, Sher, F, Wasowski, A
JournalInformation and Computation
Pagination66 - 116
KeywordsProbabilistic Automata
AbstractAbstract 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.
Work Package: