PV1 ⊧ COLAcomputes complementation, determinization and containment for Büchi automaton

Application domain/field

• Büchi automata
• Determinization
• Complementation
• Nondeterministic Büchi automata (NBAs)

Type of tool

Library for determinization of Büchi automata

Expected input

Büchi automaton

Format:

HOA

Expected output

By default, it converts a given Büchi automaton into a deterministic automaton

Internals

Built on top of [Spot](../../Tools/Frameworks/Spot.md COLA supports the following operations on Büchi automata:

• Determinization (output can be a deterministic automaton, deterministic Parity automaton or deterministic Rabin automaton)
• Complementation (outputs complement Büchi automaton of the given automaton after determinization)