A Hierarchy of Scheduler Classes for Stochastic Automata

TL;DR

This paper explores a hierarchy of scheduler classes in stochastic automata, analyzing their power and limitations in probabilistic reachability, and introduces an approximate verification technique balancing efficiency and accuracy.

Contribution

It establishes a hierarchy of scheduler classes for stochastic automata and proposes a sampling-based approximation method for verification.

Findings

Most scheduler classes are distinguishable in stochastic automata.

A hierarchy of scheduler classes is proven with respect to unbounded probabilistic reachability.

Lightweight scheduler sampling offers an effective approximation technique.

Abstract

Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata.