Reasoning About Quality in Hyperproperties

Graepler, Samuel; Monmege, Benjamin; Talbot, Jean-Marc

doi:10.4230/LIPIcs.CSL.2026.45

Reasoning About Quality in Hyperproperties

Samuel Graepler Fakultät für Mathematik und Informatik, Universität Leipzig, Germany Benjamin Monmege

Aix Marseille Univ, CNRS, LIS, Marseille, France Jean-Marc Talbot Aix Marseille Univ, CNRS, LIS, Marseille, France
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence, France

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 [2] 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.

Keywords and phrases:

Hyperlogics, Automata-based model checking, Quantitative verification

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification ; Security and privacy

Related Version:

Full Version: https://arxiv.org/abs/2512.00500 [18]

Acknowledgements:

We thank the reviewers of the different versions of this article for their valuable feedback.

Funding:

This work was partially done while the first author was an intern at Aix-Marseille Université. This work was partly supported by ANR-23-PECL-0009 TRUSTINCloudS.

DOI:

10.4230/LIPIcs.CSL.2026.45

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Software safety and security have become a critical concern. Hence, ensuring that applications are free from safety issues or security vulnerabilities is an important area of the verification process. Model checking [5] is a successful formal method to automatically verify whether a system meets a specification. This specification is often described as formulas from dedicated logics, for instance $\mathrm{LTL}$ to express properties on execution traces of a system [22] regarding safety. Model checking, in particular of $\mathrm{LTL}$ , has been widely studied and leads to several tools like SPIN [19] and Spot [9].

Over the last years, hyperlogics have been found out to be another convenient tool to express properties about systems. These logics define hyperproperties [7] that consider not single executions as $\mathrm{LTL}$ , but several of them at once. Hence, hyperlogics are often used to express properties relating multiple executions of a system, e.g., network properties like congestion [4], or security and information-flow properties [15, 24, 26]. Let us focus here on the security property of non-interference [17], which holds when executions of systems do not reveal sensitive information to malicious observers: secret information cannot be deduced from information of low sensitivity exposed by the system executions. As running examples, we consider two desirable properties to meet such requirements. We express them in the logic $\mathrm{HyperLTL}$ which extends $\mathrm{LTL}$ with a prefix of quantifications over traces variables [6]. First, the property called observational determinism [27] expresses the fact that when any two executions start with the same information of low sensitivity, then when observed all along the computation, the two traces cannot be distinguished on these low information (the system behaves deterministically with respect to them). To describe this property, we write a $\mathrm{HyperLTL}$ formula $\varphi_{\mathsf{OD}}$

\varphi_{\mathsf{OD}}\quad=\quad\forall\pi\,\forall\pi^{\prime}\quad\mathrm{% same}_{\mathrm{low}}(\pi,\pi^{\prime})\ \rightarrow\ \operatorname{\mathbf{G}}% \mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})

(1)

which uses the $\mathrm{LTL}$ formula $\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})$ , with two free trace variables, that states that at the first instant, $\pi$ and $\pi^{\prime}$ fulfil the same set of low atomic propositions.

The second property called non-inference [20] expresses the fact that high sensitive information are not exposed through low level one: for any trace, there must exist another one with arbitrary or dummy high sensitive information but with similar low-level information all along the computation. This property can be written as a $\mathrm{HyperLTL}$ formula as:

\varphi_{\mathsf{NI}}\quad=\quad\forall\pi\,\exists\pi^{\prime}\quad% \operatorname{\mathbf{G}}\Lambda_{\mathrm{high}}(\pi^{\prime})\land% \operatorname{\mathbf{G}}\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})

(2)

where the formula $\Lambda_{\mathrm{high}}(\pi^{\prime})$ is an $\mathrm{LTL}$ formula checking that the only high (i.e. non low) atomic propositions are a dummy one.

Unfortunately, most of the time, requiring strict security properties is actually ineffective as programs do not meet such requirements. To overcome this issue, it has been proposed to quantify security breaches as, e.g., in quantitative information flow [23]. Such approaches allow some information leaks provided they are acceptable, i.e. of amplitude not beyond some threshold; they have been studied in the framework of hyperproperties and hyperlogics [25, 13], in particular by considering counting extensions of $\mathrm{HyperLTL}$ where the number of models of a formula can be compared with some threshold.

In this article, we follow a different approach and base our work on the extensions of $\mathrm{LTL}$ proposed in [2]. In the latter, the authors proposed a framework enriching the syntax and semantics of LTL for reasoning about the quality of systems; the semantics of a formula is a value in $[0,1]$ reflecting the quality of a trace, that is, at which extent it is satisfied by this trace (0 when the formula is not satisfied at all and 1 when the formula is fully satisfied). Two ways on how to reason about quality in the context of LTL are explored there. The first one, the “propositional quality”, focuses on the different ways how a specification can be satisfied. It is embodied by $\mathrm{LTL}_{\mathrm{prop}}$ , an extension of $\mathrm{LTL}$ with logical operators defined as mappings over $[0,1]$ . The second one, the “temporal quality”, focuses on when eventualities are satisfied and the corresponding $\mathrm{LTL}$ extension is $\mathrm{LTL}_{\mathrm{temp}}$ . This latter considers temporal operators with discount which makes it possible to assign different values to a formula depending on when certain eventualities happen¹¹1We use different names for the two logics, to be consistent with the hyperlogics we introduce afterwards..

We lift these qualitative extensions of $\mathrm{LTL}$ to the setting of hyperproperties. In the Boolean setting, the models of a hyperproperty (e.g., a $\mathrm{HyperLTL}$ formula) are sets of traces. Hence, a $\mathrm{HyperLTL}$ formula associates a Boolean value with each set of traces. To incorporate quality, a formula thus must map each set of traces to a value in $[0,1]$ . We propose qualitative extensions of $\mathrm{HyperLTL}$ , similar to the two logics $\mathrm{LTL}_{\mathrm{prop}}$ and $\mathrm{LTL}_{\mathrm{temp}}$ wrt $\mathrm{LTL}$ , named respectively $\mathrm{HyperLTL}_{\mathrm{prop}}$ and $\mathrm{HyperLTL}_{\mathrm{temp}}$ . For the former, coming back to our example above, the condition on observational determinism can be relaxed by requiring the difference on low information to remain “small” all along the computation: a formula of $\mathrm{HyperLTL}_{\mathrm{prop}}$ thus allows one to associate with a given system a propositional quality describing guarantees about observational determinism. One may also consider as acceptable two traces that finally differ quite far from their origin: this is enabled in $\mathrm{HyperLTL}_{\mathrm{temp}}$ .

Our main objective is to study the model checking of the hyperlogics $\mathrm{HyperLTL}_{\mathrm{prop}}$ and $\mathrm{HyperLTL}_{\mathrm{temp}}$ . It consists in deciding whether the semantics of a (closed) formula is above (or below) a given threshold $v\in[0,1]$ when the set of traces in consideration is the one generated by a system (a Kripke structure). Qualitative model checking will therefore indicates to which extent the set of traces of a Kripke structure satisfies a formula.

$\mathrm{HyperLTL}_{\mathrm{prop}}$ is studied in Section 3. We show that the semantics of a $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula can take only a finite set of values in $[0,1]$ . We use this crucial property to design an automata-based model checking algorithm by building a non-deterministic Büchi automaton (NBA) from a $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula for which we test emptiness. This finiteness property also implies that $\mathrm{HyperLTL}_{\mathrm{prop}}$ is not more expressive than $\mathrm{HyperLTL}$ .

For $\mathrm{HyperLTL}_{\mathrm{temp}}$ , studied in Section 4, the situation is much more delicate as the set of possible values of a formula is no longer finite. We develop nonetheless automata-based techniques for model checking following two directions. We first solve an approximate model checking problem for $\mathrm{HyperLTL}_{\mathrm{temp}}$ that is correct modulo some $\epsilon$ term. We then consider fragments of $\mathrm{HyperLTL}_{\mathrm{temp}}$ for which we solve the exact model checking problem: the first fragment allows arbitrary quantifier prefixes but limits the interplay between negations and discounted operators. We show that in this case, the set of possible values, although infinite, enjoys a nice structure allowing automata-based model checking. For the second fragment, one considers arbitrary quantifier-free parts of formulas but forbid quantifier alternation. For these two fragments, we provide examples showing that they are still sufficient to express interesting hyperproperties on the quality of systems.

We describe our results in a weighted setting where systems (Kripke structures) that generate traces associate with each timestep a mapping giving to atomic propositions a weight in $[0,1]$ , instead of just the subset of atomic propositions that currently hold. This allows one to incorporate more meaningful qualitative reasoning since basic weights come from the system description itself. For instance, weights can encode costs, time delays or probabilities. A similar setting for $\mathrm{LTL}$ has been considered in [10].

Other kinds of logic than temporal logic, like HyperFO [14] that is a hyper-extension of the first-order logic, could also be extended with quality. However, as advocated in [2], weighted extensions of logics like FO (or even MSO, i.e. monadic second order logic) such as wMSO [8] or wFO [3] are not very suitable to define specifications due to their undecidable nature. Hence, we believe that a weighted extension of HyperFO [14] would not fit our goals.

A longer version, including all proofs, is available [18].

2 Preliminaries

Kripke structures.

We let $\mathrm{AP}$ be a finite set of atomic propositions. We consider traces that are infinite sequences of atomic propositions each weighted by a weight in $[0,1]$ , i.e. elements of $([0,1]^{\mathrm{AP}})^{\omega}$ . We denote $\mathbb{T}$ the set of all traces, and call $\mathbb{T}_{\mathbb{W}}$ the subset of traces where all weights are taken in a finite set $\mathbb{W}\subset[0,1]$ . A particular case is when $\mathbb{W}=\{0,1\}$ , in which case we recover the classical traces: we call such traces Boolean traces in the following. Amongst all traces, we call lassos the ones of the form $uv^{\omega}$ with $u,v\in([0,1]^{\mathrm{AP}})^{*}$ (a finite word, followed by the infinite repetition of some finite word). We denote $\mathbb{L}$ the set of all lassos, and $\mathbb{L}_{\mathbb{W}}$ if weights are restricted in $\mathbb{W}$ . For a trace $t\in\mathbb{T}$ , we write $t[i]$ to refer to the $i$ -th element in $t$ , for $i\in\mathbb{N}$ . We denote by $t[i,\infty]$ the suffix path starting at the $i$ -th element.

A (weighted) Kripke structure is a tuple $\mathcal{K}=\langle S,\mathbb{W},I,\rightarrow,L\rangle$ , where $S$ is a finite set of states, $\mathbb{W}\subset[0,1]$ is a finite set of weights, $I\subseteq S$ is the set of initial states, $\rightarrow\ \subseteq S\times S$ is a total transition relation, and $L\colon S\rightarrow\mathbb{W}^{\mathrm{AP}}$ is a labeling function, assigning a weight to each atomic proposition in each state. The weight can encode for example costs, time delays or probabilities for the atomic propositions to be true. In case the weights are only $0$ and $1$ , we recover the classical Kripke structures used, e.g., in the model checking of $\mathrm{LTL}$ : in this article, we call such structures Boolean Kripke structures.

A path $s$ in $\mathcal{K}$ is a sequence $s=s_{0}s_{1}\cdots$ with $s_{0}\in S$ and $s_{i}\rightarrow s_{i+1}$ for all $i\in\mathbb{N}$ . Since $\rightarrow$ is total, there are no deadlocks and thus all paths are of infinite length. The set of all traces in $\mathcal{K}$ , denoted $\mathbb{T}(\mathcal{K})$ , is defined as the set of traces $t\in\mathbb{T}_{\mathbb{W}}$ of the form $t=L(s_{0})L(s_{1})\cdots$ for a path $s_{0}s_{1}\cdots$ in $\mathcal{K}$ . $\mathbb{L}(\mathcal{K})$ denotes the set of all lassos of $\mathcal{K}$ , that is, traces from $\mathbb{T}(\mathcal{K})$ that are lassos.

Büchi automata.

The model checking of $\mathrm{LTL}$ as well as $\mathrm{HyperLTL}$ , consisting in checking whether a given (Boolean) Kripke structure satisfies a given closed formula, relies on automata-based techniques. We recall here the automata used in this context.

A non-deterministic Büchi automaton (NBA) is a tuple $\mathcal{A}=\langle\Sigma,Q,Q_{0},\delta,F\rangle$ , where $\Sigma$ is a finite alphabet, $Q$ is a finite set of states, $Q_{0}\subseteq Q$ is the set of initial states, $\delta:Q\times\Sigma\rightarrow 2^{Q}$ is a transition function and $F\subseteq Q$ is the set of accepting states. An infinite sequence $r=r_{0}r_{1}\cdots$ of states is called a run on a word $w=w_{1}w_{2}\cdots\in\Sigma^{\omega}$ if $r_{0}\in Q_{0}$ and for every $i\geq 0$ , $r_{i+1}\in\delta(r_{i},w_{i+1})$ . An NBA accepts a word if there exists a run $r$ on it that visits $F$ infinitely often, i.e. for $\inf(r)=\{q\mid r_{i}=q\text{ for infinitely many }i\in\mathbb{N}\}$ , it holds that $\inf(r)\cap F\neq\emptyset$ . The accepted language of an NBA, denoted by $\mathcal{L}(\mathcal{A})$ , is the set of words accepted by $\mathcal{A}$ .

The emptiness problem of an NBA, i.e. deciding whether the accepted language is empty, is decidable in linear time and is $\mathrm{NLOGSPACE}$ -complete [16].

Given a Kripke structure $\mathcal{K}$ defined over a set $\mathrm{AP}$ of atomic propositions and a finite set of weights $\mathbb{W}$ , one can define an NBA $\mathcal{A}_{\mathcal{K}}$ over the alphabet $\mathbb{W}^{\mathrm{AP}}$ accepting the language $\mathbb{T}(\mathcal{K})$ .

HyperLTL.

The logic $\mathrm{HyperLTL}$ , a hyperlogic extension of Linear Time Logic ( $\mathrm{LTL}$ ) was introduced in [6]. It extends $\mathrm{LTL}$ with universal and existential quantifiers over traces allowing to express properties on several traces. Models for $\mathrm{HyperLTL}$ formulas are then sets of traces and not individual traces. Hence, the set of all models of a $\mathrm{HyperLTL}$ formula is a set of sets of traces, a hyperproperty.

We let $\mathcal{V}$ be the infinite set of (trace) variables. The formulas of $\mathrm{HyperLTL}$ are defined by the following grammar, for all atomic propositions $p\in\mathrm{AP}$ and variables $\pi\in\mathcal{V}$ :

\displaystyle\psi

\displaystyle::=\exists\pi\,\psi\mid\forall\pi\,\psi\mid\varphi

\displaystyle\varphi

\displaystyle::=p_{\pi}\mid\neg\varphi\mid\varphi\vee\varphi\mid\operatorname{% \mathbf{X}}\varphi\mid\varphi\mathbin{\mathbf{U}}\varphi

As usual, additional operators can be derived : $\varphi_{1}\wedge\varphi_{2}=\neg((\neg\varphi_{1})\vee(\neg\varphi_{2}))$ , $\mathrm{true}=p_{\pi}\vee\neg p_{\pi}$ and $\mathrm{false}=\neg\mathrm{true}$ , $\varphi_{1}\rightarrow\varphi_{2}=\neg\varphi_{1}\vee\varphi_{2}$ , $\varphi_{1}\leftrightarrow\varphi_{2}=(\varphi_{1}\rightarrow\varphi_{2})\vee(% \varphi_{2}\rightarrow\varphi_{1})$ , the Finally operator $\operatorname{\mathbf{F}}\varphi=\mathrm{true}\mathbin{\mathbf{U}}\varphi$ , and the Globally operator $\operatorname{\mathbf{G}}\varphi=\neg\operatorname{\mathbf{F}}(\neg\varphi)$ .

If $\psi=Q_{1}\pi_{1}\cdots Q_{n}\pi_{n}\varphi$ for $Q_{i}\in\{\exists,\forall\}$ for $i\in\{1,\dots,n\}$ and $\varphi$ quantifier-free, we call $\varphi$ the quantifier-free part of $\psi$ .

We know explain the semantics of $\mathrm{HyperLTL}$ formulas over (weighted) traces. This differs from the classical semantics of $\mathrm{HyperLTL}$ associating with each formula a set of traces. We recover an equivalent definition in the case of a Boolean Kripke structure. Given a trace assignment $\Pi$ over $\mathbb{T}$ , mapping trace variables to traces, and a non-empty set of traces $T\subseteq\mathbb{T}$ used as a ranging set for quantified variables²²2Notice that we do not require $\Pi$ to map variables to the restricted set of traces $T$ ., the semantics $\llbracket\psi\rrbracket_{T}(\Pi)$ of a formula $\psi$ , called the satisfaction value of $\psi$ over $T$ given $\Pi$ , is the weight in $[0,1]$ defined recursively as:

$\displaystyle\llbracket p_{\pi}\rrbracket_{T}(\Pi)$	$\displaystyle=\Pi(\pi)[0](p)$	$\displaystyle\llbracket\lnot\varphi\rrbracket_{T}(\Pi)$	$\displaystyle=1-\llbracket\varphi\rrbracket_{T}(\Pi)$
$\displaystyle\llbracket\varphi_{1}\lor\varphi_{2}\rrbracket_{T}(\Pi)$	$\displaystyle=\max(\llbracket\varphi_{1}\rrbracket_{T}(\Pi),\llbracket\varphi_% {2}\rrbracket_{T}(\Pi))$	$\displaystyle\llbracket\operatorname{\mathbf{X}}\varphi\rrbracket_{T}(\Pi)$	$\displaystyle=\llbracket\varphi\rrbracket_{T}(\Pi[1,\infty])$
$\displaystyle\llbracket\varphi_{1}\mathbin{\mathbf{U}}\varphi_{2}\rrbracket_{T% }(\Pi)$	$\displaystyle=\makebox[0.0pt][l]{$\displaystyle\sup_{i\geq 0}\Big(\min\big(% \llbracket\varphi_{2}\rrbracket_{T}(\Pi[i,\infty]),\min_{0\leq j<i}\llbracket% \varphi_{1}\rrbracket_{T}(\Pi[j,\infty])\big)\Big)$}$
$\displaystyle\llbracket\forall\pi\,\psi\rrbracket_{T}(\Pi)$	$\displaystyle=\inf_{t\in T}\llbracket\psi\rrbracket_{T}(\Pi[\pi\mapsto t])$	$\displaystyle\llbracket\exists\pi\,\psi\rrbracket_{T}(\Pi)$	$\displaystyle=\sup_{t\in T}\llbracket\psi\rrbracket_{T}(\Pi[\pi\mapsto t])$

where $\Pi[\pi\mapsto t]$ is the trace assignment identical to $\Pi$ except that it maps $\pi$ to $t$ , and $\Pi[i,\infty]$ denotes the suffix trace assignment, defined for all variables $\pi$ as $\Pi[i,\infty](\pi)=\Pi(\pi)[i,\infty]$ . In case of a trace assignment that only contains Boolean traces (that we call Boolean assignments), it is easy to see that the semantics of $\mathrm{HyperLTL}$ formulas coincides with the classical semantics of $\mathrm{HyperLTL}$ , i.e. maps all Boolean assignments to $0$ or $1$ such that the set of assignments mapped to $1$ are the ones satisfying the formula.

As one may expect, for the existentially quantified formula $\exists\pi\,\psi$ , when $\psi$ in which $\pi$ is set to some trace $t$ is evaluated to $1$ , then so is $\exists\pi\,\psi$ . Hence, existential quantification is intuitively a disjunction over the set of all traces from T and thus, corresponds to a supremum. Universal quantification is defined dually as an infimum.

The semantics of the additional operators $\operatorname{\mathbf{F}}$ and $\operatorname{\mathbf{G}}$ are as follows: $\llbracket\operatorname{\mathbf{F}}\varphi\rrbracket_{T}(\Pi)=\sup_{i\geq 0}% \llbracket\varphi\rrbracket_{T}(\Pi[i,\infty])$ and $\llbracket\operatorname{\mathbf{G}}\varphi\rrbracket_{T}(\Pi)=\inf_{i\geq 0}% \llbracket\varphi\rrbracket_{T}(\Pi[i,\infty])$ .

For a closed formula $\psi$ (i.e. without free variables), the satisfaction value of $\psi$ over a Kripke structure $\mathcal{K}$ is the value $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}([\,])$ (denoted simply $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}$ from now on) taken over the empty assignment $[\,]$ .

3 Propositional quality for HyperLTL

3.1 Definitions and examples

In the same way that $\mathrm{HyperLTL}$ is built upon $\mathrm{LTL}$ , $\mathrm{HyperLTL}_{\mathrm{prop}}$ corresponds to the hyperlogic extension of the linear temporal logic $\mathrm{LTL}_{\mathrm{prop}}$ , for LTL with propositional quality [2].³³3This logic is called $\mathrm{LTL}[\mathcal{F}]$ in [2]. This logic generalises LTL by replacing the Boolean operators by a set $\mathcal{F}$ of arbitrary functions over [0,1]. Hence, the syntax of $\mathrm{LTL}$ is enriched by the construct $f(\varphi_{1},\ldots,\varphi_{k})$ for $f\in\mathcal{F}$ , the temporal operators remaining the same. Strictly speaking, it is then a family of logics, parameterized by $\mathcal{F}$ . Hence, beyond classical Boolean operators ( $\lor,\land,\lnot$ ) that can obviously be defined as such functions (and that we thus suppose to always be members of $\mathcal{F}$ ), the set $\mathcal{F}$ can contain quantitative functions like $\oplus_{\alpha}$ and $\triangledown_{\!\alpha}$ for $\alpha\in[0,1]$ , that associates with $x$ and $y$ the weighted sum $x\oplus_{\alpha}y=\alpha x+(1-\alpha)y$ and the scalar multiplication $\triangledown_{\!\alpha}x=\alpha x$ . Intuitively, the functions in $\mathcal{F}$ allow one to give weights to subformulas, i.e. parts of our specification, to moderate their “effect” in the formula where they occur. Let us point out that with such operators the semantics for formulas indeed belongs to the interval $[0,1]$ .

To reason about the propositional quality of hyperproperties, we introduce $\mathrm{HyperLTL}_{\mathrm{prop}}$ , a logic generalising both $\mathrm{HyperLTL}$ and $\mathrm{LTL}_{\mathrm{prop}}$ . A similar attempt has been achieved in [11] to lift $\mathrm{LTL}_{\mathrm{prop}}$ to the setting of alternating-time temporal logic to be able to quantify over strategies of agents in a multi-agent system: the same kind of fuzzy functions are added to talk about the quality in strategic reasoning.

