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 problem of verifying liveness for systems with a finite, butunbounded, number of processes, commonly known as parameterised systems.Typical examples of such systems include distributed protocols (e.g. for thedining philosopher problem). Unlike the case of verifying safety, provingliveness is still considered extremely challenging, especially in the presenceof randomness in the system. In this paper we consider liveness under arbitrary(including unfair) schedulers, which is often considered a desirable propertyin the literature of self-stabilising systems. We introduce an automatic methodof proving liveness for randomised parameterised systems under arbitraryschedulers. Viewing liveness as a two-player reachability game (betweenScheduler and Process), our method is a CEGAR approach that synthesises aprogress relation for Process that can be symbolically represented as afinite-state automaton. The method is incremental and exploits bothAngluin-style L*-learning and SAT-solvers. Our experiments show that ouralgorithm is able to prove liveness automatically for well-known randomiseddistributed protocols, including Lehmann-Rabin Randomised Dining PhilosopherProtocol and randomised self-stabilising protocols (such as the Israeli-JalfonProtocol). To the best of our knowledge, this is the first fully-automaticmethod that can prove liveness for randomised protocols.

Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report)