不确定离散系统模型检测与控制综合的时序逻辑树
Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems
摘要：
我们提出的算法进行模型检测和控制综合的离散时间不确定系统的线性时序逻辑（LTL）规范。我们通过可达性分析从LTL公式构造时态逻辑树（TLT）。与基于自动机的方法相比，TLT的构造对于无限系统是无抽象的，也就是说，我们不构造无限系统的离散抽象。此外，对于一个给定的转移系统和LTL公式，我们证明了存在普遍的TLT和存在的TLT的最小和最大可达性分析，分别。我们表明，普遍的TLT是一个欠近似的LTL公式和存在的TLT是一个过近似。利用TLT近似，给出了判定过渡系统是否满足LTL公式的充分条件和必要条件。作为这项工作的一个主要贡献，对于一个受控转移系统和一个LTL公式，我们证明了一个受控TLT可以通过控制相关的可达性分析从LTL公式构造。基于受控TLT，我们设计了一种在线控制综合算法，在该算法下，可以在每个时间步生成一组可行的控制输入。我们还证明了该算法是递归可行的。我们说明了所提出的方法，有限和无限的系统和突出的一般性和在线可扩展性与两个模拟的例子。
英文摘要：
We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLT) from LTL formulae via reachability analysis. In contrast to automaton-based methods, the construction of the TLT is abstraction-free for infinite systems, that is, we do not construct discrete abstractions of the infinite systems. Moreover, for a given transition system and an LTL formula, we prove that there exist both a universal TLT and an existential TLT via minimal and maximal reachability analysis, respectively. We show that the universal TLT is an underapproximation for the LTL formula and the existential TLT is an overapproximation. We provide sufficient conditions and necessary conditions to verify whether a transition system satisfies an LTL formula by using the TLT approximations. As a major contribution of this work, for a controlled transition system and an LTL formula, we prove that a controlled TLT can be constructed from the LTL formula via control-dependent reachability analysis. Based on the controlled TLT, we design an online control synthesis algorithm, under which a set of feasible control inputs can be generated at each time step. We also prove that this algorithm is recursively feasible. We illustrate the proposed methods for both finite and infinite systems and highlight the generality and online scalability with two simulated examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
