text:
\section{Introduction}

Model checking algorithms~\cite{Clarke/Design-and-Synthesis} are the cornerstone of computer-aided verification. As their input consists of both the system under verification and a logical formula that describes the property to be verified, they uniformly solve a wide range of verification problems, such as all verification problems expressible in linear-time temporal logic (LTL), computation-tree logic (CTL), or the modal $\mu$-calculus. Recently, there has been a lot of interest in extending  model checking from standard trace and tree properties to \emph{information flow} policies like observational determinism or quantitative information flow. Such policies are called \emph{hyperproperties}~\cite{journals/jcs/ClarksonS10} and can be expressed in HyperLTL~\cite{conf/post/ClarksonFKMRS14}, an extension of LTL with trace quantifiers and trace variables. For example, \emph{observational determinism}~\cite{conf/csfw/ZdancewicM03}, the requirement that any pair of traces that have the same observable input also have the same observable output, can be expressed as the following HyperLTL formula:
$ \forall \pi.\forall \pi'.\,(\LTLsquare \pi =_I {\pi'}) \rightarrow (\LTLsquare \pi =_O {\pi'}) $.
For many information flow policies of interest, including observational determinism, there is no longer a need for property-specific algorithms: it has been shown that the standard HyperLTL model checking algorithm~\cite{conf/cav/FinkbeinerRS15} performs just as well as a specialized algorithm for the respective property.

The class of hyperproperties studied in this paper is one where, by contrast, the standard model checking algorithm performes badly. We are interested in \emph{quantitative hyperproperties}, i.e., hyperproperties  that express a bound on the number of traces that may appear
  in a certain relation.
A prominent example of this class of properties is \emph{quantitative non-interference}~\cite{Smith/2009/OnTheFoundationsOfQantitativeInformationFlow,Yasuoka+Terauchi/2010/OnBoundingProblemsOfQuantitativeInformationFlow}, where we allow some flow of information but, at the same time, limit the amount of information that may be leaked. Such properties are used, for example, to describe the correct behavior of a password check, where some information flow is unavoidable (``the password was incorrect''), and perhaps some extra information flow is accceptable (``the password must contain a special character''), but the information should not suffice to guess the actual password.
In HyperLTL, quantitative non-interference can be expressed~\cite{conf/post/ClarksonFKMRS14} as the formula
	$

        \forall \pi_0.\ \forall \pi_1 \ldots \forall \pi_{2^c}.~  \left(\bigwedge_i \LTLsquare ({\pi_i} =_I {\pi_0}) \right) \rightarrow \left(\bigvee_{i \neq j} \LTLsquare ({\pi_i} =_O {\pi_j})\right).
	$
The formula states that there do not exist $2^c+1$ traces (corresponding to more than $c$ bits of information) with the same observable input but different observable output. The bad performance of the
standard model checking algorithm is a consequence of the fact that the $2^{c}+1$ traces are tracked simultaneously. For this purpose, the model checking algorithm builds and analyzes a $(2^c+1)$-fold self-composition of the system.

We present a new model checking algorithm for quantitative hyperproperties that avoids the construction of the huge self-composition. The key idea of our approach is to use \emph{counting} rather than \emph{checking} as the basic operation. Instead of building the self-composition and then \emph{checking} the satisfaction of the formula, we add new atomic propositions and then \emph{count} the number of sequences of evaluations of the new atomic propositions that satisfy the specification. Quantitative hyperproperties are expressions of the following form:
\[ \forall \pi_1. \dots \forall \pi_k.\, \varphi \rightarrow (\# \sigma: X.\, \psi \triangleleft n),\]
where $\triangleleft \in \{\leq,<,\geq,>,=\}$. The universal quantifiers introduce a set of reference traces against which other traces can be compared. The formulas $\varphi$ and $\psi$ are HyperLTL formulas. The counting quantifer $\# \sigma:X.\, \psi$ counts the number of paths $\sigma$ with different valuations of the atomic propositions $X$ that satisfy $\psi$.
The requirement that no more than $c$ bits of information are leaked is the following quantitative hyperproperty:
\[
\forall \pi.\, \# \sigma\colon O. \,  \LTLsquare({\pi} =_I \sigma)  \leq 2^c
\]
As we show in the paper, such expressions do not change the expressiveness of the logic; however, they allow us to express quantitative hyperproperties in exponentially more concise form. The counting-based model checking algorithm then maintains this advantage with a logarithmic counter, resulting in exponentially better performance in both time and space.

The viability of our counting-based model checking algorithm is demonstrated on a Max\#SAT-based prototype implementation. For quantitative hyperproperties of intrest, such as bounded leakage of a password checker, our algorithm shows promising results, as it significantly outperforms existing model checking approaches.

\subsection{Related Work}
Quantitative information-flow has been studied extensively in the literature. See, for example, the following selection of contributions on this topic:~\cite{Smith/2009/OnTheFoundationsOfQantitativeInformationFlow,DBLP:conf/ccs/KopfB07,DBLP:conf/csfw/ClarksonMS05,DBLP:journals/logcom/ClarkHM05,DBLP:journals/jcs/AlvimAP12,DBLP:conf/sp/Gray91}.
Multiple verification methods for quantitative information-flow were proposed for sequential systems. For example, with static analysis techniques~\cite{DBLP:journals/jcs/ClarkHM07}, approximation methods~\cite{DBLP:conf/csfw/KopfR10}, equivalence relations~\cite{cohen1978information,DBLP:conf/sp/BackesKR09}, and randomized methods~\cite{DBLP:conf/csfw/KopfR10}.
Quantitative information-flow for multi-threaded programs was considered in~\cite{DBLP:conf/pldi/ChenM07}.

The study of quantitative information-flow in a reactive setting gained a lot of attention recently after the introduction of hyperproperties~\cite{journals/jcs/ClarksonS10} and the idea of verifying the self-composition of a reactive system~\cite{DBLP:journals/mscs/BartheDR11} in order to relate traces to each other. There are several possibilities to measure the amount of leakage, such as Shannon entropy~\cite{DBLP:books/aw/Denning82,DBLP:journals/jcs/ClarkHM07,DBLP:conf/popl/Malacaria07}, guessing entropy~\cite{DBLP:conf/ccs/KopfB07,DBLP:conf/sp/BackesKR09}, and min-entropy~\cite{Smith/2009/OnTheFoundationsOfQantitativeInformationFlow}.
A classification of quantitative information-flow policies as safety and liveness hyperproperties was given in~\cite{DBLP:journals/tcs/YasuokaT14}.
While several verification techniques for hyperproperties exists~\cite{DBLP:journals/jfp/BanerjeeN05,DBLP:journals/ijisec/HammerS09,DBLP:conf/nordsec/MilushevC13,DBLP:conf/popl/Myers99}, the literature was missing general approaches to quantitative information-flow control. SecLTL~\cite{DBLP:conf/vmcai/DimitrovaFKRS12} was introduced as first general approach to model check (quantitative) hyperproperties, before HyperLTL~\cite{conf/post/ClarksonFKMRS14}, and its corresponding model checker~\cite{conf/cav/FinkbeinerRS15}, was introduced as a temporal logic for hyperproperties, which subsumes the previous approaches.

Using counting to compute the number of solutions of a given formula is studied in the literature as well and includes many probabilistic inference problems, such as Bayesian net reasoning~\cite{DBLP:journals/jar/LittmanMP01}, and planning problems, such as computing robustness of plans in incomplete domains~\cite{DBLP:conf/aaai/MorwoodB12}. State-of-the-art tools for propositional model counting are \texttt{Relsat}~\cite{DBLP:conf/aaai/BayardoS97} and \texttt{c2d}~\cite{DBLP:conf/ecai/Darwiche04}. Algorithms for counting models of temporal logics and automata over infinite words have been introduced in \cite{DBLP:conf/lata/FinkbeinerT14,FTATVA17,Torfah2016}.
The counting of projected models, i.e., when some parts of the models are irrelevant, was studied in~\cite{DBLP:conf/sat/AzizCMS15}, for which tools such as \texttt{\#CLASP}~\cite{DBLP:conf/sat/AzizCMS15} and~\texttt{DSharp\_P}~\cite{DBLP:conf/sat/AzizCMS15,DBLP:conf/ai/MuiseMBH12} exist. Our SAT-based prototype implementation is based on a reduction to a Max\#SAT~\cite{DBLP:conf/aaai/FremontRS17} instance, for which a corresponding tool exists.

Among the already existing tools for computing the amount of information leakage, for example, \texttt{QUAIL}~\cite{DBLP:conf/cav/BiondiLTW13}, which analyzes programs written in a specific while-language and \texttt{LeakWatch}~\cite{DBLP:conf/esorics/ChothiaKN14}, which estimates the amount of leakage in Java programs, \texttt{Moped-QLeak}~\cite{DBLP:conf/fsttcs/ChadhaMS14} is closest to our approach. However, their approach of computing a symbolic summary as an Algebraic Decision Diagram is, in contrast to our approach, solely based on model counting, not maximum model counting.

\section{Preliminaries}
\subsection{HyperLTL}

HyperLTL~\cite{conf/post/ClarksonFKMRS14} extends linear-time temporal logic (LTL) with trace variables and trace quantifiers.
\label{tracevshyper}
Let $\mathit{AP}$ be a set of \emph{atomic propositions}.
A \emph{trace} $t$ is an infinite sequence over subsets of the atomic propositions. We define the set of traces $\mathit{TR} \coloneqq (2^\mathit{AP})^\omega$.
A subset $T \subseteq \mathit{TR}$ is called a \emph{trace property} and a subset $H \subseteq 2^\mathit{TR}$ is called a \emph{hyperproperty}.
We use the following notation to manipulate traces:
let $t \in \mathit{TR}$ be a trace and $i \in \mathbb{N}$ be a natural number. $t[i]$ denotes the $i$-th element of $t$. Therefore, $t[0]$ represents the starting element of the trace. Let $j \in \mathbb{N}$ and $j \geq i$. $t[i,j]$ denotes the sequence $t[i]~t[i+1]\ldots t[j-1]~t[j]$. $t[i, \infty]$ denotes the infinite suffix of $t$ starting at position $i$.

\paragraph{HyperLTL Syntax.}
Let $\mathcal{V}$ be an infinite supply of trace variables.  The syntax of HyperLTL is given by the following grammar:
\begin{align*}
	\psi~&\Coloneqq~\exists \pi.\;\psi~~|~~\forall\pi.\;\psi~~|~~\varphi \\
	\varphi~&\Coloneqq~a_{\pi}~~|~~\neg \varphi~~|~~\varphi \vee \varphi~~|~~\LTLnext \varphi~~|~~\varphi\, \LTLuntil \varphi
\end{align*}
where $a\in \mathit{AP}$ is an atomic proposition and $\pi \in \mathcal V$ is a trace variable. Note that atomic propositions are indexed by trace variables.
The quantification over traces makes it possible to express properties like ``on all traces $\psi$ must hold'', which is expressed by $\forall \pi.~\psi$. Dually, one can express that ``there exists a trace such that $\psi$ holds'', which is denoted by $\exists \pi.~\psi$. The derived operators $\LTLdiamond$, $\LTLsquare$, and $\mathcal W$ are defined as for LTL.
We abbreviate the formula $\bigwedge_{x\in X} (x_\pi \leftrightarrow x_{\pi'})$, expressing that the traces $\pi$ and $\pi'$ are equal with respect to a set $X \subseteq \mathit{AP}$ of atomic propositions, by $\pi =_X \pi'$.
Furthermore, we call a trace variable $\pi$ free in a HyperLTL formula if there is no quantification over $\pi$ and we call a HyperLTL formula $\varphi$ closed if there exists no free trace variable in $\varphi$.

\paragraph{HyperLTL Semantics.}
A HyperLTL formula defines a \emph{hyperproperty}, i.e., a set of sets of traces. A set $T$ of traces satisfies the hyperproperty if it is an element of this set of sets.
Formally, the semantics of HyperLTL formulas is given with respect to a \emph{trace assignment} $\Pi$ from $\mathcal{V}$ to $\mathit{TR}$, i.e., a partial function mapping trace variables to actual traces. $\Pi[\pi \mapsto t]$ denotes that $\pi$ is mapped to $t$, with everything else mapped according to $\Pi$. $\Pi[i,\infty]$ denotes the trace assignment that is equal to $\Pi(\pi)[i,\infty]$ for all $\pi$.
\begin{align*}
	&\Pi \models_T~\exists \pi. \psi &&\text{iff}\hspace{5ex} \text{there exists}~t \in T~:~ \Pi[\pi \mapsto t] \models_T \psi \\
	&\Pi \models_T~\forall \pi. \psi &&\text{iff}\hspace{5ex} \text{for all}~t \in T~:~ \Pi[\pi \mapsto t] \models_T \psi \\
	&\Pi \models_T~a_{\pi} &&\text{iff}\hspace{5ex} a \in \Pi(\pi)[0] \\
	&\Pi \models_T~\neg \psi &&\text{iff}\hspace{5ex} \Pi \not \models_T \psi \\
	&\Pi \models_T~\psi_1 \vee \psi_2 &&\text{iff}\hspace{5ex} \Pi \models_T \psi_1~\text{or}~\Pi \models_T \psi_2 \\
	&\Pi \models_T~\LTLnext \psi &&\text{iff}\hspace{5ex} \Pi[1,\infty] \models_T \psi \\
	&\Pi \models_T~\psi_1 \LTLuntil \psi_2 &&\text{iff}\hspace{5ex} \text{there exists}~i \geq 0 : \Pi[i,\infty] \models_T \psi_2 \\
	& &&\hspace{7.2ex} \text{and for all}~0 \leq j < i~\text{we have}~\Pi[j,\infty] \models_T \psi_1
\end{align*}
We say a set of traces $T$ \emph{satisfies} a HyperLTL formula $\varphi$ if $\Pi \models_T \varphi$, where $\Pi$ is the empty trace assignment.

\subsection{System model}
A \emph{Kripke structure} is a tuple $K=(S,s_0,\delta,\mathit{AP},L)$ consisting of a set of states $S$, an initial state $s_0 \in S$, a transition function $\delta: S \rightarrow 2^S$, a set of \emph{atomic propositions} $\mathit{AP}$, and a \emph{labeling function} $L : S \rightarrow 2^\mathit{AP}$, which labels every state with a set of atomic propositions. We assume that each state has a successor, i.e., $\delta(s) \not = \emptyset$. This ensures that every run on a Kripke structure can always be extended to an infinite run. We define a \emph{path} of a Kripke structure as an infinite sequence of states $s_0s_1\dots \in S^\omega$ such that $s_0$ is the initial state of $K$ and $s_{i+1} \in \delta(s_i)$ for every $i \in \mathbb{N}$. We denote the set of all paths of $K$ that start in a state $s$ with $\mathit{Paths}(K,s)$. Furthermore, $\mathit{Paths}^*(K,s)$ denotes the set of all path prefixes and $\mathit{Paths}^\omega(K,s)$ the set of all path suffixes. A \emph{trace} of a Kripke structure is an infinite sequence of sets of atomic propositions $L(s_0),L(s_1),\dots \in (2^\mathit{AP})^\omega$, such that $s_0$ is the initial state of $K$ and $s_{i+1} \in \delta(s_i)$ for every $i \in \mathbb{N}$.
We denote the set of all traces of $K$ that start in a state $s$ with $\mathit{TR}(K,s)$.
We say that a Kripke structure $K$ \emph{satisfies} a HyperLTL formula $\varphi$ if its set of traces satisfies $\varphi$, i.e., if  $\Pi \models_{\mathit{TR}(K,s_0)} \varphi$, where $\Pi$ is the empty trace assignment.

\subsection{Automata over infinite words}
In our construction we use automata over infinite words. A \emph{B\"uchi automaton} is a tuple $\mathcal B = (Q,Q_0,\delta,\Sigma,F)$, where $Q$ is a set of states, $Q_0$ is a set of initial states, $\delta: Q \times \Sigma \rightarrow 2^Q$ is a transition relation, and $F\subset Q$ are the accepting states.
A run of $\mathcal B$ on an infinite word $w = \alpha_1 \alpha_2 \dots \in \Sigma^\omega$ is an infinite sequence $r = q_0 q_1 \dots \in Q^\omega$ of states, where $q_0 \in Q_0$ and for each $i \ge 0$, $q_{i+1} = \delta(q_i,\alpha_{i+1})$.
We define $\textbf{Inf}(r)=\{q \in Q \mid \forall i \exists j>i.~r_j = q\}$.
A run $r$ is called accepting if $\textbf{Inf}(r) \cap F \not = \emptyset$.
A word $w$ is accepted by $\mathcal B$ and called a \emph{model} of $\mathcal B$ if there is an accepting run of $\mathcal B$ on $w$.

Furthermore, an \emph{alternating automaton}, whose runs generalize from sequences to trees, is a tuple $\mathcal A = (Q,Q_0,\delta,\Sigma,F)$. $Q,Q_0, \Sigma$, and $F$ are defined as above and $\delta: Q \times \Sigma \rightarrow \mathbb{B}^+{Q}$ being a transition function, which maps a state and a symbol into a Boolean combination of states. Thus, a run(-tree) of an alternating B\"uchi automaton $\mathcal A$ on an infinite word $w$ is a $Q$-labeled tree.
A word $w$ is accepted by $\mathcal{A}$ and called a \emph{model} if there exists a run-tree $T$ such that all paths $p$ trough $T$ are accepting, i.e., $\textbf{Inf}(p) \cap F \not = \emptyset$.

A strongly connected component (SCC) in $\mathcal A$  is a maximal strongly connected component of the graph induced by the automaton.
An SCC is called \emph{accepting} if one of its states is an accepting state in $\mathcal A$.

\section{Quantitative Hyperproperties}

Quantitative Hyperproperties are properties of sets of computation traces that express a bound on the number of traces that may appear in a certain relation.
In the following, we study quantitative hyperproperties that are specified in terms of HyperLTL formulas.
We consider expressions of the following general form:
\[
\forall \pi_1,\dots,\pi_k.\ \varphi \rightarrow (\# \sigma: A.\ \psi  \triangleleft n)
\]
Both the universally quantified variables $\pi_1,\dots,\pi_k$ and the variable $\sigma$ after the \emph{counting} operator $\#$ are trace variables; $\varphi$ is a HyperLTL formula over atomic propositions $AP$ and free trace variables $\pi_1 \ldots \pi_k$;
$A \subseteq AP$ is a set of atomic propositions;
$\psi$ is a HyperLTL formula over atomic propositions $AP$ and free trace variables $\pi_1 \ldots \pi_k$ and, additionally $\sigma$.
The operator $\triangleleft \in \{<,\leq,=,>,\geq\}$ is a comparison operator; and $n \in \mathbb{N}$ is a natural number.

For a given set of traces $T$ and a valuation of the trace variables $\pi_1,\dots,\pi_k$, the term $\# \sigma: A.\, \psi$ computes the number of traces $\sigma$ in $T$ that differ in their valuation of the atomic propositions in $A$ and satisfy $\psi$.
The expression $\# \sigma: A.\, \psi  \triangleleft n$ is $\mathit{true}$ iff the resulting number satisfies the comparison with $n$.
Finally, the complete expression $\forall \pi_1,\dots,\pi_k.\,\varphi \rightarrow (\# \sigma: A.\, \psi  \triangleleft n)$ is $\mathit{true}$ iff for all combinations $\pi_1,\dots,\pi_k$ of traces in $T$ that satisfy $\varphi$, the comparison $\# \sigma: A.\, \psi  \triangleleft n$ is satisfied.

\begin{example}[Quantitative non-interference]
  \label{quantnon}
Quantitative information-flow policies~\cite{Gray/1991/TowardAMathematicalFoundationForIFSecurity,DBLP:journals/entcs/ClarkHM05,DBLP:conf/ccs/KopfB07,DBLP:journals/jcs/ClarksonMS09} allow the flow of a bounded amount of information.
One way to measure leakage is with \emph{min-entropy}~\cite{Smith/2009/OnTheFoundationsOfQantitativeInformationFlow}, which quantifies the amount of information an attacker can gain given the answer to a single guess about the secret.
The \emph{bounding problem}~\cite{Yasuoka+Terauchi/2010/OnBoundingProblemsOfQuantitativeInformationFlow} for min-entropy is to determine whether that amount is bounded from above by a constant $2^c$, corresponding to $c$ bits.
We assume that the program whose leakage is being quantified is deterministic, and assume that the secret input to that program is uniformly distributed.
The bounding problem then reduces to determining that there is no tuple of $2^c+1$ distinguishable traces~\cite{Smith/2009/OnTheFoundationsOfQantitativeInformationFlow,Yasuoka+Terauchi/2010/OnBoundingProblemsOfQuantitativeInformationFlow}. Let $O \subseteq AP$ be the set of observable outputs. A simple quantitative information flow policy is then the following quantitative hyperproperty, which bounds the number of distinguishable outputs to $2^c$, corresponding to a bound of $c$ bits of information:
	$$
		\# \sigma: O.\ \mathit{true} \leq 2^c
	$$
                A slightly more complicated information flow policy is quantitative non-interference. In quantitative non-interference, the bound must be satisfied for every individual input. Let $I \subseteq AP$ be the observable inputs to the system. Quantitative non-interference is the following quantitative hyperproperty\footnote{We write $\pi =_A \pi'$ short for $\pi_A = \pi'_A$ where $\pi_A$ is the $A$-projection of $\pi$}:
        $$
	\forall \pi.\, \# \sigma\colon O.\ ( \LTLsquare({\pi} =_I \sigma) ) \leq 2^c
	$$
For each trace $\pi$ in the system, the property checks whether there are more than $2^c$ traces $\sigma$ that have the same observable input as $\pi$ but different observable output.
\end{example}

\begin{example}[Deniability]
A program satisfies \emph{deniability} (see, for example,~\cite{DBLP:journals/pvldb/BindschaedlerSG17,DBLP:journals/popets/ChakrabortiCS17}) when there is no proof that a certain input occurred from simply observing the output, i.e., given an output of a program one cannot derive the input that lead to this output. A deterministic program satisfies deniability when each output can be mapped to at least two inputs. A quantitative variant of deniability is when we require that the number of corresponding inputs is larger than a given threshold. Quantitative deniability can be specified as the following quantitative Hyperproperty:
 $$
\forall \pi.\, \# \sigma \colon I.\, (\LTLsquare (\pi =_O \sigma))  > n
$$
For all traces $\pi$ of the system we count the number of sequences $\sigma$ in the system with different input sequences and the same output sequence of $\pi$, i.e., for the fixed output sequence given by $\pi $ we count the number of input sequences that lead to this output.
\end{example}

\section{Model Checking Quantitative Hyperproperties}
We present a model checking algorithm for quantitative hyperproperties based on model counting.
The advantage of the algorithm is that its runtime complexity is independent of the bound $n$ and thus avoids the $n$-fold self-composition necessary for any encoding of the quantitative hyperproperty in {\sc HyperLTL}\@\xspace.

Before introducing our novel counting-based algorithm, we start by a translation of quantitative hyperproperties into formulas in {\sc HyperLTL}\@\xspace and establishing an exponential lower bound for its representation.

\subsection{Standard model checking algorithm: encoding quantitative hyperproperties in HyperLTL}
The idea of the reduction is to check a lower bound of $n$
traces by existentially quantifying over $n$ traces, and to check an
upper bound of $n$ traces by \emph{universally} quantifying over $n+1$ traces.
The resulting HyperLTL formula can be verified using the standard
model checking algorithm for HyperLTL~\cite{conf/post/ClarksonFKMRS14}.

\begin{theorem}
  Every quantitative hyperproperty
  $
  \forall \pi_1,\dots,\pi_k.\ \psi_\iota \rightarrow (\# \sigma: A.\ \psi  \triangleleft n)
  $
  can be expressed as a HyperLTL formula. For $\triangleleft \in \{\leq\} (\{<\})$, the HyperLTL formula has $n+k+1 (\text{resp. } n+k)$ universal trace quantifiers in addition to the quantifiers in $\psi_\iota$ and $\psi$.
  For $\triangleleft \in \{\geq\} (\{>\})$, the HyperLTL formula has $k$ universal trace quantifiers and $n$ $(\text{resp. } n+1)$ existential trace quantifiers in addition to the quantifiers in $\psi_\iota$ and $\psi$. For $\triangleleft \in \{=\}$, the HyperLTL formula has $n+k+1$ universal trace quantifiers and $n$ existential trace quantifiers in addition to the quantifiers in $\psi_\iota$ and $\psi$.
\end{theorem}
\begin{proof}
For $\triangleleft \in \{\leq \}$, we encode the quantitative hyperproperty $\forall \pi_1,\dots,\pi_k.\ \psi_\iota \rightarrow (\# \sigma: A.\ \psi \triangleleft n)$ as the following HyperLTL formula:
\[
  \forall \pi_1,\dots,\pi_k.\ \forall \pi'_1, \ldots, \pi'_{n+1}.\ \left( \psi_\iota \wedge \bigwedge_{i\neq j} \LTLdiamond({\pi'_i}\neq_A {\pi'_j})\right) \rightarrow \left(\bigvee_i \neg \psi[\sigma \mapsto \pi'_i]\right)
\]
where $\psi[\sigma \mapsto \pi'_i]$ is the HyperLTL formula $\psi$ with all occurrences of $\sigma$ replaced by $\pi'_i$.
The formula states that there is no tuple of $n+1$ traces $\pi'_1, \ldots, \pi'_{n+1}$ different in the evaluation of $A$, that satisfy $\psi$. In other words, for every $n+1$ tuple of traces $\pi'_1, \ldots, \pi'_{n+1}$ that differ in the evaluation of $A$, one of the paths must violate $\psi$.
For $\triangleleft \in \{ <\}$, we use the same formula, with $\forall \pi'_1, \ldots, \pi'_{n}$ instead of $\forall \pi'_1, \ldots, \pi'_{n+1}$.

For  $\triangleleft \in \{\geq \}$, we encode the quantitative hyperproperty analogously as the HyperLTL formula
\[
  \forall \pi_1,\dots,\pi_{k}.\ \exists \pi'_1, \ldots, \pi'_{n}.\ \psi_\iota \rightarrow \left(  \bigwedge_{i\neq j} \LTLdiamond({\pi'_i}\neq_A {\pi'_j})\right) \wedge \left(\bigwedge_i \psi[\sigma \mapsto \pi'_i]\right)
\]
The formula states that there exist paths $\pi'_1, \ldots, \pi'_{n}$ that differ in the evaluation of $A$ and that all satisfy $\psi$.
For $\triangleleft \in \{ >\}$, we use the same formula, with $\exists \pi'_1, \ldots, \pi'_{n+1}$ instead of $\forall \pi'_1, \ldots, \pi'_{n}$.
Lastly, for $\triangleleft \in \{ = \}$, we encode the quantitative hyperproperty as a conjunction of the encodings for $\leq$ and for $\geq$.
\end{proof}

\begin{example}[Quantitative non-interference in HyperLTL]
	 As discussed in Example~\ref{quantnon}, quantitative non-interference is the quantitative hyperproperty
	 $$\forall \pi.\, \# \sigma\colon O. \, \LTLsquare({\pi} =_I \sigma) \leq 2^c,$$ where we measure the amount of leakage with min-entropy~\cite{Smith/2009/OnTheFoundationsOfQantitativeInformationFlow}.
	The bounding problem for min-entropy asks whether the amount of information leaked by a system is bounded by a constant $2^c$ where $c$ is the number of bits. This is encoded in HyperLTL as the requirement that there are no $2^{c}+1$ traces distinguishable in their output:
		\[

	\forall \pi_0.\ \forall \pi_1 \ldots \forall \pi_{2^c}.~  \left(\bigwedge_i \LTLsquare ({\pi_i} =_I {\pi_0}) \right) \rightarrow \left(\bigvee_{i \neq j} \LTLsquare ({\pi_i} =_O {\pi_j})\right).
	\]
        This formula is equivalent to the formalization of quantitative non-interference given in \cite{conf/cav/FinkbeinerRS15}.
\end{example}

Model checking quantitative hyperproperties via the reduction to HyperLTL is very expensive. In the best case, when $\triangleleft \in \{\leq, < \}$, $\psi_\iota$ does not contain existential quantifiers, and $\psi$ does not contain universal quantifiers, we obtain an HyperLTL formula without quantifier alternations, where the number of quantifiers grows linearly with the bound $n$. For $m$ quantifiers, the HyperLTL model checking algorithm~\cite{conf/cav/FinkbeinerRS15} constructs and analyzes the $m$-fold self-composition of the Kripke structure. The running time of the model checking algorithm is thus exponential in the bound. If  $\triangleleft \in \{\geq, >, = \}$, the encoding additionally introduces a quantifier alternation. The model checking algorithm checks quantifier alternations via a complementation of B\"uchi automata, which adds another exponent, resulting in an overall doubly exponential running time.

The model checking algorithm we introduce in the next section avoids the $n$-fold self-composition needed in the model checking algorithm of HyperLTL and its complexity is independent of the bound $n$.

\subsection{Counting-based model checking algorithm}
A Kripke structure $K= (S,s_0, \tau, \textit{AP}, L)$ violates a quantitative hyperproperty
$$\varphi = \forall \pi_1, \dots, \pi_k.~ \psi_\iota \rightarrow (\# \sigma : A. \psi \triangleleft n )$$
if there is a $k$-tuple $t=(\pi_1,\dots,\pi_k)$ of traces $\pi_i \in \textit{TR}(K)$ that satisfies the formula
\[
  \exists \pi_1,\dots,\pi_k.\ \psi_\iota \wedge (\# \sigma: A.\ \psi\,  \overline{\triangleleft}\, n)
  \]
where $\overline{\triangleleft}$ is the negation of the comparison operator $\triangleleft$. The tuple~$t$ then satisfies the property $\psi_\iota$ and the number of $(k+1)$-tuples $t'=(\pi_1,\dots, \pi_k, \sigma)$ for $\sigma \in \textit{TR}(K)$  that satisfy $\psi$ and differ pairwise in the $A$-projection of $\sigma$ satisfies the comparison $\overline\triangleleft~n$ (The $A$-projection of a sequence $\sigma$ is defined as the sequence $\sigma_A \in (2^A)^\omega$, such that for every position $i$ and every $a \in A$ it holds that $a \in \sigma_A[i]$ if and only if  $a \in \sigma[i]$).
The tuples $t'$ can be captured by the automaton composed of the product of an automaton $A_{\psi_\iota \wedge \psi}$ that accepts all $k+1$ of traces that satisfy both $\psi_\iota$ and $\psi$ and a $k+1$-self composition of $K$. Each accepting run of the product automaton presents $k+1$ traces of $K$ that satisfy $\psi_\iota \wedge \psi$. On top of the product automaton, we apply a special counting algorithm which we explain in detail in Section~\ref{sec:countingalgo} and check if the result satisfies the comparison~$\overline\triangleleft~n$.

Algorithm~\ref{alg:mcqhyper} gives a general picture of our model checking algorithm. The algorithm has two parts. The first part applies if the relation $\overline \triangleleft$ is one of $\{\ge , >\}$. In this case, the algorithm checks whether a sequence over $\textit{AP}_\psi$ (propositions in $\psi$) corresponds to infinitely many sequences over $A$. This is done by checking whether the product automaton $B$ has a so-called  \emph{doubly pumped lasso}(DPL), a subgraph with two connected lassos, with a unique sequence over $\textit{AP}_\psi$ and different sequences over $A$. Such a doubly pumped lasso matches the same sequence over $\textit{AP}_\psi$ with infinitely many sequences over $A$ (more in section~\ref{sec:countingalgo}). If no doubly pumped lasso is found, a projected model counting algorithm is applied in the second part of the algorithm in order to compute either the maximum or the minimum value, corresponding to the comparison operator $\overline \triangleleft$. In the next subsections, we explain the individual parts of the algorithm in detail.
\begin{algorithm}[t]
\scriptsize
\begin{algorithmic}[1]
	\REQUIRE Quantitative Hyperproperty $\varphi =\forall \pi_1 \dots \pi_k.~ \psi_\iota \rightarrow (\# \sigma : A. \psi \triangleleft n )$, Kripke Structure $K= (S,s_0, \tau, \textit{AP}, L)$
	\ENSURE $K \models \varphi$
	\STATE $B =\textit{QHLTL2BA}(K,\pi_1,\dots,\pi_k,\psi_\iota \wedge \psi)$
	\STATE /*Check Infinity*/
	\IF{$\overline \triangleleft \in \{\ge, >\} $}
	\STATE $\textit{ce} = \textit{DPL}(B)$
	\IF{$\textit{ce} \not = \bot$}
		\RETURN \textit{ce}
	\ENDIF
	\ENDIF
	\STATE /*Apply Projected Counting Algorithm*/
	\IF{$\overline \triangleleft \in \{\ge, >\}$}
		\STATE $\textit{ce} = \textit{MaxCount}(B,n,\overline\triangleleft)$
	\ELSE
		\STATE $\textit{ce} = \textit{MinCount}(B,n,\overline\triangleleft)$
	\ENDIF
	\RETURN \textit{ce}
\end{algorithmic}
\caption{\small Counting-based Model Checking of Quantitative Hyperproperties}
\label{alg:mcqhyper}
\end{algorithm}

\subsection{B\"uchi automata for quantitative hyperproperties}
For a quantitative hyperproperty $\varphi= \forall \pi_1 \dots \pi_k.~ \psi_\iota \rightarrow (\# \sigma : A. \psi \triangleleft n )$ and a Kripke structure $K=(S,s_0, \tau, \textit{AP}, L)$, we first construct an alternating automaton $A_{\psi_{\iota} \wedge \psi}$ for the {\sc HyperLTL}\@\xspace property $\psi_{\iota} \wedge \psi$.
Let $A_{\psi_1} = (Q_1,q_{0,1}, \Sigma_2, \delta_1, F_1)$ and $A_{\psi_2} = (Q_2,q_{0,2}, \Sigma_2, \delta_2, F_2)$ be alternating automata for subformulas $\psi_1$ and $\psi_2$. Let $\Sigma= 2^{\textit{AP}_\varphi}$ where $AP_\varphi$ are all indexed atomic propositions that appear in $\varphi$. $A_{\psi_{\iota} \wedge \psi}$ is constructed using following rules\footnote{The construction
follows the one presented in  \cite{conf/cav/FinkbeinerRS15} with a slight modification on the labeling of transitions. Labeling over atomic proposition instead of the states of the Kripke structure suffices, as any nondeterminism in the Kripke structure is inherently resolved, because we quantify over trace not paths}:
\begin{center}
\scriptsize
\begin{tabular}{|c||c|}
\hline
$\varphi = a_\pi$ & $A_\varphi = (\{q_0\},q_0,\Sigma,\delta,\emptyset)$ where $\delta(q_0,\alpha)= (a_\pi \in \alpha)$\\
\hline
$\varphi = \neg a_\pi$ & $A_\varphi = (\{q_0\},q_0,\Sigma,\delta,\emptyset)$ where $\delta(q_0,\alpha)= (a_\pi \not \in \alpha)$\\
\hline
$\varphi = \psi_1 \wedge \psi_2$ & $A_\varphi = (Q_1 \charfusion[\mathbin]{\cup}{\cdot} Q_2 \charfusion[\mathbin]{\cup}{\cdot} \{q_0\}, q_0, \Sigma, \delta, F_1 \charfusion[\mathbin]{\cup}{\cdot} F_2)$ \\
& where $\delta(q,\alpha) = \delta_1(q_{0,1},\alpha) \wedge \delta_2(q_{0,2},\alpha)$\\
& \quad and $\delta(q,\alpha) = \delta_i(q,\alpha)$ when $q\in Q_i$ for $i\in \{1,2\}$\quad \quad \\
\hline
$\varphi = \psi_1 \vee \psi_2$ & $A_\varphi = (Q_1 \charfusion[\mathbin]{\cup}{\cdot} Q_2 \charfusion[\mathbin]{\cup}{\cdot} \{q_0\}, q_0, \Sigma, \delta, F_1 \charfusion[\mathbin]{\cup}{\cdot} F_2)$ \\
& where $\delta(q,\alpha) = \delta_1(q_{0,1},\alpha) \vee \delta_2(q_{0,2},\alpha)$\\
& and $\delta(q,\alpha) = \delta_i(q,\alpha)$ when $q\in Q_i$ for $i\in \{1,2\}$\\
\hline
$\varphi = \LTLcircle \psi_1$ & $A_\varphi = (Q_1 \charfusion[\mathbin]{\cup}{\cdot}\{q_0\}, q_0, \Sigma, \delta, F_1)$  \\
& where $\delta(q,\alpha) = q_{0,1}$ \\
& and $\delta(q,\alpha) = \delta_1(q,\alpha) $ for $q \in Q_1$\\
\hline
$\varphi = \psi_1 \LTLuntil \psi_2$ & $A_\varphi = (Q_1 \charfusion[\mathbin]{\cup}{\cdot} Q_2 \charfusion[\mathbin]{\cup}{\cdot} \{q_0\}, q_0, \Sigma, \delta, F_1 \charfusion[\mathbin]{\cup}{\cdot} F_2)$\\
& where $\delta(q_0,\alpha) = \delta_2(q_{0,2}, \alpha) \vee (\delta_1(q_{0,1},\alpha) \wedge q_0)$\\
& and $\delta(q,\alpha) = \delta_i(q,\alpha)$ when $q\in Q_i$ for $i\in \{1,2\}$\\
\hline
$\varphi = \psi_1 \LTLrelease \psi_2$ & $A_\varphi = (Q_1 \charfusion[\mathbin]{\cup}{\cdot} Q_2 \charfusion[\mathbin]{\cup}{\cdot} \{q_0\}, q_0, \Sigma, \delta, F_1 \charfusion[\mathbin]{\cup}{\cdot} F_2 \charfusion[\mathbin]{\cup}{\cdot} \{q_0\})$\\
& where $\delta(q_0,\alpha) = \delta_2(q_{0,2}, \alpha) \wedge (\delta_1(q_{0,1},\alpha) \vee q_0)$\\
& and $\delta(q,\alpha) = \delta_i(q,\alpha)$ when $q\in Q_i$ for $i\in \{1,2\}$\\
\hline
\end{tabular}
\end{center}
For a quantified formula $\varphi = \exists\pi. \psi_1$, we construct the product automaton of the Kripke structure $K$ and the B\"uchi automaton  of $\psi_1$. Here we reduce the alphabet of the automaton by projecting all atomic proposition in $\textit{AP}_\pi$ away:
\begin{center}
\scriptsize
\begin{tabular}{|c||c|}
\hline
	$\varphi = \exists \pi. \psi_1$ & $A_\varphi = (Q_1 \times S \charfusion[\mathbin]{\cup}{\cdot} \{q_0\}, \Sigma \setminus \textit{AP}_\pi,\delta,  F_1 \times S ) $\\
& where $\delta(q_0, \alpha ) = \{(q',s') \mid q' \in \delta_1(q_{0,1},\alpha \cup \alpha'), s' \in \tau(s_0), (L(s_0))_\pi =_{\textit{AP}_\pi} \alpha'\}$\\
& and $\delta((q,s),\alpha) = \{(q',s') \mid  q' \in \delta_1(q, \alpha\cup \alpha'), s' \in \tau(s), (L(s))_\pi =_{\textit{AP}_\pi} \alpha' \}$\\
\hline

\end{tabular}
\end{center}
Given the B\"uchi automaton for the hyperproperty $\psi_\iota \wedge \psi$ it remains to construct the product with the $k+1$-self composition of $K$. The transitions of the automaton are defined over labels from $\Sigma= 2^{\textit{AP}^*}$ where $AP^* ={\textit{AP}_\sigma \cup \bigcup_i \textit{AP}_{\pi_i}}$. $A_{\psi_{\iota} \wedge \psi}$. This is necessary to identify which transition was taken in each copy of $K$, thus, mirroring a tuple of traces in $K$. For each of the variables $\pi_1,\dots \pi_k$ and $\sigma$ we use following rule:
\begin{center}
\scriptsize
\begin{tabular}{|c||c|}
\hline
	$\varphi = \exists \pi. \psi_1$ & $A_\varphi = (Q_1 \times S \charfusion[\mathbin]{\cup}{\cdot} \{q_0\}, \Sigma,\delta,  F_1 \times S ) $\\
& where $\delta(q_0, \alpha ) = \{(q',s') \mid q' \in \delta_1(q_{0,1},\alpha), s' \in \tau(s_0), (L(s_0))_\pi =_{\textit{AP}_\pi} \}$\\
& and $\delta((q,s),\alpha) = \{(q',s') \mid  q' \in \delta_1(q, \alpha), s' \in \tau(s), (L(s))_\pi =_{\textit{AP}_\pi}  \}$\\
\hline

\end{tabular}
\end{center}
Finally, we transform the resulting alternating automaton to an equivalent B\"uchi automaton following the construction of Miyano and Hayashi~\cite{MIYANO1984321}.

\subsection{Counting models of $\omega$-Automata}
\label{sec:countingalgo}
Computing the number of words accepted by a B\"uchi automaton can be done by examining its accepting lassos.
Consider, for example, the B\"uchi automata over the alphabet $2^{\{a\}}$ in Figure~\ref{fig:automodels}. The automaton on the left  has one accepting lasso $(q_0)^\omega$ and thus has only one model, namely $\{a\}^\omega$. The automaton on the right  has infinitely many  accepting lassos $(q_0\{\})^i\{a\}(q_1(\{\} \vee \{a\}))^\omega$ that accept infinitely many different words all of the from $\{\}^*\{a\}(\{\}\vee \{a\})^\omega$.
\begin{figure}
\centering
\begin{tikzpicture}
\node(a1)[circle,double,draw,initial]at(0,0){$q_0$};
\node(a2)[circle,draw]at(2,0){$q_1$};
\path[->,draw](a1) edge [loop above] node{$a$}(a1);
\path[->,draw](a1) edge node[above]{$\neg a$} (a2);
\path[->,draw](a2) edge [loop above] node{$*$}(a2);
\end{tikzpicture}
\hspace{2cm}
\begin{tikzpicture}
\node(a1)[circle,draw,initial]at(0,0){$q_0$};
\node(a2)[circle,double,draw]at(2,0){$q_1$};
\path[->,draw](a1) edge [loop above] node{$\neg a$}(a1);
\path[->,draw](a1) edge node[above]{$a$} (a2);
\path[->,draw](a2) edge [loop above] node{$*$}(a2);
\end{tikzpicture}
\caption[]{\scriptsize B\"uchi automata with one model (left) and infinitely many models (right).}
\label{fig:automodels}
\end{figure}
Computing the models of a B\"uchi automaton is insufficient for model checking quantitative hyperproperties as we are not interested in the total number of models. We rather \emph{maximize}, respectively \emph{minimize}, over sequences of subsets of atomic propositions \emph{the number of projected models} of the B\"uchi automaton. For instance, consider the automaton given in Figure~\ref{fig:autohypermodels}.
\begin{figure}
\centering
\begin{tikzpicture}
\node(a1)[circle,draw,initial]at(0,0){$q_0$};
\node(a2)[circle,double,draw]at(2,0){$q_1$};
\path[->,draw](a1) edge [loop above] node{$\neg a \wedge b$}(a1);
\path[->,draw](a1) edge node[above]{$a$} (a2);
\path[->,draw](a2) edge [loop above] node{$b$}(a2);
\end{tikzpicture}
\caption[]{\scriptsize A two-state B\"uchi automaton, such that there exist exactly two $\{b\}$-projected models for each $\{a\}$-projected sequence.}
\label{fig:autohypermodels}
\end{figure}
The automaton has infinitely many models. However, the maximum number of sequences $\sigma_b \in 2^{\{b\}}$ that correspond to accepting lassos in the automaton with a unique sequence $\sigma_a \in 2^{\{a\}}$ is two: For example, let $n$ be a natural number. For any model of the automaton and for each sequence $\sigma_a := \{\}^n\{a\}(\{\})^\omega$ the automaton accepts the following two sequences: $\{b\}^n\{\}\{b\}^\omega$ and $\{b\}^\omega$.
Formally, given a B\"uchi automaton $\mathcal{B}$ over $\mathit{AP}$ and a set $A$, such that $A \subseteq \mathit{AP}$, an \emph{$A$-projected model} (or projected model over $A$) is defined as a sequence $\sigma_A \in (2^\mathit{A})^\omega$ that results in the $A$-projection of an accepting sequence $\sigma \in (2^\mathit{AP})^\omega$.

In the following, we define the maximum model counting problem over automata and give an algorithm for solving the problem. We show  how to use the algorithm for model checking quantitative hyperproperties.

\begin{definition}[Maximum Model Counting over Automata (MMCA)]
	Given a B\"uchi automaton $B$ over an alphabet $2^\textit{AP}$ for some set of atomic propositions $\textit{AP}$ and sets $X,Y,Z \subseteq \textit{AP}$ the maximum model counting problem is to compute $$\max \limits_{\sigma_Y \in (2^{Y})^\omega} |\{\sigma_X \in (2^{X})^\omega \mid \exists \sigma_Z \in(2^{Z})^\omega.~ \sigma_X\cup\sigma_Y\cup\sigma_Z \in L(B)\}|$$
	where $\sigma \cup \sigma'$ is the point-wise union of $\sigma $ and $\sigma'$.
\end{definition}
As a first step in our algorithm, we show how to check whether the maximum model count is equal to infinity.
\begin{definition}[Doubly Pumped Lasso]
For a graph $G$, a doubly pumped lasso in $G$ is a subgraph that entails a cycles $C_1$ and another different cycle $C_2$ that is reachable from $C_1$.
\end{definition}
\vskip -1cm
\begin{figure}
\centering
\begin{tikzpicture}
\coordinate(p1)at(0,0);
\fill (p1) circle (1pt);
\coordinate(p2)at(0.25,0);
\fill (p2) circle (1pt);
\draw[->](p1)--(p2);
\coordinate(p3)at(0.5,0);
\fill (p3) circle (1pt);
\draw[->](p2)--(p3);
\coordinate(p4)at(0.75,0);
\fill (p4) circle (1pt);
\draw[->](p3)--(p4);
\coordinate(p5)at(1,0.25);
\fill (p5) circle (1pt);
\draw[->](p4)--(p5);
\coordinate(p6)at(0.75,.5);
\fill (p6) circle (1pt);
\draw[->](p5)--(p6);
\coordinate(p7)at(0.5,.5);
\fill (p7) circle (1pt);
\draw[->](p6)--(p7);
\coordinate(p8)at(0.25,.25);
\fill (p8) circle (1pt);
\draw[->](p7)--(p8);
\draw[->](p8)--(p3);
\coordinate(connect)at(1.17,0);
\fill (connect) circle (1pt);
\draw[->](p4)--(connect);
\coordinate(q3)at(1.5,0);
\fill (q3) circle (1pt);
\draw[->](connect)--(q3);
\coordinate(q4)at(1.75,0);
\fill (q4) circle (1pt);
\draw[->](q3)--(q4);
\coordinate(q5)at(2,0.25);
\fill (q5) circle (1pt);
\draw[->](q4)--(q5);
\coordinate(q6)at(1.75,.5);
\fill (q6) circle (1pt);
\draw[->](q5)--(q6);
\coordinate(q7)at(1.5,.5);
\fill (q7) circle (1pt);
\draw[->](q6)--(q7);
\coordinate(q8)at(1.25,.25);
\fill (q8) circle (1pt);
\draw[->](q7)--(q8);
\draw[->](q8)--(q3);
\end{tikzpicture}
\hspace{1cm}
\begin{tikzpicture}
\coordinate(p1)at(0,0);
\fill (p1) circle (1pt);
\coordinate(p2)at(0.25,0);
\fill (p2) circle (1pt);
\draw[->](p1)--(p2);
\coordinate(p3)at(0.5,0);
\fill (p3) circle (1pt);
\draw[->](p2)--(p3);
\coordinate(p4)at(0.75,0);
\fill (p4) circle (1pt);
\draw[->](p3)--(p4);
\coordinate(p5)at(1,0.25);
\fill (p5) circle (1pt);
\draw[->](p4)--(p5);
\coordinate(p6)at(0.75,.5);
\fill (p6) circle (1pt);
\draw[->](p5)--(p6);
\coordinate(p7)at(0.5,.5);
\fill (p7) circle (1pt);
\draw[->](p6)--(p7);
\coordinate(p8)at(0.25,.25);
\fill (p8) circle (1pt);
\draw[->](p7)--(p8);
\draw[->](p8)--(p3);
\coordinate(connect)at(1,0);
\fill (connect) circle (1pt);
\draw[->](p4)--(connect);
\coordinate(q5)at(1.25,-0.25);
\fill (q5) circle (1pt);
\draw[->](connect)--(q5);
\coordinate(q6)at(1,-.5);
\fill (q6) circle (1pt);
\draw[->](q5)--(q6);
\coordinate(q7)at(0.75,-.5);
\fill (q7) circle (1pt);
\draw[->](q6)--(q7);
\coordinate(q8)at(0.5,-.25);
\fill (q8) circle (1pt);
\draw[->](q7)--(q8);
\draw[->](q8)--(p3);
\end{tikzpicture}
\caption{\scriptsize Forms of doubly pumped lassos.}
\label{fig:pumpedlassos}
\end{figure}
In general, we distinguish between two types of doubly pumped lassos as shown in Figure~\ref{fig:pumpedlassos}.
We call the lassos with periods $C_1$ and $C_2$ the lassos of the doubly pumped lasso.
A doubly pumped lasso of a B\"uchi automaton $B$ is one in the graph structure of $B$. The doubly pumped lasso is called accepting when $C_2$ has an accepting state. A more generalized formalization of this idea  is given in the following theorem.

\begin{theorem}
	Let $B=(Q,q_0,\delta, 2^\textit{AP}, F)$ be a B\"uchi automaton for some set of atomic propositions $\textit{AP} = X \cup Y \cup Z$ and let $\sigma' \in ( 2^{Y})^\omega$. The automaton~$B$ has infinitely many $X \cup Y$-projected models $\sigma$ with $\sigma =_{Y} \sigma'$ if and only if $B$ has an accepting doubly pumped lasso with lassos $\rho$ and $\rho'$ such that:

			1) $\rho$ is an accepting lasso
		    2) $\textit{tr}(\rho)=_{Y} \textit{tr}(\rho')=_{Y}\sigma'$
			3) The period of $\rho'$ shares at least one state with $\rho$
			and 4) $\textit{tr}(\rho)\not =_X\textit{tr}(\rho')$.

\label{theo:infmodels}
\end{theorem}
To check whether there is a sequence $\sigma' \in (2^Y)^\omega$ such that the number of $X\cup Y$-projected models $\sigma$ of $B$ with $\sigma =_Y \sigma'$ is infinite, we search for a doubly pumped lasso satisfying the constraints given in Theorem~\ref{theo:infmodels}. This can be done by applying the following procedure:

Given a B\"uchi automaton $B=(Q,q_0,2^\textit{AP},\delta,F)$ and sets $X,Y,Z \subseteq \textit{AP}$, we construct the following product automaton $B_\times =(Q_\times,q_{\times,0},2^\textit{AP}\times 2^\textit{AP}, \delta_\times, F_\times)$ where:

	$Q_\times = Q \times Q$,

	$q_{\times,0} = (q_0,q_0)$,

	$\delta_\times = \{(s_1,s_2) \xrightarrow{(\alpha,\alpha')} (s'_1,s_2') \mid s_1 \xrightarrow{\alpha} s_2, s'_1 \xrightarrow{\alpha'} s'_2, \alpha =_{Y} \alpha'\}$ and

	$F_\times = Q\times F$.
The automaton $B$ has infinitely many models $\sigma'$ if there is an accepting lasso $\rho = (q_0,q_0)(\alpha_1,\alpha'_1) \dots ((q_j,q_j')(\alpha_{j+1},\alpha'_{j+1})$ $\dots (q_k,q'_k) (\alpha_{k+1},\alpha'_{k+1}))$ in $B_\times$ such that:
	 $\exists h\leq j.~ q'_h = q_j$, i.e., $B$ has lassos $\rho_1$ and $\rho_2$ that share a state in the period of $\rho_1$
	and $\exists h>j.~ \alpha_h \not =_X \alpha'_h$, i.e., the lassos differ in the evaluation of $X$ in a position after the shared state and thus allows infinitely many different sequence over $X$ for the a sequence over $Y$.
The lasso $\rho$ simulates a doubly pumped lasso in $B$ satisfying the constraints of Theorem~\ref{theo:infmodels}.

\begin{theorem}
	Given an alternating B\"uchi automaton $A=(Q,q_0,\delta, 2^\textit{AP}, F)$ for a set of atomic propositions $\textit{AP} = X\cup Y\cup Z$, the problem of checking whether there is a sequence  $\sigma' \in ( 2^{Y})^\omega$ such that $A$ has infinitely many $X\cup Y$-projected models  $\sigma$ with $\sigma =_Y \sigma'$ is \textsc{Pspace}-complete.
\label{theo:checkinfmodels}
\end{theorem}
The lower and upper bound for the problem can be given by a reduction from and to the satisfiability problem of LTL \cite{Baier:2008:PMC:1373322}.
Due to the finite structure of B\"uchi automata, if the number of models  of the automaton exceed the exponential bound $2^{|Q|}$, where $Q$ is the set of states, then the automaton has infinitely many models.
\begin{lemma}
\label{lem:maxnummodels}
	For any B\"uchi automaton $B$, the number of models of $B$ is less or equal to $2^{|Q|}$ otherwise it is $\infty$.
\end{lemma}
\begin{proof}
Assume the number of models is larger than $2^{|Q|}$ then there are  more than $2^{|Q|}$ accepting lassos in $B$. By the pigeonhole principle, two of them share the same $2^{|Q|}$-prefix. Thus, either they are equal or we found doubly pumped lasso in $B$.
\end{proof}

\begin{corollary}
	Let a B\"uchi automaton $B$ over a set of atomic propositions $\textit{AP}$ and sets $X,Y \subseteq \textit{AP}$. For each sequence $\sigma_Y \in (2^{Y})^\omega$ the number of $X\cup Y$-projected models $\sigma $ with $\sigma =_Y \sigma_Y $ is less or equal than $2^{|Q|}$ otherwise it is $\infty$.
\label{cor:exporinfinity}
\end{corollary}
From Corollary~\ref{cor:exporinfinity}, we know that if no sequence $\sigma_Y \in (2^Y)^\omega$ matches to infinitely many $X \cup Y$-projected models then the number of such models is bound by $2^{|Q|}$. Each of these models has a run in $B$ which ends in an accepting strongly connected component. Also from Corollary~\ref{cor:exporinfinity}, we know that every model has  a lasso run of length $|Q|$.
For each finite sequence $w_Y$ of length $|w_Y|= |Q|$ that reaches an accepting strongly connected component, we count the number $X \cup Y$-projected words $w$ of length $|Q|$ with $w =_Y w_Y$ and that end in an accepting strongly connected component. This number is equal to the maximum model counting number.

\begin{figure}[t]
\begin{minipage}[]{.52\textwidth}
\begin{algorithm}[H]
\scriptsize
\begin{algorithmic}[1]
	\REQUIRE $B = (Q,q_0,2^\textit{AP},\delta,F)$, disjoint $X,Y,Z\subseteq \textit{AP}$, $n\in \mathbb N$
	\ENSURE $\#_{X,Y,Z}(B)>n$
	\STATE $SCC = acceptingSCC(B) $
	\STATE $i=1$
	\STATE $W = \bigcup \limits_{S \in SCC} S$
	\WHILE{$i\leq|Q|$}
		\STATE $i = i+1$
		\FOR{$q\in W$}
			\FOR{$(q',\alpha,q)$}
				\STATE $W'= W'\cup \{q'\}$
				\FOR{$\sigma\in \Pi(q)$}
					\STATE $\Pi'(q') = \Pi'(q') \cup \{\alpha_{Y\cup X}\cdot \sigma\}$
				\ENDFOR
			\ENDFOR
		\ENDFOR
		\STATE $W = W'$
		\STATE $W' = \emptyset$
		\FOR{$q \in W$}
			\STATE $\Pi'(q)= \emptyset$
		\ENDFOR
	\ENDWHILE
	\RETURN $\max_{X,Y,Z} \Pi(q_0)\ge n$
\end{algorithmic}
\caption{Maximum Model Counting}
\label{alg:counting}
\end{algorithm}
\end{minipage}\begin{minipage}[]{.4\textwidth}
\begin{figure}[H]
	\begin{tikzpicture}
	\node[state](q3) {$q_3$};
	\node[state](q1) [above right=1cm and 2cm of q3]  {$q_1$};
	\node[state](q2) [below right=1cm and 2cm of q3] {$q_2$};

	\node[right of=q1] (dot1) {$\ldots$};
	\node[right of=q2] (dot2) {$\ldots$};
	\node[left of=q3] (dot3) {$\ldots$};

	\node[above of=q1] (set1) {$\Pi(q_1):=\{\sigma_1,\ldots,\sigma_k\}$};
	\node[below of=q2] (set2) {$\Pi(q_2):=\{\sigma'_1,\ldots,\sigma'_j\}$};
	\node[right=0.4cm] (set3) {$\Pi(q_3):=\{\alpha_1\sigma_1,\ldots,\alpha_1\sigma_k\}$};
	\node[below right=0.2cm] (set4) {$~~~~~~~~~~~\cup \{\alpha_2\sigma'_1,\ldots,\alpha_2\sigma_j\}$};

	\path [->] (q3) edge [bend left] node [below] {$\alpha_1$} (q1);
	\path [->] (q3) edge [bend right] node [above] {$\alpha_2$} (q2);
	\end{tikzpicture}
\end{figure}
\end{minipage}
\caption{\scriptsize Maximum Model Counting Algorithm (left) and a Sketch of a step in this algorithm (right): Current elements of our working set are $q_1,q_2 \in W$ and $q_3 \in W'$. If $i=0$, i.e., we are in the first step of the algorithm, then $q_1$ and $q_2$ are states of accepting SCCs.
\end{figure}

Algorithm~\ref{alg:counting} describes the procedure. An algorithm for the minimum model counting problem is defined in similar way.
The algorithm works in a backwards fashion starting with states of accepting strongly connected components. In each iteration $i$, the algorithm maps each state of the automaton with $X \cup Y$-projected words of length $i$ that reach an accepting strongly connected component. After $|Q|$ iterations, the algorithm determines from the mapping of initial state $q_0$ a $Y$-projected word of length $|Q|$ with the maximum number of matching $X\cup Y$-projected words.

\begin{theorem}
	The decisional version of the maximum model counting problem over automata (MMCA), i.e. the question whether the maximum is greater than a given natural number $n$, is in $\mathit{NP}^{\#P}$.
\end{theorem}
\begin{proof}
	Let a B\"uchi automaton over an alphabet $2^\mathit{AP}$ for a set of atomic propositions $\mathit{AP}$ and sets $\textit{AP}_X,\textit{AP}_Y,\textit{AP}_Z \subseteq \textit{AP}$ and a natural number $n$ be given.
	We construct a nondeterministic Turing Machine $M$ with access to a $\#P$-oracle as follows: $M$ guesses a sequence $\sigma_Y \in 2^\mathit{AP_Y}$. It then queries the oracle, to compute a number $c$, such that $c = |\{\sigma_X \in (2^{\textit{AP}_X})^\omega \mid \exists \sigma_Z \in(2^{\textit{AP}_Z})^\omega.~ \sigma_X\cup\sigma_Y\cup\sigma_Z \in L(B)\}|$, which is a $\#P$ problem~\cite{DBLP:conf/lata/FinkbeinerT14}. It remains to check whether $n>c$. If so, $M$ accepts.
\end{proof}
The following theorem summarizes the main findings of this section, which establish, depending on the property, an exponentially or even doubly exponentially better algorithm (in the quantitative bound) over the existing model checking algorithm for HyperLTL.

\begin{theorem}
Given a Kripke structure $K$ and a quantitative hyperproperty $\varphi$ with bound $n$, the problem whether $K \models \varphi$ can be decided in logarithmic space in the quantitative bound $n$ and in polynomial space in the size of $K$.
\end{theorem}

\section{A Max\#Sat-based Approach}
For existential {\sc HyperLTL}\@\xspace formulas $\psi_\iota$ and $\psi$, we give a more practical model checking approach by  encoding the automaton-based construction presented in Section~4 into a propositional formula.

 Given a Kripke structure $K=(S,s_0, \tau, \textit{AP}_K, L)$ and a quantitative hyperproperty $\varphi=\forall \pi_1, \dots, \pi_k.~ \psi_\iota \rightarrow (\# \sigma :A.~ \psi) \triangleleft n $ over a set of atomic propositions $\textit{AP}_\varphi\subseteq\textit{AP}_K$ and bound $\mu$, our algorithm constructs a propositional formula $\phi$ such that,
 every satisfying assignment of $\phi$ uniquely encodes a tuple of lassos $(\pi_1, \dots, \pi_k,\sigma)$ of length $\mu$ in $K$, where $(\pi_1, \dots, \pi_k)$ satisfies $\psi_\iota$ and $(\pi_1, \dots, \pi_k,\sigma)$ satisfies $\psi$.
 To compute the values $\max \limits_{(\pi_1,\dots,\pi_k)}|\{\sigma_A \mid (\pi_1,\dots,\pi_k,\sigma) \models \psi_\iota \wedge \psi \}|$ (in case $\triangleleft \in \{\leq, <\}$) or $\min \limits_{(\pi_1,\dots,\pi_k)}|\{\sigma_A \mid (\pi_1,\dots,\pi_k,\sigma) \models \psi_\iota \wedge \psi \}|$ (in case $\triangleleft \in \{\ge, >\}$),  we pass $\phi$ to a maximum model counter, respectively, to a minimum model counter with the appropriate sets of counting and maximization, respectively, minimization propositions.
  From Lemma~\ref{lem:maxnummodels} we know that it is enough to consider lassos of length linear in the product automaton. The size of $\phi$ is thus exponential in the size of $\varphi$ and polynomial in the size of $K$.

The construction resembles the encoding of the bounded model checking approach for LTL~\cite{Clarke:2001:BMC:510986.510987}.
Let $\psi_\iota = \exists \pi'_1 \dots \pi'_{k'}.~\psi'_{\iota}$ and $\psi=\exists \pi''_1 \dots \pi''_{k''}.~\psi''$ and let $\textit{AP}_{\psi_\iota}$ and $\textit{AP}_{\psi}$ be the sets of atomic propositions that appear in $\psi_\iota$ and $\psi$ respectively.
The propositional formula $\phi$ is given as a conjunction of the following propositional formulas:
$$\phi = \bigwedge_{i\leq k} \llbracket K \rrbracket ^{\pi_i}_\mu  \wedge \llbracket K \rrbracket ^\sigma_\mu \wedge \llbracket \psi_\iota \rrbracket _{\mu}^0 \wedge \llbracket \psi \rrbracket _{\mu}^0$$
where:
\begin{itemize}

	\item $\mu$ is  length of considered lassos and is equal to  $\mu = 2^{|\psi'_\iota \wedge \psi''|}*|S|^{k+k'+k''+1}+1$, which is one plus the size of the product automaton constructed from the $k+k'+k''+1$ self-composition and the automaton for $\psi_\iota \wedge \psi$. The "plus one" is to additionally to check whether the number of models is infinite.

	\item $\llbracket K \rrbracket ^\pi_k$ is the encoding of the transition relation of the copy of $K$ where atomic propositions are indexed with $\pi$ and up to an unrolling of length $k$. Each state of $K$ can be encoded as an evaluation of a vector of $\log{|S|}$ unique propositional variables. The encoding\footnote{We refer the reader to \cite{Clarke:2001:BMC:510986.510987} for more information on the encoding} is given by the propositional formula $ I(\vv{v}_0^\pi) \wedge \bigwedge_{i=0}^{k-1}\tau(\vv{v}_i^\pi,\vv{v}_{i+1}^\pi)$ which encodes all paths of $K$ of length $k$.
	The formula $I(\vv{v}_0^\pi)$ defines the assignment of the initial state. The formulas $\tau(\vv{v}_i^\pi,\vv{v}_{i+1}^\pi)$ define valid transitions in $K$ from the $i$th to the $(i+1)$st state of a path.

	\item $ \llbracket \psi_\iota \rrbracket _{k}^0$ and $\llbracket \psi \rrbracket _{k}^0$ are constructed using the following rules\footnote{We omitted the rules for boolean operators for the lack of space}:
		\begin{center}
			\small
			\begin{tabular}{|c||c|c|}
			\hline
			& $i<k$ & $i=k$ \\
			\hline
			$\llbracket a_\pi \rrbracket _k^i$ & $a^i_\pi$ & $\bigvee_{j=0}^{k-1} (l_j \wedge a_\pi^j)$ \\
			\hline
			$\llbracket \neg a_\pi \rrbracket _k^i$ & $\neg a^i_\pi$& $\bigvee_{j=0}^{k-1} (l_j \wedge \neg a_\pi^j)$ \\
			\hline
			$\llbracket \LTLcircle \varphi_1 \rrbracket _k^i $ & $\llbracket \varphi_1 \rrbracket _k^{i+1} $ &  $\bigvee_{j=0}^{k-1} (l_j \wedge \llbracket \varphi_1 \rrbracket_k^j)$\\
			\hline
			$\llbracket \varphi_1 \LTLuntil \varphi_2 \rrbracket _k^i$ & $\llbracket \varphi_2 \rrbracket _k^i \vee (\llbracket \varphi_1 \rrbracket _k^i \wedge \llbracket \varphi_1 \LTLuntil \varphi \rrbracket _k^{i+1})$ & $\bigvee_{j=0}^{k-1} (l_j \wedge \langle \varphi_1 \LTLuntil \varphi_2 \rangle _k^j )$ \\
			\hline
			$\langle \varphi_1 \LTLuntil \varphi_2 \rangle _k^i$ & $\llbracket \varphi_2 \rrbracket _k^i \vee (\llbracket \varphi_1 \rrbracket_k^i \wedge \langle \varphi_1 \LTLuntil \varphi \rangle _k^{i+1})$ & false \\
			\hline
			$\llbracket \varphi_1 \LTLrelease \varphi_2 \rrbracket _k^i$ & $\llbracket \varphi_2 \rrbracket _k^i \wedge (\llbracket \varphi_1 \rrbracket _k^i \vee \llbracket \varphi_1 \LTLrelease \varphi \rrbracket _k^{i+1})$ & $\bigvee_{j=0}^{k-1} (l_j \wedge \langle \varphi_1 \LTLrelease \varphi_2 \rangle _k^j )$ \\
			\hline
			$\langle \varphi_1 \LTLrelease \varphi_2 \rangle _k^i$ & $\llbracket \varphi_2 \rrbracket _k^i \wedge (\llbracket \varphi_1 \rrbracket_k^i \vee \langle \varphi_1 \LTLrelease \varphi \rangle _k^{i+1})$ & true \\
			\hline
		\end{tabular}
		\end{center}
		in case of an existential quantifier over a trace variable $\pi$, we add a copy of the encoding of $K$ with new variables distinguished by $\pi$:
		\begin{center}
		\small
		\begin{tabular}{|c|c|}
			\hline
			\quad $\llbracket \exists \pi.\varphi_1 \rrbracket _k^i $ \quad & \quad $\llbracket K \rrbracket^\pi_k  \wedge \llbracket \varphi_1 \rrbracket _k^i$ \quad \\
			\hline
		\end{tabular}
		\end{center}
\end{itemize}

We define sets $X= \{a^i_\sigma \mid a \in A , i \leq k\}$, $Y= \{a^i \mid  a \in \textit{AP}_\psi \setminus A, i\leq k\}$	and $Z = P\setminus X \cup Y$, where $P$ is the set of all propositions in $\phi$. The maximum model counting problem is then $\textit{MMC}(\phi, X,Y,Z)$.

\subsection{Experiments}
We have implemented the Max\#Sat-based model checking approach from the last section. We compare the Max\#Sat-based approach to the expansion-based approach using {\sc HyperLTL}\@\xspace~\cite{conf/cav/FinkbeinerRS15}. Our implementation uses the MaxCount tool~\cite{DBLP:conf/aaai/FremontRS17}. We use the option in MaxCount that enumerates, rather than approximates, the number of assignments for the counting variables. We furthermore instrumented the tool so that it terminates as soon as a sample is found that exceeds the given bound. If no sample is found after one hour, we report a timeout.

Table~\ref{tab:comparison} shows the results on a parameterized benchmark obtained from the implementation of an 8bit passcode checker. The parameter of the benchmark is the bound on the number of bits that is leaked to an adversary, who might, for example, enter passcodes in a brute-force manner. In all instances, a violation is found.  The results show that the Max\#Sat-based approach scales significantly better than the expansion-based approach.
\begin{table}
\scriptsize
\centering
\begin{tabular}{|c|c||c|c|c|c||c|c|c|}
\hline
	\multirow{2}{1.8cm}{\textbf{Benchmark}}& \multirow{2}{2cm}{\textbf{Specification}} & \multicolumn{4}{c||}{MCHyper} & \multicolumn{3}{c|}{MCQHyper}\\
	\cline{3-9}
	& &\#Latches & \#Gates & \#Quan. & Time(sec)  & \#max & \#count & Time(sec). \\
	\hline
	Pwd\_8bit & 1bit\_leak & \multirow{5}{1cm}{\center 9} & \multirow{5}{1cm}{\center 55} &  2 & 0.3 & 16 & 2 & 1\\
	\cline{1-2} \cline{5-9}
	& 2bit\_leak & & & 4 & 0.4 & 32 & 4 & 1\\
	\cline{1-2} \cline{5-9}
	& 3bit\_leak & & & 8 & 1.3 & 64 & 8 & 2\\
	\cline{1-2} \cline{5-9}
	& 4bit\_leak & & & 16 & 97  & 128 & 16 & 4 \\
	\cline{1-2} \cline{5-9}
	& 5bit\_leak & & &  32 & TO  & 256 & 32 & 8\\
	\cline{1-2} \cline{5-9}
	& 6bit\_leak & & & 64 &TO  & 512 & 64 & 335\\
	\cline{1-2} \cline{5-9}
	& 8bit\_leak & & &  256 &TO & 2048 & 256 & TO\\
	\hline
\end{tabular}
\caption{\scriptsize Comparison between the expansion-based approach (MCHyper) and the Max\#Sat-based approach (MCQHyper). \#max is the number of maximization variables (set $Y$). \#count is the number of the counting variables (set $X$). TO indicates a time-out after 1 hour.}
\label{tab:comparison}
\vskip -1.0cm
\end{table}

\section{Conclusion}
We have studied quantitative hyperproperties of the form $\forall \pi_1,\dots,\pi_k.\ \varphi \rightarrow (\# \sigma: A.\ \psi  \triangleleft n)$, where $\varphi$ and $\psi$ are HyperLTL formulas, and $\#\sigma:A. \varphi \triangleleft n$ compares the number of traces that differ in the atomic propositions $A$ and satisfy $\psi$ to a threshold $n$. Many quantitative information flow policies of practical interest, such as quantitative non-interference and deniability, belong to this class of properties.
Our new counting-based model checking algorithm for quantitative hyperproperties performs at least exponentially better in both time and space in the bound $n$ than a reduction to standard HyperLTL model checking.
The new counting operator makes the specifications exponentially more concise in the bound, and our model checking algorithm solves the concise specifications efficiently.

We also showed that the model checking problem for quantitative hyperproperties can be solved with a practical Max\#SAT-based algorithm. The SAT-based approach outperforms the expansion-based approach significantly for this class of properties.
An additional advantage of the new approach is that it can handle properties like deniability, which cannot be checked by MCHyper because of the quantifier alternation.

\bibliographystyle{plain}

redpajama_set_name: RedPajamaArXiv


Two of Iron Bonehead's best traits are its ability to sniff out talented bands from far flung corners of metal's underground, in the process plucking first rate music from potential obscurity and bringing it to a wider audience. This is certainly the case for one recent release from their roster as the label has just brought us Demise Rites from Australian band, Eucharist, as a special vinyl 12" MLP.
Formed in 2011 Eucharist released two demos during their formative year, Tenebrous Summoning and Demise Rites. Both demos were limited to fifty copies but unfortunately only half of them were ever circulated on dubbed cassettes featuring Xeroxed covers with Demise Rites also featuring hand numbered inlays. Total Holocaust Records then released all six tracks from both demos on a compilation cassette, also entitled Demise Rites in October 2012. This compilation was limited to 100 copies and helped introduce this malignant creation to the extreme underground. Unfortunately the label folded shortly after the compilations release, potentially condemning the music of Eucharist to obscurity in the process. Forever the source of obscure brilliance Iron Bonehead Productions has just released all six tracks on vinyl, with all being re-mastered for their special edition.
Eucharist maintains a level of secrecy regarding membership etc., with very few details currently being available online; they play verminous, smothering death metal played with a level of atavism/primitivism that draws comparison with the likes of Archgoat or Demoncy. All tracks during the MLP were originally recorded on a broken analogue tape machine which makes this release all the more appealing as the production levels on Demise Rites are exactly what you'd want and expect from this type of music and sounds every bit as good as studio releases from similar bands. The suitably murky production lends itself well to the overall suffocating and oppressive nature of their music. The first demo, Tenebrous Suffering, is featured on Side A with four tracks that serve as suitable introduction to their infectious music. At the extreme end of death metal the music of Eucharist is intended to be an uncomfortable and punishing listen. The vocals are laced with effects to give them quite an intimidating rasp, at times similar to those of Portal or Vassafor, and when you combine this with those muddy production levels and guitars down tuned to death it makes for quite a potent listen. There's no messing about with Eucharist's music, no fancy intros, just harsh, hate fueled intense blackened death.
The second Eucharist demo, Demise Rites, features on Side B with two tracks spanning close to fourteen minutes that again keep the hostility levels suitably terrifying with the main difference being the drumming is slightly more audible than on Side A. Overall the music is harsh and torturous, making for that uncomfortable and down-right hate filled listen those of us listening at the extreme end of the black/death spectrum crave. During both sides of the MLP you're surrounded and smothered by a fog of malevolent, all-consuming, bestial, blackened death – this is a must for fans of the likes of Portal, Abyssal, Ævangelist et al. Also, there's quite a lot of listening for an MLP with close to thirty minutes of Eucharist's poisonous fog to get your ears round.
I have no idea whatsoever what radar Iron Bonehead uses to detect such obscure quality but we have them to thank for bringing us the music of Eucharist which, I'm sure, had escaped the attention of a lot of us until now. My hope is this will see Eucharist write and release more music – if this was recorded on a broken analogue machine just imagine what they could achieve in a studio… Once again, Iron Bonehead Productions has brought us a true underground gem that's not to be missed.
IV – Below the Earth.
Demise Rites by Eucharist has just been released by Iron Bonehead Productions on 12" MLP.


text:
Q: Joomla component development: Save, apply and cancel toolbar buttons not working I am following the lessons on component development in the "Learning Joomla! 1.5 Extension Development" book. I've followed the instructions in the chapter exactly, creating a component I call "carousel". I've only created the Admin back-end, and I'm able to view the form for creating a new entry or edit existing one, but cannot save or apply changes. Clicking the "Save", "Apply", and "Cancel" buttons only takes me to the Admin index page, but no changes in the DB. However, if I add entries directly in the DB using SQL I'm able to view a listing of them in the Admin interface correctly.
I am using Joomla 1.5.20, PHP 5.2.3 and MySQL 5.0.41 on Windows XP. You can download a zip file of the "com_carousel" folder (which I have in the "administrator/components" folder) from here. I've also correctly registered the component in the DB, such that I'm able to see it under the "Components" menu in the back-end. Here is the SQL am using to create the table "jos_carousel":
CREATE TABLE `jos_carousel` (
`id` INT( 11 ) UNSIGNED NOT NULL AUTO_INCREMENT PRIMARY KEY ,
`title` VARCHAR( 255 ) NOT NULL ,
`description` TEXT NOT NULL ,
`published` TINYINT( 1 ) UNSIGNED NOT NULL DEFAULT '0'
) ENGINE = innodb;

Please help.
Rgds,
Simon

A: I took some time debugging your extension and found the reason for the strange behaviour you are experiencing. You do not pass the $option variable to the edit form. Therefore, when the form is submitted Joomla does not now which component should be loaded to deal with the request and that is why it just renders the main admin page.
The simplest way to solve this issue is to manually add 'com_carousel' to the hidden field in the edit form (function editCarousel() in admin.carousel.html.php).
Replace
<input type="hidden" name="option" value="<?php echo $option; ?>" />

With
<input type="hidden" name="option" value="com_carousel" />

If you really want to use the $option variable you need to pass it from the admin.carousel.php file.
There are still some things that are not working (mainly publishing/unpublishing), but that is covered later in the book. Once you are done with Learning Joomla! Extension Development your best bet is to read Mastering Joomla.... I am just about to finish reading it and it has been an invaluable resource for me.
Good luck with all your Joomla! extensions :)

A: Not sure if that is the problem but in your main switch you call saveCarousel with one parameter:
case "apply"://NOT WORKING!
    case "save"://NOT WORKING!
        saveCarousel($option);
        break;

and in the function definition it has two parameters:
function saveCarousel($option, $task)

Try adding the $task variable to the function call inside the switch and let us know if that changed anything...

redpajama_set_name: RedPajamaStackExchange


text:
Osian oder Osiyan (Hindi: ओसियां) ist eine Kleinstadt mit etwa 12.500 Einwohnern im indischen Bundesstaat Rajasthan, die vor allem wegen ihrer mittelalterlichen Tempel (mandira) bekannt ist. Der alte Name des Ortes lautete Ukesha oder Upkeshapur.

Lage
Osian liegt am westlichen Rand des Aravalligebirges im Übergang zur Wüste Thar in einer Höhe von etwa  etwa 68 km (Fahrtstrecke) nördlich von Jodhpur an der Straße in Richtung Bikaner. Der Ort verfügt auch über einen Bahnhof an der Strecke Jodhpur – Phalodi. Das Klima ist meist heiß und trocken; Regen fällt eigentlich nur in den sommerlichen Monsunmonaten.

Bevölkerung
Die Bevölkerung besteht fast ausschließlich aus Hindus mit einem geringen Anteil an Jains und Moslems. Wie bei Volkszählungen im Norden Indiens üblich übersteigt der Anteil der männlichen Einwohner den der weiblichen um etwa 10 %.

Wirtschaft
Der Ort ist ein kleines Wirtschaftszentrum für die Dörfer der Umgebung; es dominieren Kleinhandel, Handwerk und kleinere Dienstleistungsbetriebe. Der Tourismus spielt ebenfalls eine wichtige Rolle im Wirtschaftsleben der Gemeinde. Zu Beginn des 21. Jahrhunderts wurde im Gemeindebezirk (tehsil) eine Solarstromanlage mit einer Leistung von 5 MW installiert.

Geschichte
Die nachweisbare Geschichte des Ortes reicht bis in das 8. Jahrhundert n. Chr. zurück, als der Gurjara-Pratihara-König Vatsaraja (reg. etwa 775–805) für die vorwiegend Handel treibende Jain-Gemeinschaft einen Mahavira-Tempel stiftete. Der über Osian führende Handelsweg war bis in das 15./16. Jahrhundert von Bedeutung und so entstanden auch mehrere Hindu-Tempel sowie ein stufenbrunnenartiger Tempelteich im Ort.

Sehenswürdigkeiten
 Der Mahavira-Tempel geht auf das Jahr 783 zurück und ist ein wichtiges Heiligtum der Jain-Sekte. Er ist dem 24. Tirthankara geweiht, dessen historische Authentizität jedoch umstritten ist. Die Cella (garbhagriha) des Tempels stammt wohl noch aus der Gründerzeit – der plastische Schmuck ist recht einfach und vor allem die Pfeilerreliefs sind in nur geringem Maße tiefenräumlich gearbeitet. Die auf acht Pfeilern stehende zentrale Kragkuppel sowie andere Bauteile zeigen dagegen deutlich entwickeltere Formen und scheinen später hinzugefügt worden zu sein.
 Der auf einer kleinen Anhöhe gelegene Sachiya Mata Tempel stammt in seinen Ursprüngen wohl ebenfalls dem 8. Jahrhundert; er wurde jedoch später mehrfach umgebaut und erweitert. Eins der imposantesten Baudetails ist der von mehreren Torbögen (toranas) überspannte Treppenaufgang. Die Außenwände des Tempels sind mit Figuren geschmückt, die in Ikonographie und Stil dem figürlichen Bauschmuck der Tempel von Khajuraho ähneln.
 Der Surya-Tempel ist ein Bestandteil des Sachiya Mata Tempels und dem Sonnengott geweiht, dessen imposantes Kultbild im Sanktum steht.
 In Osian stehen drei Harihara-Tempel, von denen der erste und der dritte am interessantesten sind. Während der Harihara-Tempel I noch dem 8. Jahrhundert zuzuordnen ist, zeigt sich am Harihara-Tempel III der entwickelte, d. h. beinahe freiplastische Figurenstil der ersten Hälfte des 9. Jahrhunderts, der sich nur wenig später in Khajuraho zur Blüte entwickeln sollte.
 Ein verschlammter und versandeter Tempelteich aus dem 8. Jahrhundert(?) vervollständigt das architektonische Ensemble.

Literatur

Weblinks

 Osian, Tempel – Fotos + Infos
 Impressionen aus Osian – Video
 Osian, Tempel – Fotos + Infos (englisch)
 Narasimha-Figur am Harihara-Tempel – Foto

Einzelnachweise

Distrikt Jodhpur
Ort in Rajasthan

redpajama_set_name: RedPajamaWikipedia


Greetings for your Monday! Your writer's laptop is very sick and it is in the hospital trying to get resuscitated. Stand by for news about gayness! Or go to one of those OTHER websites if you just HAVE to know about news of gayness right now. You are so impatient.
ANYWAY, check back very soon!
Here is a dog playing piano and singing.


Editor's Note: Art Jonak is an investment analyst with both a wide and deep synthesis approach to research data. His commentary threads on titans like Netflix, Amazon and Facebook are a minor legend for their insight, detail and clarity. He also navigates venture funding, and emerging sector data, in a narrative, often with striking visualization, that reveals trends in their formation long before they are visible. It should not need to be said for investment disclosure that Art is holding crypto assets himself. He is obviously making a case of why everyone should.
Here is Art's 2019 message thread for investing in Bitcoin, in particular. In our eyes, it slams the case for why every single portfolio on the planet should be holding Bitcoin, and treated as a portfolio asset class.
* Bitcoin is a non-correlated asset — This is the holy grail of any portfolio. Bitcoin's current 180 day correlation to the S&P 500 is 0 and the correlation to the dollar index is near zero as well. Investing in non-correlated assets should reduce the risk and increase the returns of a portfolio according to modern portfolio theory.
* Bitcoin has an asymmetric return profile — There is much more upside than downside in owning the asset. The downside (loss of capital) is capped at the total amount of capital invested, yet the upside is ~100X+ (if Bitcoin only becomes gold equivalent).
The modern portfolio theory argument for investing in Bitcoin is quite strong. But how has theory played out in practice?
Bitcoin has been the best performing asset over the last 10 years. It has experienced a 1,300,000X+ increase in value from $0.003 to ~$4,000 today. It has beat the S&P 500 for the last 10 years, the last 5 years, and the last 2 years. As a fixed supply asset, I believe Bitcoin will continue to outperform traditional assets in the future as demand continues to increase too.
Although I believe in Bitcoin's future outlook, most people should not put significant funds at risk in this investment opportunity. It is risky and speculative. They could lose 100% of the money that they invest. For that reason, each person needs to evaluate their current situation, their goals, and the amount of capital they would be willing to lose.
If the thesis plays out how many smart people anticipate though, an investment of 100 basis points or less would materially change the performance of your portfolio fund, which ultimately changes the quality of life you will live when you retire. Most institutions have permanent, long-term capital which allows them to stomach more volatility than most investors.
For example, an investment of 1% of assets at $4,000 BTC price would yield a 25% increase in your portfolio total assets if Bitcoin reached $100,000. If you decided to invest 0.1% of assets, the same price appreciation would increase total assets by 2.5%.
However, the exciting part is that many people believe Bitcoin will not only reach $100,000 one day, but rather be worth $1,000,000+. If that comes to fruition, a 0.1% investment today could lead to the same 25% increase in total assets for your portfolio. These types of trade-offs are the definition of an asymmetric return profile.
And still, most people's portfolios have 0% exposure to Bitcoin and crypto. Something to consider as we head into 2019.


text:
LANCE KING – Former PYRAMAZE, BALANCE OF POWER Singer Announces New Release Date For ReProgram Album
Written by megarock on February 2, 2019
LANCE KING – Former PYRAMAZE, BALANCE OF POWER Singer Announces New Release Date For ReProgram AlbumLegendary singer Lance King, original voice behind Pyramaze, Avian, Balance Of Power and Gemini will release his second solo album on March 29th on Nightmare Records. Originally due February 15th, King's ReProgam album is now digitally available to preorder on iTunes and Amazon.
Of course, given Lance King's pedigree, and…Sat, 02 Feb 2019 03:00:00 GMT
Legendary singer Lance King, original voice behind Pyramaze, Avian, Balance Of Power and Gemini will release his second solo album on March 29th on Nightmare Records. Originally due February 15th, King's ReProgam album is now digitally available to preorder on iTunes and Amazon. Of course, given L…
Link to original source

redpajama_set_name: RedPajamaCommonCrawl


To be a globally recognized Chemical Engineering department with excellence in teaching, research and consultancy services.
To prepare our students to become successful professional Chemical Engineers capable of undertaking advanced studies and life-long learning.
To produce Chemical Engineers who will contribute to the process industries worldwide.
To provide the students a strong fundamental technical education that makes them capable of catering to the needs of a changing technological environment and the society.
To nurture the innovative capabilities of students by providing them with a research platform and exposure to current technologies.


text:
Howard Group »
Keith Howard
Matthew R. Hagen
Terry Harshman
Myra Williams
Bill Bubel
Dana Hahn
Karen McNevin
Lawrence Kellogg
Partner/Testimonials
Grand Boulevard at Sandestin® Town Center
Silver Sands Premium Outlets
Heron Harbor Water-front Redevelopment
Vizcaya and Stallworth Preserve
Leasing »
Keith Howard | President and CEO
Matthew R. Hagen | Executive VP, CFO
Terry Harshman | Vice President of Planning, Design and Construction
Myra Williams | Vice President of Marketing
Bill Bubel | Vice President of Operations
Dana Hahn | Vice President of Real Estate
Karen McNevin | Vice President of Hospitality & Human Resources
Lawrence Kellogg | Chief Investment Officer
Vice President of Operations of Northwest Florida Real Estate Projects | Howard Group
Bill Bubel joined Howard Group in June 2008 and is Vice President of Operations for the company. He is responsible for leading the property teams and overseeing all aspects of property management for Howard Group including operations and contractors, financial reporting, marketing, tenant and customer relations. He works closely with the leasing, tenant coordination and construction departments as Howard Group moves forward with new tenant opportunities and future developments in Destin, Florida and Northwest Florida.
Mr. Bubel comes to Howard Group with over 20 years of experience including specializing in client relationships, tenant and customer relations, financial management, regional and local leasing, marketing, construction management and much more. For the previous nine years, he worked for Jones Lang LaSalle Retail, the largest third-party shopping center manager of more than 100 different properties. Jones Lang LaSalle Retail is a division of Jones Lang LaSalle, a real estate money management and services firm with over 600 shopping centers.
Mr. Bubel's many accomplishments throughout his career include a Merit Award from the International Council of Shopping Centers' (ICSC) Maxi program, an international marketing competition that recognizes excellence in shopping center marketing, for a specialty leasing program. He also has earned his Certified Shopping Center Manager (CSM) certification.
Since his arrival to Northwest Florida's Gulf Coast six years ago, Mr. Bubel has been an active member of various civic and community organizations, serving on the board of directors of local chambers and convention visitors bureaus. He resides in South Walton along with his wife, Susan, and his two sons, Brad and Brandon.
Howard Group | 585 Grand Boulevard, Suite 201, Miramar Beach, Florida 32550 | 850.837.1886


text:
Montana Steps Up Fight Against Invasive Mussels
Montana is on the front line in the war against two species of invasive freshwater mussels, zebras and quaggas, which can cause enormous damage to underwater equipment with blankets of hard, calciferous shells.
Fish And Wildlife Project Cost Savings
Cost savings in existing fish and wildlife projects could be shifted to higher-priority projects including scientific research, habitat evaluations, and projects addressing sturgeon and lamprey without adding money to the program.
Stay the Course on Scientific Research, Idaho's Top Fish and Wildlife Official Says
Virgil Moore, director of the Idaho Department of Fish and Game, touts the benefits of research, maintenance of investments, and collaboration.
Lower Columbia Wetlands Restoration Benefits Wildlife, Birds, and Fish
Just a dozen miles northwest of downtown Portland, a cornucopia of wildlife, notably song birds and more than 200,000 migrating waterfowl annually, inhabit the low-lying, marshy
Strategic Plan Will Protect Fish and Wildlife Investments Over Time
In revising the Columbia River Basin Fish and Wildlife Program in 2014, the Council committed to define and develop a long-term maintenance plan and process to ensure that past
Ninth Circuit Appeals Court upholds Council's consideration of fish and wildlife interests in developing regional power plan
On September 18, 2013, the U.S. Court of Appeals for the Ninth Circuit issued a decision affirming the Council's consideration of fish and wildlife interests in developing its Sixth Northwest Conser
Council adopts 25 subbasin plans to guide fish and wildlife mitigation in the Columbia River Basin
PORTLAND — Twenty-five locally developed plans that will guide efforts to mitigate the impacts of hydropower dams on fish and wildlife in Columbia River tributaries and parts of the mainstem river w
Council adopts 23 subbasin plans to guide fish and wildlife mitigation in Columbia River Basin
Twenty-three locally developed plans that will guide efforts to mitigate the impacts of hydropower dams on fish and wildlife in Columbia River tributaries and parts of the mainstem river were adopted
Council adopts fish and wildlife protection plan for Montana's Blackfoot River
Feb 9, 2011 John Harrison
The Council added a fish and wildlife protection plan for the Blackfoot River in western Montana to its Columbia River Basin Fish and Wildlife Program this week, paving the way for potential funding t


text:
Traffic & Parking Around Denistone East Public School
Consultation closed on 02 April 2018
As part of the City of Ryde's commitment to road safety, Council is investigating traffic and parking issues around Denistone East Public School with the aim to improve safety for users in the Denistone East Public School catchment area.
As part of this project Council will be undertaking traffic investigations, surveys and community consultation in consideration with population growth and school enrolment forecasts to identify:
Community concerns, such as the ones raised by you
Improvements to pedestrian access routes to and from the schools, such as footpaths and road crossings, in order to reduce reliance on driving
Improvements to vehicle access routes to and from schools, such as road widening, traffic calming and drop-off/pick-up zones, to assist those who must drive to school
Localised education and enforcement needs, to address the behavioural issues for each school
Therefore, as part of the community consultation process we would like your feedback on the traffic and safety issues in the Denistone East Public School catchment area through our online mapping tool. We would also like to know how people are travelling to and from the school through a short travel to school survey. You can also provide any further comments or concerns on how we can improve traffic flow and safety in the area through the online submission form below or at our information session (details below).
Published on 3 April 2018
Have Your Say on the Traffic & Parking Around Denistone East Public School is now closed.
Have Your Say on traffic and parking around Denistone East Public School is now extended to Monday 2 April 2018.
Have Your Say on the Traffic & Parking Around Denistone East Public School is now open.
You can have your say on Traffic and Parking Around Denistone East Public School by using the interactive mapping tool, completing the online submission form, or at the community event. We would also like to know how people are travelling to and from the school through a short travel to school survey.
Social Pinpoint
Use the interactive map here to tell us where you've experienced traffic and parking issues around the school.
Travel to School Survey
Tell us how you are travelling to and from Denistone East Public School through the survey here.
Join us for an information session where there will be a presentation by the Mayor and Council's traffic team. Also at this session you will be able to identify any traffic and parking issues you have experienced around Denistone East Public School.
When Wednesday 14 March 2018
Time 6.00 - 7.00pm
Where Denistone East Public School Library
Further information about this item
Comments * (Required)
* (Required)
Yes, I understand the Privacy Notification (below)
Privacy Notification
Personal information collected from you is held and used by Council under the provisions of the Privacy and Personal Information Protection Act 1998. The supply of information is voluntary, however if you cannot provide, or do not wish to provide the information sought, Council may be unable to process your application or request, or consider your submission. Please note that the exchange of information between the public and Council, may be accessed by others and could be made publicly available under the Government Information Public Access Act 2009 (GIPA Act). If you require further information please contact Council's Customer Service Centre on 9952 8222.
Traffic & Parking Around Denistone East Public School - Information Session 14 March 2018 to 14 March 2018
Traffic & Parking around Meadowbank Public School online submission form
Traffic & Parking around all other schools online submission form
If you require more information about Traffic & Parking Around Schools please call Customer Service on 9952 8222.
Subscribe to project updates
Fields marked as 'Required' must be completed.
Last updated on 3 April 2018


Social Media is dramatically changing the way we build relationships, lead our organizations, and inspire social change. Coupled with new technologies is an increased demand from consumers and clients for accountability, access to information and transparent institutional conduct. This course will focus on how your organization can make the cultural shift required to capitalize on technology's capacity for creating meaningful public participation and social change. You'll leave this course with fresh perspectives and concrete ideas about how your organization can embrace technology to further your social mission.
Who should attend: This course is of interest to managers and leaders in the public and non profit sectors who want to better use social media to engage their constituents and further their social mission. Seating is limited to 40 participants.
Great opportunity for this in Vancouver to learn from an experienced leader in the field of social media and online campaigning.
The event is on March 5, 2010 and the cost to attend is $195. The registration site is here.


The UK's Largest Caribbean Party Is In Town Again For Our Day Party Edition! With A Vast Array Of Electric Concert-Like Parties, We Return In The Heart Of Central London! 100% Carnival Vibes… Dancehall… Soca… & Hundreds Of Whistles & Horns… And YOU! Get Ready To BRUK OUT!


text:
Newmont Mining may halt Indonesia operations
Julienne Bay | May 7, 2014 | 4:51 pm Base Metals Precious Metals Top Companies Asia Europe Copper Gold
Source: Wikicommons
US giant Newmont Mining Corp. (NYSE: NEM) said Wednesday it expects to cease its Indonesian gold and copper operations in June due to unresolved issues over export permits.
The Indonesian government imposed an immediate 25% export tax in January for the country's copper concentrates, and it will increase to 35% on January 2015.
Newmont and Freeport-McMoRan Copper & Gold Inc. (NYSE: FCX), which account for 97 % of Indonesia's copper output combined, said the rule conflicts with contracts they signed exempting them from new taxes and duties.
The Colorado,US-based miner is currently discussing with the government to complete the process of securing an initial export permit. The company has obtained registered exporter status from the Ministry of Trade in April, necessary milestone prior to receiving the permit.
Newmont is the world's third largest gold producer, supplying roughly 30% of its Indonesian copper concentrate output to the country's only copper smelter, PT Smelting at Gresik.
"This is a very unfortunate and difficult situation for all of us, as it will disrupt the lives of our 8,000 employees and contractors and impact thousands of more people in the Sumbawa Barat area who derive their incomes from our operation," said Martiono Hadianto, president director of PT Newmont Nusa Tenggara in the statement.
Newmont's Batu Hijau copper and gold mine on the island of Sumbawa Barat began its operations in 2000. The company had forcasted copper concentrate output for 2014 at 110,000-125,000 tonnes before the new export rules.
The company has made it clear the ban is a pressing issue, which has already affected its ratings.
Indonesia, with a population of 240 million, is the world's premier thermal coal exporter, a nickel, bauxite and tin powerhouse and is also rich in gold and copper.
Sign Up for the Copper Digest
Turquoise Hill's stock tanks on Mongolia troubles
The Vancouver-based miner reported expansion costs at its Oyu Tolgoi mine could increase over $1 billion.
More Copper News
Rio faces $1.9bn cost blowout, delays at Oyu Tolgoi
China's commodity demand holds up, with copper the exception


text:
With the right messaging, we can win back Labour Leavers
Labour has done an admirable job of not letting Brexit force an unnecessary division between its Leave and…
Mike Buckley & Christabel Cooper
10th December, 2019, 4:14 pm
Rayner says she could back a Labour Brexit deal
Angela Rayner, often tipped as a future party leadership contender, revealed that she could back a Labour-negotiated Brexit…
10th December, 2019, 8:20 am
I'm a staunch Remainer – and I think Corbyn's Brexit position makes sense
A few weeks ago, Jeremy Corbyn made clear what had been hinted at for months: he would remain…
Josiah Mortimer
9th December, 2019, 11:00 am
"Johnson is deliberately misleading the people" – Jeremy Corbyn's full speech
Below is the full text of Jeremy Corbyn's speech on Brexit this morning, in which he revealed leaked…
Our message from Labour's battle bus? This is not a Brexit election
It was heartwarming to see so many activists out in the cold weather and enthused by our transformative…
Lara McNeill
6th December, 2019, 8:49 am
Urgent memo to Labour activists. Go where you are most needed.
There is just one week to go until polling day, and Labour is not currently on track to…
Pro-EU campaign group draws up list of 25 target seats
New pro-EU campaign group Vote for a Final Say is set to target 25 seats across the country…
26th November, 2019, 7:00 pm
Corbyn reveals plan to adopt "neutral stance" as PM in EU referendum
Jeremy Corbyn has revealed during the BBC Question Time Leaders Special programme that he would take a "neutral stance"…
22nd November, 2019, 7:41 pm
WATCH: Labour candidate suggests Corbyn would back soft Brexit
Lloyd Russell-Moyle, who is standing for Labour in Brighton Kemptown, suggested today that Jeremy Corbyn would back a…
Brexit or no Brexit, Labour must reset the immigration system
The immigration system is needlessly complex and getting worse. The public has little confidence in it, and those…


text:
Home » News » MNRE Eases Bidder Selection Norms under PM KUSUM Scheme
MNRE Eases Bidder Selection Norms under PM KUSUM Scheme
By Manu Tayal/ Updated On Tue, Aug 20th, 2019
MNRE further added that, to have wider competition all eligible bidders shortlisted on the basis of technical and financial criteria stipulated in the bidding document and under the price bracket of (L1 + 10 percent of L1) will be empanelled on acceptance of L1 price and have equal opportunity to work in market mode.
In a bid to provide further boost for the installation of 17.50 lakh solar powered agricultural pumps in the country, the Ministry of New and Renewable Energy (MNRE) has made some amendments in its earlier issued guidelines for implementation of Pradhan Mantri Kisan Urja Suraksha evam utthan Mahabhiyan (PM KUSUM) scheme.
For centralized tendering, the designated CPSUs will issue region-wise/ state-wise tenders, however, their role will be limited to selection of bidders and discovery of rates.
As per the new amendments of the government, to ensure quality and post installation services only manufacturers of solar water pumps or manufacturers of solar panels would be allowed to participate in the bidding process.
However, in case the number of such bidders empanelled within the price bracket of (L1 + 10 percent of L1) are less than 5, the price bracket shall be extended to (L1 + 15 percent of L1), so that enough number of bidders are empanelled for better competition, it added.
Further, the selection of beneficiaries and implementation of scheme would be the responsibility of the State Implementation Agency.
However, MNRE's earlier guidelines says "for centralized tendering the designated CPSUs may come out region-wise/State-wise tenders, however, their role will be limited to selection of bidders and discovery of rates. To ensure quality and post installation services only manufacturers of solar water pumps or controllers or manufacturers of solar panels would be allowed to participate in the bidding process. Normally, three bidders would be selected and they have to match L1 rates and the quantity allocated to those who agree to match the L1 rates them would be 50 percent, 30 percent, and 20 percent of the total tender quantity respectively in the ascending order of rates quoted by them. Number of bidders selected may vary depending upon the tender quantity. The selection of beneficiaries and implementation of scheme would be the responsibility of the State Implementation Agency. Cluster based approach would be used for allocation of districts to the selected bidders to optimize the resources and ensure quality services made available to the farmer. As far as possible contiguous districts would be allotted to the successful bidders, with the total requirements of pumps in the allocated area matching the quantity allotted to them."
Tags: India, KUSUM Scheme, MNRE, PM KUSUM Scheme, Solar Panels, solar panels manufacturers, solar water pumps, solar water pumps manufacturers
Manu Tayal
Manu is an Associate Editor at Saur Energy International where she writes and edits clean & green energy news, featured articles and interview industry veterans with a special focus on solar, wind and financial segments.