Embedded systems require very novel, very challenging specifications that have to deal with synchronization, sequencing, and temporal ordering of different tasks. Mathematically formulating such desired specifications cannot be achieved using traditional mathematical formulations in control theory. On the other hand, computer aided verification has popularized the use of several temporal logics to describe complex specifications. However, the emphasis has been on verification of these properties for purely discrete systems, and not on synthesis for systems with a continuous component. In this research, a novel approach for automatically synthesizing hybrid controllers is pursued in order to satisfy specifications that are expressed in temporal logics. The proposed framework will provide algorithms and tools for the computation of discrete controllers, which by refinement will lead to embedded, hybrid controllers for the original system while providing performance and correctness guarantees.
Description