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.

Summary and Discussion

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/correct 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, i.e. since a robot cannot jump, there is an edge from A to B if regions A and B are adjacent. [nok: Question: If from the system requirements, we know, for example, that we cannot go to region C (say, it is occupied by an obstacle), can we just remove all the edges to C (or even remove the node C) at this stage, so we can speed up the search we need to do in the next step? It may not matter if we extract an automaton offline but if we want to do it online, incorporating requirements in this stage may save computation time a bit.]
• 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 requirements. 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 (or the sequence of desired states, in case we need to visit several checkpoints) 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. Using the idea from online/offline MPC, one thing we can do is to build a coarse finite state model offline and keep refining some portion of it online as the vehicle moves. In this case, extracting an automaton to be executed needs to be done online so we need to make sure that this process is fast enough.

• Possible uses of MPC type ideas
  • More complicated dynamics beyond ${\dot {x}}=u$
  • The properties of the MPC solutions (how much online computation, margins in the solutions, feasibility, etc) may guide the partitioning of the space (relates to Nok's 500m examples).

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.
• How to reason about the correctness of the composition of two FSA which are correct-by-design? Conversely, given the high level system specification/requirement, how to come up with the requirements for each mode? For example, given the high level requirements for Alice (go from one checkpoint to another one, avoid obstacles, etc) how to come up with the requirements for the intersection, road, and zone modes and the transitions between these modes?