PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Tue 25 Jun 2024 14:13 - 14:46 at Helsinki - Session 3

The paper studies the problem of reducing liveness properties into safety properties for distributed systems with arbitrary topologies. The reduction is based on using justice (weak fairness) properties in liveness proof rules to define a planner – sequences of just states that guarantee liveness, and thus replacing the liveness rule with a monitor for the planner, that guarantees that a liveness goal is reached by the time the planner is satisfied. The method is extended to protocols with probabilistic elements. The method is applied to three protocols, one that induces a spanning tree on a network, one that chooses a leader in each tree of a forest of trees, and one that identifies a maximal independent set in a network.

Tue 25 Jun

Displayed time zone: Windhoek change