Formal interpretation of cyber-physical system performance with temporal logic

The inherent and increasing complexity of many cyber-physical systems (CPSs) makes it challenging for human users or designers to comprehend and interpret their performance. This issue, without proper attention paid, may lead to unwanted and even catastrophic consequences, particularly with safety-critical CPSs. This paper presents a new methodology of enabling (i) a human to interrogate a CPS by inquiring with questions written in formal logic and (ii) the CPS to interpret its performance precisely in the context of the inquiry. This formal interpretation problem is first formulated as temporal logic inference problem, which, aided by the concept of robustness degree, can be converted into an optimisation problem with probably approximately correct solutions. A new Gaussian-process-based active learning algorithm is then proposed to address the potential computational budget issue arising from solving the optimisation problem. Both theoretical and empirical analyses are carried out to demonstrate the performance of the proposed algorithm. Finally, a detailed case study on automotive mechatronic design is provided to showcase the proposed formal interpretation methodology.