Background
Model checking verifies whether a system exhibits a given behaviour or property, but classic algorithms need full knowledge of the system under analysis.
Machine learning model checking recasts the problem as learning: a predictor is trained in a continuous latent space that captures the semantics of formulae. A kernel for Signal Temporal Logic (STL) extracts features of specifications automatically through the kernel trick. A new formula can then be verified without access to a (generative) model of the system, using only a set of formulae and their satisfaction values.
The question
This suggests a potentially privacy-preserving method: specifications of a system could be queried without giving access to the system itself. The paper investigates whether this promise actually holds.