View in EDS

Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems.

Saved in:
Bibliographic Details
Title: Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems.
Authors: Gao, Yulong1 yulongg@kth.se, Abate, Alessandro2 aabate@cs.ox.ac.uk, Jiang, Frank J.1 frankji@kth.se, Giacobbe, Mirco3 mirco.giacobbe@cs.ox.ac.uk, Xie, Lihua4 elhxie@ntu.edu.sg, Johansson, Karl Henrik1 kallej@kth.se
Source: IEEE Transactions on Automatic Control. Oct2022, Vol. 67 Issue 10, p5071-5086. 16p.
Subjects: Discrete-time systems, Uncertain systems, Logic, Linear systems, Adaptive control systems
Abstract: 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 (TLTs) 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 a 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. [ABSTRACT FROM AUTHOR]
Copyright of IEEE Transactions on Automatic Control is the property of IEEE and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract: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 (TLTs) 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 a 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. [ABSTRACT FROM AUTHOR]
ISSN:00189286
DOI:10.1109/TAC.2021.3118335