Distributed Implementation of Constrained Systems Based on Knowledge

Building correct distributed systems is challenging, and any attempt for providing a direct, global proof of correctness of a distributed system is bound to fail. An interesting alternative approach consists in starting from a specification or program of the system under construction, verifying all properties of interest on it - which has a much lower complexity than the verification on a distributed implementation - and finally derive a distributed implementation using some correct by-construction approach. Note that this topic is related to distributed control, where the objective is to enforce in a distributed manner some global constraint on a plant. Deriving such a distributed controller directly is difficult, and the correctness of the resulting controller is difficult to prove. A more feasible approach in this context is to first construct a global controller, then transform it into distributed one, again by means of a correct-by-construction approach.