Liveness of randomised parameterised systems under arbitrary schedulers

DOI10.1007/978-3-319-41540-6_7MaRDI QIDQ4633552zbMATH OpenOpenAlexFDO

Authors Philipp Rümmer, Anthony Widjaja Lin

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1606.01451, http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-309990

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. In this paper we consider liveness under arbitrary (including unfair) schedulers, which is often considered a desirable property in the literature of self-stabilising systems. We introduce an automatic method of proving liveness for randomised parameterised systems under arbitrary schedulers. Viewing liveness as a two-player reachability game (between Scheduler and Process), our method is a CEGAR approach that synthesises a progress relation for Process that can be symbolically represented as a finite-state automaton. The method is incremental and exploits both Angluin-style L*-learning and SAT-solvers. Our experiments show that our algorithm is able to prove liveness automatically for well-known randomised distributed protocols, including Lehmann-Rabin Randomised Dining Philosopher Protocol and randomised self-stabilising protocols (such as the Israeli-Jalfon Protocol). To the best of our knowledge, this is the first fully-automatic method that can prove liveness for randomised protocols.

Recommendations

• scientific article; zbMATH DE number 1956507
• Checking qualitative liveness properties of replicated systems with stochastic scheduling
• \(P^5\): planner-less proofs of probabilistic parameterized protocols
• scientific article; zbMATH DE number 1670786

Cited in

(11)

• Regular model checking revisited
• \(P^5\): planner-less proofs of probabilistic parameterized protocols
• Learning probabilistic termination proofs
• Learning union of integer hypercubes with queries (with applications to monadic decomposition)
• Checking qualitative liveness properties of replicated systems with stochastic scheduling
• Mechanically verifying the fundamental liveness property of the Chord protocol
• On strings in software model checking
• The complexity of verifying population protocols
• scientific article; zbMATH DE number 7649941 (Why is no real title available?)
• Fair termination for parameterized probabilistic concurrent systems
• Polynomial-time optimal liveness enforcement for guidepath-based transport systems

This page was built for publication: Liveness of randomised parameterised systems under arbitrary schedulers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4633552)