2024/10/15 by Nicolas Waldburger, Waldburger, Nicolas, Chana Weil-Kennedy +5
Computer Science · #Advanced Database Systems and Queries #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Mobile Agent-Based Network Management
paper · pdf · doi:10.48550/arxiv.2410.11572
openalex publication_date 2024/10/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.