Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory

Industrial fault diagnosis exhibits the perennial problem of reasoning with partial and real-valued information. This is mainly due to the fact that in real-world applications, industrial systems are only instrumented insofar, as sensor information is required for their functioning. However, such instrumentation leaves out much information that would be useful for fault diagnosis. This is problematic since consistency-based fault diagnosis uses available information and computes intermediate values within a system description. These values are then used to compare expected normal behaviour to actual observed values. In the past, this was done only for Boolean circuits. Recently, satisfiability modulo non-linear arithmetic (SMT) formulations have been developed that allow the calculation of real values, instead of only Boolean ones. Leveraging those formulations, we in this article present a novel method to infer missing sensor values using an SMT system description and the notion of critical pairs. We show on a running example and also empirically that we can infer novel measurements for five process industrial systems. We conclude that, although SMT calculations accumulate some error, we can infer novel optimal measurements for all systems.