Distributed Probabilistic-Control Hybrid Automata (DPCHA) are a model for systems having discrete dynamics (such as computation and control), continuous dynamics (such as real-world physics), a changing number of participants, some of which may exhibit probabilistic behaviour.

Quantified Bounded Linear Temporal Logic (QBLTL) is a logic that we use for specifying properties of DPCHA, including support for (bounded) temporal operators and quantification and aggregation over the elements of the distributed system.

Statistical Model Checking (SMC) is an efficient (but unsound) verification technique that allows us to arbitrarily estimate the probability that a certain property of the system holds in a probabilistic system. We can use it to check important safety or efficiency conditions of a system modelled with DPCHA.