Decision-Theoretic Monitoring of Cyber-Physical Systems

Cyber-physical systems (CPS) represent "engineered systems that are built from, and depend upon, the seamless integration of computational algorithms and physical components". They can be found in such areas as aerospace, manufacturing, transportation, entertainment, healthcare, and automotive. For some of these systems the top priority is correct functioning; incorrect operation of systems like autonomous vehicles, medical devices or aircraft may lead to catastrophic consequences. But formally proving system correctness is a challenging problem. In recent years, runtime monitoring, where a monitor observes the outputs of the system and determines whether a system specification has been violated, has emerged as an attractive alternative. In this thesis, we focus on the decision-theoretic approach to monitoring of safety properties in CPS. In particular, we formulate the monitoring problem as a Partially Observable Markov Decision Process (POMDP) whereby deciding whether a run is safe corresponds to executing the optimal policy of the monitoring POMDP. We show how Monte-Carlo planning algorithm (POMCP) can be used to compute the optimal policy of the monitoring POMDP. The monitoring POMDP reward structure is naturally described with four parameters and an important question is how it affects the monitoring performance, quantified through acceptance accuracy, rejection accuracy and monitoring time. We analyze the performance of the POMDP-based monitors for special choices of the reward structure and compare them with the performance of the traditional threshold-based monitors. Our results show that using POMDPs we can sometimes simultaneously improve both accuracies of the monitor while decreasing the monitoring time. Further, we study POMDP-based monitors for systems with terminal strongly connected components. For this class of systems, we derive the expressions for the POMDP value function. The expressions allow us to demonstrate how the POMDP-policy can take advantage of the properties of the monitored system and thus provide an enhanced monitoring performance. In order to study decision-theoretic monitors and experiment with them, we have developed a software called Decision-Theoretic Monitoring Tool (DTMT). This tool implements the architecture that allows easy integration of new monitoring decision rules and experimentation with an arbitrary user-defined system and property models. Finally, we evaluate POMDP monitors on an experimental robotic system. We simulate the operation of a simplified transmission system on a mobile robot that was developed specifically for this purpose. The experiments confirm that POMDP-based monitors provide an improvement over traditional threshold-based approaches. Further, we show that POMDP-based monitors implemented through POMCP can be used online even for large problems and thus provide an attractive and flexible alternative to traditional threshold-based monitors.