Definition 1.

Assuming $\mathcal{F}$ is a finite set of function symbols, the syntax of $\mathrm{HyperLTL}_{\mathrm{prop}}$ is given by

\displaystyle\psi

\displaystyle::=\forall\pi\,\psi\mid\exists\pi\,\psi\mid\varphi

\displaystyle\varphi

\displaystyle::=\mathrm{true}\mid\mathrm{false}\mid p_{\pi}\mid f(\varphi,% \dots,\varphi)\mid\operatorname{\mathbf{X}}\varphi\mid\varphi\mathbin{\mathbf{% U}}\varphi

for all $p\in\mathrm{AP}$ , $\pi\in\mathcal{V}$ , and $f\in\mathcal{F}$ . These functions $f$ being interpreted as mappings from $[0,1]^{k}$ to $[0,1]$ (for functions of arity $k$ ), the $\mathrm{HyperLTL}$ semantics is extended for $\mathrm{HyperLTL}_{\mathrm{prop}}$ as

\llbracket f(\varphi_{1},\dots,\varphi_{k})\rrbracket_{T}(\Pi)=f(\llbracket% \varphi_{1}\rrbracket_{T}(\Pi),\dots,\llbracket\varphi_{k}\rrbracket_{T}(\Pi))

for all trace assignments $\Pi$ over $\mathbb{T}$ , and non-empty sets of traces $T\subseteq\mathbb{T}$ .

We give two examples showing that this extension of $\mathrm{HyperLTL}$ with propositional quality allows to model hyperproperties with a very different flavour than other quantitative extensions of $\mathrm{HyperLTL}$ (like counting extensions considered in [13]). The two first examples deal with Boolean Kriple structures, while the last one is a more general example that can be applied to a weighted Kripke structure.

Example 2.

We propose some quantitative versions of the observational determinism property presented in the introduction. First, let us formally define the subformula $\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})$ of the formula $\varphi_{\mathsf{OD}}$ , having two free variables $\pi$ and $\pi^{\prime}$ , as $\bigwedge_{p\in\mathrm{low}}p_{\pi}\leftrightarrow p_{\pi^{\prime}}$ , where $\mathrm{low}$ is the subset of “low sensitivity” atomic propositions. To compute the propositional quality of observational determinism, we adapt this formula by using the $\oplus$ weighted function in order to express the ratio of the agreement of two traces at the current step: $\ratio\pi{\pi^{\prime}}:=\bigoplus_{p\in\mathrm{low}}\frac{1}{|\mathrm{low}|}(% p_{\pi}\leftrightarrow p_{\pi^{\prime}})$ . Then, the formula $\operatorname{\mathbf{G}}\ratio\pi{\pi^{\prime}}$ aggregates these values at every step by considering an infimum. Thus, we can modify formula $\varphi_{\mathsf{OD}}$ to compute the smallest total ratio separating two traces of the system that agree on the first step, thus relaxing the Boolean observational determinism:

\forall\pi\,\forall\pi^{\prime}\quad\mathrm{same}_{\mathrm{low}}(\pi,\pi^{% \prime})\to\operatorname{\mathbf{G}}\ratio\pi{\pi^{\prime}}

One may use the interval $[0,1]$ in a less strict way and split it into several pieces, each of them encoding different “truth” status of the specification. For instance, we can refine this formula by separating the values $1$ obtained when the system non trivially fulfils observational determinism from the degenerated case where there are no two different traces which agree on the low atomic propositions on the first step:

\varphi_{\mathsf{OD}}^{\mathrm{prop}}\quad=\quad\forall\pi\,\forall\pi^{\prime% }\quad\triangledown_{\!\frac{1}{2}}\operatorname{\mathbf{G}}\ratio\pi{\pi^{% \prime}}\lor\triangledown_{\!\frac{3}{4}}(\lnot\mathrm{same}_{\mathrm{low}}(% \pi,\pi^{\prime})\lor\pi=\pi^{\prime})

where the subformula $\pi=\pi^{\prime}$ is used as a shortcut for the Boolean formula $\operatorname{\mathbf{G}}(\bigwedge_{p\in\mathrm{AP}}p_{\pi}\leftrightarrow p_% {\pi^{\prime}})$ . Here we get half of the smallest ratio of corresponding low atomic propositions (and thus a value in interval $[0,1/2]$ ), if there are two different traces which agree on the low atomic propositions of the first step, or $\frac{3}{4}$ (any value outside of $[0,1/2]$ could be convenient) if there are no such traces. The universal quantifications in the formula correspond to some minimisation and thus enable to consider the worst-case scenario. We could also consider the formula $\forall\pi\,\forall\pi^{\prime}\quad\mathrm{same}_{\mathrm{low}}(\pi,\pi^{% \prime})\to\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}(\ratio\pi{\pi^{% \prime}})$ with the addition of an operator $\operatorname{\mathbf{F}}$ to compute a $\lim\sup$ ratio, allowing for traces to vary a lot at the beginning, as long as they become close on the long term.

Example 3.

We present also a modification of the non-inference property $\varphi_{\mathsf{NI}}$ from the introduction. First, the subformula $\Lambda_{\mathrm{high}}(\pi^{\prime})$ can be described as $\lambda_{\pi^{\prime}}\land\bigwedge_{p\notin\mathrm{low}\cup\{\lambda\}}\lnot p% _{\pi^{\prime}}$ . Then, to describe the propositional quality of non-inference, we could ask whether, for every trace, we can find another trace with $\lambda$ as the only high atomic proposition, but which behaves almost the same for a low user. This approximation in the quality can be obtained by using a new weighted function $\mathit{threshold}_{>k}(x)$ , with $k\in[0,1]$ that equals $1$ if $x$ is greater than $k$ , and $0$ otherwise. The non-inference can then be relaxed as follows:

\varphi_{\mathsf{NI}}^{\mathrm{prop}}\quad=\quad\forall\pi\,\exists\pi^{\prime% }\quad\operatorname{\mathbf{G}}\Lambda_{\mathrm{high}}(\pi^{\prime})\land% \mathit{threshold}_{>k}(\ratio\pi{\pi^{\prime}})

The semantics of the formula is Boolean, though it uses weighted functions to compute it.

Example 4.

As a last example, we demonstrate what happens when we deal with a weighted Kripke structure that maps every atomic proposition to a probability that it holds in a given state. We can replace the formula $\ratio\pi{\pi^{\prime}}$ of Example 2 by its probabilistic version: $\bigwedge_{p\in\mathrm{low}}f(p_{\pi},p_{\pi^{\prime}})$ , where $f$ is the mapping defined for $x,y\in[0,1]$ by $f(x,y)=xy+(1-x)(1-y)$ , giving the probability that $p_{\pi}$ and $p_{\pi^{\prime}}$ are the same, $x$ being the probability of $p_{\pi}$ , and $y$ of $p_{\pi^{\prime}}$ . By considering the formula $\operatorname{\mathbf{G}}\big(\bigwedge_{p\in\mathrm{low}}f(p_{\pi},p_{\pi^{% \prime}})\big)$ , we thus compute the smallest probability over all steps that low atomic propositions coincide. The formula below thus computes the smallest such probability over any two traces:

\forall\pi\,\forall\pi^{\prime}\quad\mathrm{same}_{\mathrm{low}}(\pi,\pi^{% \prime})\to\operatorname{\mathbf{G}}\Big(\bigwedge_{p\in\mathrm{low}}f(p_{\pi}% ,p_{\pi^{\prime}})\Big)

If the semantics of this formula is $1$ , the system fulfils observational determinism. If the semantics of this formula is $0$ , the system contains two traces where a certain proposition $p$ differs with probability $1$ at some position. The values between $0$ and $1$ give a probabilistic quality of observational determinism: value $1/2$ , e.g., means that in any two traces, at any position, and for any low atomic proposition, the probability that the proposition coincides is at least $1/2$ .

3.2 A finite-valued property

We fix in this section a finite set $\mathbb{W}$ of weights in $[0,1]$ . Even though the family $\mathcal{F}$ may contain functions ranging over the whole interval $[0,1]$ , it turns out that every $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ enjoys a finite-valued property: it has only a finite number of possible satisfaction values, that is $\{\llbracket\psi\rrbracket_{T}(\Pi)\mid\Pi\colon\mathcal{V}\rightharpoonup% \mathbb{T}_{\mathbb{W}},\;T\subseteq\mathbb{T}_{\mathbb{W}}\text{ non empty}\}$ (denoted $V_{\mathbb{W}}(\llbracket\psi\rrbracket)$ from now on) is finite. Moreover, this set can be computationally over-approximated. This has been shown for $\mathrm{LTL}_{\mathrm{prop}}$ in [2, Lemma 2.5] (when $\mathbb{W}=\{0,1\}$ ), and we extend the proof here to $\mathrm{HyperLTL}_{\mathrm{prop}}$ ; this property will be used afterwards in our model checking algorithm.

Definition 5.

For any $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ , the set $V_{\mathbb{W}}(\psi)$ included in $[0,1]$ is defined inductively by:

	$\displaystyle V_{\mathbb{W}}(p_{\pi})=\mathbb{W}\cup\{0,1\}\qquad V_{\mathbb{W% }}(\operatorname{\mathbf{X}}\varphi)=V_{\mathbb{W}}(\varphi)\qquad V_{\mathbb{% W}}(\varphi_{1}\mathbin{\mathbf{U}}\varphi_{2})=V_{\mathbb{W}}(\varphi_{1})% \cup V_{\mathbb{W}}(\varphi_{2})$
	$\displaystyle V_{\mathbb{W}}(f(\varphi_{1},\dots,\varphi_{k}))=\{f(v_{1},\dots% ,v_{k})\mid v_{1}\in V_{\mathbb{W}}(\varphi_{1}),\ldots,v_{k}\in V_{\mathbb{W}% }(\varphi_{k})\}$
	$\displaystyle V_{\mathbb{W}}(\forall\pi\,\psi)=V_{\mathbb{W}}(\exists\pi\,\psi% )=V_{\mathbb{W}}(\psi)$

for $p\in\mathrm{AP}$ , $\pi\in\mathcal{V}$ , $f\in\mathcal{F}$ .

This set $V_{\mathbb{W}}(\psi)$ turns out to be finite as, essentially, the number of approximated satisfaction values only depends on $\#\psi$ , the number of occurrences of atomic propositions in the formula $\psi$ . For instance, $\#(p_{\pi}\mathbin{\mathbf{U}}f(p_{\pi},q_{\pi},p_{\pi^{\prime}}))=4$ since the formula uses atomic propositions $p_{\pi}$ (twice), $q_{\pi}$ and $p_{\pi^{\prime}}$ .

Lemma 6.

