Liveness in Broadcast Networks

TL;DR

This paper presents polynomial-time algorithms for liveness and fair liveness verification in broadcast networks, resolving open complexity questions and enabling model checking against linear temporal logic specifications.

Contribution

It introduces efficient algorithms for liveness verification in broadcast networks, closing a decade-long complexity gap and extending to model checking with temporal logic.

Findings

Polynomial-time algorithm for Liveness Verification.

Polynomial-time algorithm for Fair Liveness Verification.

Reduction techniques for model checking problems.

Abstract

We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is Liveness Verification. It asks whether there is a computation such that one of the clients visits a final state infinitely often. The complexity of the problem has been open since 2010 when it was shown to be P-hard and solvable in EXPSPACE. We close the gap by a polynomial-time algorithm. The algorithm relies on a characterization of live computations in terms of paths in a suitable graph, combined with a fixed-point iteration to efficiently check the existence of such paths. The second problem is Fair Liveness Verification. It asks for a computation where all participating clients visit a final state infinitely often. We adjust the algorithm to also solve fair liveness in polynomial time. Both problems can be instrumented to answer model checking questions for broadcast networks against linear time temporal logic specifications. The first problem in this context is Fair Model Checking. It demands that for all computations of a broadcast network, all participating clients satisfy the specification. We solve the problem via the Vardi-Wolper construction and a reduction to Liveness Verification. The second problem is Sparse Model Checking. It asks whether each computation has a participating client that satisfies the specification. We reduce the problem to Fair Liveness Verification.

Equations

$${post}_{?a}(S)=\{r^{\prime }\in Q\mid \exists r\in S:r\stackrel{?a}{\to }{r}^{\prime }\}$$

$${enabled}_{?a}(S)=\{r\in S\mid {post}_{?a}(\{r\})\ne \varnothing \}.$$

