On Verifying Timed Hyperproperties

Hsi-Ming Ho, Ruoyu Zhou, Timothy M. Jones

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of event…