Mixed Nondeterministic-Probabilistic Interfaces

TL;DR

This paper introduces Modal Mixed Interfaces, a new interface theory for systems with both nondeterminism and probabilistic behavior, along with a novel component model called Mixed Markov Decision Processes.

Contribution

It presents the first interface theory for mixed nondeterministic-probabilistic systems and introduces a new component model that generalizes existing models.

Findings

Defines Modal Mixed Interfaces for combined nondeterministic and probabilistic systems

Introduces Mixed Markov Decision Processes as a unifying component model

Subsumes both Markov Decision Processes and Probabilistic Automata

Abstract

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.