kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Zonotope-Based Symbolic Controller Synthesis for Linear Temporal Logic Specifications
Dalian Univ Technol, Key Lab Intelligent Control & Optimizat Ind Equipm, Minist Educ, Dalian 116024, Peoples R China..ORCID iD: 0000-0002-3300-0993
UCLouvain, ICTEAM Inst, B-1348 Louvain La Neuve, Belgium..
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0001-7309-8086
2024 (English)In: IEEE Transactions on Automatic Control, ISSN 0018-9286, E-ISSN 1558-2523, Vol. 69, no 11, p. 7630-7645Article in journal (Refereed) Published
Abstract [en]

This article studies the controller synthesis problem for nonlinear control systems under linear temporal logic (LTL) specifications using zonotope techniques. A local-to-global control strategy is proposed for the desired specification expressed as an LTL formula. First, a novel approach is developed to divide the state space into finite zonotopes and constrained zonotopes, which are called cells and allowed to intersect with the neighbor cells. Second, from the intersection relation, a graph among all cells is generated to verify the realization of the accepting path for the LTL formula. The realization verification determines if there is a need for the control design, and also results in finite local LTL formulas. Third, once the accepting path is realized, a novel abstraction-based method is derived for the controller design. In particular, we only focus on the cells from the realization verification and approximate each cell thanks to properties of zonotopes. Based on local symbolic models and local LTL formulas, an iterative synthesis algorithm is proposed to design all local abstract controllers, whose existence and combination establish the global controller for the LTL formula. Finally, the proposed framework is illustrated via a path planning problem of mobile robots.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2024. Vol. 69, no 11, p. 7630-7645
Keywords [en]
Dynamical systems, Aerospace electronics, Task analysis, Heuristic algorithms, Planning, Nonlinear systems, Iterative algorithms, Controller synthesis, linear temporal logic (LTL), symbolic control, zonotope-based covering
National Category
Control Engineering
Identifiers
URN: urn:nbn:se:kth:diva-359171DOI: 10.1109/TAC.2024.3394313ISI: 001342803200054Scopus ID: 2-s2.0-85191865047OAI: oai:DiVA.org:kth-359171DiVA, id: diva2:1933028
Note

QC 20250130

Available from: 2025-01-30 Created: 2025-01-30 Last updated: 2025-01-30Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Dimarogonas, Dimos V.

Search in DiVA

By author/editor
Ren, WeiDimarogonas, Dimos V.
By organisation
Decision and Control Systems (Automatic Control)
In the same journal
IEEE Transactions on Automatic Control
Control Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 16 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf