  We propose a hybrid probabilistic process calculus for modelling and
reasoning on cyber-physical systems (CPSs). The dynamics of the calculus is
expressed in terms of a probabilistic labelled transition system in the SOS
style of Plotkin. This is used to define a bisimulation-based probabilistic
behavioural semantics which supports compositional reasonings. For a more
careful comparison between CPSs, we provide two compositional probabilistic
metrics to formalise the notion of behavioural distance between systems, also
in the case of bounded computations. Finally, we provide a non-trivial case
study, taken from an engineering application, and use it to illustrate our
definitions and our compositional behavioural theory for CPSs.

Logic in Computer Science;Formal Languages and Automata Theory;Systems and Control;Systems and Control