Carter,
Thanks for your question, it pointed out to me something I realized I previously thought about but then forgot because I internalized it. The question is:
don’t understand how variables are picked out in the notation AAE\phi
In my mind, this basically deals with the strange binding structure in HyperLTL. I think this is covered in section 3, though probably not as concretely as to answer this question. The answer is that in HyperLTL, variables are not explicitly bound via binders, but instead they are manipulated by means of focus formulas <\phi_1,...,\phi_n> or multi-state propositions
If we have a formula like:
A A E \phi
then inside \phi we are allowed to write focus formulas and multi state propositions. The focus formulas consist of n propositions that speak about single traces, and the multi state propositions (e.g., LE_{1,3}) take values along an n trace corresponding to the function's valuation along that n trace. (e.g., ( 1,1,2,... | 1,2,2,... | 1,3,3,.... ) would be one 3-trace).
Focus formulas (those of the form <\phi_1,...,\phi_n>) say "to be valid in this collection of states, each of my components has to be valid pointwise." Note that I didn't say set of states, because the focus formula is ordered in a way that corresponds to the structure in the top level formula (A A E, etc...). The way to visualize this is taking a set of n traces and silmautaneously walking along them at the same time (in a security sense, this roughly corresponds to secure multi execution) and applying the formula pointwise to each trace in the walk. So if I consider the formula <T,T,F> (where t is \top and F is \bot) it will never be valid, because it will essentially say that the last state I "walk along" will never have the opportunuity to be true. If I consider a formula <T,p,T> it will be true only in the collection of traces (t1,t2,t3) where in t2 p is always true.
The multi state propositions can be thought of as n-ary (where n is the number of A's and E's) functions functions from state^n -> Bool, and we presuppose that the function has been defined. Because of this, you would define functions such as:
LE_{1,2}(s1,s2,s3) = { the set of states where s1 and s2 are low equivalent }
Note that in HyperLTL you have to define this set yourself: the logic doesn't include any of the machinery to talk about what a state is, and which are low equivalent, etc..
In the end:
A A E G( high-in-equiv_{1,3} ∧ low-equiv_{2,3})
Says, this formula is true whenever it is globally true that along any 3 trace: ((the first and last states are low equivalent) and (the second and last states are low equivalent)), and we have to define which states are low equivalent. (e.g., we can write them down explicitly or use the bonding construction given in the paper.)
Thanks for the feedback, I'll have to think about how to phrase this so it makes sense in the paper.