$$S_i^{\prime }=\{\begin{array}{rlr}& (S_i\setminus {Kill}_i)\cup {Gen}_i,& \text{ for }i\ne j,\\ & (U_j\setminus {Kill}_j)\cup {Gen}_j\cup \{s^{\prime }\},& \text{ for }i=j\end{array}$$

$$(\{s_1\},\dots ,\{s_m\}){\to }_G({\mathrm{Target}}_c(s_1,c_1),\dots ,{\mathrm{Target}}_c(s_m,c_1))$$

$$(\{s_1\},\dots ,\{s_m\})$$

$${\to }_G({\mathrm{Target}}_c(s_1,c_2),\dots ,{\mathrm{Target}}_c(s_m,c_2))$$

$${\to }_G\dots$$

$${\to }_G({\mathrm{Target}}_c(s_1,c),\dots ,{\mathrm{Target}}_c(s_m,c)).$$

$$S_{j+1}^t=(U_t\setminus {Kill}_t)\cup {Gen}_t\cup \{s^{\prime }\}.$$

$$c_j\stackrel{a}{\to }{d}^1\stackrel{a}{\to }{d}^2\stackrel{a}{\to }\cdots \stackrel{a}{\to }{d}^{|Q{|}^{\ell -(j+1)}}=d.$$

$$|Q{|}^{\ell -(j+1)}\cdot |{post}_{?a}(p)\cup \{p,s^{\prime }\}|\le |Q{|}^{\ell -(j+1)}\cdot |Q|=|Q{|}^{\ell -j}$$

$$X_i^{\prime }=$$

$$\cup$$

$$X_i^{\prime }=$$

$$\cup$$

$$C={post}_C^{+}(\{s_1\},\dots ,\{s_m\})\cap {pre}_C^{\ast }(\{s_1\},\dots ,\{s_m\}).$$

$$P_F=(\bar{Q},\tilde{I},\bar{\delta })\text{where}\bar{Q}=Q\cup \hat{Q}\cup \tilde{Q}.$$

$$c{\stackrel{u^{\prime }}{\to }}_{{\mathcal{N}}_F}f({\sigma }_1){\stackrel{a}{\to }}_{{\mathcal{N}}_F}g{\stackrel{n}{\to }}_{{\mathcal{N}}_F}\cdots {\stackrel{n}{\to }}_{{\mathcal{N}}_F}d(\sigma ).$$

$$c(\pi )[j]=\{\begin{array}{rl}q,& \text{if}{pr}_j(\pi )=\epsilon ,\\ \tilde{q},& \text{otherwise}.\end{array}$$

$$c{\to }_{{\mathcal{N}}_F}^{+}c(\pi ){\stackrel{!n}{\to }}_{{\mathcal{N}}_F}\cdots {\stackrel{!n}{\to }}_{{\mathcal{N}}_F}c.$$

$$c_0=c\stackrel{w_1}{\to }{d}_1{\stackrel{n}{\to }}^{\ast }{c}_1\stackrel{w_2}{\to }{d}_2{\stackrel{n}{\to }}^{\ast }{c}_2\to \cdots \to c_{n-1}\stackrel{w_n}{\to }{d}_n{\stackrel{n}{\to }}^{\ast }c.$$

$$\mathcal{N}(d)[j]=q\text{if}d[j]=q/\tilde{q}/\hat{q}.$$

$$c=\mathcal{N}(c_0)\stackrel{w_1}{\to }\mathcal{N}(d_1)\stackrel{w_2}{\to }\mathcal{N}(d_2)\stackrel{w_3}{\to }\cdots \stackrel{w_n}{\to }\mathcal{N}(d_n)=c.$$

$$\phi ::=p\in \mathcal{A}|\neg \phi |\phi \vee \phi |\mathcal{X}\phi |\phi \mathcal{U}\phi .$$

$$w,i$$

$$w$$

$$w\models \psi \text{if and only if}w\in L(B_{\psi }).$$

$$(q,p)\stackrel{op}{\to }(q^{\prime },p^{\prime })\in {\delta }_{\neg \phi }\text{if}q\stackrel{op}{\to }{q}^{\prime }\in \delta \text{and}p\stackrel{\lambda (q)}{\to }{p}^{\prime }\in {\delta }_B.$$

$$b=(b_1,\dots ,b_k).$$

$${\mathrm{proj}}_Q:(Q\times Q_B{)}^k\to Q^k$$

$${\pi }^{\prime }(0)=\pi (0)\times (b_1(0),\dots ,b_k(0)).$$

Full text

Both problems can be instrumented to answer model checking questions for broadcast networks against linear time temporal logic specifications. The first problem in this context is Fair Model Checking. It demands that for all computations of a broadcast network, all participating clients satisfy the specification. We solve the problem via the Vardi-Wolper construction and a reduction to Liveness Verification. The second problem is Sparse Model Checking. It asks whether each computation has a participating client that satisfies the specification. We reduce the problem to Fair Liveness Verification.

1 Introduction

Parameterized systems consist of an arbitrary number of identical clients that communicate via some mechanism like shared memory or message passing [3]. Parameterized systems appear in various applications. In distributed algorithms, a group of clients has to form a consensus [32]. In cache-coherence protocols, coherence has to be guaranteed for data shared among threads [12]. Developing parameterized systems is difficult. The desired functionality has to be achieved not only for a single system instance but for an arbitrary number of clients that is not known a priori. The proposed solutions are generally tricky and sometimes buggy [2], which has lead to substantial interest in parameterized verification [7], verification algorithms for parameterized systems.

Broadcast networks are a particularly successful model for parameterized verification [39, 26, 22, 23, 19, 8, 14, 13, 9, 6, 4]. A broadcast network consists of an arbitrary number of identical finite-state automata communicating via passing messages. We call these automata clients, because they reflect the interaction of a single client in the parameterized system with its environment. When a client sends a message (by taking a send transition), at the same time a number of clients receive the message (by taking a corresponding receive transition). A client ready to receive a message may decide to ignore it, and it may be the case that nobody receives the message.

What makes broadcast networks interesting is the surprisingly low complexity of their verification problems. Earlier works have concentrated on safety verification. In the coverability problem, the question is whether at least one participating client can reach an unsafe state. The problem has been shown to be solvable in polynomial time [13]. In the synchronization problem, all clients need to visit a final state at the same time. Although seemingly harder than coverability, it turned out to be solvable in polynomial time as well[25]. Both problems remain in $\P$ if the communication topology is slightly restricted [4], a strengthening that usually leads to undecidability results [14, 4].

The focus of our work is on liveness verification and model checking. Liveness properties formulate good events that should happen during a computation. To give an example, one would state that every request has to be followed by a response. In the setting of broadcast networks, liveness verification was studied in [14]. The problem generalizes coverability in that at least one client needs to visit a final state infinitely many times. The problem was shown to be solvable in $\EXPSPACE$ by a reduction to repeated coverability in Petri Nets [24, 20]. The only known lower bound, however, is $\P$-hardness [13].

Our main contribution is an algorithm that solves the liveness verification problem in polynomial time. It closes the aforementioned gap. We also address a fair variant of liveness verification where all clients participating infinitely often in a computation have to see a final state infinitely often, a requirement known as compassion [36]. We give an instrumentation that compiles away compassion and reduces the problem to finding cycles. By our results, safety and liveness verification have the same complexity, a phenomenon that has been observed in other models as well [26, 21, 19, 27].

At the heart of our liveness verification algorithm is a fixed-point iteration terminating in polynomial time. It relies on an efficient representation of computations. We first characterize live computations in terms of paths in a suitable graph. Since the graph is of exponential size, we cannot immediately apply a path finding algorithm. Instead, we show that a path exists if and only if there is a path in some normal form, a result inspired by [25]. Paths in normal form can then be found efficiently by the fixed-point iteration.

Our results yield efficient algorithms for model checking broadcast networks against linear time temporal logic (LTL) specifications [35]. Formally, we consider two variants of model checking, like for liveness verification. The first variant incorporates a notion of fairness. Given a broadcast network and a specification, it demands that in each computation, all clients satisfy the specification. The second variant asks for each computation having at least one client satisfying it. We solve both problems by employing the Vardi-Wolper construction [40] and by applying the aforementioned fixed-point iteration for liveness verification. The results show that the given broadcast network only contributes a polynomial factor to the running time needed for model checking.

The paper at hand is an extension of the conference version that appeared in [11]. It features a new section, namely Section 5, which shows how model checking problems for broadcast networks can be solved by applying the fixed-point iteration for liveness verification. More precise, the section introduces two new model checking problems and presents algorithms as well as the corresponding time-complexity analyses.

Related Work

We already discussed the related work on safety and liveness verification of broadcast networks. Broadcast networks [14, 39, 22] were introduced to verify ad hoc networks [31, 38]. Ad hoc networks are reconfigurable in that the number of clients as well as their communication topology may change during the computation. If the transition relation is compatible with the topology, safety verification has been shown to be decidable [29]. Related studies do not assume compatibility but restrict the topology [28]. If the dependencies among clients are bounded [33], safety verification is decidable independent of the transition relation [41, 42]. Verification tools turn these decision procedures into practice [34, 17]. D’Osualdo and Ong suggested a typing discipline for the communication topology [18]. In [4], decidability and undecidability results for reachability problems were proven for a locally changing topology. The case when communication is fixed along a given graph was studied in [1]. Topologies with bounded diameter were considered in [15]. Perfect communication where a sent message is received by all clients was studied in [22]. Networks with communication failures were considered in [16]. Probabilistic broadcast networks were studied in [5]. In [6], a variant of broadcast networks was considered where the clients follow a local strategy.

Broadcast networks are related to the leader-contributor model. It has a fixed leader and an arbitrary number of identical contributors that communicate via a shared memory. The model was introduced in [26]. The case when the leader and all contributors are finite-state automata was considered in [23] and the corresponding reachability problem was proven to be $\NP$-complete. In [9], the authors took a parameterized complexity look at the reachability problem and proved it fixed-parameter tractable. Liveness verification for this model was studied in [19]. The authors show that repeated reachability is $\NP$-complete. From a viewpoint of parameterized complexity, the problem was considered in [10]. Networks with shared memory and randomized scheduler were studied in [8]. For a survey of parameterized verification we refer to [7].

2 Broadcast Networks

We introduce the model of broadcast networks of interest in this paper. Our presentation avoids an explicit characterization of the communication topology in terms of graphs. A broadcast network is a concurrent system consisting of an arbitrary but finite number of identical clients that communicate by passing messages to each other. Formally, it is a pair $\mathcal{N}=(D,P)$. The domain $D$ is a finite set of messages that can be used for communication. A message $a\in D$ can either be sent, $!a$, or received, $?a$. The set $\mathit{Ops}(D)=\{!a,?a\mid a\in D\}$ captures the communication operations a client can perform. For modeling the identical clients, we abstract away the internal behavior and focus on the communication with others via $\mathit{Ops}(D)$. With this, the clients are given in the form of a finite state automaton $P=(Q,I,\delta)$, where $Q$ is a finite set of states, $I\subseteq Q$ is a set of initial states, and $\delta\subseteq Q\times\mathit{Ops}(D)\times Q$ is the transition relation. We extend $\delta$ to words in $\mathit{Ops}(D)^{*}$ and write $q\xrightarrow{w}q^{\prime}$ instead of $(q,w,q^{\prime})\in\delta$.

During a communication phase in $\mathcal{N}$, one client sends a message that is received by a number of other clients. This induces a change of the current state in each client participating in the communication. We use configurations to display the current states of the clients. A configuration is a tuple $c~{}=~{}(q_{1},\dots,q_{k})\in Q^{k}$, $k\in\mathbb{N}$. We use $\operatorname{Set}(c)$ to denote the set of client states occurring in $c$. To access the components of $c$, we use $c[i]=q_{i}$. As the number of clients in the system is arbitrary but fixed, we define the set of all configurations to be $\mathit{CF}=\bigcup_{k\in\mathbb{N}}Q^{k}$. The set of initial configurations is given by $\mathit{CF}_{0}=\bigcup_{k\in\mathbb{N}}I^{k}$. The communication is modeled by a transition relation among configurations. Let $c^{\prime}=(q^{\prime}_{1},\dots,q^{\prime}_{k})$ be another configuration with $k$ clients and $a\in D$ a message. We have a transition $c\xrightarrow{a}_{\mathcal{N}}c^{\prime}$ if the following conditions hold: (1) there is a sender, an $i\in[1..k]$ such that $q_{i}\xrightarrow{!a}q^{\prime}_{i}$, (2) there is a number of receivers, a set $R\subseteq[1..k]\setminus\{i\}$ such that $q_{j}\xrightarrow{?a}q^{\prime}_{j}$ for each $j\in R$, and (3) all other clients stay idle, for all $j\notin R\cup\{i\}$ we have $q_{j}=q^{\prime}_{j}$. We use $\mathit{idx}(c\xrightarrow{a}_{\mathcal{N}}c^{\prime})=R\cup\{i\}$ to denote the indices of clients that contributed to the transition. For $i\in\mathit{idx}(c\xrightarrow{a}_{\mathcal{N}}c^{\prime})$, we let $\mathit{pr}_{i}(c\xrightarrow{a}_{\mathcal{N}}c^{\prime})=c[i]\xrightarrow{!a/?a}c^{\prime}[i]$ be the contribution of client $i$. If $i\notin\mathit{idx}(c\xrightarrow{a}_{\mathcal{N}}c^{\prime})$, we set $\mathit{pr}_{i}(c\xrightarrow{a}_{\mathcal{N}}c^{\prime})=\epsilon$.

We extend the transition relation to words $w\in D^{*}$ and write $c\xrightarrow{w}_{\mathcal{N}}c^{\prime}$. Such a sequence of consecutive transitions is called a computation of $\mathcal{N}$. Note that all configurations appearing in a computation have the same number of clients. We write $c\rightarrow^{*}_{\mathcal{N}}c^{\prime}$ if there is a word $w\in D^{*}$ with $c\xrightarrow{w}_{\mathcal{N}}c^{\prime}$. If $|w|\geq 1$, we also use $c\rightarrow^{+}_{\mathcal{N}}c^{\prime}$. Where appropriate, we skip $\mathcal{N}$ in the index. The definition of $\mathit{idx}$ can be extended to computations by combining all clients that contribute to one of the transitions. We also extend the definition of $\mathit{pr}_{i}$ to computations by appending the individual contributions to transitions.

We are interested in infinite computations, sequences $\pi=c_{0}\rightarrow c_{1}\rightarrow\ldots$ of infinitely many consecutive transitions. Such a computation is called initialized, if $c_{0}\in\mathit{CF}_{0}$. We use $\operatorname{Inf}(\pi)=\{i\in\mathbb{N}\mid\exists^{\infty}j:i\in\mathit{idx}(c_{j}\rightarrow c_{j+1})\}$ to denote the set of clients that participate in the computation infinitely often. Let $F\subseteq Q$ be a set of final states. Then we let $\operatorname{Fin}(\pi)=\{i\in\mathbb{N}\mid\exists^{\infty}j:c_{j}[i]\in F\}$ represent the set of clients that visit final states infinitely often.

3 Liveness

We consider the liveness verification problem for broadcast networks. Given a broadcast network $\mathcal{N}=(D,P)$ with $P=(Q,I,\delta)$ and a set of final states $F\subseteq Q$, the problem asks whether there is an infinite initialized computation $\pi$ in which at least one client visits a state from $F$ infinitely often, $\operatorname{Fin}(\pi)\neq\emptyset$. {myproblem}

Liveness Verification was introduced as Repeated Coverability in[14]. Our main contribution is the following theorem.

Theorem 3.1

Liveness Verification is $\P$-complete.

$\P$-hardness is due to [13]. Our contribution is a matching polynomial-time decision procedure. Key to our algorithm is the following lemma which relates the existence of an infinite computation to the existence of a finite one.

Lemma 1

There is an infinite computation $c_{0}\rightarrow c_{1}\rightarrow\ldots$ that visits states in $F$ infinitely often if and only if there is a finite computation of the form $c_{0}\rightarrow^{*}c\rightarrow^{+}c$ with $\operatorname{Set}(c)\cap F\neq\emptyset$.

If there is a computation of the form $c_{0}\rightarrow^{*}c\rightarrow^{+}c$ with $\operatorname{Set}(c)\cap F\neq\emptyset$, then $c\rightarrow^{+}c$ can be iterated infinitely often to obtain an infinite computation visiting $F$ infinitely often. In turn, in any infinite sequence from $Q^{k}$ one can find a repeating configuration (pigeon hole principle). This in particular holds for the infinite sequence of configurations containing final states.

Our polynomial-time algorithm for Liveness Verification looks for an appropriate reachable configuration $c$ that can be iterated. The difficulty is that we have a parameterized system, and therefore the number of configurations is not finite. Our approach is to devise a finite graph in which we search for a cycle that mimics the cycle on $c$. While the graph yields a decision procedure, it will be of exponential size and a naive search for a cycle requires exponential time. We show in a second step how to find a cycle in polynomial time.

The graph underlying our algorithm is inspired by the powerset construction for the determinization of finite state automata [37]. The vertices keep track of sets of states $S$ that a client may be in. Different from finite-state automata, however, there is not only one client in a state $s\in S$ but arbitrarily (but finitely) many. As a consequence, a transition from $s$ to $s^{\prime}$ may have two effects. Some of the clients in $s$ change their state to $s^{\prime}$ while others stay in $s$. In that case, the set of states is updated to $S^{\prime}=S\cup\{s^{\prime}\}$. Alternatively, all clients may change their state to $s^{\prime}$, in which case we get $S^{\prime}=(S\setminus\{s\})\cup\{s^{\prime}\}$.

Formally, the graph of interest is $G=(V,\rightarrow_{G})$. Vertices are tuples of sets of states, $V=\bigcup_{k\leq|Q|}\mathcal{P}(Q)^{k}$. The parameter $k$ will become clear in a moment. To define the edges, we need some more notation. For $S\subseteq Q$ and $a\in D$, let

[TABLE]

denote the set of successors of $S$ under transitions receiving $a$. The set of states in $S$ where receives of $a$ are enabled is denoted by

[TABLE]

There is a directed edge $V_{1}\rightarrow_{G}V_{2}$ from vertex $V_{1}=(S_{1},\ldots,S_{k})$ to vertex $V_{2}=(S^{\prime}_{1},\ldots,S^{\prime}_{k})$ if the following three conditions are satisfied: (1) there is an index $j\in[1..k]$, states $s\in S_{j}$ and $s^{\prime}\in S^{\prime}_{j}$, and an element $a$ from the domain $D$ such that $s\xrightarrow{!a}s^{\prime}$ is a send transition. (2) For each $i\in[1..k]$ there are sets of states $\mathit{Gen}_{i}\subseteq\mathit{post}_{?a}(S_{i})$ and $\mathit{Kill}_{i}\subseteq\mathit{enabled}_{?a}(S_{i})$ such that

[TABLE]

where $U_{j}$ is either $S_{j}$ or $S_{j}\setminus\{s\}$. (3) For each index $i\in[1..k]$ and state $q\in\mathit{Kill}_{i}$, the intersection $\mathit{post}_{?a}(q)\cap\mathit{Gen}_{i}$ is non-empty.

Intuitively, an edge in the graph mimics a transition in the broadcast network without making explicit the configurations. Condition (1) requires a sender, a component $j$ capable of sending a message $a$. Clients receiving this message are represented by (2). The set $\mathit{Gen}_{i}$ consists of those states that are reached by clients performing a corresponding receive transition. These states are added to $S_{i}$. As mentioned above, states can get killed. If, during a receive transition, all clients move to the target state, the original state will not be present anymore. We capture those states in the set $\mathit{Kill}_{i}$ and remove them from $S_{i}$. Condition (3) is needed to guarantee that each killed state is replaced by a target state. Note that for component $j$ we add $s^{\prime}$ due to the send transition. Moreover, we need to distinguish whether state $s$ gets killed or not.

The following lemma relates a cycle in the constructed graph with a cyclic computation of the form $c\rightarrow^{+}c$. It is crucial for our result.

Lemma 2

There is a cycle $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}(\{s_{1}\},\dots,\{s_{m}\})$ in $G$ if and only if there is a configuration $c$ with $\operatorname{Set}(c)=\{s_{1},\dots s_{m}\}$ and $c\rightarrow^{+}c$.

The lemma explains the restriction of the nodes in the graph to $k$-tuples of sets of states, with $k\leq|Q|$. We explore the transitions for every possible state in $c$, and there are at most $|Q|$ different states that have to be considered. We have to keep the sets of states separately to make sure that, for every starting state, the corresponding clients perform a cyclic computation.

Proof

We fix some notations that we use throughout the proof. Let $c\in Q^{n}$ be any configuration and $s\in\operatorname{Set}(c)$. By $\operatorname{Pos}_{c}(s)=\{i\in[1..n]\mid c[i]=s\}$ we denote the positions of $c$ storing state $s$. Given a second configuration $d\in Q^{n}$, we use the set $\operatorname{Target}_{c}(s,d)=\{d[i]\mid i\in\operatorname{Pos}_{c}(s)\}$ to represent those states that occur in $d$ at the positions $\operatorname{Pos}_{c}(s)$. Intuitively, if there is a sequence of transitions from $c$ to $d$, these are the target states of those positions of $c$ storing $s$.

Consider a computation $\pi=c\rightarrow^{+}c$ with $\operatorname{Set}(c)=\{s_{1},\dots,s_{m}\}$. We show that there is a cycle $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}(\{s_{1}\},\dots,\{s_{m}\})$ in $G$. To this end, assume $\pi$ is of the form $\pi=c\rightarrow c_{1}\rightarrow\dots\rightarrow c_{\ell}\rightarrow c$. Since $c\rightarrow c_{1}$ is a transition in the broadcast network, there is an edge

