A Probabilistic Calculus of Cyber-Physical Systems

TL;DR

This paper introduces a probabilistic process calculus tailored for modeling and analyzing cyber-physical systems, enabling compositional reasoning and behavioral distance measurement.

Contribution

It presents a novel hybrid probabilistic calculus with bisimulation semantics and metrics for CPSs, supported by a practical engineering case study.

Findings

Defined a probabilistic labelled transition system for CPSs

Developed bisimulation-based behavioral semantics for compositional reasoning

Introduced probabilistic metrics for behavioral distance in CPSs

Abstract

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.