A Fully Automated Framework for Control of Linear Systems from LTL Specifications
A Fully Automated Framework for Control of Linear Systems from LTL Specifications
复制标题
根据 LTL 规范控制线性系统的全自动框架
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
C. Belta
中科院分区：
文献类型：
--
作者：
Marius Kloetzer;C. Belta
我们考虑以下问题：给定一个线性系统和一个LTL−−X公式，在其状态变量的一组线性谓词上，找到一个具有多面体边界和一组初始状态的反馈控制律，使得闭环系统的所有轨迹都满足该公式。我们对这个问题的解决方案包括三个主要步骤。首先，我们根据公式中的谓词划分状态空间，并在划分商上构造一个转移系统，这捕获了我们设计控制器的能力。其次，利用模型检测，我们确定运行的过渡系统满足的公式。第三，生成控制策略。说明性的例子包括在内。
We consider the following problem: given a linear system and an LTL−−X formula over a set of linear predicates in its state variables, find a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula. Our solution to this problem consists of three main steps. First, we partition the state space in accordance with the predicates in the formula and construct a transition system over the partition quotient, which captures our capability of designing controllers. Second, using model checking, we determine runs of the transition system satisfying the formula. Third, we generate the control strategy. Illustrative examples are included.