Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
Event details
| Date | 14.07.2016 |
| Hour | 14:00 › 15:30 |
| Location | |
| Category | Conferences - Seminars |
by Philipp Ruemmer
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. In
this paper 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 incrementally constructs a
progress relation, exploiting both Angluin's $L*$ algorithm 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.
Joint work with Anthony W. Lin.
SPEAKER BIOGRAPHY
Philipp Ruemmer is an assistant professor at Uppsala University, Sweden.
He received his doctorate in Computer Science from Chalmers University
and Gothenburg University in 2008. Before joining Uppsala University as
an assistant professor, he has been research assistant at the Oxford
University Computing Laboratory. His research interests include various
directions in program verification, theorem proving and SMT reasoning,
and application of such methods in the area of embedded systems. Philipp
received the Oscar Prize of Uppsala University in 2013, for
contributions to the field of program correctness, and the IJCAR best
paper award in 2014; the theorem prover Princess resulting from his
research won the TFA division of the theorem proving competition CASC in
2012.
More information
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. In
this paper 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 incrementally constructs a
progress relation, exploiting both Angluin's $L*$ algorithm 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.
Joint work with Anthony W. Lin.
SPEAKER BIOGRAPHY
Philipp Ruemmer is an assistant professor at Uppsala University, Sweden.
He received his doctorate in Computer Science from Chalmers University
and Gothenburg University in 2008. Before joining Uppsala University as
an assistant professor, he has been research assistant at the Oxford
University Computing Laboratory. His research interests include various
directions in program verification, theorem proving and SMT reasoning,
and application of such methods in the area of embedded systems. Philipp
received the Oscar Prize of Uppsala University in 2013, for
contributions to the field of program correctness, and the IJCAR best
paper award in 2014; the theorem prover Princess resulting from his
research won the TFA division of the theorem proving competition CASC in
2012.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch