Nondeterminism in Interactive Markov Chains, with Application to the Erlangen Mainframe

Hubert Garavel and Holger Hermanns

Principles of Formal Quantitative Analysis - Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday, volume 15760 of Lecture Notes in Computer Science, pages 15-69. Springer, August 2025

Abstract:

To formally describe and numerically analyse the performance of systems consisting of concurrent stochastic processes, there exist two orthogonal approaches: "compound" models, each transition of which carries both an event (as in process algebra) and a rate (as in exponential distributions), and Interactive Markov Chains, each transition of which carries either an event or a rate. We investigate the subtle differences between both approaches, with a particular focus on the presence of nondeterminism in Interactive Markov Chains, and the ways nondeterminism can be either handled (resulting in Markov automata) or eliminated (resulting in Continuous-Time Markov Chains). We apply these ideas to the Erlangen mainframe, a challenging problem that exhibits the limitations of classical queueing theory by featuring multiple processors, job queues of different priorities, parallel composition with multiway synchronisation between two or more concurrent processes, and aperiodic failure/repair events.

55 pages

PDF

PostScript