Analysis of Markov models is of high importance for formal verification. Until now, analysis of Markov Automata required them to be fully specified, which is a considerable restriction as rates may be unknown or influenced by uncertainty of the environment. We introduce parametric Markov Automata (pMA) to capture this uncertainty with parametric transition functions. In this talk, we introduce and motivate the need of pMAs, as well as cover an approach to compute time-bounded reachability probabilities up to arbitrary precision.
