Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications
Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications
复制标题
DOI：
10.1109/cdc45484.2021.9683328
复制
发表时间：
2021-03
期刊：
影响因子：
--
通讯作者：
Sasinee Pruekprasert;Clovis Eberhart;Jérémy Dubut
中科院分区：
文献类型：
--
作者：
Sasinee Pruekprasert;Clovis Eberhart;Jérémy Dubut
我们扩展了以前的工作，符号自触发控制的非确定性连续时间非线性系统的稳定性假设更大的一类规格。我们的目标是合成一个控制器的两个目标：第一个是建模为一个右递归LTL公式，第二个是确保控制器和系统之间的平均通信速率保持在一个给定的阈值以下。我们将控制问题转化为求解一个离散图上的平均支付平价博弈。除了扩展类的规格，我们提出了一种启发式方法，以缩短计算时间。最后，我们举例说明我们的结果的导航非完整机器人的几个规格。
We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller for two objectives: the first one is modelled as a right-recursive LTL formula, and the second one is to ensure that the average communication rate between the controller and the system stays below a given threshold. We translate the control problem to solving a mean-payoff parity game played on a discrete graph. Apart from extending the class of specifications, we propose a heuristic method to shorten the computation time. Finally, we illustrate our results on the example of a navigating nonholonomic robot with several specifications.