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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 160621539
AccessLevel: 6
PubType: Periodical
PubTypeId: serialPeriodical
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Gao%2C+Yulong%22">Gao, Yulong</searchLink><relatesTo>1</relatesTo><i> yulongg@kth.se</i><br /><searchLink fieldCode="AR" term="%22Abate%2C+Alessandro%22">Abate, Alessandro</searchLink><relatesTo>2</relatesTo><i> aabate@cs.ox.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Jiang%2C+Frank+J%2E%22">Jiang, Frank J.</searchLink><relatesTo>1</relatesTo><i> frankji@kth.se</i><br /><searchLink fieldCode="AR" term="%22Giacobbe%2C+Mirco%22">Giacobbe, Mirco</searchLink><relatesTo>3</relatesTo><i> mirco.giacobbe@cs.ox.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Xie%2C+Lihua%22">Xie, Lihua</searchLink><relatesTo>4</relatesTo><i> elhxie@ntu.edu.sg</i><br /><searchLink fieldCode="AR" term="%22Johansson%2C+Karl+Henrik%22">Johansson, Karl Henrik</searchLink><relatesTo>1</relatesTo><i> kallej@kth.se</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22IEEE+Transactions+on+Automatic+Control%22">IEEE Transactions on Automatic Control</searchLink>. Oct2022, Vol. 67 Issue 10, p5071-5086. 16p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Discrete-time+systems%22">Discrete-time systems</searchLink><br /><searchLink fieldCode="DE" term="%22Uncertain+systems%22">Uncertain systems</searchLink><br /><searchLink fieldCode="DE" term="%22Logic%22">Logic</searchLink><br /><searchLink fieldCode="DE" term="%22Linear+systems%22">Linear systems</searchLink><br /><searchLink fieldCode="DE" term="%22Adaptive+control+systems%22">Adaptive control systems</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=160621539
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1109/TAC.2021.3118335
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 16
        StartPage: 5071
    Subjects:
      – SubjectFull: Discrete-time systems
        Type: general
      – SubjectFull: Uncertain systems
        Type: general
      – SubjectFull: Logic
        Type: general
      – SubjectFull: Linear systems
        Type: general
      – SubjectFull: Adaptive control systems
        Type: general
    Titles:
      – TitleFull: Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Gao, Yulong
      – PersonEntity:
          Name:
            NameFull: Abate, Alessandro
      – PersonEntity:
          Name:
            NameFull: Jiang, Frank J.
      – PersonEntity:
          Name:
            NameFull: Giacobbe, Mirco
      – PersonEntity:
          Name:
            NameFull: Xie, Lihua
      – PersonEntity:
          Name:
            NameFull: Johansson, Karl Henrik
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 10
              Text: Oct2022
              Type: published
              Y: 2022
          Identifiers:
            – Type: issn-print
              Value: 00189286
          Numbering:
            – Type: volume
              Value: 67
            – Type: issue
              Value: 10
          Titles:
            – TitleFull: IEEE Transactions on Automatic Control
              Type: main
ResultId 1