PV1 ⊧ FORKLIFTchecks language-inclusion for Büchi automata

Application domain/field

• Inclusion
• Automata
• Büchi automata

Type of tool

Inclusion checker for Büchi automata

Expected input

Two Büchi automata A & B

Format:

Two .ba files (ba)

Expected output

0 if the language of automata A is a subset of the language of automata B. 1 if the language of automata A is not a subset of the language of automata B. 127 if the inclusion was not computed.

Internals

FORKLIFT is an inclusion checker for Büchi automata.