Conformance Relations and Hyperproperties for Doping Detection in Time and Space

We present a novel and generalised notion of doping cleanness forcyber-physical systems that allows for perturbing the inputs and observing theperturbed outputs both in the time- and value-domains. We instantiate ourdefinition using existing notions of conformance for cyber-physical systems. Asa formal basis for monitoring conformance-based cleanness, we develop thetemporal logic HyperSTL*, an extension of Signal Temporal Logics with tracequantifiers and a freeze operator. We show that our generalised definitions areessential in a data-driven method for doping detection and apply ourdefinitions to a case study concerning diesel emission tests