In the quantitative automata zoo

Arnd Hartmanns, Holger Hermanns

Research output: Contribution to journalArticleAcademicpeer-review

11 Citations (Scopus)
14 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)3-23
JournalScience of computer programming
Issue numberPart 1
Publication statusPublished - Nov 2015
Externally publishedYes


  • n/a OA procedure


Dive into the research topics of 'In the quantitative automata zoo'. Together they form a unique fingerprint.

Cite this