A Correctness Result for Synthesizing Plans With Loops in Stochastic Domains

In AI, FSCs are much sought after for automated planning paradigms such as generalized planning, as in Figure 1, where one attempts to synthesize a controller that works in multiple initial states. Such controllers are usually handwritten by domain experts, which is problematic when expert knowledge is either unavailable or unreliable. To that end, the automated synthesis of FSCs has received considerable attention in recent years, e.g., [16, 7, 26, 24, 11, 27]. Of course, FSCs synthesis is closely related to program synthesis [16], and FSCs are frequently seen as program-like plans [17], and recent synthesis literature involves an exciting exchange of technical insights between the two fields [26]; representative examples include the use of program synthesis to infer high-level action types [25], and the use of partial order planning for imperative program synthesis [13]. Naturally, from an algorithmic perspective, the two most immediate questions are: in which sense are controllers correct, and how do we synthesize controllers that are provably correct?