A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL

HeyVL is a recently introduced intermediate verification language for prototyping and automating proof rules for reasoning about quantitative properties of probabilistic programs, such as expected runtimes, failure probabilities, or space usage. While HeyVL and its accompanying verification infrastructure caesar have successfully been applied to automate a variety of verification techniques from the probabilistic program verification literature, the original language lacked a formal “ground truth” in terms of a small-step operational semantics that enables an intuitive reading of HeyVL programs. In this paper, we define an operational semantics for a cleaned-up version of HeyVL in terms of refereed stochastic games, a novel extension of simple stochastic games in which a referee may perform quantitative reasoning about the expected outcome of sub-games and give one player an advantage if those sub-game are outside of certain boundaries. Apart from improving the intuition and ergonomics of the HeyVL language, our operational semantics may also pave the way for the development of alternative verification engines that leverage, for example, existing probabilistic model checking tools.