Workshop: Specification and Verification of Embedded Systems

From MurrayWiki
Revision as of 08:28, 22 November 2008 by Utopcu (Talk | contribs)

Jump to: navigation, search


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.

Possible questions/ideas

  • It is said that Synthesis constructs FSA as the solution of a two-player game. Can this game be expressed as a min-max optimization problem? If so, starting from that interpretation, can the problem be simplified/restructured for more efficient/smaller FSA construction?
  • Is it possible to construct the FSA partially?
    • Drive the construction with some objective. Imposing some kind of optimality may reduce the number of states to be visited.
  • Varying detail construction: Finer requirements/partitioning close to the initial point and reduced details away from the initial point (just enough detail to ``guarantee" some ``safety" properties). Nok's 500m examples motivates this.