PV1 ⊧ Owlformally manipulates LTL formulae, Büchi automata and ω-automata

"A tool collection and library for Omega-words, $\omega$-automata, and Linear Temporal Logic (LTL)."

Application domain/field

• Linear Temporal Logic (LTL)
• Automata
• ω-automata
• Automata translation
• Determinisation
• Büchi automata

Type of tool

Library

Expected input

LTL formula or non-deterministic Büchi automaton,

Format:

HOA

Expected output

Depends on how the library is used. See Internals below.

Internals

The library can be used to e.g. translate LTL to $\omega$-automata, determinise Büchi automata, or to simplify an LTL formula. A complete list of what Owl can be used for is available on the repository.

Comments

License: GPL v3.0