Hypernode Automata

TL;DR

Hypernode automata introduce a novel automata-based framework for asynchronous hyperproperties by combining fully asynchronous hypernode logic at the node level with automata-driven synchronization through action-labeled transitions. The logic FO[precsim] allows expressing trace-relational properties via stutter-reduced prefixing, while the hypernode automata provide a scalable, decidable model-checking route over action-labeled Kripke structures using stutter-free automata and an automata-theoretic filtration. The authors demonstrate practical expressiveness by formalizing observational determinism and dynamic declassification, and prove decidability with a doubly exponential bound in the number of trace variables. This approach decouples asynchrony from synchronization and opens avenues for extending to Büchi acceptance and more complex verification tasks, offering a principled, automata-based path to automatic verification of asynchronous hyperproperties.

Abstract

We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automaton. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.

Figures (8)

• Figure 1: Hypernode automaton $\mathcal{H}$ specifying the mutually exclusive declassification of secure information, where $\varphi_{\text{od}}(L) \overset{\text{def}}{=} \forall \pi \forall\pi' \bigwedge_{l\in L} (l(\pi) \mathop{\precsim} l(\pi') \vee l(\pi') \mathop{\precsim} l(\pi))$.
• Figure 1: Program $\mathcal{P}_{\mathrm{var}}$
• Figure 2: Run defined by the action sequence $\textit{Deb}_{y}\textit{Deb}_{z}\textit{Clear}_{}$ in the hypernode automaton from Figure \ref{['fig:spec:declass:vars']}.
• Figure 3: Stutter-free automaton $\mathcal{A}$, where $x$-trace segments have odd size, and $y$-trace segments have even size, and the first values of $x$ and $y$ are $0$.
• Figure 4: The universal stutter-free automaton $\mathcal{U}_{\{x,y\}}$ over the boolean variables $\{x,y\}$. It accepts all stutter-free unzipped trace segments over $\{x,y\}$. All states are both initial and final.

Theorems & Definitions (24)

• Example 1
• Proposition 2
• Definition 3
• Definition 4
• Definition 5
• Proposition 6
• Definition 7
• Proposition 8
• Proposition 9
• Definition 10