Skip to main content
Top

2018 | OriginalPaper | Chapter

Owl: A Library for \(\omega \)-Words, Automata, and LTL

Authors : Jan Křetínský, Tobias Meggendorfer, Salomon Sickert

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present the library Owl (Omega-Words, automata, and LTL) for \(\omega \)-automata and linear temporal logic. It forms a backbone of several translations from LTL to automata and related tools by different authors. We describe the functionality of the library and the recent experience, which has already shown the library is apt for easy prototyping of new tools in this area.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Authored by Florian Barta, Matthias Franze, and Sebastian Fiss, respectively.
 
2
Originally implemented by Daniel Neider.
 
Literature
4.
go back to reference Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008) Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)
5.
go back to reference Blahoudek, F., Duret-Lutz, A., Klokočka, M., Křetínský, M., Strejček, J.: Seminator: a tool for semi-determinization of omega-automata. In: LPAR (2017) Blahoudek, F., Duret-Lutz, A., Klokočka, M., Křetínský, M., Strejček, J.: Seminator: a tool for semi-determinization of omega-automata. In: LPAR (2017)
10.
go back to reference Emerson, E.A., Lei, C.: Modalities for model checking: branching time strikes back. In: POPL (1985) Emerson, E.A., Lei, C.: Modalities for model checking: branching time strikes back. In: POPL (1985)
13.
go back to reference Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata - a safraless compositional approach. Form. Methods Syst. Des. (2016) Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata - a safraless compositional approach. Form. Methods Syst. Des. (2016)
14.
go back to reference Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata. In: LICS (2018) Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata. In: LICS (2018)
18.
go back to reference Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Fifth Workshop on Synthesis (SYNT\(@\)CAV) (2016) Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Fifth Workshop on Synthesis (SYNT\(@\)CAV) (2016)
25.
go back to reference Křetínský, J., Meggendorfer, T., Sickert, S.: LTL store: repository of LTL formulae from literature and case studies. CoRR, abs/1807.03296 (2018) Křetínský, J., Meggendorfer, T., Sickert, S.: LTL store: repository of LTL formulae from literature and case studies. CoRR, abs/1807.03296 (2018)
32.
go back to reference Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Gandalf (2017) Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Gandalf (2017)
33.
go back to reference Pnueli, A.: The temporal logic of programs. In: FOCS (1977) Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
34.
go back to reference Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL (1989) Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL (1989)
35.
go back to reference Rodger, S.H., Qin, H., Su, J.: Changes to JFLAP to increase its use in courses. In: SIGCSE (2011) Rodger, S.H., Qin, H., Su, J.: Changes to JFLAP to increase its use in courses. In: SIGCSE (2011)
36.
go back to reference Safra, S.: On the complexity of omega-automata. In: FOCS (1988) Safra, S.: On the complexity of omega-automata. In: FOCS (1988)
Metadata
Title
Owl: A Library for -Words, Automata, and LTL
Authors
Jan Křetínský
Tobias Meggendorfer
Salomon Sickert
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_34

Premium Partner