Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Temporal Hyperproperties for Population Protocols

Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty, César Sánchez

TL;DR

It is shown that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable.

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.

Temporal Hyperproperties for Population Protocols

TL;DR

It is shown that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable.

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.

Paper Structure

This paper contains 18 sections, 24 theorems, 14 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Population Protocols
  4. LTL and HyperLTL
  5. Rabin Automata and LTL
  6. Why Strong Fairness?
  7. Undecidability of HyperLTL
  8. Verification of HyperLTL for IOPP
  9. Immediate Observation PP and Preliminary Results
  10. Product Systems
  11. Satisfiability as a Reachability Problem
  12. K-blind Sets
  13. LTL and HyperLTL Verification
  14. A Structural Bound in Product Systems
  15. Transfer Flows
  16. ...and 3 more sections

Key Result

theorem 1

Given $\Sigma$ a finite set and $\varphi$ an "LTL formula" over $\Sigma$, one can compute, in time doubly-exponential in $|\varphi|$, a "deterministic Rabin automaton" $\mathcal{A}_{\varphi}$ over $\Sigma$, of doubly-exponential size, that recognizes (the language of) $\varphi$.

Figures (5)

  • Figure 1: Gadget for the monomial $X_1 X_2 X_3$ for variables $\{X_1,X_2,X_3,X_4,X_5,X_6\}$.
  • Figure 2: Gadget initializing three copies of variables $X_1$ and $X_2$.
  • Figure 3: Gadget simulating instruction $l_k:\mathsf{inc}(c_i)$. The notation is Petri net-inspired: circles are states, squares are transitions and a dashed line is an observation.
  • Figure 4: Gadget simulating instruction $l_k:\mathsf{test_0}(c_i,j)$.
  • Figure 5: Dashed arrows correspond to value $0$, no arrow corresponds to $\#$. The product witness $H$ is represented with colored arrows. We do not depict $H$ when its value is $0$.

Theorems & Definitions (47)

  • theorem 1: EKS18
  • theorem 2
  • proposition 1: Hack76
  • lemma 1
  • proof
  • lemma 2
  • proof
  • definition 1
  • remark 1
  • definition 2
  • ...and 37 more