Incremental Discrete Controller Synthesis for communicating systems based on modular decomposition

The symbolic Discrete Controller Synthesis (DCS) is applied incrementally on successive abstractions of the system to be controlled, which is composed of two or more concurrent communicating components. We keep one component while abstract away all others. DCS is applied on the resulting abstract system and produces an intermediate approximate control solution. We refine the abstract model incrementally by adding concrete model of the abstracted components one by one. At each refinement, the previous intermediate solution is used as a starting point synthesizing a more precise solution until the precise supervisor is reached. The efficiency of the incremental technique is illustrated with performance assessments on several models.