Temporal Hyperproperties for Population Protocols

TL;DR

This paper explores hyperproperties in population protocols, revealing that verifying HyperLTL properties is generally undecidable, but certain restricted cases are decidable with high complexity.

Contribution

It introduces the first study of hyperproperties in infinite-state population protocols and establishes decidability results for specific subclasses.

Findings

Verification of monadic HyperLTL without next operator is decidable in 2-EXPSPACE.

HyperLTL verification becomes undecidable with extensions such as the next operator.

Population protocols serve as a suitable model for hyperproperty analysis in distributed systems.

Abstract

Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL called HyperLTL. Most verification efforts for HyperLTL are restricted to finite-state systems, usually defined as Kripke structures. In this paper we study hyperproperties for an important class of infinite-state systems. We consider population protocols, a popular distributed computing model in which arbitrarily many identical finite-state agents interact in pairs. Population protocols are a good candidate for studying hyperproperties because the main decidable verification problem, well-specification, is a hyperproperty. We first show that even for simple (monadic) formulas, HyperLTL verification for population protocols is undecidable. We then turn our attention to immediate observation population protocols, a simpler and well-studied subclass of population protocols. We show that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable.