# MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the $\exists^*\forall^*$ Fragment

## TL;DR

MGHyper is a new tool that extends satisfiability checking for HyperLTL hyperproperties beyond the decidable fragment, enabling automatic verification, equivalence checking, and counterexample generation for complex hyperproperties.

## Contribution

It introduces a semi-decision procedure for the full HyperLTL logic, surpassing previous limitations to the $orall^* herefore^*$ fragment, and provides practical verification capabilities.

## Key findings

- Successfully checked complex hyperproperties beyond the $orall^* herefore^*$ fragment.
- Demonstrated effectiveness on literature and randomly generated HyperLTL formulas.
- Enabled automatic counterexample generation and property equivalence verification.

## Abstract

Hyperproperties are properties that refer to multiple computation traces. This includes many information-flow security policies, such as observational determinism, (generalized) noninterference, and noninference, and other system properties like symmetry or Hamming distances between in error-resistant codes. We introduce MGHyper, a tool for automatic satisfiability checking and model generation for hyperproperties expressed in HyperLTL. Unlike previous satisfiability checkers, MGHyper is not limited to the decidable $\exists^* \forall^*$ fragment of HyperLTL, but provides a semi-decisionprocedure for the full logic. An important application of MGHyper is to automatically check equivalences between different hyperproperties (and different formalizations of the same hyperproperty) and to build counterexamples that disprove a certain claimed implication. We describe the semi-decisionprocedure implemented in MGHyper and report on experimental results obtained both with typical hyperproperties from the literature and with randomly generated HyperLTL formulas.