[TABLE]

in $G$ where each state $s_{i}$ gets replaced by the set of target states in $c_{1}$. Applying this argument inductively, we get a path in the graph:

[TABLE]

Since $\operatorname{Target}_{c}(s_{i},c)=\{s_{i}\}$,we found the desired cycle.

For the other direction, let a cycle $\sigma=(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}(\{s_{1}\},\dots,\{s_{m}\})$ be given. We construct from $\sigma$ a computation $\pi=c\rightarrow^{+}c$ in the broadcast network such that $\operatorname{Set}(c)=\{s_{1},\dots,s_{m}\}$. The difficulty in constructing $\pi$ is to ensure that at any point in time there are enough clients in appropriate states. For instance, if a transition $s\xrightarrow{!a}s^{\prime}$ occurs, we need to decide on how many clients to move to $s^{\prime}$. Having too few clients in $s^{\prime}$ may stall the computation at a later point: there may be a number of sends required that can only be obtained by transitions from $s^{\prime}$. If there are too few clients in $s^{\prime}$, we cannot guarantee the sends. The solution is to start with enough clients in any state. With invariants we guarantee that at any point in time, the number of clients in the needed states suffices.

Let cycle $\sigma$ be $V_{0}\rightarrow_{G}V_{1}\rightarrow_{G}\dots\rightarrow_{G}V_{\ell}$ with $V_{0}=V_{\ell}=(\{s_{1}\},\dots,\{s_{m}\})$. Further, let $V_{j}=(S^{1}_{j},\dots,S^{m}_{j})$. We will construct the computation $\pi$ over configurations in $Q^{n}$ where $n=m\cdot|Q|^{\ell}$. The idea is to have $|Q|^{\ell}$ clients for each of the $m$ components of the vertices $V_{i}$ occurring in $\sigma$. To access the clients belonging to a particular component, we split up configurations in $Q^{n}$ into blocks, intervals $I(i)=[(i-1)\cdot|Q|^{\ell}+1\;..\;i\cdot|Q|^{\ell}]$ for each $i\in[1..m]$. Let $d\in Q^{n}$ be arbitrary. For $i\in[1..m]$, let $B_{d}(i)=\{d[t]\mid t\in I(i)\}$ be the set of states occurring in the $i$-th block of $d$. Moreover, we blockwise collect clients that are currently in a particular state $s\in Q$. Let the set $\operatorname{Pos}_{d}(i,s)=\{t\in I(i)\mid d[t]=s\}$ be those positions of $d$ in the $i$-th block that store state $s$.

We fix the configuration $c\in Q^{n}$. For each component $i\in[1..m]$, in the $i$-th block it contains $|Q|^{\ell}$ copies of the state $s_{i}$. Formally, $B_{c}(i)=\{s_{i}\}$. Our goal is to construct the computation $\pi=c_{0}\rightarrow^{+}c_{1}\rightarrow^{+}\dots\rightarrow^{+}c_{\ell}$ with $c_{0}=c_{\ell}=c$ such that the following two invariants are satisfied. (1) For each $j\in[0..\ell]$ and $i\in[1..m]$ we have $B_{c_{j}}(i)\subseteq S^{i}_{j}$. (2) For any state $s$ in a set $S^{i}_{j}$ we have $|\operatorname{Pos}_{c_{j}}(i,s)|\geq|Q|^{\ell-j}$. Intuitively, (1) means that during the computation $\pi$ we visit at most those states that occur in the cycle $\sigma$. Invariant (2) guarantees that at each configuration $c_{j}$ there are enough clients available in these states.

We construct $\pi$ inductively. The base case is given by configuration $c_{0}=c$ which satisfies Invariants (1) and (2) by definition. For the induction step, assume $c_{j}$ is already constructed such that (1) and (2) hold for the configuration. Our first goal is to construct a configuration $d$ such that $c_{j}\rightarrow^{+}d$ and $d$ satisfies Invariant (2). In a second step we construct a computation $d\rightarrow^{*}c_{j+1}$.

In the cycle $\sigma$ there is an edge $V_{j}\rightarrow_{G}V_{j+1}$. From the definition of $\rightarrow_{G}$ we get a component $t\in[1..m]$, states $s\in S^{t}_{j}$ and $s^{\prime}\in S^{t}_{j+1}$, and an $a\in D$ such that there is a send transition $s\xrightarrow{!a}s^{\prime}$. Moreover, there are sets $\mathit{Gen}_{t}\subseteq\mathit{post}_{?a}(S^{t}_{j})$ and $\mathit{Kill}_{t}\subseteq\mathit{enabled}_{?a}(S^{t}_{j})$ such that the following holds:

[TABLE]

Here, $U_{t}$ is either $S^{t}_{j}$ or $S^{t}_{j}\setminus\{s\}$. We focus on $t$ and take care of other components later. We apply a case distinction for the states in $S_{j+1}^{t}$.

Let $q$ be a state in $S_{j+1}^{t}\setminus\{s^{\prime}\}$. If $q\in\mathit{Gen}_{t}$, there exists a $p\in S^{t}_{j}$ such that $p\xrightarrow{?a}q$. We apply this transition to $|Q|^{\ell-(j+1)}$ many clients in the $t$-th block of configuration $c_{j}$. If $q\in U_{t}\setminus\mathit{Kill}_{t}$ and $q$ not in $\mathit{Gen}_{t}$, then certainly $q\in U_{t}\subseteq S^{t}_{j}$. In this case, we let $|Q|^{\ell-(j+1)}$ many clients of block $t$ stay idle in state $q$. For state $s^{\prime}$, we apply a sequence of sends. More precise, we apply the transition $s\xrightarrow{!a}s^{\prime}$ to $|Q|^{\ell-(j+1)}$ many clients in block $t$ of $c_{j}$. The first of these sends synchronizes with the previously described receive transitions. The other sends do not have any receivers. For components different from $t$, we apply the same procedure. Since there are only receive transitions, we also let them synchronize with the first send of $a$. This leads to a computation $\tau$

[TABLE]

We argue that the computation $\tau$ is valid: there are enough clients in $c_{j}$ such that $\tau$ can be carried out. We again focus on component $t$, the reasoning for the other components is similar. Let $p\in\operatorname{Set}(c_{j})=S_{j}^{t}$. Note that the equality is due to Invariants (1) and (2). We count the clients of $c_{j}$ in state $p$ (in block $t$) that are needed to perform $\tau$. We need

[TABLE]

