Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published June 2012 | public
Book Section - Chapter

Switching protocol synthesis for temporal logic specifications

Abstract

We consider the problem of synthesizing a robust switching controller for nonlinear hybrid systems to guarantee that the trajectories of the system satisfy a high level specification expressed in linear temporal logic. Two different types of finite transition systems, namely under-approximations and over-approximations, that abstract the behavior of the underlying continuous dynamical system are defined. Using these finite abstractions, it is possible to leverage tools from logic and automata theory to synthesize discrete mode sequences or strategies. In particular, we show that the discrete synthesis problem for an under-approximation can be reformulated as a model checking problem and that for an over-approximation can be transformed into a two-player game, which can then be solved by using off-the-shelf tools. By construction, existence of a discrete switching strategy for the discrete synthesis problem guarantees the existence of a continuous switching protocol for the continuous synthesis problem, which can be implemented at the continuous level to ensure the correctness of the trajectories for the nonlinear hybrid system. Moreover, in the case of over-approximations, it is shown that one can easily accommodate specifications that require reacting to possibly adversarial external events within the same framework.

Additional Information

© 2012 AACC. Date of Current Version: 01 October 2012. This work was supported in part by the NSERC of Canada, the Multiscale Systems Center, and the Boeing Corporation. A full length version of this document is available at [1].

Additional details

Created:
August 19, 2023
Modified:
October 19, 2023