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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We consider the parameterized verification problem for distributed algorithmswhere the goal is to develop techniques to prove the correctness of a givenalgorithm regardless of the number of participating processes. Motivated by anasynchronous binary consensus algorithm [J. Aspnes, Fast deterministicconsensus in a noisy environment. Journal of Algorithms, 2002], we considerround-based distributed algorithms communicating with shared memory. Aparticular challenge in these systems is that 1) the number of processes isunbounded, and, more importantly, 2) there is a fresh set of registers at eachround. A~verification algorithm thus needs to manage both sources of infinity.In this setting, we prove that the safety verification problem, which consistsin deciding whether all possible executions avoid a given error state, isPSPACE-complete. For~negative instances of the safety verification problem,we~also provide exponential lower and upper bounds on the minimal number ofprocesses needed for an error execution and on the minimal round on which theerror state can be covered.

Parameterized safety verification of round-based shared-memory systems