Symbolic Synthesis of Knowledge-based Program Implementations with Synchronous Semantics

TL;DR

This paper presents a symbolic synthesis method for knowledge-based program implementations under synchronous semantics, extending the MCK model checker, with applications to puzzles and leader election.

Contribution

It introduces a symbolic approach to synthesize knowledge-based programs with synchronous semantics, implemented as an extension to MCK, and demonstrates its effectiveness on specific problems.

Findings

The symbolic synthesis method outperforms explicit state methods in the muddy children puzzle.

The approach successfully synthesizes a leader election protocol in a ring of processes.

Implementation as an MCK extension enables practical application of the synthesis technique.

Abstract

This paper deals with the automated synthesis of implementations of knowledge-based programs with respect to two synchronous semantics (clock and synchronous perfect recall). An approach to the synthesis problem based on the use of symbolic representations is described. The method has been implemented as an extension to the model checker MCK. Two applications of the implemented synthesis system are presented: the muddy children puzzle (where performance is compared to an explicit state method for a related problem implemented in the model checker DEMO), and a knowledge-based program for a dynamic leader election problem in a ring of processes.