Semantic Inference for Cyber-Physical Systems with Signal Temporal Logic

Formal specification plays crucial roles in the rigorous verification and design of cyber-physical systems (CPS). The challenge of getting high-quality formal specifications is well documented. This challenge is further exacerbated in CPS with artificial-intelligence- or machine-learning-based components. This paper presents a problem called ‘semantic inference’, the goal of which is to automatically translate the behavior of a CPS to a formal specification written in signal temporal logic (STL). To reduce the potential combinatorial explosion inherent to the problem, this paper adopts a search strategy called agenda-based computation, which is inspired by natural language processing. Based on such a strategy, the semantic inference problem can be formulated as a Markov decision process (MDP) and then solved using reinforcement learning (RL). The obtained formal specification can be viewed as an interpretable classifier, which, on the one hand, can classify desirable and undesirable behaviors, and, on the other hand, is expressed in a human-understandable form. The performance of the proposed method is demonstrated with a case study.