of these clients. The set $\mathit{post}_{?a}(p)\cup\{p,s^{\prime}\}$ appears as a consequence of the case distinction above: there may be transitions mapping $p$ to a state in $\mathit{post}_{?a}(p)$, it may happen that clients stay idle in $p$, and in the case $p=s$, we need to add $s^{\prime}$ for the send transition. Since $|\operatorname{Pos}_{c_{j}}(t,p)|\geq|Q|^{\ell-j}$ by Invariant (2), we get that $\tau$ is a valid computation. Moreover, note that configuration $d$ satisfies Invariant (2) for $j+1$: for each state $q\in S_{j+1}^{t}$, the computation $\tau$ was constructed such that $|\operatorname{Pos}_{d}(t,q)|\geq|Q|^{\ell-(j+1)}$.

To satisfy Invariant (1), we need to erase states that are present in $d$ but not in $S_{j+1}^{t}$. To this end, we reconsider the set $\mathit{Kill}_{t}\subseteq\mathit{enabled}_{?a}(S_{j}^{t})$. For each state $p\in\mathit{Kill}_{t}$, we know by the definition of $\rightarrow_{G}$ that $\mathit{post}_{?a}(p)\cap\mathit{Gen}_{t}\neq\emptyset$. Hence, there is a $q\in S_{j+1}^{t}$ such that $p\xrightarrow{?a}q$. We apply this transition to all clients in $d$ currently in state $p$ that were not active in the computation $\tau$. In case $U_{t}=S_{j}^{t}\setminus\{s\}$, we apply the send $s\xrightarrow{!a}s^{\prime}$ to all clients that are still in $s$ and were not active in $\tau$. Altogether, this leads to a computation $\eta=d\rightarrow^{*}c_{j+1}$.

There is a subtlety in the definition of $\eta$. There may be no send transition for the receivers to synchronize with since $s$ may not need to be erased. In this case, we synchronize the receive transitions of $\eta$ with the last send of $\tau$.

Computation $\eta$ substitutes the states in $\mathit{Kill}_{t}$ and state $s$, depending on $U_{t}$, by states in $S_{j+1}^{t}$. But this means that in the $t$-th block of $c_{j+1}$, there are only states of $S_{j+1}^{t}$ left. Hence, $B_{c_{j+1}}(t)\subseteq S_{j+1}^{t}$, and Invariant (1) holds.

After the construction of $\pi=c\rightarrow^{+}c_{\ell}$, it is left to argue that $c_{\ell}=c$. But this is due to the fact that (1) holds for $c_{\ell}$ and $S_{\ell}^{t}=(\{s_{1}\},\dots,\{s_{m}\})$. ∎

The graph $G$ is of exponential size. To obtain a polynomial-time procedure, we cannot just search it for a cycle as required by Lemma 2. Instead, we now show that if such a cycle exists, then there is a cycle in a certain normal form. Hence, it suffices to look for a normal-form cycle. As we will show, this can be done in polynomial time. We define the normal form more generally for paths.

A path is in normal form, if it takes the shape $V_{1}\rightarrow_{G}^{*}V_{m}\rightarrow_{G}^{*}V_{n}$ such that the following conditions hold. In the prefix $V_{1}\rightarrow_{G}^{*}V_{m}$ the sets of states increase monotonically, $V_{i}\sqsubseteq V_{i+1}$ for all $i\in[1..m-1]$. Here, $\sqsubseteq$ denotes the componentwise inclusion. In the suffix $V_{m}\rightarrow_{G}^{*}V_{n}$, the sets of states decrease monotonically, $V_{i}\sqsupseteq V_{i+1}$ for all $i\in[m..n-1]$. The following lemma states that if there is a path in the graph, then there is also a path in normal form. The intuition is that the variants of the transitions that decrease the sets of states can be postponed towards the end of the computation.

Lemma 3

There is a path from $V_{1}$ to $V_{2}$ in $G$ if and only if there is a path in normal form from $V_{1}$ to $V_{2}$.

Proof

If $V_{1}\rightarrow^{*}_{G}V_{2}$ is a path in normal form, there is nothing to prove. For the other direction, let $\sigma=V_{1}\rightarrow^{*}_{G}V_{2}$ be an arbitrary path. To get a path in normal form, we first simulate the edges of $\sigma$ in such a way that no states are deleted. In a second step, we erase the states that should have been deleted. We have to respect a particular deletion order to obtain a valid path.

Let $\sigma=U_{1}\rightarrow_{G}U_{2}\rightarrow_{G}\dots\rightarrow_{G}U_{\ell}$ with $U_{1}=V_{1}$ and $U_{\ell}=V_{2}$. We inductively construct an increasing path $\sigma_{\operatorname{inc}}=U^{\prime}_{1}\rightarrow_{G}\dots\rightarrow_{G}U^{\prime}_{\ell}$ with $U^{\prime}_{j}\sqsupseteq U_{i}$ or all $i\leq j$ by mimicking the edges of $\sigma$.

For the base case, we set $U^{\prime}_{1}=U_{1}$. Now assume $\sigma_{\operatorname{inc}}$ has already been constructed up to vertex $U^{\prime}_{j}$. There is an edge $e=U_{j}\rightarrow_{G}U_{j+1}$ in $\sigma$. Since $U^{\prime}_{j}\sqsupseteq U_{j}$, we can simulate $e$ on $U^{\prime}_{j}$: all states needed for execution are present in $U^{\prime}_{j}$. Moreover, we can mimic $e$ such that no state gets deleted. This is achieved by setting the corresponding $\mathit{Kill}$-sets to be empty. Hence, we get an edge $U^{\prime}_{j}\rightarrow U^{\prime}_{j+1}$ with $U^{\prime}_{j+1}\sqsupseteq U^{\prime}_{j}$ (no deletion) and $U^{\prime}_{j+1}\sqsupseteq U_{j+1}$ (simulation of $e$).

The states in $V^{\prime}_{2}=U^{\prime}_{\ell}$ that are not in $V_{2}$ are those states that were deleted along $\sigma$. We construct a decreasing path $\sigma_{\operatorname{dec}}=V^{\prime}_{2}\rightarrow_{G}^{*}V_{2}$, deleting all these states. To this end, let $V^{\prime}_{2}=(T_{1},\dots,T_{m})$ and $V_{2}=(S_{1},\dots,S_{m})$. An edge in $\sigma$ deletes sets of states in each component $i\in[1..m]$. Hence, to mimic the deletion, we need to consider subsets of $\mathit{Del}=\bigcup_{i\in[1..m]}(T_{i}\setminus S_{i})\times\{i\}$. Note that the index $i$ in a tuple $(s,i)$ displays the component the state $s$ is in.

Consider the equivalence relation $\sim$ over $\mathit{Del}$ defined by $(x,i)\sim(y,t)$ if and only if the last occurrence of $x$ in component $i$ and $y$ in component $t$ in the path $\sigma$ coincide. Intuitively, two elements are equivalent if they get deleted at the same time and do not appear again in $\sigma$. We introduce an order on the equivalence classes: $[(x,i)]_{\sim}<[(y,t)]_{\sim}$ if and only if the last occurrence of $(x,i)$ was before the last occurrence of $(y,t)$. Since the order is total, we get a partition of $\mathit{Del}$ into equivalence classes $P_{1},\dots,P_{n}$ such that $P_{j}<P_{j+1}$.

We construct $\sigma_{\operatorname{dec}}=K_{0}\rightarrow_{G}\dots\rightarrow_{G}K_{n}$ with $K_{0}=V^{\prime}_{2}$ and $K_{n}=V_{2}$ as follows. During each edge $K_{j-1}\rightarrow_{G}K_{j}$, we delete precisely the elements in $P_{j}$ and do not add further states. Deleting $P_{j}$ is due to an edge $e=U_{k}\rightarrow_{G}U_{k+1}$ of $\sigma$. We mimic $e$ in such a way that no state gets added and set the corresponding Gen sets to the empty set. Since we respect the order $<$ with the deletions, the simulation of $e$ is possible. Suppose, we need a state $s$ in component $t$ to simulate $e$ but the state is not available in component $t$ of $K_{j-1}$. Then it was deleted before, $(s,t)\in P_{1}\cup\dots\cup P_{j-1}$. But this contradicts that $s$ is present in $U_{k}$. Hence, all the needed states are available.

Since after the last edge of $\sigma_{\operatorname{dec}}$ we have deleted all elements from $\mathit{Del}$, we get that $K_{n}=V_{2}$. This concludes the proof. ∎

Using the normal-form result in Lemma 3, we now give a polynomial-time algorithm to check whether $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}(\{s_{1}\},\dots,\{s_{m}\})$. The idea is to mimic the monotonically increasing prefix of the path by a suitable post operator, the monotonically decreasing suffix by a suitable pre operator, and intersect the two. The difficulty in computing an appropriate post operator is to ensure that the receive operations are enabled by sends leading to a state in the intersection, and similar for pre. The solution is to use a greatest fixed-point computation. In a first Kleene iteration step, we determine the ordinary $\mathit{post}^{+}$ of $(\{s_{1}\},\dots,\{s_{m}\})$ and intersect it with the $\mathit{pre}^{*}$. In the next step, we constrain the $\mathit{post}^{+}$ and the $\mathit{pre}^{*}$ computations to visiting only states in the previous intersection. The results are intersected again, which may remove further states. Hence, the computation is repeated relative to the new intersection. The thing to note is that we do not work with standard post and pre operators but with operators that are constrained by (tuples of) sets of states.

For the definition of the operators, consider $C=(C_{1},\dots,C_{m})\in{\mathcal{P}(Q)}^{m}$ for an $m\leq|Q|$. Given a sequence of sets of states $X_{1},\dots,X_{m}$ where each $X_{i}\subseteq C_{i}$, we define $\mathit{post}_{C}(X_{1},\dots,X_{m})=(X^{\prime}_{1},\dots,X^{\prime}_{m})$ with

[TABLE]

Here, $P\!\downarrow_{C_{i}}$ denotes the automaton obtained from $P$ by restricting it to the states $C_{i}$. Similarly, we define $\mathit{pre}_{C}(X_{1},\dots,X_{m})=(X^{\prime}_{1},\dots,X^{\prime}_{m})$ with

