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
Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
KTH, School of Electrical Engineering and Computer Science (EECS), Centres, Centre for Autonomous Systems, CAS.ORCID iD: 0000-0002-4633-6787
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0001-6653-5508
School of Computation, Information and Technology, Technical University of Munich, Heilbronn, Germany, 74076, Bildungscampus 2.
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0001-9940-5929
2024 (English)In: 2024 European Control Conference, ECC 2024, Institute of Electrical and Electronics Engineers (IEEE) , 2024, p. 579-584Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we introduce a hybrid zonotope-based approach for formally verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications. In particular, we formally verify the LTL formula by constructing temporal logic trees (TLT)s via backward reachability analysis (BRA). In previous works, TLTs are predominantly constructed with either highly general and computationally intensive level set-based BRA or simplistic and computationally efficient polytope-based BRA. In this work, we instead propose the construction of TLTs using hybrid zonotope-based BRA. By using hybrid zonotopes, we show that we are able to formally verify LTL specifications in a computationally efficient manner while still being able to represent complex geometries that are often present when deploying autonomous systems, such as non-convex, disjoint sets. Moreover, we evaluate our approach on a parking example, providing preliminary indications of how hybrid zonotopes facilitate computationally efficient formal verification of LTL specifications in environments that naturally lead to non-convex, disjoint geometries.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2024. p. 579-584
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-351942DOI: 10.23919/ECC64448.2024.10590925ISI: 001290216500085Scopus ID: 2-s2.0-85200604183OAI: oai:DiVA.org:kth-351942DiVA, id: diva2:1890158
Conference
2024 European Control Conference, ECC 2024, Stockholm, Sweden, Jun 25 2024 - Jun 28 2024
Note

Part of ISBN [9783907144107]

QC 20240830

Available from: 2024-08-19 Created: 2024-08-19 Last updated: 2025-04-28Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Hadjiloizou, LoizosJiang, FrankJohansson, Karl H.

Search in DiVA

By author/editor
Hadjiloizou, LoizosJiang, FrankJohansson, Karl H.
By organisation
Centre for Autonomous Systems, CASDecision and Control Systems (Automatic Control)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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