Performance modeling and quantitative evaluation for cyber-physical systems based on LTS

Cyber-physical systems (CPS) are complex systems that can be understood as a hybrid system, a real-time system with probabilistic behavior, and a concurrent system. With the increasing use of CPS, there is a growing demand for higher reliability and performance. Additionally, the large amount of information in CPS requires processing, exacerbating the state space explosion problem caused by model checking methods used for the quantitative evaluation of CPS. Therefore, evaluating the functionality, performance, and reliability of CPS is not only an important research topic but also an inevitable challenge. This paper aims to establish a comprehensive and efficient CPS performance model and a quantitative evaluation method and proposes solutions to existing problems based on the specific practical application environment of the system. First, we extend the labeled transition system (LTS) and propose a hybrid probability time cost transition system (HPTCTS) that provides a detailed description of the continuous behavior, probabilistic behavior, time characteristics, and performance of CPS. Furthermore, we propose HPTCTS temporal logic (HPTCTS-TL) to describe the performance characteristic of HPTCTS. To alleviate the state space explosion problem when quantitatively evaluating the HPTCTS model, we propose the corresponding quantitative evaluation algorithm based on symbolic model checking. Finally, we discuss a typical example of CPS to demonstrate the feasibility of our approach. Overall, our work contributes to a better understanding of CPS and provides a more effective and comprehensive way to evaluate CPS performance, which is crucial for the successful development and deployment of CPS in real-world applications.