kth.sePublications
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
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, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control). KTH, School of Electrical Engineering and Computer Science (EECS), Centres, Digital futures.ORCID iD: 0000-0001-9940-5929
2025 (English)In: 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, p. 64-78Chapter in book (Other academic)
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.

Place, publisher, year, edition, pages
Springer Nature , 2025. Vol. 15230 LNCS, p. 64-78
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
Keywords [en]
Formal control synthesis, Linear temporal logic, Real-time systems, Task planning, Temporal logic tree
National Category
Computer Sciences Control Engineering
Identifiers
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
Note

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

QC 20250924

Available from: 2024-11-13 Created: 2024-11-13 Last updated: 2025-09-24Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Johansson, Karl H.

Search in DiVA

By author/editor
Johansson, Karl H.
By organisation
Decision and Control Systems (Automatic Control)Digital futures
Computer SciencesControl Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 127 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