For all formulas $\psi$ of $\mathrm{HyperLTL}_{\mathrm{prop}}$ , $V_{\mathbb{W}}(\llbracket\psi\rrbracket)\subseteq V_{\mathbb{W}}(\psi)$ and $|V_{\mathbb{W}}(\psi)|\leq|\mathbb{W}|^{\#\psi}$ .

The exponential bound is tight, since it is already so for $\mathrm{LTL}_{\mathrm{prop}}$ [2]. In general the inclusion $V_{\mathbb{W}}(\llbracket\psi\rrbracket)\subseteq V_{\mathbb{W}}(\psi)$ is strict (see [18] for an example). Indeed, it is not surprising that the set $V_{\mathbb{W}}(\psi)$ is a strict over-approximation of the possible satisfaction values of $\psi$ as the satisfiability for $\mathrm{HyperLTL}$ (and thus of $\mathrm{HyperLTL}_{\mathrm{prop}}$ ) is undecidable [12]. Note that, as a consequence of this result, in the semantics of $\mathrm{HyperLTL}_{\mathrm{prop}}$ , the various occurrences of operators $\inf$ and $\sup$ can be replaced by $\min$ and $\max$ respectively.

3.3 The model checking problem for $\mathrm{HyperLTL}_{\mathrm{prop}}$

The natural generalisation of the model checking of $\mathrm{HyperLTL}$ to $\mathrm{HyperLTL}_{\mathrm{prop}}$ is as follows

Definition 7.

Given a Kripke structure $\mathcal{K}$ , a closed $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ , and a rational threshold $v\in[0,1]$ , the model checking problem is to decide whether $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ (or whether $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ , depending on the cases of interest).

We propose a model checking algorithm for $\mathrm{HyperLTL}_{\mathrm{prop}}$ . Its complexity will be non elementary with a tower of exponentials depending on the number of quantifier alternations of the $\mathrm{HyperLTL}$ formula. It relies, as a base case, on the construction proposed in [2] (Theorem 2.9 for the Boolean case, and section 3.1 for the extension to weighted Kripke structures) to translate a formula of $\mathrm{LTL}_{\mathrm{prop}}$ run on a Kripke structure into an NBA:

Proposition 8 ([2]).

Let $\varphi$ be an $\mathrm{LTL}_{\mathrm{prop}}$ formula, $\mathcal{K}$ be a Kripke structure, and $P\subseteq[0,1]$ . There exists an NBA $\mathcal{A}^{P}_{\mathcal{K},\varphi}$ such that for every trace $t\in\mathbb{T}(\mathcal{K})$ , it holds that $\llbracket\varphi\rrbracket(t)\in P$ iff $\mathcal{A}^{P}_{\mathcal{K},\varphi}$ accepts $t$ . Furthermore, $\mathcal{A}^{P}_{\mathcal{K},\varphi}$ has at most $|\mathbb{W}|^{|\varphi|^{2}}|\varphi|$ states where $\mathbb{W}$ is the set of weights in $\mathcal{K}$ , and $|\varphi|$ is the size of $\varphi$ .

In this proposition, the set $P$ can take various forms, provided that testing membership in $P$ of values in $[0,1]$ is decidable, so that the NBA $\mathcal{A}^{P}_{\mathcal{K},\varphi}$ is computable. For instance, if $P$ is of the form $[0,a)$ or $(a,1]$ , with some rational number $a$ , the membership test can be performed.

From this, to decide the model checking problem $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ for a given $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ and a Kripke structure $\mathcal{K}$ , we build an NBA $\mathcal{A}_{\mathcal{K},\psi}^{[0,v)}$ and check the emptiness of its language. We base the construction of this NBA on two crucial ideas used before separately. First, we make use of the NBA from Proposition 8 on a Krikpe structure obtained as a product of multiple copies of $\mathcal{K}$ (to deal with the quantified variables of $\psi$ ), by treating the quantifier-free part of a $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula as an $\mathrm{LTL}_{\mathrm{prop}}$ formula (as done in [6] for $\mathrm{HyperLTL}$ model checking). Second, following the semantics of a quantified formula, we compute $\inf$ and $\sup$ over $\mathbb{T}(\mathcal{K})$ , by checking finitely many values, as $V_{\mathbb{W}}(\psi)$ is finite (with $\mathbb{W}$ the set of weights in $\mathcal{K}$ ).

For the first step, we explain how to treat a non-quantified formula of $\mathrm{HyperLTL}_{\mathrm{prop}}$ as a formula of $\mathrm{LTL}_{\mathrm{prop}}$ over an extended set of atomic propositions. Formally, for all $n\in\mathbb{N}$ , we will consider trace variables $\pi_{1},\ldots,\pi_{n}$ , and denote by $\mathrm{AP}_{i}=\{p_{\pi_{i}}\mid p\in\mathrm{AP}\}$ the set of atomic propositions indexed by the trace variable $\pi_{i}$ . We then let $\mathrm{AP}_{\leq n}$ be the set $\bigcup_{1\leq i\leq n}\mathrm{AP}_{i}$ . Notice that $\mathrm{AP}_{\leq 0}$ is empty. Hence, a non-quantified formula $\psi$ of $\mathrm{HyperLTL}_{\mathrm{prop}}$ , having $\pi_{1},\ldots,\pi_{m}$ as free variables, can be considered as a formula of $\mathrm{LTL}_{\mathrm{prop}}$ , a trace assignment being encoded as a single trace as follows:

Definition 9.

Let $\Pi=[\pi_{1}\mapsto t_{1},\dots,\pi_{n}\mapsto t_{n}]$ be a trace assignment with $t_{i}\in\mathbb{T}(\mathcal{K})$ for all $1\leq i\leq n$ . The trace $t_{\Pi}$ is an element of $(\mathbb{W}^{\mathrm{AP}_{\leq n}})^{\omega}$ and is defined for all $k\in\mathbb{N}$ , for all $1\leq i\leq n$ , for all $p\in\mathrm{AP}$ , by $(t_{\Pi}[k])(p_{\pi_{i}})=(t_{i}[k])(p)$ .

By an inductive generalisation of Proposition 8, we are then able to obtain:

Proposition 10.

Let $\psi$ be a $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula, $P\subseteq[0,1]$ , and $\mathcal{K}$ be a Kripke structure. We can build an NBA $\mathcal{A}_{\mathcal{K},\psi}^{P}$ such that $\mathcal{L}(\mathcal{A}_{\mathcal{K},\psi}^{P})$ is the set of traces $t_{\Pi}$ , with $\Pi$ an assignment of free variables to traces of $\mathcal{K}$ , such that $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi)\in P$ . The size of $\mathcal{A}^{P}_{\mathcal{K},\psi}$ is non-elementary, with the tower of exponentials of linear height in the number of quantifier alternations of $\psi$ .

Note that for a closed formula and thus, the empty trace assignment, the NBA $\mathcal{A}_{\mathcal{K},\psi}$ can accept at most the unique trace $t_{[\,]}$ defined as $u^{\omega}$ with $u$ the mapping of empty domain. As a corollary, for a closed $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ , we obtain:

Theorem 11.

The model checking problem of $\mathrm{HyperLTL}_{\mathrm{prop}}$ is decidable with a non-elementary complexity.

The height of the tower of exponentials in the non elementary complexity depends only on the number of quantifier alternations, similarly to the case of $\mathrm{HyperLTL}$ [6]. Notice, as a final corollary, that we also obtain the decidability of the model checking problem for $\mathrm{HyperLTL}$ over weighted Kripke structures (which was not known so far, to the best of our knowledge), since $\mathrm{HyperLTL}$ is a fragment of $\mathrm{HyperLTL}_{\mathrm{prop}}$ :

Corollary 12.

The model checking problem of $\mathrm{HyperLTL}$ (over weighted Kripke structures) is decidable with a non-elementary complexity.

3.4 Expressiveness of $\mathrm{HyperLTL}_{\mathrm{prop}}$ in the Boolean case

In this section, we focus on Boolean Kripke structures, and we show that any $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula can be translated into a somewhat equivalent $\mathrm{HyperLTL}$ formula. This is an extension of the analogous result for $\mathrm{LTL}_{\mathrm{prop}}$ and $\mathrm{LTL}$ [2]. This implies $\mathrm{HyperLTL}_{\mathrm{prop}}$ is not more expressive than $\mathrm{HyperLTL}$ . However, it makes it a lot easier to express quantitative specifications, since the resulting $\mathrm{HyperLTL}$ formulas get very big and not very intuitive.

Theorem 13.

For every $P\subseteq[0,1]$ and $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ , there exists a $\mathrm{HyperLTL}$ formula $\mathrm{Bool}(\psi,P)$ such that for all subset $T\subseteq\mathbb{T}_{\{0,1\}}$ and trace assignments $\Pi$ , $\llbracket\psi\rrbracket_{T}(\Pi)\in P$ iff $\llbracket\mathrm{Bool}(\psi,P)\rrbracket_{T}(\Pi)=1$ . Moreover, $\mathrm{Bool}(\psi,P)$ has size at most $O(2^{(k+2)|\varphi|})$ if $k$ is the quantifier depth of $\varphi$ , and $\varphi$ is the quantifier-free part of $\psi$ .

The proof of this theorem heavily uses the fact that the formula $\psi$ has only finitely many possible satisfaction values and thus, that only those which also belong to $P$ matter. Hence, as a first step, it is possible to consider $P$ by means of each of its elements $c$ that is also a possible satisfaction value of $\psi$ . Then, recursively it is possible to define $\mathrm{Bool}(\psi,\{c\})$ as a Boolean combination of some $\mathrm{Bool}(\varphi_{i},P_{i})$ where $\varphi_{i}$ is an subformula of $\psi$ and $P_{i}$ is a subset of $P$ defined relatively to $c$ .

Some Boolean functions can only be expressed by exponential size Boolean formulas [21]. Therefore, as noticed in [2] already, the translation of an $\mathrm{LTL}_{\mathrm{prop}}$ formula to an equivalent $\mathrm{LTL}$ formula can grow exponentially: in our setting, there exists a sequence of quantifier-free formulas $\varphi$ , of growing length, and a predicate $P\subseteq[0,1]$ such that $|\mathrm{Bool}(\varphi,P)|\in\Omega(2^{|\varphi|})$ . In [2, Theorem 2.8], again in the case of $\mathrm{LTL}_{\mathrm{prop}}$ , a thorough discussion on the complexity of computing $\mathrm{Bool}(\varphi,P)$ explains that the computation can be performed in PSPACE (under reasonable assumptions on the complexity of the functions $f$ that appear in the formula), and that a super-polynomial blow-up (i.e. at least $|\varphi|^{c}$ for all constants $c$ ) is unavoidable.

The above translation of a $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ into an equivalent Boolean $\mathrm{HyperLTL}$ formula (whose model checking is non elementary [6]) yields an alternative model checking algorithm for $\mathrm{HyperLTL}_{\mathrm{prop}}$ , with non-elementary complexity. However the height of exponentials depends on the number of quantifiers in $\psi$ (instead on the number of quantifier alternations in Theorem 10); indeed, the number of alternations in $\mathrm{Bool}(\psi,P)$ depends on the number of quantifiers in the original formula $\psi$ (and not only on its number of alternations).

4 Temporal quality for HyperLTL

4.1 Definitions and examples

In this section we consider another qualitative extension of $\mathrm{HyperLTL}$ named $\mathrm{HyperLTL}_{\mathrm{temp}}$ (for $\mathrm{HyperLTL}$ with temporal quality). This logic is based upon $\mathrm{LTL}_{\mathrm{temp}}$ , another qualitative extension of LTL proposed in [2]⁴⁴4This logic is called $\mathrm{LTL}^{\mathit{Disc}}[\mathcal{D}]$ in that paper.. This latter generalises $\mathrm{LTL}$ by considering new temporal operators $\mathbin{\mathbf{U}}_{\eta}$ where $\eta$ is taken from a set $\mathcal{D}$ of discounting sequences which parameterises the logic: $(\eta_{i})_{i\in\mathbb{N}}$ is a discounting sequence if for all $i$ , $\eta_{i}\in[0,1]$ , $\lim_{i\to\infty}\eta_{i}=0$ , and $\eta$ is decreasing. Note, that this implies in particular that $\eta_{i}>0$ for all $i\in\mathbb{N}$ . Common examples for discounting sequences are $\eta_{i}=\alpha^{i}$ , for some $\alpha\in(0,1)$ , and $\eta_{i}=\frac{1}{i+1}$ .

In contrast to propositional quality which allows to mitigate the weights of subformulas, temporal quality aims to give weights depending on when events happen. Intuitively, for a formula $\varphi_{1}\mathbin{\mathbf{U}}_{\eta}\varphi_{2}$ , the further $\varphi_{2}$ is considered the least its value will impact the value of $\varphi_{1}\mathbin{\mathbf{U}}_{\eta}\varphi_{2}$ .

Definition 14.

Assuming $\mathcal{D}$ is a finite set of discounting sequences, the syntax of $\mathrm{HyperLTL}_{\mathrm{temp}}$ is given by

\displaystyle\psi

\displaystyle::=\forall\pi\,\psi\mid\exists\pi\,\psi\mid\varphi

\displaystyle\varphi

\displaystyle::=p_{\pi}\mid\neg\varphi\mid\varphi\vee\varphi\mid\operatorname{% \mathbf{X}}\varphi\mid\varphi\mathbin{\mathbf{U}}\varphi\mid\varphi\mathbin{% \mathbf{U}}_{\eta}\varphi

for all $p\in\mathrm{AP}$ , $\pi\in\mathcal{V}$ , and $\eta\in\mathcal{D}$ . The $\mathrm{HyperLTL}$ semantics is extended for $\mathrm{HyperLTL}_{\mathrm{temp}}$ as

\llbracket\varphi_{1}\mathbin{\mathbf{U}}_{\eta}\varphi_{2}\rrbracket_{T}(\Pi)% =\sup_{i\geq 0}\Big(\min\big(\eta_{i}\,\llbracket\varphi_{2}\rrbracket_{T}(\Pi% [i,\infty]),\min_{0\leq j<i}(\eta_{j}\,\llbracket\varphi_{1}\rrbracket_{T}(\Pi% [j,\infty]))\big)\Big)

for all trace assignments $\Pi$ over $\mathbb{T}$ , and a non-empty set of traces $T\subseteq\mathbb{T}$ .

We add as syntactic sugar the operators $\operatorname{\mathbf{F}}_{\eta}\varphi=\mathrm{true}\mathbin{\mathbf{U}}_{% \eta}\varphi$ and $\operatorname{\mathbf{G}}_{\eta}\varphi=\lnot\operatorname{\mathbf{F}}_{\eta}\lnot\varphi$ . Their semantics can be simplified as

\llbracket\operatorname{\mathbf{F}}_{\eta}\varphi\rrbracket_{T}(\Pi)=\sup_{i% \geq 0}(\eta_{i}\,\llbracket\varphi\rrbracket_{T}(\Pi[i,\infty]))\text{ and }% \llbracket\operatorname{\mathbf{G}}_{\eta}\varphi\rrbracket_{T}(\Pi)=\inf_{i% \geq 0}(1-\eta_{i}\,(1-\llbracket\varphi\rrbracket_{T}(\Pi[i,\infty])))

We propose now two examples showing this extension of $\mathrm{HyperLTL}$ with temporal quality allows to model hyperproperties; again it has a very different flavour than other quantitative extensions of $\mathrm{HyperLTL}$ as the ones from [13], for instance:

Example 15.

We can formulate another version of observational determinism in the logic $\mathrm{HyperLTL}_{\mathrm{temp}}$ . We refine $\varphi_{\mathsf{OD}}$ by replacing the global operator with a discounted one:

\varphi_{\mathsf{OD}}^{\mathrm{temp}}\quad=\quad\forall\pi\,\forall\pi^{\prime% }\quad\underbrace{\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})\ \rightarrow% \ \operatorname{\mathbf{G}}_{\eta}\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime% })}_{\varphi^{\prime}}

(3)

Note that, since discounted sequences are injective, the subformula $\varphi^{\prime}$ gives information about the moment where the two traces $\pi$ and $\pi^{\prime}$ disagree on low atomic propositions. The prefix of universal quantifiers captures this earliest moment in the full system. This could be of practical interest since the further in the future we leak information about secrets, the less probable a malicious adversary will dedicate that much time on an attack. So this amounts to verify that the satisfaction value of $\varphi_{\mathsf{OD}}^{\mathrm{temp}}$ is greater than a certain value.

Example 16.

We can also formulate another version of non-inference in $\mathrm{HyperLTL}_{\mathrm{temp}}$ . We refine the formula $\varphi_{\mathsf{NI}}$ by discounting the second part of the formula on the equality of low atomic propositions:

\varphi_{\mathsf{NI}}^{\mathrm{temp}}\quad=\quad\forall\pi\,\exists\pi^{\prime% }\quad\operatorname{\mathbf{G}}\Lambda_{\mathrm{high}}(\pi^{\prime})\land% \operatorname{\mathbf{G}}_{\eta}\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})

(4)

For a Boolean Kripke structure $\mathcal{K}$ , it computes either $1$ if the non-inference is satisfied, or $1-\eta_{i}$ where $i$ corresponds to the greatest value where every possible trace $t\in\mathbb{T}(\mathcal{K})$ has a trace $t^{\prime}\in\mathbb{T}(\mathcal{K})$ satisfying $\operatorname{\mathbf{G}}\Lambda_{\mathrm{high}}(t^{\prime})$ and $\mathrm{same}_{\mathrm{low}}(t,t^{\prime})$ until step $i$ . Hence, it computes a value giving us the longest possible time where the non-inference is satisfied in $\mathcal{K}$ .

4.2 Model checking for $\mathrm{HyperLTL}_{\mathrm{temp}}$

The model checking for $\mathrm{HyperLTL}_{\mathrm{temp}}$ aims to compare with some threshold the semantical value of a formula when applied to the set of traces of some Kripke structure.

For computability reasons, we assume from now on that the discounting sequences $(\eta_{i})_{i\in\mathbb{N}}$ are recursively enumerable sequences of rational numbers. Being recursively enumerable and strictly decreasing, the elements of such a sequence form therefore a recursive set of rationals.

Notice that, even in the case of Boolean Kripke structures, there is no hope to apply the strategy used in Section 3.4 to model check $\mathrm{HyperLTL}_{\mathrm{prop}}$ by translating a formula and a threshold to an equivalent Boolean $\mathrm{HyperLTL}$ formula. Indeed, it is already impossible to find an equivalent $\mathrm{LTL}$ formula for an $\mathrm{LTL}_{\mathrm{temp}}$ formula, since $\mathrm{LTL}_{\mathrm{temp}}$ formulas can generate non $\omega$ -regular languages, as noticed in [2] and recalled in the example below.

Example 17.

Consider for instance the formula $\varphi=\operatorname{\mathbf{G}}(\operatorname{\mathbf{F}}_{\eta}p)\lor% \operatorname{\mathbf{F}}\operatorname{\mathbf{G}}\lnot p$ . For a trace $t\in\mathbb{T}_{\{0,1\}}$ , either $\llbracket\varphi\rrbracket(t)=1$ if $p$ is seen only finitely often in $t$ (with weight 1), or $\llbracket\varphi\rrbracket(t)=\liminf_{k}\eta_{i_{k+1}-i_{k}-1}$ where $(i_{k})_{k\in\mathbb{N}}$ is the sequence of positions where $p$ holds in $t$ . In particular, $\llbracket\varphi\rrbracket(t)$ is always different from 0 when $t$ is a lasso trace; however $\llbracket\varphi\rrbracket(t)$ could be equal to 0 for some non-lasso trace $t$ , for instance when $i_{k}=k^{2}$ . This shows that the language of the traces $t$ such that $\llbracket\varphi\rrbracket(t)=0$ is not $\omega$ -regular as it is non empty, yet does not contain any lasso trace (although, there exist lassos with a semantics arbitrarily close to $0$ ).

Nonetheless, the notion of lassos remains useful regarding model checking purposes and we introduce the notion of lasso assignments:

Definition 18.

A trace assignment $\Pi$ is a lasso assignment if for all trace variables $\pi$ where it is defined, $\Pi(\pi)\in\mathbb{L}$ . Equivalently, the associated trace $t_{\Pi}$ is also a lasso.

Over lasso assignments, we show that Büchi automata can be used to describe the set of traces satisfying some $\mathrm{HyperLTL}_{\mathrm{temp}}$ formula wrt some threshold. This will also imply that, on a semantical point of view, formulas coincide when interpreted over traces and over lassos, and thus, will provide some automata-based tools to decide model checking for some fragments of $\mathrm{HyperLTL}_{\mathrm{temp}}$ .

Automata models for $\mathrm{HyperLTL}_{\mathrm{temp}}$ .

The following result from [2] (Theorem 4.6, and section 5.1 for the extension to weighted Kripke structures) relates models of $\mathrm{LTL}_{\mathrm{temp}}$ formulas in a Krikpe structure, and traces accepted by some NBA.

Proposition 19 ([2]).

Given an $\mathrm{LTL}_{\mathrm{temp}}$ formula $\varphi$ , a Kripke structure $\mathcal{K}$ , and a threshold $v\in[0,1]$ , for an ordering relation $\bowtie$ in $\{<,>\}$ , there exists an NBA $\mathcal{A}^{\bowtie v}_{\mathcal{K},\varphi}$ such that for every trace $t\in\mathbb{T}$ :

1.

If $\llbracket\varphi\rrbracket(t)\bowtie v$ , then $\mathcal{A}^{\bowtie v}_{\mathcal{K},\varphi}$ accepts $t$ .
2.

If $\mathcal{A}^{\bowtie v}_{\mathcal{K},\varphi}$ accepts $t$ and $t$ is a lasso, then $\llbracket\varphi\rrbracket(t)\bowtie v$ .

We build upon this result by extending it to formulas with quantifiers, and going from the classical semantics (in the first item) to the lasso semantics (in the second item). We use the same encodings of trace assignments as described in Section 3.3 for $\mathrm{HyperLTL}_{\mathrm{prop}}$ .

Lemma 20.

For an ordering relation $\bowtie$ in $\{<,>\}$ and $\underline{\bowtie}$ its reflexive closure, for all formulas $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}$ , for all Kripke structures $\mathcal{K}$ , for all $v\in[0,1]$ , we can build an NBA $\mathcal{A}_{\mathcal{K},\psi}^{\bowtie v}$ such that for every trace assignment $\Pi$ over the free variables of $\psi$ , it holds that:

1.

if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi)\bowtie v$ and all traces in $\Pi$ belong to $\mathbb{T}(\mathcal{K})$ , then $\mathcal{A}_{\mathcal{K},\psi}^{\bowtie v}$ accepts $t_{\Pi}$ ;
2.

if $\mathcal{A}_{\mathcal{K},\psi}^{\bowtie v}$ accepts a lasso $t_{\Pi}$ , then all traces in $\Pi$ belong to $\mathbb{L}(\mathcal{K})$ and $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)\ \underline{\bowtie}\ v$ .

If we only count the dependency in the quantifier part of $\mathrm{HyperLTL}_{\mathrm{temp}}$ , the NBA $\mathcal{A}_{\mathcal{K},\psi}^{\bowtie v}$ has a size that is bounded by a tower of exponentials of height depending linearly on the quantifier alternation of $\psi$ . Thanks to this technical result, we obtain as expected:

Corollary 21.

For all formulas $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}$ , Kripke structures $\mathcal{K}$ , and lasso assignments $\Pi$ such that $\Pi(\pi)\in\mathbb{L}(\mathcal{K})$ for all free variables $\pi$ in $\psi$ , $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi)=\llbracket\psi% \rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)$ .

Proof.

The proof is by induction on the quantifier depth of the formula $\psi$ .

If $\psi$ is non quantified, the result is trivial since no quantifications remains to be evaluated.

If $\psi=\exists\pi\;\psi^{\prime}$ , by definition of the semantics of the existential quantifier, and then by induction hypothesis, we have $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi)\geq\llbracket\psi% \rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)$ . Suppose that the inequality is strict, and let $v\in(\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi),\llbracket\psi% \rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi))$ . Since $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi)>v$ , by Lemma 20.1, $t_{\Pi}$ is then accepted by $\mathcal{A}_{\mathcal{K},\psi}^{>v}$ . Now, by Lemma 20.2, since $\Pi$ is a lasso assignment, $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)\geq v$ , which contradicts the hypothesis that $v>\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)$ .

If $\psi=\forall\pi\;\psi^{\prime}$ , by definition and by induction hypothesis, we have $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi)\leq\llbracket\psi% \rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)$ . Suppose that the inequality is strict, and let $v\in(\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}(\Pi),\llbracket\psi% \rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi))$ . By Lemma 20.1, $t_{\Pi}$ is then accepted by $\mathcal{A}_{\mathcal{K},\psi}^{<v}$ . Now, by Lemma 20.2, as $\Pi$ is a lasso assignment, $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)\leq v<\llbracket\psi% \rrbracket_{\mathbb{L}(\mathcal{K})}(\Pi)$ . Contradiction. $\hfill\blacktriangleleft$

In Example 17, notice that although all lassos are associated by $\varphi$ with a positive semantics, we indeed get $\llbracket\forall\pi\,\varphi\rrbracket_{\mathbb{L}(\mathcal{K})}=0$ by a convergence phenomenon. In contrast, we have also $\llbracket\forall\pi\;\varphi\rrbracket_{\mathbb{T}(\mathcal{K})}=0$ as there exists (non-lasso) traces associated by $\varphi$ with a zero semantics.

Issues relative to automata-based model checking.

In [2], the model checking problem amounts to deciding whether all traces of a Kripke structure $\mathcal{K}$ have a semantics wrt to an $\mathrm{LTL}_{\mathrm{temp}}$ formula $\varphi$ greater than or equal to a threshold $v$ . This translates to our setting in deciding whether $\llbracket\forall\pi\;\varphi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ . They check this by testing emptiness of the NBA $\mathcal{A}^{<v}_{\mathcal{K},\varphi}$ : this is correct because of item 2 of Proposition 19, since if $\mathcal{A}^{<v}_{\mathcal{K},\varphi}$ would accept a lasso $t$ , it would be such that $\llbracket\varphi\rrbracket(t)<v$ .

In the setting of $\mathrm{HyperLTL}_{\mathrm{temp}}$ , this leads to two difficulties. First, the second item of our Lemma 20 is weaker than the one of Proposition 19 as the comparison with the value $v$ is no longer strict, preventing the same argument as before in $\mathrm{LTL}_{\mathrm{temp}}$ . Second, our formulas contain $\forall$ and $\exists$ quantifiers (whose semantics are $\sup$ and $\inf$ operators) and thus, we should be able to solve the model checking problems $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ and $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ , for a closed formula $\psi$ . Once again, the reasoning above fails in this case since it is not true a priori that $\llbracket\forall\pi\;\varphi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ if and only if the NBA $\mathcal{A}^{>v}_{\mathcal{K},\varphi}$ has an empty language. We demonstrate this more carefully in the example below.

Example 22.

We continue Example 17. Consider $\varphi_{\pi}=\operatorname{\mathbf{G}}(\operatorname{\mathbf{F}}_{\eta}p_{\pi% })\lor\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}\lnot p_{\pi}$ , and $\psi=\forall\pi\;\varphi_{\pi}$ . As we discussed, for a trivial Kripke structure $\mathcal{K}$ allowing every trace, we have $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}=\llbracket\psi\rrbracket_{% \mathbb{L}(\mathcal{K})}=0$ : there exist witnesses $t\in\mathbb{T}(\mathcal{K})$ where $\varphi_{\pi}$ evaluates to $0$ , but no such witness is a lasso of $\mathcal{K}$ . For this formula, we would like to solve the model checking problem $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq 0$ (which indeed implies that $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}=0$ ). If we would use Lemma 20, this would require to build the NBA $\mathcal{A}_{\mathcal{K},\psi}^{>0}$ to check its emptiness. This automaton could be obtained by computing first the NBA $\mathcal{A}_{\mathcal{K},\varphi_{\pi}}^{>0}$ that accepts all lassos, complementing it (obtaining then an NBA with empty language) before taking the intersection with the traces generated by $\mathcal{K}$ , then projecting away the trace $\pi$ , and finally, complementing it again. The so-obtained NBA accepts the trace $t_{[\,]}$ , and the model checking algorithm would thus wrongly declare that $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}>0$ .

We therefore cannot directly rely on the construction of an NBA to fully and exactly model check $\mathrm{HyperLTL}_{\mathrm{temp}}$ . However, we propose two kinds of solutions in the rest of this section based on automata. First, we relax the problem, solving approximate model checking; second, we study several fragments for which the (exact) model checking task can be solved.

Approximate model checking.

We weaken the model checking problem to only give an approximate solution instead:

Definition 23.

The approximate model checking of $\mathrm{HyperLTL}_{\mathrm{temp}}$ (associated with the exact problem $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ ) is the following: given a Kripke structure $\mathcal{K}$ , a closed $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula $\psi$ , a rational threshold $v\in[0,1]$ , and a rational approximation factor $\varepsilon>0$ , it answers positively when $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v+\varepsilon$ , negatively when $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v-\varepsilon$ , and arbitrarily otherwise. We can consider alternatively the symmetric question associated with the exact question $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ .

Theorem 24.

The approximate model checking of $\mathrm{HyperLTL}_{\mathrm{temp}}$ is decidable with a non-elementary complexity.

Proof.

Let $\mathcal{K}$ be a Kripke structure, $\psi$ be a closed $\mathrm{HyperLTL}_{\mathrm{prop}}$ formula, $v\in[0,1]$ a rational threshold, and $\varepsilon>0$ a rational approximation factor. Thanks to Corollary 21, $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}=\llbracket\psi\rrbracket_{% \mathbb{L}(\mathcal{K})}$ . Consider then the NBA $\mathcal{A}_{\mathcal{K},\psi}^{<v}$ of Lemma 20. Note that, since $\psi$ is closed, it runs on trace assignments over no traces: it either accepts the single infinite trace $t_{[]}$ that is a lasso (and thus, it is not empty), or it rejects it (and then, it is empty). The approximate model checking algorithm amounts to test emptiness for $\mathcal{A}_{\mathcal{K},\psi}^{<v}$ . Indeed, if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v+\varepsilon$ , i.e. $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}\geq v+\varepsilon$ , we have $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}\leq v$ for no lassos, and thus (by property 2 of Lemma 20) the NBA $\mathcal{A}_{\mathcal{K},\psi}^{<v}$ cannot accept any lasso: the emptiness check of this NBA declares that its language is empty and the algorithm answers positively. Symmetrically, if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v-\varepsilon$ , i.e. $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}\leq v-\varepsilon$ , we have $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}\leq v$ , and thus the single infinite lasso fulfills that; then, by property 2 of Lemma 20, it is accepted by the NBA $\mathcal{A}_{\mathcal{K},\psi}^{<v}$ : the emptiness check of this NBA declares that its language is non empty. Hence, the algorithm answers negatively. $\hfill\blacktriangleleft$

We now show in the next two subsections the fragments of $\mathrm{HyperLTL}_{\mathrm{temp}}$ for which one can answer the (exact) model checking problem.

Model checking of the positive and negative fragments.

We propose two first fragments for which we show the decidability of model checking. One is the fragment where negation is no longer allowed in $\mathrm{HyperLTL}_{\mathrm{temp}}$ formulas above $\mathbin{\mathbf{U}}_{\eta}$ operator. For this reason, we call this restriction the positive fragment.

Definition 25.

The fragment $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ of $\mathrm{HyperLTL}_{\mathrm{temp}}$ is the subset of formulas $\psi$ described by the grammar (where $p\in\mathrm{AP}$ , $\pi\in\mathcal{V}$ , and $\eta\in\mathcal{D}$ ):

	$\displaystyle\psi$	$\displaystyle::=\exists\pi\,\psi\mid\forall\pi\,\psi\mid\varphi\hskip 56.9055% pt\varphi::=\beta\mid\varphi\vee\varphi\mid\varphi\land\varphi\mid% \operatorname{\mathbf{X}}\varphi\mid\varphi\mathbin{\mathbf{U}}\varphi\mid% \varphi\mathbin{\mathbf{U}}_{\eta}\varphi$
	$\displaystyle\beta$	$\displaystyle::=p_{\pi}\mid\neg\beta\mid\beta\vee\beta\mid\operatorname{% \mathbf{X}}\beta\mid\beta\mathbin{\mathbf{U}}\beta$		(Boolean $\mathrm{LTL}$ formulas)

The two model checking problems we solve for $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ are the following ones:

$\blacksquare$

given a closed formula $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ , a Kripke structure $\mathcal{K}$ and a threshold $v\in[0,1]$ , decide if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ ;
$\blacksquare$

given a closed formula $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ , a Kripke structure $\mathcal{K}$ and a threshold $v\in(0,1]$ , decide if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ . ⁵⁵5Notice that the threshold $0$ is not allowed here, to avoid convergence issues.

In a symmetric fashion, we can define the fragment $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ obtained by considering negations of formulas of $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ . By pushing negations, this corresponds to the syntax

	$\displaystyle\psi$	$\displaystyle::=\exists\pi\,\psi\mid\forall\pi\,\psi\mid\varphi\hskip 56.9055% pt\varphi::=\beta\mid\varphi\vee\varphi\mid\varphi\land\varphi\mid% \operatorname{\mathbf{X}}\varphi\mid\varphi\mathbin{\mathbf{R}}\varphi\mid% \varphi\mathbin{\mathbf{R}}_{\eta}\varphi$
	$\displaystyle\beta$	$\displaystyle::=p_{\pi}\mid\neg\beta\mid\beta\vee\beta\mid\operatorname{% \mathbf{X}}\beta\mid\beta\mathbin{\mathbf{U}}\beta$		(Boolean $\mathrm{LTL}$ formulas)

where the semantics of the release operators $\mathbin{\mathbf{R}}$ and $\mathbin{\mathbf{R}}_{\eta}$ is obtained by a negation of the until operators, as usual. The model checking problems that we solve for this dual fragment are the following ones: given a closed formula $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ , a Kripke structure $\mathcal{K}$ and a threshold $v\in[0,1]$ (resp. $v\in[0,1)$ ), decide if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ (resp. $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ ).

