PV1 ⊧ ROLL: Regular Omega Language Learninglearns, transforms, inverts, complements Büchi automata

ROLL 1.0 is an 𝜔-regular language learning library with command line tools to learn and complement Büchi automata

Application domain/field

• Büchi automata
• Automata learning
• Active automata learning
• 𝜔-regular languages

Type of tool

Library for automata learning

Expected input

• Command indicating the running mode (e.g. learn, convert, complement, include)
• Optional: Depending on the command used, the user might need to give zero, one or two Büchi automata.

Format:

• Command: Argument that is passed when calling ROLL
• Büchi automata: Hanoi Omega Automata (HOA) format and the ba format

Expected output

Depends on how the library is used. Typically it will output a learned or complement automaton along with some execution information.

Internals

This is a library for learning 𝜔-regular languages, which can be used to describe liveness properties. Uses RABIT to check the equivalence of two Büchi automata. The library can be used for:

• Learning an input Büchi automaton
• Converting files in the BA format to the HOA format or the other way around.
• Computing the complement of a Büchi automaton
• Check the language inclusion between two Büchi automata

Comments

License: GPL v3.0