A well-defined semantics in terms of some mathematically well-understood object is a cornerstone of formal models.
For quantitative models, we use automata-based formalisms—that represent the evolution of a system from state to state via (randomised) transitions—building on labelled transition systems (LTS, or Kripke structures) and discrete- and continuous-time Markov chains (DTMC and CTMC, respectively) [1]}.
By combining these basic mathematical formalisms in various ways, and extending them with features such as real-time clocks and continuous variables evolving according to differential equations, we obtain further formalisms as depicted in fig:ModelFamilyTree.
Since writing real-life models as, say, large Markov chains would be cumbersome, we specify them using a higher-level modelling language that offers at least discrete variables with standard arithmetic and Boolean operators plus a notion of parallel composition for the natural specification of distributed and component- or actor-based systems.
