Translating LTL to Lasso Automata

Ehlers, Rüdiger; Hölzner, Nils; Kühnel, Tobias

doi:10.34727/2026/isbn.978-3-85448-093-8_37

Record link:

http://hdl.handle.net/20.500.12708/230502
https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_37

Title:

Citation:

Ehlers, R., Hölzner, N., & Kühnel, T. (2026). Translating LTL to Lasso Automata. In B. Dutertre & B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 321–327). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_37

reposiTUm DOI:

10.34727/2026/isbn.978-3-85448-093-8_37

CatalogPlus:

AC17999082

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Ehlers, Rüdiger
Hölzner, Nils
Kühnel, Tobias

Editors:

Dutertre, Bruno
Könighofer, Bettina

Organisational Unit:

E000 - Technische Universität Wien

Series:

Conference Series: Formal Methods in Computer-Aided Design

Published in:

Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026

Date (published):

Sep-2026

Number of Pages:

Publisher:

TU Wien Academic Press

Peer reviewed:

Yes

Keywords:

formal methods; computer-aided system design; hardware and system verification

Abstract:

We provide a novel approach for translating linear temporal logic (LTL) formulas to deterministic lasso automata, which accept those words of the form u$v (for some finite words u and v) for which uvω satisfies the LTL formula. Such lasso automata characterize ω-regular languages, can be minimized in polynomial time, and have found first applications, such as for the computation of tight B ¨uchi automata. We experimentally compare the new translation approach to an existing indirect approach based on a construction by Calbrix, Nivat, and Podelski.

Is part of:

10.34727/2026/isbn.978-3-85448-093-8

Research Areas:

Logic and Computation: 40%
Computer Engineering and Software-Intensive Systems: 40%
Computer Science Foundations: 20%

Science Branch:

1020 - Informatik: 100%

License:

CC BY 4.0