PV4 ⊧ EAHyperchecks satisfiability, implication and equivalence of hyperproperties

Tool for the automatic checking of satisfiability, implication and equivalence of hyperproperties.

Application domain/field

• Hyperproperties
• Temporal logic
• Execution traces

Type of tool

Satisfiability solver

Expected input

HyperLTL formula in the ${\exists }^{*}{\forall }^{*}$ fragment, or an implication between two alternation-free formulas.

Expected output

• If given a formula in the ${\exists }^{*}{\forall }^{*}$ fragment, then it reports satisfiability
• If given an implication between two alternation-free formulas, then it reports validity.

Internals

• 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 ${\exists }^{*}{\forall }^{*}$ 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.

Comments

License: ISC License