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 correct- ness 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 dynam- ics 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 vehi- cles, 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.1