[TABLE]

The next lemma shows that the (reflexive) transitive closures of these operators can be computed in polynomial time.

Lemma 4

The closures $\mathit{post}^{+}_{C}(X_{1},\dots,X_{m})$ and $\mathit{pre}^{*}_{C}(X_{1},\dots,X_{m})$ can be computed in polynomial time.

Proof

Both closures can be computed by a saturation. For $\mathit{post}^{+}_{C}(X_{1},\dots,X_{m})$, we keep $m$ sets $R_{1},\dots,R_{m}$, each being the post of a component. Initially, we set $R_{i}=X_{i}$. The defining equation of $X^{\prime}_{i}$ in $\mathit{post}^{+}_{C}(X_{1},\dots,X_{m})$ gives the saturation. One just needs to substitute $X_{i}$ by $R_{i}$ and $X_{\ell}$ by $R_{\ell}$ on the right hand side. The resulting set of states is added to $R_{i}$. This process is applied consecutively to each component and then repeated until the sets $R_{i}$ do not change anymore, the fixed point is reached.

The saturation terminates in polynomial time. After updating $R_{i}$ in each component, we either already terminated or added at least one new state to a set $R_{i}$. Since there are $m\leq|Q|$ of these sets and each one is a subset of $Q$, we need to update the sets $R_{i}$ at most $|Q|^{2}$ many times. For a single of these updates, the dominant time factor comes from finding appropriate send and receive transitions. This can be achieved in $\mathcal{O}(|\delta|^{2})$ time.

Computing the closure $\mathit{pre}^{*}_{C}(X_{1},\dots,X_{m})$ is similar. One can apply the above saturation and only needs to reverse the transitions in the client. ∎

As argued above, the existence of a cycle reduces to finding a fixed point. The following lemma shows that it can be computed efficiently.

Lemma 5

There is a cycle $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}(\{s_{1}\},\dots,\{s_{m}\})$ if and only if there is a non-trivial solution to the equation

[TABLE]

Such a solution can be found in polynomial time.

Proof

We use a Kleene iteration to compute the greatest fixed point. It invokes Lemma 4 as a subroutine. Every step of the Kleene iteration reduces the number of states in $C$ by at least one, and initially there are at most $|Q|$ entries with $|Q|$ states each. Hence, we terminate after quadratically many iterations.

It is left to prove correctness. Let $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}(\{s_{1}\},\dots,\{s_{m}\})$ be a cycle in $G$. By Lemma 3 we can assume it to be in normal form. Let $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}C$ be the increasing part and $C\rightarrow^{*}_{G}(\{s_{1}\},\dots,\{s_{m}\})$ the decreasing part. Then, $C$ is a solution to the equation.

For the other direction, let a solution $C$ be given. Since $C$ is contained in $\mathit{post}^{+}_{C}(\{s_{1}\},\dots,\{s_{m}\})$ we can construct a monotonically increasing path $(\{s_{1}\},\dots,\{s_{m}\})\rightarrow^{+}_{G}C$. Similarly, since $C\subseteq\mathit{pre}^{*}_{C}(\{s_{1}\},\dots,\{s_{m}\})$, we get a decreasing path $C\rightarrow^{*}_{G}(\{s_{1}\},\dots,\{s_{m}\})$. Hence, we get the desired cycle. ∎

What is yet open is the question on which states $s_{1}$ to $s_{m}$ to perform the search for a cycle. After all, we need that the corresponding configuration is reachable from an initial configuration. The idea is to use the set of all states reachable from an initial state in the client. Note that there is a live computation if and only if there is a live computation involving all those states. Indeed, if a state is not active during the cycle, the corresponding clients will stop moving after an initial set-up phase. Since the states reachable from an initial state can be computed in polynomial time [13], the proof of Theorem 3.1 follows.

Liveness Verification does not take fairness into account. A client may contribute to the live computation (and help the distinguished client reach a final state) without ever making progress towards its own final state.

4 Fair Liveness

We study the fair liveness verification problem that strengthens the requirement on the computation. Given a broadcast network $\mathcal{N}=(D,P)$ with clients $P=(Q,I,\delta)$ and a set of final states $F\subseteq Q$, the problem asks whether there is an infinite initialized computation $\pi$ in which clients that send or receive infinitely often also visit their final states infinitely often, $\operatorname{Inf}(\pi)\subseteq\operatorname{Fin}(\pi)$. Computations satisfying the requirement are called fair, a notion that dates back to [36] where it was introduced as compassion or strong fairness. {myproblem}

We solve the problem by applying the cycle finding algorithm from Section 3 to an instrumentation of the given broadcast network. Formally, given an instance $(\mathcal{N},F)$ of Fair Liveness Verification, we construct a new broadcast network $\mathcal{N}_{F}$, containing several copies of $Q$. Recall that $Q$ is the set of client states in $\mathcal{N}$. The construction ensures that cycles over $Q$ in $\mathcal{N}_{F}$ correspond to cycles in $\mathcal{N}$ where each participating client sees a final state. Such cycles make up a fair computation. The main result is the following.

Theorem 4.1

Fair Liveness Verification is $\P$-complete.

Hardness follows from [13]. To explain the aforementioned instrumentation, we need the notion of a good computation, where good means fairness is respected. A computation $c_{1}\rightarrow c_{2}\rightarrow\dots\rightarrow c_{n}$ with $n>1$ is called good for $F$, denoted $c_{1}\Rightarrow_{F}c_{n}$, if every client that makes a move during the computation also sees a final state. Formally, if $i\in\mathit{idx}(c_{1}\rightarrow^{+}c_{n})$ then there exists a $k\in[1..n]$ such that $c_{k}[i]\in F$. The following strengthens Lemma 1.

Lemma 6

There is a fair computation from $c_{0}$ if and only if $c_{0}\rightarrow^{*}c\Rightarrow_{F}c$.

Proof

If there is a computation of the form $c_{0}\rightarrow^{*}c\Rightarrow_{F}c$, then the good cycle $c\Rightarrow_{F}c$ can be iterated infinitely often to obtain a fair computation.

For the other direction, let a fair computation $\pi$ starting in $c_{0}$ be given. Since the configurations visited by $\pi$ are over $Q^{k}$ for some $k$, there is a configuration $c$ that repeats infinitely often in $\pi$. Hence, we obtain a prefix $c_{0}\rightarrow^{*}c$.

Let $\operatorname{Inf}(\pi)=\{i_{1},\dots,i_{n}\}$ be the clients that participate infinitely often in computation $\pi$. By the definition of a fair computation, we have $\operatorname{Inf}(\pi)\subseteq\operatorname{Fin}(\pi)$. This means that each of the clients in $\{i_{1},\dots,i_{n}\}$ visits a state from $F$ infinitely often along $\pi$. Hence, for each $j\in[1..n]$ we can find a subcomputation $\pi_{j}=c\rightarrow^{+}c$ of $\pi$, in which client $i_{j}$ visits a state from $F$. Combining all $\pi_{j}$ yields desired good cycle $c\Rightarrow_{F}c$. ∎

The broadcast network $\mathcal{N}_{F}$ is designed to detect good cycles $c\Rightarrow_{F}c$. The idea is to let the clients compute in phases. The original state space $Q$ is the first phase. As soon as a client participates in the computation, it moves to a second phase given by a copy $\hat{Q}$ of $Q$. From this copy it enters a third phase $\tilde{Q}$ upon seeing a final state. From $\tilde{Q}$ it may return to $Q$.

Let the given broadcast network be $\mathcal{N}=(D,P)$ with $P=(Q,I,\delta)$. We define $\mathcal{N}_{F}=(D\cup\{n\},P_{F})$ with fresh symbol $n\notin D$ and extended client

[TABLE]

Note that the initial phase is $\tilde{Q}$. For every transition $(q,\mathit{op},q^{\prime})\in\delta$, we have $(q,\mathit{op},\hat{q}^{\prime}),(\hat{q},\mathit{op},\hat{q}^{\prime}),(\tilde{q},\mathit{op},\tilde{q}^{\prime})\in\bar{\delta}$. For every final state $q\in F$ we have $(\hat{q},!n,\tilde{q})\in\bar{\delta}$. Finally, for every state $q\in Q$ we have $(\tilde{q},!n,q)\in\bar{\delta}$. Configuration $c$ admits a good cycle if and only if there is a cycle at $c$ in the instrumented network. An initial prefix can be mimicked by computations within $\tilde{Q}$.

Lemma 7

$c_{0}\rightarrow^{*}c\Rightarrow_{F}c$* in $\mathcal{N}$ if and only if $\tilde{c}_{0}\rightarrow^{*}c\rightarrow^{+}c$ in $\mathcal{N}_{F}$.*

In the proof, we argue that a good cycle entails a cycle in the instrumented broadcast network. The reasoning for a prefix is simpler. For the reverse direction, note that in $c$ all clients are in states from $Q$. As soon as a client participates in the computation, it will move to $\hat{Q}$. To return to $Q$, the client will have to see a final state. This makes the computation good.

Proof

First note that by construction, a prefix $c_{0}\rightarrow^{*}c$ exists in $\mathcal{N}$ if and only if $\tilde{c}_{0}\rightarrow^{*}\tilde{c}$ exists in $\mathcal{N}_{F}$. Since one can always move from configuration $\tilde{c}$ to $c$ in $\mathcal{N}_{F}$, we obtain that $c_{0}\rightarrow^{*}c$ in $\mathcal{N}$ if and only if $\tilde{c}_{0}\rightarrow^{*}c$ in $\mathcal{N}_{F}$.

It is left to show that there is a good cycle $c\Rightarrow_{F}c$ if and only if there is a cycle $c\rightarrow^{+}c$ in $\mathcal{N}_{F}$. We first show that good cycles entail cycles in $\mathcal{N}_{F}$. To this end, we prove a slightly more general result: if there is a computation $\sigma=c\xrightarrow{w}_{\mathcal{N}}d$, we can derive a computation $c\xrightarrow{w^{\prime}}_{\mathcal{N}_{F}}d(\sigma)$ where $w^{\prime}$ is a word over $D\cup\{n\}$ such that its projection to $D$ is $w$. The configuration $d(\sigma)$ is defined componentwise. Assume $d\in Q^{k}$ and let $i\in[1..k]$. Moreover, let $d[i]=q$, then the $i$-th component of $d(\sigma)$ is defined via a case distinction:

