Compositional Verification and Optimization of Interactive Markov Chains

TL;DR

This paper introduces a framework and algorithms for the compositional verification and optimization of Interactive Markov Chains (IMC), focusing on time-bounded properties and environment assumptions.

Contribution

It provides a new specification formalism for IMC and a synthesis method for schedulers that optimize property satisfaction probabilities under environment assumptions.

Findings

Framework for compositional verification of IMC

Algorithms for scheduler synthesis optimizing time-bounded properties

Formalism enabling modular analysis of IMC components

Abstract

Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms for compositional verification and optimization of IMC with respect to time-bounded properties. Firstly, we give a specification formalism for IMC. Secondly, given a time-bounded property, an IMC component and the assumption that its unknown environment satisfies a given specification, we synthesize a scheduler for the component optimizing the probability that the property is satisfied in any such environment.