A probabilistic calculus of cyber-physical systems

(CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow physical processes to affect computations and vice versa. Although CPSs can be found in several real-world domains, their verification often relies on rather than .We propose a for modelling and reasoning on CPSs. The dynamics of the calculus is expressed in terms of a in the SOS style of Plotkin. This is used to define a probabilistic behavioural semantics which supports compositional reasonings. For a more careful comparison between CPSs, we provide two compositional 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.