Designing Distributed Systems Using SAT Solvers

This paper addresses a classical problem of distributed computing: Given a labelled transition system (LTS), how to synthesise a distributed labelled transition system (DLTS) such that the global behaviour of the DLTS is isomorphic to the given LTS. It has been proved that it is not possible to synthesise a DLTS for every LTS. Only LTSs that satisfy certain conditions are distributable. These conditions are complex and difficult to understand. This paper contributes by showing how to encode a propositional logic formula against a given LTS. The formula thus encoded is satisfiable if and only if the LTS is distributable. The satisfiability of the encoded formula can be determined automatically using SAT solvers.