Decomposing controller synthesis for safety specifications
Eric Dallal, Paulo Tabuada · 2016
We present a method to decompose synthesis of controllers for safety specifications into smaller controller synthesis problems. The method applies to systems that we call decomposable, which means that their transition relations can be expressed as the meet of some number of transition relations over disjoint inputs. The method presented here is based on assume-guarantee reasoning and is shown to be correct and complete: a controller enforces the safety specification if and only if it can be obtained by this method.