English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Broadcast networks allow one to model networks of identical nodescommunicating through message broadcasts. Their parameterized verification aimsat proving a property holds for any number of nodes, under any communicationtopology, and on all possible executions. We focus on the coverability problemwhich dually asks whether there exists an execution that visits a configurationexhibiting some given state of the broadcast protocol. Coverability is known tobe undecidable for static networks, i.e. when the number of nodes andcommunication topology is fixed along executions. In contrast, it is decidablein PTIME when the communication topology may change arbitrarily alongexecutions, that is for reconfigurable networks. Surprisingly, no lower norupper bounds on the minimal number of nodes, or the minimal length of coveringexecution in reconfigurable networks, appear in the literature.  In this paper we show tight bounds for cutoff and length, which happen to belinear and quadratic, respectively, in the number of states of the protocol. Wealso introduce an intermediary model with static communication topology andnon-deterministic message losses upon sending. We show that the same tightbounds apply to lossy networks, although, reconfigurable executions may belinearly more succinct than lossy executions. Finally, we show NP-completenessfor the natural optimisation problem associated with the cutoff.

Reconfiguration and Message Losses in Parameterized Broadcast Networks