Monitoring Signal Temporal Logic in Distributed Cyber-physical Systems

This paper solves the problem of runtime verification for signal temporal logic in distributed cyber-physical systems (CPS). We assume a partially synchronous setting, where a clock synchronization algorithm guarantees a bound on clock drifts among all signals. We introduce a formula progression and a signal retiming technique that allow reasoning about the correctness of formulas among continuous-time and continuous-valued signals that do not share a global view of time. The resulting problem is encoded as a satisfiability modulo theory (SMT) solving problem, and we introduce techniques to solve the SMT encoding efficiently. We also conduct two case studies on monitoring a network of aerial vehicles and a water distribution system.