Symbolic Self-triggered Control of Continuous-time Non-deterministic\n Systems without Stability Assumptions for 2-LTL Specifications

Abstract

We propose a symbolic self-triggered controller synthesis procedure for\nnon-deterministic continuous-time nonlinear systems without stability\nassumptions. The goal is to compute a controller that satisfies two objectives.\nThe first objective is represented as a specification in a fragment of LTL,\nwhich we call 2-LTL. The second one is an energy objective, in the sense that\ncontrol inputs are issued only when necessary, which saves energy. To this end,\nwe first quantise the state and input spaces, and then translate the controller\nsynthesis problem to the computation of a winning strategy in a mean-payoff\nparity game. We illustrate the feasibility of our method on the example of a\nnavigating nonholonomic robot.\n