# Verifying hyperproperties with TLA --- ### Preliminaries - A **behavior** is a sequence of states. - A **step** is a pair of consecutive states. - A **state machine** is a behavior model which is described by an **initial predicate** $\mathcal{I}$ and a **next-state predicate** $\mathcal{N}$. --- ### Example A 12-hour hour-minute clock with initial state 12:00. $$\mathcal{I} \triangleq (min = 0) \land (hour = 12)$$ The next state predicate would be \begin{align} \mathcal{N} \triangleq \; &\land\; min' = (min + 1) \bmod 60 \\ & \begin{aligned}\land\; hour' = &\text{ if } min = 59 \\ &\text{ then } hour' = (hour \bmod 12) + 1 \\ & \text{ else } hour\end{aligned} \end{align} --- ### Example (contd.) The spec of our clock is then: $$ Spec = \mathcal{I} \land \Box\:\mathcal {N}$$ --- ### Properties A **property** is a predicate on behaviors. We denote that the property $P$ is true for behaviour $b$ by $b \vDash P$ --- ### Properties There is a correspondence: \begin{align} \text{Subsets of a set S} \quad&\Leftrightarrow \quad\text{Predicates on S}\\ \{s \in S : P(s)\} \quad &\leftrightarrow \quad P\\ \cup \quad&\leftrightarrow \quad\lor\\ \dots\end{align} We may thus think of a property as -- a predicate on behaviors -- a set of behaviors satisfying the predicate --- ### Hyperproperties A **hyperproperty** is a predicate on sets of behaviors, and by the earlier correspondence, a predicate on properties. For example, for a property $P$, define the hyperproperty $\mathcal{H}(P)$ to be true if any two terminating behaviors satisfying $P$ having different initial values of $x$ have different terminal values of $y$. --- ### Hyperpoperties Since we can "pull out" all the quantifiers, $\mathcal{H}(P)$ may be written as $$\circ\: b_1\in P: \dots :\circ b_k\in P : J(b_1,\dots, b_k)$$ where $\circ$ can be $\exists$ or $\forall$ and J doesn't depend on P. If $\circ = \forall$ then we can let $P^k$ be the state machine running $k$ copies of $P$ in parallel we can write $$\forall\: b\in P^k : J(\pi_1(b), \dots, \pi_k(b))$$ --- ### Hyperpoperties We will deal with something more general, formulas of the form \begin{align} \forall\: b_1 \in P: \dots \forall\: b_j\in P : K(b_1, \dots, b_j) \Rightarrow& \\ \exists\: b_{j+1}\in P: \dots \exists \:b_k \in P : L (b_1, \dots b_k). \end{align} If we replace "$\forall\: b\in P$" by "$\forall\: b : P(b) \Rightarrow$" and "$\exists\: b\in P :$" by "$b: P(b) \land$" and simplify a little, \begin{align}\forall b_1,\dots,b_j : P(b_1) \land \dots \land P(b_j) \land K(b_1,\dots, b_j) \Rightarrow \\ \exists\: b_{j+1}, \dots b_k : P(b_{j+1}) \land \dots \land P(b_k) \land L (b_1, \dots , b_k). \end{align} --- ### Temporal logic formulas We've already the seen the temporal operator $\Box$ which we read as *henceforth*. The temporal existential quantifier $\#$ is used as follows. An expression of the form $b\vDash \:\# x: F$ means there exists a behavior (which we denote by $b$) such that $\hat{b}\vDash F$ is true. A temporal logic fomula (TLF) contains only these two operators and predicate-logic expressions. --- ### TLFs We want to express the hyperproperty in terms of a single-variable TLF. The $k$ behaviors $b_i$ are encoded in a single variable $b$. We assume the formula depends only on the values that the states of $b_i$ assign to certain variables, say $V_i = \{v_1^i, \dots, v_n^i\}$, and there's one such set for each $b_i$. **Step 1** Rewrite $P$ as $\tilde{P}$ which contains only elements of $V$. --- ### TLFs To express this in terms of a single behavior $b$ for the state machine $P^k$, we need to substitute $V_i$ with new variables, let's call them $\mathbf{x_i}$. **Step 2** Replace $P(b_i)$ with $\tilde{P}(\mathbf{x_i})$. The values that $b$ assigns to $\mathbf{x_i}$ are thus the values that the behavior $b_i$ assigns to $V$. --- It's now easy to write down a TLF. \begin{align} \vDash \tilde{P}(\mathbf{x_1}) \land &\dots \tilde{P}(\mathbf{x_j})\land \tilde{K} (\mathbf{x_1}, \dots, \mathbf{x_j}) \Rightarrow \\ &\#\:\mathbf{x_{j+1}}, \dots, \mathbf{x_k} : \tilde{P}(\mathbf{x_{j+1}})\land \dots \land \tilde{P}(\mathbf{x_k}) \land \tilde{L}(\mathbf{x_1}, \dots, \mathbf{x_k})\end{align} *We can express this in terms of RTLA and then by taking into account stuttering insensitivity, write it in terms of TLA!*