Language Guided Controller Synthesis
In Chap. 9, we treated the temporal logic control problem for a PWA system.While being able to accommodate full LTL specifications, the method from Chap. 9 was conservative, mainly because the original (rough) partition of the state space was not refined if a control strategy was not found. In this chapter, we address this limitation. We restrict our attention to specifications given in the co-safe fragment of LTL (scLTL) and present a language-guided synthesis method. Central to our approach is the construction and refinement of an automaton that restricts the search for initial states and control strategies in such a way that the satisfaction of the specification is guaranteed at all times. We focus on fixed-parameter control PWA systems.