The formula $\varphi_{\mathsf{OD}}^{\mathrm{temp}}$ of Example 15 is in the fragment $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ . Indeed, the negation of the formula can be rewritten as $\psi:=\exists\pi\,\exists\pi^{\prime}\ \ \mathrm{same}_{\mathrm{low}}(\pi,\pi^% {\prime})\land\operatorname{\mathbf{F}}_{\eta}\lnot\mathrm{same}_{\mathrm{low}% }(\pi,\pi^{\prime})$ , where $\mathrm{same}_{\mathrm{low}}(\pi,\pi^{\prime})$ is a Boolean $\mathrm{LTL}$ formula, and the operator $\operatorname{\mathbf{F}}_{\eta}$ does not involve any negation. This formula belongs to $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ . To model check the formula $\varphi_{\mathsf{OD}}^{\mathrm{temp}}$ against a threshold $\geq v$ (resp. $\leq v$ ), it suffices to model check the formula $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ against the threshold $\leq 1-v$ (resp. $\geq 1-v$ ). Similarly, the formula $\varphi_{\mathsf{NI}}^{\mathrm{temp}}$ of Example 16 is in the fragment $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ .

The first ingredient for decidability of the model checking comes from Corollary 21. This allows us to only model check the lasso semantics, which can faithfully be done by using an automata-based construction. Another ingredient is the characterisation of the set of possible satisfaction values that can generate a positive formula, helping us controlling the convergence phenomena in infimums/supremums of the semantics. To make this ingredient more precise, we introduce, for all $k\in\mathbb{N}$ , finite sets $H\subseteq\mathcal{D}$ , and finite sets $\mathbb{W}\subset[0,1]$ , the infinite set of values

$V_{k,H,\mathbb{W}}=\{0,1\}\cup\mathbb{W}\cup\{w\times\prod_{\ell=1}^{k^{\prime% }}\eta^{(\ell)}_{i_{\ell}}\mid w\in\mathbb{W},k^{\prime}\leq k,(i_{\ell})_{1% \leq\ell\leq k^{\prime}}\in\mathbf{N}^{k^{\prime}},(\eta^{(\ell)})_{1\leq\ell% \leq k^{\prime}}\in H^{k^{\prime}}\}$

This set has the following properties, using as natural hypotheses that we only consider computable discounted sequences $\eta$ :

Lemma 26.

For all $k\in\mathbb{N}$ , finite sets $H\subseteq\mathcal{D}$ , and finite sets $\mathbb{W}\subset[0,1]$ ,

$\blacksquare$

for all $a\in(0,1)$ , the set $V_{k,H,\mathbb{W}}\cap[a,1]$ is finite and computable;
$\blacksquare$

every non-decreasing sequence of $V_{k,H,\mathbb{W}}$ is stationary;
$\blacksquare$

every non-increasing sequence of $V_{k,H,\mathbb{W}}$ either converges to 0 or is stationary.

Proof.

$\blacksquare$

Let $a\in(0,1)$ . Since the functions $\eta\in H$ are decreasing and $H$ is finite, there is $i_{0}\in\mathbf{N}$ such that for all $i\geq i_{0}$ and $\eta\in H$ , $\eta(i)<a$ . Thus, $V_{k,H,\mathbb{W}}\cap[a,1]\subseteq\{1\}\cup\mathbb{W}\allowbreak\cup\{w% \times\prod_{\ell\leq k^{\prime}}\eta_{i_{\ell}}\mid w\in\mathbb{W},k^{\prime}% \leq k,\,\forall\ell\leq k\quad i_{\ell}\leq i_{0},\eta\in H\}$ is finite and enumerable.
$\blacksquare$

Let $(u_{n})$ be a non-decreasing sequence of $V_{k,H,\mathbb{W}}$ . Thus, it has values in $V_{k,H,\mathbb{W}}\cap[u_{0},1]$ that is finite, and thus is stationary.
$\blacksquare$

Let $(u_{n})$ be a non-increasing sequence of $V_{k,H,\mathbb{W}}$ . If the sequence does not converge to $0$ , it has a positive lower bound $a$ , and thus has values in $[a,1]$ . Since this set is finite, the sequence is stationary.

$\hfill\blacktriangleleft$

Moreover, this set can indeed be used to obtain an over-approximation of the set of satisfaction values of a formula in $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ .

Lemma 27.

Let $\psi$ be a formula of $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ . Let $k_{\psi}$ be the depth of $\mathbin{\mathbf{U}}_{\eta}$ operators, and $H_{\psi}$ be the finite set of functions $\eta$ appearing in these operators. Let $\mathbb{W}\subset[0,1]$ be a finite set. Then, for all $T\subseteq\mathbb{T}_{\mathbb{W}}$ , and $\Pi$ assignments to traces of $\mathbb{T}_{\mathbb{W}}$ , $\llbracket\psi\rrbracket_{T}(\Pi)\in V_{k_{\psi},H_{\psi},\mathbb{W}}$ .

This is enough to obtain an automata-based algorithm to model check $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ and $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ :

Theorem 28.

The model checking problems for $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ and $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ are decidable with a non-elementary complexity.

Proof.

Let $\psi$ be a closed formula of $\mathrm{HyperLTL}_{\mathrm{temp}}^{+}$ , $\mathcal{K}$ be a Kripke structure. Let $\mathbb{W}$ be the set of weights appearing in $\mathcal{K}$ .

$\blacksquare$

Let $v\in[0,1]$ . To decide whether $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ (with $v\neq 0$ otherwise the answer is trivially true), we consider, by Lemma 27, the greatest value $v^{\prime}$ of $V_{k_{\psi},H_{\psi},\mathbb{W}}$ smaller than $v$ . This value can be computed as a search in the finite and enumerable set of possibles values $S=V_{k_{\psi},H_{\psi},\mathbb{W}}\cap[a,1]$ with $a=\sup_{i\mid\eta_{i}<v}\eta_{i}$ for any $\eta\in H_{\psi}$ (since the set $S$ contains $\eta_{i}$ and thus values smaller than $v$ ). We then let $v^{\prime\prime}=(v^{\prime}+v)/2$ , and build the NBA $\mathcal{A}_{\mathcal{K},\psi}^{<v^{\prime\prime}}$ to check the emptiness of its language. If the language of $\mathcal{A}_{\mathcal{K},\psi}^{<v^{\prime\prime}}$ is empty, by Lemma 20.1, we cannot have $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}<v^{\prime\prime}$ , and thus $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v^{\prime\prime}$ and then, $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ as there are no values in $V_{k_{\psi},H_{\psi}}$ in-between $v^{\prime\prime}$ and $v$ . Reciprocally, if the language of $\mathcal{A}_{\mathcal{K},\psi}^{<v^{\prime\prime}}$ is non empty, it accepts the unique word over the alphabet with a single $\emptyset$ letter, which is thus a lasso. By Lemma 20.2, we have $\llbracket\psi\rrbracket_{\mathbb{L}(\mathcal{K})}\leq v^{\prime\prime}$ . By Corollary 21, $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v^{\prime\prime}<v$ .
$\blacksquare$

Let $v\in(0,1]$ . To decide whether $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ (with $v\neq 1$ otherwise the answer is trivially true), we consider, by Lemma 27, the lowest value $v^{\prime}$ of $V_{k_{\psi},H_{\psi},\mathbb{W}}$ greater than $v$ : it exists (and can be computed) since $v$ is taken different from $0$ . We then let $v^{\prime\prime}=(v+v^{\prime})/2$ , and conclude the proof in this case symmetrically as in the previous case, showing that $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}=\llbracket\psi\rrbracket_{% \mathbb{L}(\mathcal{K})}\geq v^{\prime\prime}>v$ .

We obtain the decidability for $\mathrm{HyperLTL}_{\mathrm{temp}}^{-}$ by a dual argument. $\hfill\blacktriangleleft$

The complexity of this model checking algorithm is at least as high as computing the automata given in Lemma 20, and thus at least non-elementary (with respect to the quantifier depth of the formulas): this is non-surprising since the model checking of $\mathrm{HyperLTL}$ has already a non-elementary lower bound in complexity. Formally, it also depends on the search for the value $v^{\prime}$ that is the greatest (resp. lowest) value smaller (resp. greater) than a value $v$ in a set of the form $V_{k,H,\mathbb{W}}$ . This heavily depends on the sequences $\eta$ in $H$ . If we suppose that these sequences are indeed geometrical, as it is the case for usual discounted automata where the current weight is always multiplied by a power $\lambda^{i}$ of a discounted parameter, this is easy, and thus does not change the complexity of the model checking algorithm.

Model checking of the alternation-free fragments.

The other two fragments that we consider, orthogonal to the previous ones, are the alternation-free fragments: $\mathrm{HyperLTL}_{\mathrm{temp}}^{\exists}$ is the fragment containing formulas of the form $\exists\pi_{1}\cdots\exists\pi_{n}\;\varphi$ with $\varphi$ quantifier-free, and $\mathrm{HyperLTL}_{\mathrm{temp}}^{\forall}$ is the fragment containing formulas of the form $\forall\pi_{1}\cdots\forall\pi_{n}\;\varphi$ .

The formula $\varphi_{\mathsf{OD}}^{\mathrm{temp}}$ describing observational determinism is in $\mathrm{HyperLTL}_{\mathrm{temp}}^{\forall}$ (as it contains simply two universal quantifications), but not the formula $\varphi_{\mathsf{NI}}^{\mathrm{temp}}$ describing non-inference (as it alternates between a universal quantification and an existential one).

The model checking problems we consider for these two logics are asymmetric: given a closed formula $\psi$ of $\mathrm{HyperLTL}_{\mathrm{temp}}^{\exists}$ (resp. $\mathrm{HyperLTL}_{\mathrm{temp}}^{\forall}$ ), a Kripke structure $\mathcal{K}$ and a threshold $v\in[0,1]$ , decide if $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\leq v$ (resp. $\llbracket\psi\rrbracket_{\mathbb{T}(\mathcal{K})}\geq v$ ). These are tailored to mimick the model checking problem of $\mathrm{LTL}_{\mathrm{temp}}$ in [2], in order to correspond to the Boolean variants of classical model checking questions: for the existential fragment, the semantics of the existential quantification being a supremum over traces, asking whether the semantics of the formula is at most a certain threshold requires to decide if all traces have an associated value at most the threshold; for the universal fragment, the semantics of the universal quantification being a infimum over traces, asking whether the semantics of the formula is at least a certain threshold requires to decide if all traces have an associated value at least the threshold. By a proof building upon Proposition 19, and the techniques of Theorem 10, we obtain:

Theorem 29.

The model checking of $\mathrm{HyperLTL}_{\mathrm{temp}}^{\exists}$ and $\mathrm{HyperLTL}_{\mathrm{temp}}^{\forall}$ is decidable with a non-elementary complexity..

5 Conclusion

We have proposed a framework for qualitative reasoning about hyperproperties, by considering formulas whose semantics range in $[0,1]$ . We introduce two logics extending $\mathrm{HyperLTL}$ , namely $\mathrm{HyperLTL}_{\mathrm{prop}}$ and $\mathrm{HyperLTL}_{\mathrm{temp}}$ , and study their model checking problem. For the former, we propose an algorithm with a complexity similar to the one of $\mathrm{HyperLTL}$ . For the latter, we propose some model checking algorithms for fragments of this logic as well an approximate algorithm for the full logic. Notice that our approximation scheme is different from the one mentioned in [2] for $\mathrm{LTL}_{\mathrm{temp}}$ . There, approximation is performed on the “discounted” sequences whose values are set to 0 when they become smaller than a given threshold $\delta$ . Such approach could also be followed for $\mathrm{HyperLTL}_{\mathrm{temp}}$ . We leave as open the decidability of the exact model checking problem for the whole logic $\mathrm{HyperLTL}_{\mathrm{temp}}$ . As future works, we would like to study qualitative extensions of HyperPCTL [1], a temporal logic for reasoning about probabilistic hyperproperties of discrete-time Markov chains.

