In the quantitative automata zoo

• We survey compositional automata models for quantitative verification.
• The models allow probabilistic decisions, real-time phenomena and continuous dynamics.
• We give an intuitive definition and a small illustrative example for each model.
• We systematically classify the models and summarise available formal analysis techniques.

Quantitative model checking and performance evaluation deal with the analysis of complex systems that must not only satisfy correctness requirements, but also meet performance and reliability goals. Models of such systems therefore need to represent the necessary quantitative information about probabilistic decisions, real-time phenomena, or continuous dynamics. At the same time, nondeterminism needs to be properly captured as in classical verification, so as to enable abstraction and compositional modelling. These aspects span a large spectrum of automata-based quantitative models which have been studied in the verification and performance evaluation literature. In this paper, we embark on a guided tour through this zoo of quantitative models. Starting from the basic formalisms of labelled transition systems and also Markov chains, we look at how timed and hybrid automata add real-time aspects as well as continuous dynamics, and we study extensions that provide for behaviour governed by discrete and continuous probability distributions. For each of the automata models, we outline its definition, provide a small illustrative example, summarise its expressive power, and survey available formal analysis techniques as well as selected practical applications.