Formal verification of hyperproperties for control systems
Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, Majid Zamani · 2021
In recent years, there has been a great deal of interest and research in verifying complex cyber-physical systems (CPS) against rich and expressive specifications [2] such as safety and liveness, to provide formal guarantees for safety-critical systems. While linear temporal logic (LTL) [1] can capture these properties of interest, it is incapable of specifying many information-flow properties that rely on information of multiple traces. These properties, which are described over sets of traces, are called hyperproperties [4] and their corresponding temporal logics have been well studied. The extension of LTL to capture a fragment of hyperproperties, namely, HyperLTL [3], makes use of trace variables to specify individual execution traces and allows for quantification of trace variables to precede a (trace) quantifier-free formula. Here, we present a sound approach for verifying discrete-time control systems against HyperLTL formulae through the use of so-called augmented barrier certificates (ABCs).