On computing optimal controllers for finite state systems

From a computational point of view many control problems involve synthesis of controllers for finite state systems (FSSs). We address the problem of automatic synthesis of optimal controllers (OCs) for FSSs. Such a problem has been widely studied and many algorithms are known for it. However, because of state explosion their use is limited to quite small dynamical system. We devised a symbolic algorithm for automatic synthesis of OCs for FSSs. We show the practical usefulness of our techniques by giving experimental results on the use of our symbolic algorithm to synthesize a C program implementing an OC for a semiconductor manufacturing facility. This entails computing OCs for plants with about 3×10⁹ states. To the best of our knowledge no previous algorithm can handle systems of such size