Mixed Nondeterministic-Probabilistic Interfaces

Interface theories are powerful frameworks supporting incremental and compositional design of systems through refinements and constructs for conjunction, and parallel composition. In this report we present a first Interface Theor – |Modal Mixed Interfaces – for systems exhibiting both non-determinism and randomness in their behaviour. The associated component model – Mixed Markov Decision Processes – is also novel and subsumes both ordinary Markov Decision Processes and Probabilistic Automata.