Reasoning about Quality in Hyperproperties
Samuel Graepler, Benjamin Monmege, Jean-Marc Talbot
TL;DR
The paper advances the study of hyperproperties by introducing qualitative extensions of HyperLTL that map sets of traces to values in [0,1], enabling graded guarantees rather than strict satisfaction. It defines HyperLTL_prop (propositional quality) and HyperLTL_temp (temporal quality) and develops automata-based model checking techniques, including finite-value results for the propositional case and approximate/fragmented strategies for the temporal case. Key contributions include a finite-valued property for HyperLTL_prop, a non-elementary but automata-based decision procedure, and a framework for automata-based approximate model checking alongside exact results for tractable fragments of HyperLTL_temp. The work lays groundwork for practical qualitative reasoning about security and performance in systems, with potential extensions to probabilistic and other weighted logics."
Abstract
Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.