(1) $d(\sigma)[i]=q$ if $\mathit{pr}_{i}(\sigma)=\varepsilon$. So if client $i$ does not contribute to $\sigma$, it will not change its state. Note that $c[i]=q$ in this case.

(2) $d(\sigma)[i]=\tilde{q}$ if $\mathit{pr}_{i}(\sigma)=c[i]\rightarrow^{+}e[i]\rightarrow^{*}d[i]=q$ with $e[i]\in F$. Here, $e$ is some intermediary configuration visited along $\sigma$. Hence, client $i$ visits a final state during the computation, leading it into $\tilde{Q}$ in the instrumented network.

(3) $d(\sigma)[i]=\hat{q}$ otherwise. In this case, client $i$ contributes to computation $\sigma$ but does not visit a final state along it.

We construct the computation $c\xrightarrow{w^{\prime}}_{\mathcal{N}_{F}}d(\sigma)$ by induction. In the case $w=\varepsilon$, we set $w^{\prime}=\varepsilon$ and obtain $d(\sigma)=d$. Hence, we get the desired (empty) computation in the network $\mathcal{N}_{F}$.

Now let $w=u.a$ for a word $u\in D^{*}$ and $a\in D$. Then the computation $\sigma=c\xrightarrow{w}_{\mathcal{N}}d$ splits into two parts. There is an intermediary configuration $f$ with $\sigma=\sigma_{1}.\sigma_{2}$ where $\sigma_{1}=c\xrightarrow{u}_{\mathcal{N}}f$ and $\sigma_{2}=f\xrightarrow{a}_{\mathcal{N}}d$. We apply the induction to $\sigma_{1}$ and obtain a computation $\sigma^{\prime}_{1}=c\xrightarrow{u^{\prime}}_{\mathcal{N}_{F}}f(\sigma_{1})$. Let $\mathcal{J}=\mathit{idx}(\sigma_{2})$ be the clients contributing to transition $\sigma_{2}$. We extend the computation $\sigma^{\prime}_{1}$ for each $j\in\mathcal{J}$ as follows. Let $f[j]=q\in Q$ and $d[j]=p\in Q$ and let $\mathit{pr}_{j}(\sigma_{2})=q\xrightarrow{\mathit{op}}p$ with $\mathit{op}\in\mathit{Ops}(D)$.

(1) If $\mathit{pr}_{j}(\sigma_{1})=\varepsilon$, then by definition $f(\sigma_{1})[j]=q$. Hence, by construction of $\mathcal{N}_{F}$, there is a transition $q\xrightarrow{\mathit{op}}\hat{p}$ which we perform in the $j$-th component.

(2) If $\mathit{pr}_{j}(\sigma_{1})$ visits an intermediary final state of $F$, then $f(\sigma_{1})[j]=\tilde{q}$. In this case, we extend $\sigma^{\prime}_{1}$ by the transition $\tilde{q}\xrightarrow{\mathit{op}}\tilde{p}$ in the $j$-th component.

(3) If $\mathit{pr}_{j}(\sigma_{1})\neq\varepsilon$ and does not visit a final state, we get that $f(\sigma_{1})[j]=\hat{q}$. Then we extend $\sigma_{1}$ by the transition $\hat{q}\xrightarrow{\mathit{op}}\hat{p}$ in the $j$-th component.

Clients $j\notin\mathit{idx}(\sigma_{2})$ do not change their current state during the extension of $\sigma^{\prime}_{1}$. Altogether, we obtain a computation of the form $c\xrightarrow{u^{\prime}}_{\mathcal{N}_{F}}f(\sigma_{1})\xrightarrow{a}_{\mathcal{N}_{F}}g$, where $g$ is the resulting configuration of the above extension. We extend the computation such that it reaches $d(\sigma)$. To this end, let $j\in[1..k]$. If $g[j]=\hat{p}$ and $p\in F$, we add the transition $\hat{p}\xrightarrow{!n}\tilde{p}$ without any receiving clients in $\mathcal{N}_{F}$. By this, we get that all clients visiting a final state along $\sigma$, finally move to phase $\tilde{Q}$. Hence, we obtain the following desired computation:

[TABLE]

Now assume a good cycle $\pi=c\Rightarrow_{F}c$ in $\mathcal{N}$ is given. We apply the above result and obtain a computation $c\rightarrow^{+}_{\mathcal{N}_{F}}c(\pi)$. Since $\pi$ is good for $F$, each participating client visits a final state along $\pi$. Hence, the configuration $c(\pi)$ can be described as follows. Let $j\in[1..k]$ and $c[j]=q$. We have

[TABLE]

Note that there is not state in phase $\hat{Q}$.

We extend the computation $c\rightarrow^{+}_{\mathcal{N}_{F}}c(\pi)$ for each $j\in[1..k]$ with $\mathit{pr}_{j}(\pi)\neq\varepsilon$. Since $c(\pi)[j]=\tilde{q}$ in this case, we add the transition $\tilde{q}\xrightarrow{!n}q=c[j]$. Hence, we obtain a cycle

[TABLE]

For the other direction, assume that a cycle $c\rightarrow^{+}_{\mathcal{N}_{F}}c$ in $\mathcal{N}_{F}$ is given. By construction, such a cycle can be decomposed as follows:

[TABLE]

Here, each $w_{i}\in D^{*}$ and the computation between $d_{i}$ and $c_{i}$ is a repeated sending of $n$ without receivers, needed to transition between different phases.

Out of this computation, we construct a good cycle $c\Rightarrow_{F}c$. To this end, we define for each configuration $d$ of $\mathcal{N}_{F}$ with $k$ components a configuration $\mathcal{N}(d)$ that retrieves the original states out of $d$. For each $j\in[1..k]$, we set

[TABLE]

By construction of $\mathcal{N}_{F}$, we can mimic the transitions occurring in $c_{i-1}\xrightarrow{w_{i}}_{\mathcal{N}_{F}}d_{i}$ by transitions on $Q$ and hence infer a corresponding computation $\mathcal{N}(c_{i-1})\xrightarrow{w_{i}}_{\mathcal{N}}\mathcal{N}(d_{i})$ on the original network. A computation $d_{i}\xrightarrow{n}^{*}_{\mathcal{N}_{F}}c_{i}$ can be ignored on the original network since $\mathcal{N}(d_{i})=\mathcal{N}(c_{i})$. The reason is that sending $n$ only shifts copies within $\mathcal{N}_{F}$. Altogether, we obtain a cycle

[TABLE]

The obtained cycle in $\mathcal{N}$ is good for $F$. Let $j\in[1..k]$ be a client participating in the cycle. Then, $j\in\mathit{idx}(c\rightarrow^{+}_{\mathcal{N}_{F}}c)$. This means that $j$ starts in a state $q\in Q$ and reaches back to $q$. By construction of $\mathcal{N}_{F}$, this is only possible if $j$ visits a state $p$ from $F$ during the cycle. Hence, $p$ is also visited during the obtained cycle on $\mathcal{N}$. ∎

For the proof of Theorem 4.1, it is left to state the algorithm for finding a computation $\tilde{c}_{0}\rightarrow^{*}c\rightarrow^{+}c$ in $\mathcal{N}_{F}$. We compute the states reachable from an initial state in $\mathcal{N}_{F}$. As we are interested in a configuration $c$ over $Q$, we intersect this set with $Q$. Both steps can be done in polynomial time. Let $s_{1},\dots,s_{m}$ be the states in the intersection. To these we apply the fixed-point iteration from Lemma 5. By Lemma 2, the iteration witnesses the existence of a cycle over a configuration $c$ of $\mathcal{N}_{F}$ that involves only the states $s_{1}$ up to $s_{m}$.

5 Model Checking Broadcast Networks

We consider model checking for broadcast networks against linear time specifications. Given a specification, described in linear time temporal logic (LTL) [35], we test whether all (infinite) computations of a broadcast network satisfy the specification. Like for liveness verification, we consider two variants of the problem. These differ in when a computation of a broadcast network actually satisfies a specification. Fair Model Checking demands that the individual computations of all clients participating infinitely often satisfy the specification. Sparse Model Checking asks for at least one client that participates infinitely often and satisfies the specification. We show how to solve both problems by reducing them to Liveness Verification and Fair Liveness Verification via incorporating the Vardi-Wolper construction [40].

Before we consider both mentioned problems, we briefly recall syntax and semantics of linear time temporal logic. Let $\mathcal{A}$ be a set of atomic propositions. An LTL formula $\varphi$ over the set of propositions is defined as follows:

[TABLE]

An LTL formula consists of propositions and combinations of the same via negation, union, next operator $\mathcal{X}$, and until operator $\mathcal{U}$. Semantics is defined in terms of the satisfaction relation $\models$. It describes when a formula is fulfilled. We define it inductively along the structure of LTL formulas. Let $w\in\mathcal{P}(\mathcal{A})^{\omega}$ be an infinite word consisting of sets of propositions and let $i\in\mathbb{N}$. We have

[TABLE]

For model checking broadcast networks against LTL specifications, we need to define when a network computation satisfies an LTL formula. Since network computations consist of concurrently running client computations, the definition of satisfaction is based upon the latter.

Let $\mathcal{N}=(D,P)$ be a broadcast network with clients $P=(Q,I,\delta)$ and let $\varphi$ be an LTL formula. Moreover, let $\lambda:Q\rightarrow\mathcal{P}(\mathcal{A})$ be a map associating to each state of $P$ a set of atomic proposition. An infinite computation $\sigma=q_{0}\rightarrow q_{1}\rightarrow\cdots$ of $P$ with $q_{0}\in I$ is said to satisfy formula $\varphi$ if $\lambda(\sigma)\models\varphi$. Here, $\lambda(\sigma)=\lambda(q_{0}).\lambda(q_{1})\ldots\in\mathcal{P}(\mathcal{A})^{\omega}$ is the infinite word obtained by applying $\lambda$ to the whole computation. We also write $\sigma\models\varphi$.

