Workshop: Specification and Verification of Embedded Systems

From Murray Wiki
Jump to navigationJump to search

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 properties provides a way to construct a supervisory controller that is correct by construction. To describe how this works, we distinguish between system specifications (all the possible behaviors of the system) and requirements (the valid/desirable behaviors of the system).

  • Using the system (and environment) specifications, construct a finite state model which represents all the possible state transitions of the system. For example, in robot motion planning, we discretize the space into regions. These regions are represented by the nodes of the finite state model. An edge from node A to node B means that from region A, the robot can go to region B.
  • From the system requirements and the previously constructed finite state model, use a graph search algorithm similar to that used in model checkers to extract an automaton from the finite state model which satisfies the requirement.

A serious drawback of this technique is that it suffers from state explosion (the finite state model of the system can get quite large) and thus, in practice, is not applicable for a complex system. In addition, extracting an automaton which satisfies the LTL requirements 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. 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.
Retrieved from "https://murray.cds.caltech.edu/index.php?title=Workshop:_Specification_and_Verification_of_Embedded_Systems&oldid=8441"