A declarative approach to specifying distributed algorithms using three-valued modal logic

Murdoch J. Gabbay, Luca Zanolini

We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus alg…