For network computations, we consider two different notions of satisfaction for LTL formulas. Like for the liveness verification problems, one of the notions incorporates a fairness assumption, the other one focuses on a single client.

Let $\mathcal{N}=(D,P)$ be a broadcast network with client states $Q$, $\lambda:Q\rightarrow\mathcal{P}(\mathcal{A})$ a map, and $\varphi$ an LTL formula. An initialized infinite computation $\pi$ of $\mathcal{N}$ satisfies $\varphi$ under fairness if each client $i\in\operatorname{Inf}(\pi)$ satisfies $\varphi$ with its contribution, $\mathit{pr}_{i}(\pi)\models\varphi$. We write $\pi\models_{\mathit{fair}}\varphi$. Hence, satisfaction under fairness ensures that each client that participates infinitely often also satisfies the specification. An initialized infinite computation $\pi$ of $\mathcal{N}$ sparsely satisfies $\varphi$ if there is a client $i\in\operatorname{Inf}(\pi)$ that satisfies $\varphi$, $\mathit{pr}_{i}(\pi)\models\varphi$. We denote it by $\pi\models_{\mathit{sparse}}\varphi$. In contrast to fairness, a single client satisfying the specification suffices.

The two notions of satisfaction yield two decision problems: Fair Model Checking and Sparse Model Checking. We state both in the subsequent sections and develop algorithms based on the results from Sections 3 and 4.

Fair Model Checking

We want to test whether all computations of a broadcast network satisfy a given LTL formula under the fairness assumption. Formally, a broadcast network $\mathcal{N}$ is said to satisfy an LTL formula $\varphi$ under fairness, written $\mathcal{N}\models_{\mathit{fair}}\varphi$, if for each initialized infinite computation $\pi$ we have that $\pi\models_{\mathit{fair}}\varphi$. With this notion at hand, we can formalize the corresponding decision problem Fair Model Checking. Note that we do not explicitly mention the map $\lambda$ as part of the input. We assume it to be given with the broadcast network. {myproblem}

Our goal is to prove the following theorem by presenting an algorithm for Fair Model Checking. Note that the exponential factor in the time estimation only depends on the size of the formula. The size $|\mathcal{N}|=\max\{|D|,|Q|\}$ of the broadcast network only contributes a polynomial factor.

Theorem 5.1

Fair Model Checking can be solved in time $2^{\mathcal{O}({|\varphi|})}\cdot|\mathcal{N}|^{\mathcal{O}(1)}$.

We need to develop an algorithm for checking $\mathcal{N}\models_{\mathit{fair}}\varphi$. A direct iteration over all computations $\pi$ of $\mathcal{N}$ along with a test whether $\pi\models_{\mathit{fair}}\varphi$ is not tractable since there are infinitely many candidates for $\pi$. We rather search for a computation that violates $\varphi$. The non-existence of such a computation ensures that $\mathcal{N}$ satisfies the formula. Phrased differently, we have $\mathcal{N}\not\models_{\mathit{fair}}\varphi$ if and only if there is a computation $\pi$ of $\mathcal{N}$ with $\pi\not\models_{\mathit{fair}}\varphi$.

The latter can be reformulated. Let $\pi$ be a computation with $\pi\not\models_{\mathit{fair}}\varphi$. Then there is a client $i\in\operatorname{Inf}(\pi)$ that violates $\varphi$, we have $\mathit{pr}_{i}(\pi)\models\neg\varphi$. But by definition this means $\pi\models_{\mathit{sparse}}\neg\varphi$. Hence, we obtain that $\pi\not\models_{\mathit{fair}}\varphi$ if and only if $\pi\models_{\mathit{sparse}}\neg\varphi$. The following lemma summarizes the reasoning.

Lemma 8

We have $\mathcal{N}\not\models_{\mathit{fair}}\varphi$ if and only if there is an initialized infinite computation $\pi$ of $\mathcal{N}$ such that $\pi\models_{\mathit{sparse}}\neg\varphi$.

Due to Lemma 8 it suffices to find a computation of $\mathcal{N}$ that sparsely satisfies the negation of $\varphi$. We develop an algorithm for this task along the following two steps. (1) We employ the Vardi-Wolper construction [40] to build a new broadcast network $\mathcal{N}_{\neg\varphi}$ such that all computations of $\mathcal{N}_{\neg\varphi}$ visiting final states infinitely often are computations of $\mathcal{N}$ that sparsely satisfy $\neg\varphi$. (2) We decide the existence of a former computation with the fixed-point iteration for Liveness Verification, developed in Section 3.

Step (1) relies on the following well-known characterization of LTL formulas in terms of automata. The result is crucial for our development since it allows for representing all words that satisfy a given formula as a language of a Büchi automaton. We assume familiarity with the notion of Büchi automata [30].

Theorem 5.2

[40]** For any LTL formula $\psi$ over $\mathcal{A}$, one can construct a Büchi automaton $B_{\psi}$ of size at most $2^{\mathcal{O}(|\psi|)}$ such that for any word $w\in\mathcal{P}(\mathcal{A})^{\omega}$

[TABLE]

Apply Theorem 5.2 to the formula $\neg\varphi$ of interest. We obtain an automaton $B_{\neg\varphi}=(Q_{B},I_{B},\delta_{B},F_{B})$ over the alphabet $\mathcal{P}(\mathcal{A})$ with states $Q_{B}$, initial states $I_{B}$, transitions $\delta_{B}$, and final states $F_{B}$. Further, we assume $B_{\neg\varphi}$ to be non-blocking: in each state we have an outgoing transition on each letter. The language of $B_{\neg\varphi}$ consists of exactly those words in $\mathcal{P}(\mathcal{A})^{\omega}$ that satisfy $\neg\varphi$.

In order to obtain computations of $\mathcal{N}$ that satisfy $\neg\varphi$, we have to build a cross product of $P$, the clients in $\mathcal{N}$, with $B_{\neg\varphi}$. Intuitively, a computation in the cross product is then a computation of a client which at the same time satisfies the formula $\neg\varphi$. The construction however needs to take into account that $B_{\neg\varphi}$ is an automaton over a different alphabet than $\mathit{Ops}(D)$.

Let $P=(Q,I,\delta)$ be the clients of $\mathcal{N}$ and $\lambda:Q\rightarrow\mathcal{P}(\mathcal{A})$ the given map. We define the new client $P_{\neg\varphi}=(Q_{\neg\varphi},I_{\neg\varphi},\delta_{\neg\varphi})$ over the alphabet $\mathit{Ops}(D)$. The states are given by $Q_{\neg\varphi}=Q\times Q_{B}$, the initial states by $I_{\neg\varphi}=I\times I_{B}$. Transitions in $\delta_{\neg\varphi}$ are defined as follows:

[TABLE]

We also define a set of final states by $F_{\neg\varphi}=Q\times F_{B}$. Then, a computation of $P_{\neg\varphi}$ that visits $F$ infinitely often is a computation of $P$ that satisfies $\neg\varphi$.

The broadcast network of interest is $\mathcal{N}_{\neg\varphi}=(D,P_{\neg\varphi})$. It uses $P_{\neg\varphi}$ as clients and yields the desired result: a computation of $\mathcal{N}_{\neg\varphi}$ in which a client visits $F_{\neg\varphi}$ infinitely often is a computation of $\mathcal{N}$ that sparsely satisfies $\neg\varphi$.

Lemma 9

There is a computation $\pi$ of $\mathcal{N}$ such that $\pi\models_{\mathit{sparse}}\neg\varphi$ if and only if there is a computation $\pi^{\prime}$ of $\mathcal{N}_{\neg\varphi}$ with $\operatorname{Fin}(\pi^{\prime})\neq\emptyset$.

Note that the lemma reasons about initialized infinite computations and the set $\operatorname{Fin}(\pi^{\prime})$ is defined via the final states $F_{\neg\varphi}$.

Putting Lemmas 8 and 9 together yields a reduction to Liveness Verification. It is left to test whether there is a computation $\pi^{\prime}$ of $\mathcal{N}_{\neg\varphi}$ in which a client visits $F_{\neg\varphi}$ infinitely often. Step (2) decides the existence of such a computation by applying the fixed-point iteration from Section 3 to $(\mathcal{N}_{\neg\varphi},F_{\neg\varphi})$.

Regarding the complexity stated in Theorem 5.1, consider the following. By Theorem 5.2, the automaton $B_{\neg\varphi}$ has at most $2^{\mathcal{O}(|\varphi|)}$ many states and can be constructed in time $2^{\mathcal{O}(|\varphi|)}$. Hence, the clients $P_{\neg\varphi}$ have at most $|Q|\cdot 2^{\mathcal{O}(|\varphi|)}$ many states. The size of the alphabet is $\mathcal{O}(|D|)$. Constructing the new clients $P_{\neg\varphi}$ can thus be achieved in time polynomial in $2^{\mathcal{O}(|\varphi|)}\cdot|\mathcal{N}|$. The size of $\mathcal{N}_{\neg\varphi}$ is at most $2^{\mathcal{O}(|\varphi|)}\cdot|\mathcal{N}|$. Since the fixed-point iteration for solving Liveness verification runs in polynomial time, we obtain the desired complexity estimation. It is left to prove Lemma 9.

Proof

First, let $\pi$ be an initialized infinite computation of the broadcast network $\mathcal{N}$ such that $\pi\models_{\mathit{sparse}}\neg\varphi$. Assume that $\pi$ involves $k\in\mathbb{N}$ clients. By definition there is a client $i\in\operatorname{Inf}(\pi)$ with $\mathit{pr}_{i}(\pi)\models\neg\varphi$. This means that the word $\lambda(\mathit{pr}_{i}(\pi))\in\mathcal{P}(\mathcal{A})^{\omega}$ satisfies $\neg\varphi$ and thus lies in the language $L(B_{\neg\varphi})$. Hence, there is an initialized computation $r_{i}$ of $B_{\neg\varphi}$ on the word that accepts it. Let $b_{i}\in Q_{B}^{\omega}$ be the sequence of states appearing in $r_{i}$.

