Workshop: Specification and Verification of Embedded Systems

Aim

These notes aim at refreshing our memory on the discussion we had on verification on Oct 28, 09 at Caltech and initializing a discussion on Richard's question/suggestion how model predictive control type ideas may play a role in constructing FSA from specifications and then translating to hybrid controllers.

Nok's summary

Automatically generating a finite state machine from LTL specifications provides a way to construct a supervisory controller that is correct by construction. A serious drawback of this technique is that it suffers from state explosion and thus, in practice, is not applicable for a complex system. In addition, extracting an automaton which satisfies the LTL specifications may take a long time since all the possible behaviors from the beginning to the end of the execution need to be considered in detail.

Receding horizon control is an effective approach to deal with large constrained control problems. The main idea is to choose the control action by repeatedly solving on line an optimal control problem over a finite horizon with certain cost associated with the end state. That is, we do not need to solve the whole sequence of the control actions from the beginning to the end of the execution. Instead, we only solve the optimization problem over a short period of time and use the cost associated with the end state of the horizon to guarantee (the stability of the system and the optimality of the solution?). We may be able to apply similar idea to the construction of finite state machine from LTL specifications. For example, we do not really care about what exactly may happen more than 500 m ahead of the vehicle, we only need to know that from each of those points, we can get to the desired end state with some approximated cost. This allows us to reduce the number of states that need to be considered while extracting an automaton which satisfies the LTL specifications.