PV1 ⊧ RABIT: Ramsey-based Büchi automata inclusion testingchecks inclusion of languages generated by two Büchi automata

Language inclusion solver

Application domain/field

• Büchi automata (BAs)
• Language inclusion
• Nondeterministic Büchi automata
• Nondeterministic finite automata (NFAs)

Type of tool

Property checker/language inclusion solver

Expected input

• Two Büchi or nondeterministic automata
• The metagraph $M_{A,B}^I$?

Format:

ba format

Expected output

Returns TRUE iff $L(A)\subseteq L(B)$ otherwise FALSE

Internals

Language inclusion solver, i.e. it can check language inclusion between Büchi automata, and thus also language equivalence and language universality.

Comments

Checking language inclusion between nondeterministic Büchi automata is computationally hard (PSPACE-complete).