Contract-Based Distributed Logical Controller Synthesis

We consider the problem of computing distributed logical controllers for two interacting system components via a novel sound and complete contract-based synthesis framework.Based on a discrete abstraction of component interactions as a two-player game over a finite graph and specifications for both components given as -regular (e.g.LTL) properties over this graph, we co-synthesize contract and controller candidates locally for each component and propose a negotiation mechanism which iteratively refines these candidates until a solution to the given distributed synthesis problem is found.Our framework relies on the recently introduced concept of permissive templates which collect an infinite number of controller candidates in a concise data structure.We utilize the efficient computability, adaptability and compositionality of such templates to obtain an efficient, yet sound and complete negotiation framework for contract-based distributed logical control.We showcase the superior performance of our approach by comparing our prototype tool CoSMo to the state-of-the-art tool on a robot motion planning benchmark suite.