# On Verifying Timed Hyperproperties

## TL;DR

This paper investigates the satisfiability and model-checking problems for HyperMTL, a timed logic for hyperproperties, revealing decidability results and limitations depending on semantics and restrictions.

## Contribution

It introduces HyperMTL with asynchronous and synchronous semantics, analyzing decidability of satisfiability and model-checking, and identifies conditions for decidability in timed hyperproperties.

## Key findings

- Satisfiability for HyperMTL is decidable similar to HyperLTL.
- Model checking is undecidable for most cases unless the specification is alternation-free.
- Decidability can be achieved under certain conditions with quantifier alternations in synchronous semantics or bounded time domain.

## Abstract

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: asynchronous and synchronous. While the satisfiability problem can be decided similarly to HyperLTL regardless of the choice of semantics, we show that the model-checking problem, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.