Liveness of randomised parameterised systems under arbitrary schedulers

DOI10.1007/978-3-319-41540-6_7zbMATH Open1411.68075arXiv1606.01451OpenAlexW2478824155MaRDI QIDQ4633552FDOQ4633552

Anthony Widjaja Lin, Philipp Rümmer

Publication date: 3 May 2019

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

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.

Full work available at URL: https://arxiv.org/abs/1606.01451

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
• Model checking parameterized asynchronous shared-memory systems

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)

Cited In (8)

• Learning probabilistic termination proofs
• Learning union of integer hypercubes with queries (with applications to monadic decomposition)
• Polynomial-time optimal liveness enforcement for guidepath-based transport systems
• Fair Termination for Parameterized Probabilistic Concurrent Systems
• Regular model checking revisited
• Title not available (Why is that?)
• The complexity of verifying population protocols
• On strings in software model checking

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)