2017/07/07 by Ruggero Lanotte, Lanotte, Ruggero, Massimo Merro +3
Computer Science · Engineering · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Systems and Control (eess.SY) #cs.FL #cs.LO #cs.SY #eess.SY #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1707.02279
arXiv admin note: text overlap with arXiv:1612.00484
arxiv created 2020/04/27 · arxiv updated 2021/05/25
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.