Digitala Vetenskapliga Arkivet

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
Pyspect: An Extensible Toolbox for Automatic Construction of Temporal Logic Trees via Reachability Analysis
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control). KTH, School of Industrial Engineering and Management (ITM), Centres, Integrated Transport Research Lab, ITRL. KTH, School of Electrical Engineering and Computer Science (EECS), Centres, Digital futures.ORCID iD: 0009-0007-3871-5828
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Robotics, Perception and Learning, RPL. KTH, School of Industrial Engineering and Management (ITM), Centres, Integrated Transport Research Lab, ITRL. KTH, School of Electrical Engineering and Computer Science (EECS), Centres, Digital futures.ORCID iD: 0000-0002-4633-6787
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control). KTH, School of Industrial Engineering and Management (ITM), Centres, Integrated Transport Research Lab, ITRL. KTH, School of Electrical Engineering and Computer Science (EECS), Centres, Digital futures.ORCID iD: 0000-0001-6653-5508
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control). KTH, School of Industrial Engineering and Management (ITM), Centres, Integrated Transport Research Lab, ITRL. KTH, School of Electrical Engineering and Computer Science (EECS), Centres, Digital futures.ORCID iD: 0000-0001-9940-5929
Show others and affiliations
2025 (English)In: 2025 IEEE 64th Conference on Decision and Control, CDC 2025, Institute of Electrical and Electronics Engineers (IEEE) , 2025, p. 6911-6918Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we present pyspect, a Python toolbox that simplifies the use of reachability analysis for temporal logic problems. Currently, satisfying complex requirements in cyber-physical systems requires significant manual effort and domain expertise to develop the underlying reachability programs. This high development effort limits the broader adoption of reachability analysis for complex verification problems. To address this, pyspect provides a method-agnostic approach to performing reachability analysis for verifying a temporal logic specification via temporal logic trees (TLTs). It enables the specification of complex safety and liveness requirements using high-level logic formulations that are independent of any particular reachability technique or set representation. As a result, pyspect allows for the comparison of different reachability implementations, such as Hamilton-Jacobi and Hybrid Zonotope-based reachability analysis, for the same temporal logic specification. This design separates the concerns of implementation developers (who develop numerical procedures for reachability) and end-users (who write specifications). Through a simple vehicle example, we demonstrate how pyspect simplifies the synthesis of reachability programs, promotes specification reusability, and facilitates side-by-side comparisons of reachability techniques for complex tasks.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2025. p. 6911-6918
National Category
Computer Sciences Control Engineering
Identifiers
URN: urn:nbn:se:kth:diva-385622DOI: 10.1109/CDC57313.2025.11311974Scopus ID: 2-s2.0-105031897814OAI: oai:DiVA.org:kth-385622DiVA, id: diva2:2086988
Conference
64th IEEE Conference on Decision and Control, CDC 2025, Rio de Janeiro, Brazil, December 9-12, 2025
Note

Part of ISBN 9798331526276

QC 20260717

Available from: 2026-07-17 Created: 2026-07-17 Last updated: 2026-07-17Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Munhoz Arfvidsson, KajHadjiloizou, LoizosJiang, Frank J.Johansson, Karl H.Mårtensson, Jonas
By organisation
Decision and Control Systems (Automatic Control)Integrated Transport Research Lab, ITRLDigital futuresRobotics, Perception and Learning, RPL
Computer SciencesControl Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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