Predicate monitoring in distributed cyber-physical systems

This paper solves the problem of detecting violations of predicates over distributed continuous-time and continuous-valued signals in cyber-physical systems (CPS). CPS often operate in a safety-critical context, where their correctness is crucially important. Large CPS that consist of many autonomous and communicating components distributed across a geographical area must maintain global correctness and safety. We assume a partially synchronous setting, where a clock synchronization algorithm guarantees a bound on clock drifts among all signals. We introduce a novel retiming method that allows reasoning about the correctness of predicates among continuous-time signals that do not share a global view of time. The resulting problem is encoded as an SMT problem and we introduce techniques to solve the SMT encoding efficiently. Leveraging simple knowledge of physical dynamics allows further runtime reductions. We fully implement our approach on three distributed CPS applications: monitoring of a network of autonomous ground vehicles, a network of aerial vehicles, and a water distribution system. The results show that in some cases it is even possible to monitor a distributed CPS sufficiently fast for online deployment on fleets of autonomous vehicles.