Since $B_{\neg\varphi}$ is non-blocking, there is also in initialized computation $r_{j}$ on the word $\lambda(\mathit{pr}_{j}(\pi))\in\mathcal{P}(\mathcal{A})^{\omega}$, for each client $j\neq i$. Note that $r_{j}$ is not necessarily accepting. We extract the sequence of states $b_{j}\in Q_{B}^{\omega}$ from each $r_{j}$. Denote by $b$ the vector of all sequences

[TABLE]

We show how to combine the computation $\pi$ and the vector $b$ to obtain a computation $\pi^{\prime}$ of $\mathcal{N}_{\neg\varphi}$ that satisfies $\operatorname{Fin}(\pi^{\prime})\neq\emptyset$. To this end, we will use the following notations. Let $\ell\in\mathbb{N}$, then the $\ell$-th configuration of $\pi$ is denoted by $\pi(\ell)\in Q^{k}$. For $\ell^{\prime}\geq\ell$, the notation $\pi(\ell,\ell^{\prime})$ refers to the subcomputation of $\pi$ starting in $\pi(\ell)$ and ending in $\pi(\ell^{\prime})$. Moreover, we use $b_{j}(\ell)$ to access the $\ell$-th state in the sequence $b_{j}$.

We define $\pi^{\prime}$ inductively. Roughly, each client of $\pi$ gets joined with the corresponding sequence of states in $b$. This yields a sequence of configurations of $\mathcal{N}_{\neg\varphi}$. Assume we have already constructed the subcomputation $\pi^{\prime}(0,\ell)$. Throughout the induction, we maintain two invariants: (1) $\pi^{\prime}(0,\ell)$ is in fact an initialized computation of $\mathcal{N}_{\neg\varphi}$. (2) When we project a configuration visited by $\pi^{\prime}(0,\ell)$ to $Q$, the client states of $\mathcal{N}$, we obtain the corresponding configuration of $\pi$. Formally, we have $\operatorname{proj}_{Q}(\pi^{\prime}(\ell^{\prime}))=\pi(\ell^{\prime})$, where the map

[TABLE]

denotes the componentwise projection onto $Q$ and $\ell^{\prime}\leq\ell$.

We will use a map $\mathit{idx}_{b}:[1..k]\rightarrow\mathbb{N}$ to store, for each client $j\in[1..k]$, the latest position up to which $b_{j}$ has already processed.

As induction basis, we define the initial configuration of $\pi^{\prime}$:

[TABLE]

Here, $\times$ denotes the componentwise product. Since $I_{\neg\varphi}=I\times I_{B}$, Invariant (1) is satisfied. Invariant (2) holds true by construction. Moreover, for each client $j\in[1..k]$ we set $\mathit{idx}_{b}(j)=1$.

For the induction step, let $\pi^{\prime}(0,\ell)$ already be constructed. We show how to construct the configuration $\pi^{\prime}(\ell+1)$ such that $\pi^{\prime}(0,\ell+1)$ is a proper computation satisfying the invariants (1) and (2). Let $\pi^{\prime}(\ell)=((q_{1},p_{1}),\dots,(q_{k},p_{k}))$. By Invariant (2) we have $\pi(\ell)=(q_{1},\dots,q_{k})$. Moreover, let $\pi(\ell+1)=(q^{\prime}_{1},\dots,q^{\prime}_{k})$.

Since $\pi$ is a computation of $\mathcal{N}$, there is a transition $\tau=\pi(\ell)\xrightarrow{a}\pi(\ell+1)$ on an $a\in D$. Let $\mathcal{J}$ denote the set of clients that contribute to $\tau$, $\mathcal{J}=\mathit{idx}(\tau)$. We extend the computation $\pi^{\prime}(0,\ell)$ by a transition $\tau^{\prime}$ that leads to $\pi^{\prime}(\ell+1)$.

The configuration $\pi^{\prime}(\ell+1)$ is defined componentwise as follows:

[TABLE]

where $p^{\prime}_{j}=b_{j}(\mathit{idx}_{b}(j))$. Further we increase $\mathit{idx}_{b}(j)$ by $1$ for all $j\in\mathcal{J}$. We define the transition $\tau^{\prime}$ for each client $j\in[1..k]$. Consider $\mathit{pr}_{j}(\tau)=q_{j}\xrightarrow{\mathit{op}}q^{\prime}_{j}$. Then we set the contribution of client $j$ to be $(q_{j},p_{j})\xrightarrow{\mathit{op}}(q^{\prime}_{j},p^{\prime}_{j})$ with $p^{\prime}_{j}$ as defined before. The resulting transition is $\tau^{\prime}$.

Invariant (1) still holds since $\pi^{\prime}(0,\ell)$ is an initialized computation of $\mathcal{N}_{\neg\varphi}$ and $\tau^{\prime}$ is a proper transition. Note that $\mathit{pr}_{j}(\tau^{\prime})=(q_{j},p_{j})\xrightarrow{\mathit{op}}(q^{\prime}_{j},p^{\prime}_{j})$ is a proper transition in $P_{\neg\varphi}$. Hence, $\tau^{\prime}=\pi^{\prime}(\ell)\xrightarrow{a}\pi^{\prime}(\ell+1)$ is a transition in $\mathcal{N}_{\neg\varphi}$. Invariant (2) holds by construction of $\pi^{\prime}(\ell+1)$.

This finishes the construction of $\pi^{\prime}(0,\ell)$. Via induction, we obtain the whole infinite computation $\pi^{\prime}$ that is a proper computation of $\mathcal{N}_{\neg\varphi}$. Since $b_{i}$ is the sequence of states of $r_{i}$, an accepting run of $B_{\neg\varphi}$, we get that $\pi^{\prime}$ visits the set of states $F_{\neg\varphi}=Q\times F_{B}$ infinitely often. Phrased differently, we obtain $\operatorname{Fin}(\pi^{\prime})\neq\emptyset$ which finishes the first direction of the proof.

For the other direction, let $\pi^{\prime}$ be a computation of $\mathcal{N}_{\neg\varphi}$ with $\operatorname{Fin}(\pi^{\prime})\neq\emptyset$. We assume that $\pi^{\prime}$ involves $k$ clients. Let $i\in\operatorname{Fin}(\pi^{\prime})$ be a client of the computation visiting the final states infinitely often.

Consider the computation $\pi=\operatorname{proj}_{Q}(\pi^{\prime})$. By definition of $\mathcal{N}_{\neg\varphi}$, $\pi$ is an initialized infinite computation of $\mathcal{N}$. Since $i\in\operatorname{Fin}(\pi^{\prime})$, the word $\lambda(\mathit{pr}_{i}(\pi))$ lies in the language $L(B_{\neg\varphi})$. This means that $\mathit{pr}_{i}(\pi)\models\neg\varphi$. Thus, we have a client $i\in\operatorname{Inf}(\pi)$ that satisfies $\neg\varphi$. By definition, $\pi\models_{\mathit{sparse}}\neg\varphi$. ∎

Sparse Model Checking

The second model checking problem that we consider is Sparse Model Checking. It demands that all computations of a broadcast network sparsely satisfy an LTL specification. We design an algorithm similar to Fair Model Checking that invokes the Vardi-Wolper construction to establish a reduction to Fair Liveness Verification. The latter can then be solved with the algorithm from Section 4.

We state the decision problem. To this end, a broadcast network $\mathcal{N}$ is said to sparsely satisfy an LTL formula $\varphi$ if for each initialized infinite computation $\pi$ we have that $\pi\models_{\mathit{sparse}}\varphi$. In this case, we write $\mathcal{N}\models_{\mathit{sparse}}\varphi$. {myproblem}

The following theorem states the main result. Note that the size of the broadcast network only contributes a polynomial factor.

Theorem 5.3

Sparse Model Checking can be solved in time $2^{\mathcal{O}({|\varphi|})}\cdot|\mathcal{N}|^{\mathcal{O}(1)}$.

Like for Fair Liveness Verification it is simpler to find a computation violating the given specification than checking whether all computations satisfy it. Hence, we give an algorithm deciding $\mathcal{N}\not\models_{\mathit{sparse}}\varphi$. If a computation $\pi$ of $\mathcal{N}$ does not sparsely saitsfy $\varphi$, all clients in $\operatorname{Inf}(\pi)$ will satisfy $\neg\varphi$. But this means that $\pi\models_{\mathit{fair}}\neg\varphi$. We obtain the following lemma.

Lemma 10

We have $\mathcal{N}\not\models_{\mathit{sparse}}\varphi$ if and only if there is an initialized infinite computation $\pi$ of $\mathcal{N}$ such that $\pi\models_{\mathit{fair}}\neg\varphi$.

As above, we construct a broadcast network $\mathcal{N}_{\neg\varphi}$ with a set of final states $F_{\neg\varphi}$. We invoke Theorem 5.2 on $\neg\varphi$ and obtain an automaton $B_{\neg\varphi}$. Now we construct the clients $P_{\neg\varphi}$ as before, as a cross product of $P$ and $B_{\neg\varphi}$. The resulting broadcast network is $\mathcal{N}_{\neg\varphi}=(D,P_{\neg\varphi})$. The final states are $F_{\neg\varphi}=Q\times F_{B}$. Computations of $\mathcal{N}_{\neg\varphi}$ in which each client that moves infinitely often also visits $F_{\neg\varphi}$ infinitely often are precisely those computations of $\mathcal{N}$ that satisfy $\neg\varphi$ under fairness. The following lemma summarizes the statement.

Lemma 11

There is a computation $\pi$ of $\mathcal{N}$ such that $\pi\models_{\mathit{fair}}\neg\varphi$ if and only if there is a computation $\pi^{\prime}$ of $\mathcal{N}_{\neg\varphi}$ with $\operatorname{Inf}(\pi^{\prime})\subseteq\operatorname{Fin}(\pi^{\prime})$.

From Lemmas 10 and 11, we obtain a reduction to Fair Liveness Verification. Hence, we can apply the algorithm from Section 4 to decide the existence of $\pi^{\prime}$. Since the algorithm takes only polynomial time, the complexity estimation given in Theorem 5.3 follows similar to the estimation of Theorem 5.1.