PV4 ⊧ EAHyperchecks satisfiability, implication and equivalence of hyperpropertiesTool for the automatic checking of satisfiability, implication and equivalence of hyperproperties.
- Temporal logic
- Execution traces
Type of toolSatisfiability solver
Expected inputHyperLTL formula in the fragment, or an implication between two alternation-free formulas.
- If given a formula in the fragment, then it reports satisfiability
- If given an implication between two alternation-free formulas, then it reports validity.
- EAHyper is a tool for automatically checking satisfiability, implication and equivalence of hyperproperties. EAHyper analyzes hyperproperties that are specified in HyperLTL.
- EAHyper can therefore be used to detect specifications that inconsistent, vacuously true, or to check implication and equivalence between multiple formalizations of the same requirement.
- EAHyper supports the fragment of HyperLTL, which is the largest decidable fragment of HyperLTL.
- This fragment consists of all formulas with at most one quantifier alternation, where no existential quantifier is in the scope of a universal quantifier.
- EAHyper reduces a HyperLTL formula to the satisfiability of an LTL formula. It then uses an external tool (pltl or aalta) to decide the satisfiability of the LTL formula.
- Hyperproperties: system properties that relate multiple computation traces.
- HyperLTL: Extension of LTL. It uses trace variables and trace quantifiers to refer to multiple execution traces simultaneously.