The goal of logical controller synthesis is to automatically compute a control strategy that regulates the discrete, event-driven behavior of a given plant s.t. a temporal logic specification holds over all remaining traces. Standard approaches to this problem construct a two-player game by composing a given complete plant model and the logical specification and applying standard algorithmic techniques to extract a control strategy. However, due to the often enormous state space of a complete plant model, this process can become computationally infeasible. In this paper, we introduce a novel synthesis approach that constructs a universal controller derived solely from the game obtained by the standard translation of the logical specification. The universal controller's moves are annotated with prophecies - predictions about the plant's behavior that ensure the move is safe. By evaluating these prophecies, the universal controller can be adapted to any plant over which the synthesis problem is realizable. This approach offers several key benefits, including enhanced scalability with respect to the plant's size, adaptability to changes in the plant, and improved explainability of the resulting control strategy. We also present encouraging experimental results obtained with our prototype tool, UNICON.
Permissive Controller Synthesis for Probabilistic Systems
Faculty of Informatics, Masaryk University（马萨里克大学信息学院）；EECS, Queen Mary, University of London（伦敦大学玛丽女王学院电气电子与计算机科学与工程系）；Department of Computer Science, University of Oxford（牛津大学计算机科学系）；School of Computer Science, University of Birmingham（伯明翰大学计算机科学学院）