References

[1] Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Quantitative Evaluation of Systems. Springer, 2018. doi:10.1007/978-3-319-99154-2_2.
[2] Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. Journal of the ACM, 63(3):1–56, 2016. doi:10.1145/2875421.
[3] Benedikt Bollig, Paul Gastin, Benjamin Monmege, and Marc Zeitoun. Pebble weighted automata and weighted logics. ACM Trans. Comput. Log., 15(2):15:1–15:35, 2014. doi:10.1145/2579819.
[4] Marco Chiesa, Guy Kindler, and Michael Schapira. Traffic engineering with equal-cost-multipath: An algorithmic perspective. IEEE/ACM Transactions on Networking, 25(2):779–792, 2017. doi:10.1109/TNET.2016.2614247.
[5] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer Cham, 2020. doi:10.1007/978-3-319-10575-8.
[6] M. R. Clarkson, Bernd Finkbeiner, M. Koleini, K. K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In POST 2014, volume 8414 of LNCS, pages 265–284. Springer, 2014. doi:10.1007/978-3-642-54792-8_15.
[7] M. R. Clarkson and F. Schneider. Hyperproperties. Journal of Computer Security, 18:1157–1210, 2010. doi:10.1109/CSF.2008.7.
[8] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theor. Comput. Sci., 380(1-2):69–86, 2007. doi:10.1016/J.TCS.2007.02.055.
[9] Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In CAV 2022, volume 13372 of LNCS, pages 174–187. Springer, 2022. doi:10.1007/978-3-031-13188-2_9.
[10] Marco Faella, Axel Legay, and Mariëlle Stoelinga. Model checking quantitative linear time logic. Electronic Notes in Theoretical Computer Science, 220:61–77, 2008. doi:10.1016/j.entcs.2008.11.019.
[11] Angelo Ferrando, Giulia Luongo, Vadim Malvone, and Aniello Murano. Theory and practice of quantitative ATL. In PRIMA 2024: Principles and Practice of Multi-Agent Systems, volume 15395 of LNCS. Springer, 2024. doi:10.1007/978-3-031-77367-9_18.
[12] Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In CONCUR 2016, volume 59 of LIPIcs, pages 13:1–13:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.CONCUR.2016.13.
[13] Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. Model checking quantitative hyperproperties. In CAV 2018, volume 10981 of LNCS. Springer, 2018. doi:10.1007/978-3-319-96145-3_8.
[14] Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 30:1–30:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.STACS.2017.30.
[15] R. Focardi and R. Gorrieri. Classification of security properties (part I: Information flow). In FOSAD 2000, volume 2171 of LNCS, pages 331–396. Springer, 2000. doi:10.1007/3-540-45608-2_6.
[16] Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV 1995, pages 3–15. Springer, 1995. doi:10.1007/978-0-387-34892-6_1.
[17] Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11–20. IEEE, 1982. doi:10.1109/SP.1982.10014.
[18] Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning about quality in hyperproperties. Technical Report 2512.00500, arXiv, 2025. doi:10.48550/arXiv.2512.00500.
[19] Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279–295, 1997. doi:10.1109/32.588521.
[20] John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In Symposium on Research in Security and Privacy, pages 79–93. IEEE Computer Society, 1994. doi:10.1109/RISP.1994.296590.
[21] C. E. Shannon. The synthesis of two terminal switching circuits. The Bell System Technical Journal, 28(1):59–98, 1949. doi:10.1002/j.1538-7305.1949.tb03624.x.
[22] A. P. Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733–749, 1985. doi:10.1145/3828.3837.
[23] G. Smith. On the foundations of quantitative information flow. In FoSSaCS 2009, volume 5504 of LNCS. Springer, 2009. doi:10.1007/978-3-642-00596-1_21.
[24] Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. In Chris Hankin and Igor Siveroni, editors, Static Analysis, pages 352–367, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. doi:10.1007/11547662_24.
[25] Hirotoshi Yasuoka and Tachio Terauchi. Quantitative information flow as safety and liveness hyperproperties. Theoretical Computer Science, 538:167–182, 2014. doi:10.1016/J.TCS.2013.07.031.
[26] A. Zakinthinos and E.S. Lee. A general theory of security properties. In Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pages 94–102, 1997. doi:10.1109/SECPRI.1997.601322.
[27] Steve Zdancewic and Andrew C. Myers. Observational determinism for concurrent program security. In CSFW 2003. IEEE Computer Society, 2003. doi:10.1109/CSFW.2003.1212703.

[bib.bib1] [1] Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Quantitative Evaluation of Systems. Springer, 2018. doi:10.1007/978-3-319-99154-2_2.

[bib.bib2] [2] Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. Journal of the ACM, 63(3):1–56, 2016. doi:10.1145/2875421.

[bib.bib3] [3] Benedikt Bollig, Paul Gastin, Benjamin Monmege, and Marc Zeitoun. Pebble weighted automata and weighted logics. ACM Trans. Comput. Log., 15(2):15:1–15:35, 2014. doi:10.1145/2579819.

[bib.bib4] [4] Marco Chiesa, Guy Kindler, and Michael Schapira. Traffic engineering with equal-cost-multipath: An algorithmic perspective. IEEE/ACM Transactions on Networking, 25(2):779–792, 2017. doi:10.1109/TNET.2016.2614247.

[bib.bib5] [5] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer Cham, 2020. doi:10.1007/978-3-319-10575-8.

[bib.bib6] [6] M. R. Clarkson, Bernd Finkbeiner, M. Koleini, K. K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In POST 2014, volume 8414 of LNCS, pages 265–284. Springer, 2014. doi:10.1007/978-3-642-54792-8_15.

[bib.bib7] [7] M. R. Clarkson and F. Schneider. Hyperproperties. Journal of Computer Security, 18:1157–1210, 2010. doi:10.1109/CSF.2008.7.

[bib.bib8] [8] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theor. Comput. Sci., 380(1-2):69–86, 2007. doi:10.1016/J.TCS.2007.02.055.

[bib.bib9] [9] Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In CAV 2022, volume 13372 of LNCS, pages 174–187. Springer, 2022. doi:10.1007/978-3-031-13188-2_9.

[bib.bib10] [10] Marco Faella, Axel Legay, and Mariëlle Stoelinga. Model checking quantitative linear time logic. Electronic Notes in Theoretical Computer Science, 220:61–77, 2008. doi:10.1016/j.entcs.2008.11.019.

[bib.bib11] [11] Angelo Ferrando, Giulia Luongo, Vadim Malvone, and Aniello Murano. Theory and practice of quantitative ATL. In PRIMA 2024: Principles and Practice of Multi-Agent Systems, volume 15395 of LNCS. Springer, 2024. doi:10.1007/978-3-031-77367-9_18.

[bib.bib12] [12] Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In CONCUR 2016, volume 59 of LIPIcs, pages 13:1–13:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.CONCUR.2016.13.

[bib.bib13] [13] Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. Model checking quantitative hyperproperties. In CAV 2018, volume 10981 of LNCS. Springer, 2018. doi:10.1007/978-3-319-96145-3_8.

[bib.bib14] [14] Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 30:1–30:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.STACS.2017.30.

[bib.bib15] [15] R. Focardi and R. Gorrieri. Classification of security properties (part I: Information flow). In FOSAD 2000, volume 2171 of LNCS, pages 331–396. Springer, 2000. doi:10.1007/3-540-45608-2_6.

[bib.bib16] [16] Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV 1995, pages 3–15. Springer, 1995. doi:10.1007/978-0-387-34892-6_1.

[bib.bib17] [17] Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11–20. IEEE, 1982. doi:10.1109/SP.1982.10014.

[bib.bib18] [18] Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning about quality in hyperproperties. Technical Report 2512.00500, arXiv, 2025. doi:10.48550/arXiv.2512.00500.

[bib.bib19] [19] Gerard J. Holzmann. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279–295, 1997. doi:10.1109/32.588521.

[bib.bib20] [20] John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In Symposium on Research in Security and Privacy, pages 79–93. IEEE Computer Society, 1994. doi:10.1109/RISP.1994.296590.

[bib.bib21] [21] C. E. Shannon. The synthesis of two terminal switching circuits. The Bell System Technical Journal, 28(1):59–98, 1949. doi:10.1002/j.1538-7305.1949.tb03624.x.

[bib.bib22] [22] A. P. Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733–749, 1985. doi:10.1145/3828.3837.

[bib.bib23] [23] G. Smith. On the foundations of quantitative information flow. In FoSSaCS 2009, volume 5504 of LNCS. Springer, 2009. doi:10.1007/978-3-642-00596-1_21.

[bib.bib24] [24] Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. In Chris Hankin and Igor Siveroni, editors, Static Analysis, pages 352–367, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. doi:10.1007/11547662_24.

[bib.bib25] [25] Hirotoshi Yasuoka and Tachio Terauchi. Quantitative information flow as safety and liveness hyperproperties. Theoretical Computer Science, 538:167–182, 2014. doi:10.1016/J.TCS.2013.07.031.

[bib.bib26] [26] A. Zakinthinos and E.S. Lee. A general theory of security properties. In Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pages 94–102, 1997. doi:10.1109/SECPRI.1997.601322.

[bib.bib27] [27] Steve Zdancewic and Andrew C. Myers. Observational determinism for concurrent program security. In CSFW 2003. IEEE Computer Society, 2003. doi:10.1109/CSFW.2003.1212703.

Reasoning About Quality in Hyperproperties

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

Kripke structures.

Büchi automata.

HyperLTL.

3 Propositional quality for HyperLTL

3.1 Definitions and examples

Definition 1.

Example 2.

Example 3.

Example 4.

3.2 A finite-valued property

Definition 5.

Lemma 6.

3.3 The model checking problem for 𝐇𝐲𝐩𝐞𝐫𝐋𝐓𝐋𝐩𝐫𝐨𝐩

Definition 7.

Proposition 8 ([2]).

Definition 9.

Proposition 10.

Theorem 11.

Corollary 12.

3.4 Expressiveness of 𝐇𝐲𝐩𝐞𝐫𝐋𝐓𝐋𝐩𝐫𝐨𝐩 in the Boolean case

Theorem 13.

4 Temporal quality for HyperLTL

4.1 Definitions and examples

Definition 14.

Example 15.

Example 16.

4.2 Model checking for 𝐇𝐲𝐩𝐞𝐫𝐋𝐓𝐋𝐭𝐞𝐦𝐩

Example 17.

Definition 18.

Automata models for 𝐇𝐲𝐩𝐞𝐫𝐋𝐓𝐋𝐭𝐞𝐦𝐩.

Proposition 19 ([2]).

Lemma 20.

Corollary 21.

Proof.

Issues relative to automata-based model checking.

Example 22.

Approximate model checking.

Definition 23.

Theorem 24.

Proof.

Model checking of the positive and negative fragments.

Definition 25.

Lemma 26.

Proof.

Lemma 27.

Theorem 28.

Proof.

Model checking of the alternation-free fragments.

Theorem 29.

5 Conclusion

References

3.3 The model checking problem for $\mathrm{HyperLTL}_{\mathrm{prop}}$

3.4 Expressiveness of $\mathrm{HyperLTL}_{\mathrm{prop}}$ in the Boolean case

4.2 Model checking for $\mathrm{HyperLTL}_{\mathrm{temp}}$

Automata models for $\mathrm{HyperLTL}_{\mathrm{temp}}$ .