kth.sePublikationer KTH
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Adaptive Task Planning and Formal Control Synthesis Using Temporal Logic Trees
Department of Electrical and Electronic Engineering, Imperial College London, London, UK.
Department of Electrical and Electronic Engineering, Imperial College London, London, UK.
Department of Computer Science, University of Oxford, Oxford, UK.
KTH, Skolan för elektroteknik och datavetenskap (EECS), Intelligenta system, Reglerteknik. KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Digital futures.ORCID-id: 0000-0001-9940-5929
2025 (Engelska)Ingår i: Real Time and Such: Essays Dedicated to Wang Yi to Celebrate His Scientific Career / [ed] Susanne Graf, Paul Pettersson, Bernhard Steffen, Springer Nature , 2025, Vol. 15230 LNCS, s. 64-78Kapitel i bok, del av antologi (Övrigt vetenskapligt)
Abstract [en]

Temporal logics have garnered significant attention in the control community due to their use for formal control synthesis, namely for the synthesis of control policies with provable correctness guarantees for more complex and interesting properties than traditional control objectives. Formal control under temporal logics is fundamentally challenging though, particularly when dealing with uncertain infinite systems and complex temporal logic specifications for real-time task planing, as the established methods struggle with handling models in high dimensions and with accommodating online deployment. In this article, we propose Temporal Logic Trees (TLT) as a mitigation for these challenges. TLT are constructed from Linear Temporal Logic (LTL) formulae via reachability analysis, offering an abstraction-free design method. Building upon the TLT framework, we present approaches for adaptive task planning and formal control synthesis that are usable on both finite and infinite systems. Furthermore, we demonstrate the applicability of our approach for online control synthesis, particularly in addressing time-varying tasks: namely, our method allows for dynamic online updates of the specifications, which showcases its practical utility and flexibility.

Ort, förlag, år, upplaga, sidor
Springer Nature , 2025. Vol. 15230 LNCS, s. 64-78
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
Nyckelord [en]
Formal control synthesis, Linear temporal logic, Real-time systems, Task planning, Temporal logic tree
Nationell ämneskategori
Datavetenskap (datalogi) Reglerteknik
Identifikatorer
URN: urn:nbn:se:kth:diva-356285DOI: 10.1007/978-3-031-73751-0_7ISI: 001400370700008Scopus ID: 2-s2.0-85208045321OAI: oai:DiVA.org:kth-356285DiVA, id: diva2:1912869
Anmärkning

Part of ISBN 978-3-031-73750-3, 978-3-031-73751-0

QC 20250924

Tillgänglig från: 2024-11-13 Skapad: 2024-11-13 Senast uppdaterad: 2025-09-24Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Person

Johansson, Karl H.

Sök vidare i DiVA

Av författaren/redaktören
Johansson, Karl H.
Av organisationen
ReglerteknikDigital futures
Datavetenskap (datalogi)Reglerteknik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 239 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf