Synthesizing Controllers from Closed Loop Formal Specifications

摘要

The main obstruction to automatic synthesis of optimal controllers for finite state Discrete Event Systems (DESs) is state explosion. We present a new symbolic (i.e. based on Binary Decision Diagrams, BDDs) algorithm to automatically synthesize a program implementing a controller from the plant (finite state) model and the given formal specifications for the closed loop system (plant + controller). This guarantees that the controller program is correct by construction. We show practical usefulness of our techniques by giving experimental results on their use to synthesize a C program implementing an optimal controller (OC) for a semiconductor manufacturing facility (fab). This synthesis experiment entails computing OCs for plants with about 10~(10) states. To the best of our knowledge no previously published algorithm for automatic OC synthesis can handle plants of such size.