System monitoring with a five-valued LTL

In runtime verification, an appropriate monitoring result can only be achieved according to a complete and accurate observation. Unfortunately, such an observation is not always available in practice. On one hand, in a finite amount of time, an observation is incomplete up to a certain moment, and the future execution is unknown. On the other hand, an observation is possibly inaccurate due to lack of detailed design information of the system under monitoring. In this paper, we investigate a monitoring approach based on linear temporal logic (LTL) specifications. We propose a five-valued semantics for LTL to deal with both dimensions of uncertainty. We develop an efficient runtime verification algorithm using formula rewriting, and show the feasibility of our approach with a case study in the railway domain.