Labelled Control Improvisation

Engineering

CSE Senior Thesis (CSE 195)

As computer systems grow more complicated and we rely on them more and more for safety critical tasks, it has become imperative that we can verify that they perform correctly. One method to be sure a system (a program, circuit, controller for a robot, etc.) performs correctly is to generate it automatically based on a formal specification of what it should do. This is referred to as a synthesis problem. Synthesis, however, is inadequate when one desires multiple random systems that are correct, as compared to a single correct system. One example is in robotic planning, where one wishes to generate a plan (the system in this case) that meets mission requirements. Advanced knowledge about a plan could be exploited by an adversary, so picking a single plan for all every time the robot goes on a mission is not acceptable. In this case one would ideally like to generate a wide variety of diverse and correct plans. Recently, an extension to traditional synthesis named Control Improvisation (CI) was proposed, which allows one to generate diverse systems while balancing the randomness of what is generated with control over what is generated. Despite the control over randomness that CI gives, it is still inadequate in certain respects. CI requires that all systems are roughly equally likely, when what is really required is meaningful randomness over certain aspects of a system. For example, in robotic planning, one might primarily be concerned about randomness over which roads or charging points are used, not over which slightly different routes a robot takes over the same road. In this thesis we introduce Labelled Control Improvisation (LCI), an extension of Control Improvisation that allows one to provide a label function and enforce randomness over and within these labels. We define two different problems, the simpler LCI problem and Maximum Entropy LCI problem, providing efficient algorithms for solving both these problems along with rigorous proofs of correctness. We also present several motivating examples that illustrate the usefulness of LCI, and provide upper and lower bounds on the computational complexity of these problems when using different types of constraints.