Second-Order Hyperproperties and Common Knowledge

Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger

In this blogpost, we explain the essential concepts of the paper Second-Order Hyperproperties [1] based on common knowledge. Unlike hyperlogics with first-order trace quantification, the new logic Hyper²LTL can express complex properties like common knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties.

Hyperproperties and the Muddy Children

Hyperproperties express specifications over relations of traces. One of the famous properties in distributed, multi-agent systems that relates traces is knowledge. In a multi-agent system, if an agent knows a fact, then this fact has to be true on every execution of the system that the agent cannot distinguish from the current one. The following is an example of a distributed system with five agents and is a variation of the Muddy Children problem with agents Alice, Bob, Suzy, Charly, and Eve. The agents are standing in a circle facing each other such that everyone sees everyone, each wearing a colored helmet. The specification of the problem is that, in a turn-based manner, every agent turns red exactly when it knows the color of its helmet. It is a known fact that helmets are partitioned into blue and black. In this instance of the problem, there is exactly one blue helmet. We now check what agent Charly (C) knows:

Charly sees that Suzy wears a blue helmet and that Eve, Alice, and Bob wear black helmets. Does he know what color his own helmet has? To verify that he knows the color, Charly has to check every possible (indistinguishable) case where his current observation would be the same. Exactly two scenarios are possible, the one where only Suzy wears a blue helmet and the one where both, Suzy and Charly wear blue helmets. Since in both scenarios, the truth value of “Charly wears a blue helmet” is different, he cannot know the color of his helmet yet. Using the knowledge operator indexed by the agent and an atomic proposition that is true iff Charly's helmet is blue, we say

\[\neg K_C (\mathit{CharlyHelmetBlue}),\]

i.e., it is not true that Charly knows that his helmet is blue. The same reasoning works for Alice, Eve, and Bob. The situation is different for Suzy. In her observation, no agent that she sees wears a blue helmet. However, it is known by everyone that there must be at least one blue helmet. If she compares the color of her helmet in all indistinguishable scenarios, i.e., only the current one, it is always blue. Therefore, she actually knows the color of her helmet and turns red immediately to show everyone that she knows it.

The reasoning continues in round two. Eve, Alice, Bob, and Charly see only one blue helmet and know that Suzy voted in the first round, i.e., she didn’t see another blue helmet. Otherwise, her turning red would be incorrect behavior. Therefore, after the second round, all agents know the color of their helmets since no world is indistinguishable from the current one.

HyperLTL [2] is designed to specify hyperproperties like knowledge over multiple traces. With HyperLTL, we can verify that whenever an agent turns red, it knows the color of its helmet. We use the standard LTL operator U, which specifies that “some formula holds until another one is true”:

This formula checks that for all trace pairs \(\pi, \pi’\), such that \(\pi’\) looks the same for Suzy as \(\pi\) until Suzy turns red, on all these traces the color of the helmet has to be the same. The quantification is over pairs of individual traces, which is sufficient to verify knowledge and, in general, relational properties over traces. But can we go one step further? What about verifying that everyone knows that everyone knows that everyone knows… the color of its helmet?

Common Knowledge

This property is called common knowledge. To verify common knowledge, we first look at the property everyone knows, i.e., \(E \varphi\). This property does not relate knowledge of different agents, the only thing to verify is the knowledge of each agent separately. We can clearly see each agent knows the color of their helmet after two steps. The formula we verify is the same as for knowledge but with an additional conjunction over all agents. In general for the muddy children, every agent knows their color after \(j+1\) steps, where \(j\) is the number of blue helmets. Common Knowledge, however, specifies certain knowledge of agents over the knowledge of other agents. The operator is \(C\) and is defined as \[C\varphi = E^\omega \varphi,\] which means an infinite chain of everyone knows that everyone knows that … \(\varphi\) holds. Not only does everyone know the fact, but also everyone knows that everyone knows the fact, and so forth. In our example, we can state that after \(j+1\) steps, each helmet color is common knowledge. The reasoning is iterative: starting from every agent with its own partial view, we have to add all indistinguishable worlds for all other agents based on their local view. For example, if we start from Suzy’s point of view, she knows every other helmet color but her own. If we project her view to, for example, Charly, then we also have to add the possible world where Charly wears a blue helmet. This is clearly a possible scenario for Charly.

