Online monitoring of distributed systems with a five-valued LTL

In this paper, we deal with two kinds of uncertainties in distributed systems. On one hand, the order of causally unrelated executions is not determined when a global clock is not available. On the other hand, in a finite amount of time, the behaviour can be observed only up to a certain moment, and the future behaviour is unknown. 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 kinds of uncertainties. 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.