PV1 FORKLIFTchecks language-inclusion for Büchi automata

Application domain/field

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.
Automaton

Links

Related papers

FORQ-Based Language Inclusion Formal Testing (CAV 2022)

Last publication date

6 August 2022

Related tools

Other tools that can solve inclusion problems: Spot, GOAL, RABIT, ROLL, BAIT

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.