During these iterations, all possible worlds are collected, adding all possible helmet colors to the agents. In our example, common knowledge is only true in the second step after one round of communication. Here, common knowledge is equal to everyone knows that everyone knows.

Common knowledge is not expressible in HyperLTL. It is not expressible in any decidable hyperproperty language with first-order quantification over traces 3]. Instead, second-order quantification, i.e., quantification over sets of traces, is necessary and introduced with the logic Hyper²LTL.

Second-Order Hyperproperties

The logic Hyper²LTL introduces quantifications over arbitrary sets of traces. The syntax and semantics are a direct extension of HyperLTL. The following formula specifies the set of traces that must be considered when verifying common knowledge.

There are multiple conceptual changes in the semantics compared to HyperLTL. We explain each of those in the following:

(1) Existential and universal quantification over sets of traces. We use variables (denoted as capitalized letters) to refer to and restrict the set of traces in the body of the formula. In this formula, we check for all sets of traces that satisfy a certain property.

(2) First-order quantification over traces can now be defined with respect to previously quantified sets of traces and

(3) with respect to traces in the system. The system traces are captured by a special symbol, in this case, \(\mathit{System}\).

(4) We can state that explicit traces are in a certain trace set. This is especially useful when defining a set of traces as fixpoints surrounding a starting trace, as in common knowledge.

(5) HyperLTL formulas can be used to define the trace sets.

(6) The body of the formula can then be an arbitrary HyperLTL formula with trace variables originating in the trace set variables or the system traces.

To precisely express common knowledge, we need to add an additional constraint to the formula: The set X has to be the least fixpoint that satisfies the indistinguishability condition. We achieve this by stating that all subsets of X do not satisfy the property, which can directly be expressed in Hyper²LTL. Many second-order properties follow similar fixpoint reasoning to define the trace sets. Aiming for algorithmic solutions to verify second-order hyperproperties, we introduce the fragment Hyper²LTL_fp.

Model-Checking Second-Order Hyperproperties

The huge expressivity of Hyper²LTL leads to an undecidable model-checking problem. However, there is a rich fragment of Hyper²LTL, called fixpoint-Hyper²LTL_fp, for which we propose a sound and efficient algorithm. The “fp” in Hyper²LTL_fp stands for “fixpoint”, and the definition of quantified sets of traces is limited to fixpoint reasoning. The common knowledge formula in Hyper²LTL_fp is the following:

The minimality condition of the fixpoint that we did not state in the Hyper²LTL common knowledge formula is now baked in the formalism with the operator \(\curlyvee\). It specifies that all quantified sets satisfy a minimality condition. In the shown formula, the reasoning is iterative, starting from \(\pi\), we add every indistinguishable trace until a fixpoint is reached, i.e., all traces in \(X\) have at least one indistinguishable trace in the set. In the restricted setting of every second-order trace set being unique, we can verify second-order hyperproperties. Our iterative model-checking algorithm works with over-and underapproximations of the quantified sets of traces.

In each iteration, we first traverse the second-order quantifiers in an outside-in direction and compute lower- and upper-bounds on each trace set. We then traverse the first-order prefix in an inside-out fashion using the current second-order approximations. We use the under- and overapproximations for the verification of existentially and universally quantified trace variables, respecitvely. If the current approximations are not precise enough to witness a property’s satisfaction (or violation), we repeat and try to compute better approximations. We use standard automata constructions on first-order hyperproperties to verify the remaining first-order property. Over-approximations can, for example, be obtained by automata learning, and under-approximations by fixpoint computiations. We used these techniqes in our tool HySo, which can be found here.

Summary

With Hyper²LTL, we have introduced a natural specification language and a general model-checking approach for second-order hyperproperties. Hyper²LTL provides a general framework for a wide range of relevant hyperproperties, including common knowledge and asynchronous hyperproperties, which could previously only be studied with specialized logics and mechanisms.

References

[1] Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger: Second-Order Hyperproperties. CAV 2023.

[2] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez: Temporal Logics for Hyperproperties. POST 2014

[3] Ron van der Meyden, Nikolay V. Shilov: Model Checking Knowledge and Time in Systems with Perfect Recall (Extended Abstract). FSTTCS 1999